Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Definition df-mp 6684
 Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 6835, and is intended to be used only by the construction. From Proposition 9-3.7 of [Gleason] p. 124.
Assertion
Ref Expression
df-mp
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-mp
StepHypRef Expression
1 cmp 6583 . 2
2 vx . . . . . . 7
32cv 1614 . . . . . 6
4 cnp 6580 . . . . . 6
53, 4wcel 1617 . . . . 5
6 vy . . . . . . 7
76cv 1614 . . . . . 6
87, 4wcel 1617 . . . . 5
95, 8wa 433 . . . 4
10 vz . . . . . 6
1110cv 1614 . . . . 5
12 vw . . . . . . . . . 10
1312cv 1614 . . . . . . . . 9
14 vv . . . . . . . . . . 11
1514cv 1614 . . . . . . . . . 10
16 vu . . . . . . . . . . 11
1716cv 1614 . . . . . . . . . 10
18 cmq 6577 . . . . . . . . . 10
1915, 17, 18co 5020 . . . . . . . . 9
2013, 19wceq 1615 . . . . . . . 8
2120, 16, 7wrex 2386 . . . . . . 7
2221, 14, 3wrex 2386 . . . . . 6
2322, 12cab 2157 . . . . 5
2411, 23wceq 1615 . . . 4
259, 24wa 433 . . 3
2625, 2, 6, 10copab2 5021 . 2
271, 26wceq 1615 1
 Colors of variables: wff set class This definition is referenced by:  mpv 6709  dmmp 6711  mulclprlem 6716  mulclpr 6717  mulasspr 6721  distrlem1pr 6722  distrlem2pr 6723  distrlem5pr 6726  1idpr 6728  reclem3pr 6753  reclem4pr 6754