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	syl5eq	⊢ ( 𝑤 ∈ 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	syl5eq	⊢ ( 𝑤 ∈ 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	syl5eq	⊢ ( 𝑤 ∈ 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	syl5eq	⊢ ( 𝑤 ∈ 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	syl5eq	⊢ ( 𝑤 ∈ 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 · 𝑦 ) ) )