This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axcnre

Description: A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of Gleason p. 130. Axiom 17 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre . (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion axcnre ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 df-c ⊢ ℂ = ( R × R )
2 eqeq1 ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝐴 → ( ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) )
3 2 2rexbidv ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝐴 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) )
4 opelreal ⊢ ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ↔ 𝑧 ∈ R )
5 opelreal ⊢ ( ⟨ 𝑤 , 0R ⟩ ∈ ℝ ↔ 𝑤 ∈ R )
6 4 5 anbi12i ⊢ ( ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ⟨ 𝑤 , 0R ⟩ ∈ ℝ ) ↔ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) )
7 6 biimpri ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ⟨ 𝑤 , 0R ⟩ ∈ ℝ ) )
8 df-i ⊢ i = ⟨ 0R , 1R ⟩
9 8 oveq1i ⊢ ( i · ⟨ 𝑤 , 0R ⟩ ) = ( ⟨ 0R , 1R ⟩ · ⟨ 𝑤 , 0R ⟩ )
10 0r ⊢ 0R ∈ R
11 1sr ⊢ 1R ∈ R
12 mulcnsr ⊢ ( ( ( 0R ∈ R ∧ 1R ∈ R ) ∧ ( 𝑤 ∈ R ∧ 0R ∈ R ) ) → ( ⟨ 0R , 1R ⟩ · ⟨ 𝑤 , 0R ⟩ ) = ⟨ ( ( 0R ·R 𝑤 ) +R ( -1R ·R ( 1R ·R 0R ) ) ) , ( ( 1R ·R 𝑤 ) +R ( 0R ·R 0R ) ) ⟩ )
13 10 11 12 mpanl12 ⊢ ( ( 𝑤 ∈ R ∧ 0R ∈ R ) → ( ⟨ 0R , 1R ⟩ · ⟨ 𝑤 , 0R ⟩ ) = ⟨ ( ( 0R ·R 𝑤 ) +R ( -1R ·R ( 1R ·R 0R ) ) ) , ( ( 1R ·R 𝑤 ) +R ( 0R ·R 0R ) ) ⟩ )
14 10 13 mpan2 ⊢ ( 𝑤 ∈ R → ( ⟨ 0R , 1R ⟩ · ⟨ 𝑤 , 0R ⟩ ) = ⟨ ( ( 0R ·R 𝑤 ) +R ( -1R ·R ( 1R ·R 0R ) ) ) , ( ( 1R ·R 𝑤 ) +R ( 0R ·R 0R ) ) ⟩ )
15 mulcomsr ⊢ ( 0R ·R 𝑤 ) = ( 𝑤 ·R 0R )
16 00sr ⊢ ( 𝑤 ∈ R → ( 𝑤 ·R 0R ) = 0R )
17 15 16 eqtrid ⊢ ( 𝑤 ∈ R → ( 0R ·R 𝑤 ) = 0R )
18 17 oveq1d ⊢ ( 𝑤 ∈ R → ( ( 0R ·R 𝑤 ) +R ( -1R ·R ( 1R ·R 0R ) ) ) = ( 0R +R ( -1R ·R ( 1R ·R 0R ) ) ) )
19 00sr ⊢ ( 1R ∈ R → ( 1R ·R 0R ) = 0R )
20 11 19 ax-mp ⊢ ( 1R ·R 0R ) = 0R
21 20 oveq2i ⊢ ( -1R ·R ( 1R ·R 0R ) ) = ( -1R ·R 0R )
22 m1r ⊢ -1R ∈ R
23 00sr ⊢ ( -1R ∈ R → ( -1R ·R 0R ) = 0R )
24 22 23 ax-mp ⊢ ( -1R ·R 0R ) = 0R
25 21 24 eqtri ⊢ ( -1R ·R ( 1R ·R 0R ) ) = 0R
26 25 oveq2i ⊢ ( 0R +R ( -1R ·R ( 1R ·R 0R ) ) ) = ( 0R +R 0R )
27 0idsr ⊢ ( 0R ∈ R → ( 0R +R 0R ) = 0R )
28 10 27 ax-mp ⊢ ( 0R +R 0R ) = 0R
29 26 28 eqtri ⊢ ( 0R +R ( -1R ·R ( 1R ·R 0R ) ) ) = 0R
30 18 29 eqtrdi ⊢ ( 𝑤 ∈ R → ( ( 0R ·R 𝑤 ) +R ( -1R ·R ( 1R ·R 0R ) ) ) = 0R )
31 mulcomsr ⊢ ( 1R ·R 𝑤 ) = ( 𝑤 ·R 1R )
32 1idsr ⊢ ( 𝑤 ∈ R → ( 𝑤 ·R 1R ) = 𝑤 )
33 31 32 eqtrid ⊢ ( 𝑤 ∈ R → ( 1R ·R 𝑤 ) = 𝑤 )
34 33 oveq1d ⊢ ( 𝑤 ∈ R → ( ( 1R ·R 𝑤 ) +R ( 0R ·R 0R ) ) = ( 𝑤 +R ( 0R ·R 0R ) ) )
35 00sr ⊢ ( 0R ∈ R → ( 0R ·R 0R ) = 0R )
36 10 35 ax-mp ⊢ ( 0R ·R 0R ) = 0R
37 36 oveq2i ⊢ ( 𝑤 +R ( 0R ·R 0R ) ) = ( 𝑤 +R 0R )
38 0idsr ⊢ ( 𝑤 ∈ R → ( 𝑤 +R 0R ) = 𝑤 )
39 37 38 eqtrid ⊢ ( 𝑤 ∈ R → ( 𝑤 +R ( 0R ·R 0R ) ) = 𝑤 )
40 34 39 eqtrd ⊢ ( 𝑤 ∈ R → ( ( 1R ·R 𝑤 ) +R ( 0R ·R 0R ) ) = 𝑤 )
41 30 40 opeq12d ⊢ ( 𝑤 ∈ R → ⟨ ( ( 0R ·R 𝑤 ) +R ( -1R ·R ( 1R ·R 0R ) ) ) , ( ( 1R ·R 𝑤 ) +R ( 0R ·R 0R ) ) ⟩ = ⟨ 0R , 𝑤 ⟩ )
42 14 41 eqtrd ⊢ ( 𝑤 ∈ R → ( ⟨ 0R , 1R ⟩ · ⟨ 𝑤 , 0R ⟩ ) = ⟨ 0R , 𝑤 ⟩ )
43 9 42 eqtrid ⊢ ( 𝑤 ∈ R → ( i · ⟨ 𝑤 , 0R ⟩ ) = ⟨ 0R , 𝑤 ⟩ )
44 43 oveq2d ⊢ ( 𝑤 ∈ R → ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) = ( ⟨ 𝑧 , 0R ⟩ + ⟨ 0R , 𝑤 ⟩ ) )
45 44 adantl ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) = ( ⟨ 𝑧 , 0R ⟩ + ⟨ 0R , 𝑤 ⟩ ) )
46 addcnsr ⊢ ( ( ( 𝑧 ∈ R ∧ 0R ∈ R ) ∧ ( 0R ∈ R ∧ 𝑤 ∈ R ) ) → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 0R , 𝑤 ⟩ ) = ⟨ ( 𝑧 +R 0R ) , ( 0R +R 𝑤 ) ⟩ )
47 10 46 mpanl2 ⊢ ( ( 𝑧 ∈ R ∧ ( 0R ∈ R ∧ 𝑤 ∈ R ) ) → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 0R , 𝑤 ⟩ ) = ⟨ ( 𝑧 +R 0R ) , ( 0R +R 𝑤 ) ⟩ )
48 10 47 mpanr1 ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ( ⟨ 𝑧 , 0R ⟩ + ⟨ 0R , 𝑤 ⟩ ) = ⟨ ( 𝑧 +R 0R ) , ( 0R +R 𝑤 ) ⟩ )
49 0idsr ⊢ ( 𝑧 ∈ R → ( 𝑧 +R 0R ) = 𝑧 )
50 addcomsr ⊢ ( 0R +R 𝑤 ) = ( 𝑤 +R 0R )
51 50 38 eqtrid ⊢ ( 𝑤 ∈ R → ( 0R +R 𝑤 ) = 𝑤 )
52 opeq12 ⊢ ( ( ( 𝑧 +R 0R ) = 𝑧 ∧ ( 0R +R 𝑤 ) = 𝑤 ) → ⟨ ( 𝑧 +R 0R ) , ( 0R +R 𝑤 ) ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
53 49 51 52 syl2an ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ⟨ ( 𝑧 +R 0R ) , ( 0R +R 𝑤 ) ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
54 45 48 53 3eqtrrd ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ⟨ 𝑧 , 𝑤 ⟩ = ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) )
55 opex ⊢ ⟨ 𝑧 , 0R ⟩ ∈ V
56 opex ⊢ ⟨ 𝑤 , 0R ⟩ ∈ V
57 eleq1 ⊢ ( 𝑥 = ⟨ 𝑧 , 0R ⟩ → ( 𝑥 ∈ ℝ ↔ ⟨ 𝑧 , 0R ⟩ ∈ ℝ ) )
58 eleq1 ⊢ ( 𝑦 = ⟨ 𝑤 , 0R ⟩ → ( 𝑦 ∈ ℝ ↔ ⟨ 𝑤 , 0R ⟩ ∈ ℝ ) )
59 57 58 bi2anan9 ⊢ ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ↔ ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ⟨ 𝑤 , 0R ⟩ ∈ ℝ ) ) )
60 oveq1 ⊢ ( 𝑥 = ⟨ 𝑧 , 0R ⟩ → ( 𝑥 + ( i · 𝑦 ) ) = ( ⟨ 𝑧 , 0R ⟩ + ( i · 𝑦 ) ) )
61 oveq2 ⊢ ( 𝑦 = ⟨ 𝑤 , 0R ⟩ → ( i · 𝑦 ) = ( i · ⟨ 𝑤 , 0R ⟩ ) )
62 61 oveq2d ⊢ ( 𝑦 = ⟨ 𝑤 , 0R ⟩ → ( ⟨ 𝑧 , 0R ⟩ + ( i · 𝑦 ) ) = ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) )
63 60 62 sylan9eq ⊢ ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) → ( 𝑥 + ( i · 𝑦 ) ) = ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) )
64 63 eqeq2d ⊢ ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) → ( ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ↔ ⟨ 𝑧 , 𝑤 ⟩ = ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) ) )
65 59 64 anbi12d ⊢ ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) → ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ) ↔ ( ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ⟨ 𝑤 , 0R ⟩ ∈ ℝ ) ∧ ⟨ 𝑧 , 𝑤 ⟩ = ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) ) ) )
66 55 56 65 spc2ev ⊢ ( ( ( ⟨ 𝑧 , 0R ⟩ ∈ ℝ ∧ ⟨ 𝑤 , 0R ⟩ ∈ ℝ ) ∧ ⟨ 𝑧 , 𝑤 ⟩ = ( ⟨ 𝑧 , 0R ⟩ + ( i · ⟨ 𝑤 , 0R ⟩ ) ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ) )
67 7 54 66 syl2anc ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ) )
68 r2ex ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) ) )
69 67 68 sylibr ⊢ ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ⟨ 𝑧 , 𝑤 ⟩ = ( 𝑥 + ( i · 𝑦 ) ) )
70 1 3 69 optocl ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )