This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Dedekind-cut construction of real and complex numbers df-mp
Definition df-mp
Description: Define multiplication on positive reals. This is a "temporary" set used
in the construction of complex numbers df-c , and is intended to be
used only by the construction. From Proposition 9-3.7 of Gleason
p. 124. (Contributed by NM , 18-Nov-1995)
(New usage is discouraged.)
Ref
Expression
Assertion
df-mp ⊢ ·P 𝑥 ∈ P 𝑦 ∈ P 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) } )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cmp ⊢ ·P
1
vx ⊢ 𝑥
2
cnp ⊢ P
3
vy ⊢ 𝑦
4
vw ⊢ 𝑤
5
vv ⊢ 𝑣
6
1
cv ⊢ 𝑥
7
vu ⊢ 𝑢
8
3
cv ⊢ 𝑦
9
4
cv ⊢ 𝑤
10
5
cv ⊢ 𝑣
11
cmq ⊢ ·Q
12
7
cv ⊢ 𝑢
13
10 12 11
co ⊢ ( 𝑣 ·Q 𝑢 )
14
9 13
wceq ⊢ 𝑤 = ( 𝑣 ·Q 𝑢 )
15
14 7 8
wrex ⊢ ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 )
16
15 5 6
wrex ⊢ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 )
17
16 4
cab ⊢ { 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) }
18
1 3 2 2 17
cmpo ⊢ ( 𝑥 ∈ P 𝑦 ∈ P 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) } )
19
0 18
wceq ⊢ ·P 𝑥 ∈ P 𝑦 ∈ P 𝑤 ∣ ∃ 𝑣 ∈ 𝑥 ∃ 𝑢 ∈ 𝑦 𝑤 = ( 𝑣 ·Q 𝑢 ) } )