Theorem axcnre 4087

Description: A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. One of the 28 axioms for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
axcnre	⊢ (A ∈ ℂ → ∃x ∈ ℝ ∃y ∈ ℝ A = (x + (y · i)))

Distinct variable group(s):   x,y,A

TD>47, 50

Proof of Theorem axcnre

Step	Hyp	Ref	Expression
1		df-c 4034	. 2 ⊢ ℂ = (R × R)
2		cleq1 1107	. . . 4 ⊢ (⟨z, w⟩ = A → (⟨z, w⟩ = (x + (y · i)) ↔ A = (x + (y · i))))
3	2	birexdv 1220	. . 3 ⊢ (⟨z, w⟩ = A → (∃y ∈ ℝ ⟨z, w⟩ = (x + (y · i)) ↔ ∃y ∈ ℝ A = (x + (y · i))))
4	3	birexdv 1220	. 2 ⊢ (⟨z, w⟩ = A → (∃x ∈ ℝ ∃y ∈ ℝ ⟨z, w⟩ = (x + (y · i)) ↔ ∃x ∈ ℝ ∃y ∈ ℝ A = (x + (y · i))))
5		opex 1893	. . . . 5 ⊢ ⟨z, 0R⟩ ∈ V
6		opex 1893	. . . . 5 ⊢ ⟨w, 0R⟩ ∈ V
7		eleq1 1149	. . . . . . 7 ⊢ (x = ⟨z, 0R⟩ → (x ∈ ℝ ↔ ⟨z, 0R⟩ ∈ ℝ))
8		eleq1 1149	. . . . . . 7 ⊢ (y = ⟨w, 0R⟩ → (y ∈ ℝ ↔ ⟨w, 0R⟩ ∈ ℝ))
9	7, 8	bi2anan9 478	. . . . . 6 ⊢ ((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) → ((x ∈ ℝ ∧ y ∈ ℝ) ↔ (⟨z, 0R⟩ ∈ ℝ ∧ ⟨w, 0R⟩ ∈ ℝ)))
10		opreq1 3006	. . . . . . . 8 ⊢ (x = ⟨z, 0R⟩ → (x + (y · i)) = (⟨z, 0R⟩ + (y · i)))
11		opreq1 3006	. . . . . . . . 9 ⊢ (y = ⟨w, 0R⟩ → (y · i) = (⟨w, 0R⟩ · i))
12	11	opreq2d 3013	. . . . . . . 8 ⊢ (y = ⟨w, 0R⟩ → (⟨z, 0R⟩ + (y · i)) = (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)))
13	10, 12	sylan9eq 1144	. . . . . . 7 ⊢ ((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) → (x + (y · i)) = (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)))
14	13	cleq2d 1112	. . . . . 6 ⊢ ((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) → (⟨z, w⟩ = (x + (y · i)) ↔ ⟨z, w⟩ = (⟨z, 0R⟩ + (⟨w, 0R⟩ · i))))
15	9, 14	anbi12d 476	. . . . 5 ⊢ ((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) → (((x ∈ ℝ ∧ y ∈ ℝ) ∧ ⟨z, w⟩ = (x + (y · i))) ↔ ((⟨z, 0R⟩ ∈ ℝ ∧ ⟨w, 0R⟩ ∈ ℝ) ∧ ⟨z, w⟩ = (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)))))
16	5, 6, 15	cla4e2v 1406	. . . 4 ⊢ (((⟨z, 0R⟩ ∈ ℝ ∧ ⟨w, 0R⟩ ∈ ℝ) ∧ ⟨z, w⟩ = (⟨z, 0R⟩ + (⟨w, 0R⟩ · i))) → ∃x∃y((x ∈ ℝ ∧ y ∈ ℝ) ∧ ⟨z, w⟩ = (x + (y · i))))
17		opelreal 4043	. . . . . 6 ⊢ (⟨z, 0R⟩ ∈ ℝ ↔ z ∈ R)
18		opelreal 4043	. . . . . 6 ⊢ (⟨w, 0R⟩ ∈ ℝ ↔ w ∈ R)
19	17, 18	anbi12i 369	. . . . 5 ⊢ ((⟨z, 0R⟩ ∈ ℝ ∧ ⟨w, 0R⟩ ∈ ℝ) ↔ (z ∈ R ∧ w ∈ R))
20	19	biimpr 134	. . . 4 ⊢ ((z ∈ R ∧ w ∈ R) → (⟨z, 0R⟩ ∈ ℝ ∧ ⟨w, 0R⟩ ∈ ℝ))
21		0r 3983	. . . . . . . . . . 11 ⊢ 0R ∈ R
22		1r 3984	. . . . . . . . . . . . 13 ⊢ 1R ∈ R
23	21, 22	pm3.2i 234	. . . . . . . . . . . 12 ⊢ (0R ∈ R ∧ 1R ∈ R)
24		mulcnsr 4048	. . . . . . . . . . . 12 ⊢ (((w ∈ R ∧ 0R ∈ R) ∧ (0R ∈ R ∧ 1R ∈ R)) → (⟨w, 0R⟩ · ⟨0R, 1R⟩) = ⟨((w ·R 0R) +R (-1R ·R (0R ·R 1R))), ((0R ·R 0R) +R (w ·R 1R))⟩)
25	23, 24	mpan2 519	. . . . . . . . . . 11 ⊢ ((w ∈ R ∧ 0R ∈ R) → (⟨w, 0R⟩ · ⟨0R, 1R⟩) = ⟨((w ·R 0R) +R (-1R ·R (0R ·R 1R))), ((0R ·R 0R) +R (w ·R 1R))⟩)
26	21, 25	mpan2 519	. . . . . . . . . 10 ⊢ (w ∈ R → (⟨w, 0R⟩ · ⟨0R, 1R⟩) = ⟨((w ·R 0R) +R (-1R ·R (0R ·R 1R))), ((0R ·R 0R) +R (w ·R 1R))⟩)
27		opeq12 1878	. . . . . . . . . . 11 ⊢ ((((w ·R 0R) +R (-1R ·R (0R ·R 1R))) = 0R ∧ ((0R ·R 0R) +R (w ·R 1R)) = w) → ⟨((w ·R 0R) +R (-1R ·R (0R ·R 1R))), ((0R ·R 0R) +R (w ·R 1R))⟩ = ⟨0R, w⟩)
28		00sr 4002	. . . . . . . . . . . . 13 ⊢ (w ∈ R → (w ·R 0R) = 0R)
29	28	opreq1d 3012	. . . . . . . . . . . 12 ⊢ (w ∈ R → ((w ·R 0R) +R (-1R ·R (0R ·R 1R))) = (0R +R (-1R ·R (0R ·R 1R))))
30		1idsr 4001	. . . . . . . . . . . . . . . . 17 ⊢ (0R ∈ R → (0R ·R 1R) = 0R)
31	21, 30	ax-mp 6	. . . . . . . . . . . . . . . 16 ⊢ (0R ·R 1R) = 0R
32	31	opreq2i 3010	. . . . . . . . . . . . . . 15 ⊢ (-1R ·R (0R ·R 1R)) = (-1R ·R 0R)
33		m1r 3985	. . . . . . . . . . . . . . . 16 ⊢ -1R ∈ R
34		00sr 4002	. . . . . . . . . . . . . . . 16 ⊢ (-1R ∈ R → (-1R ·R 0R) = 0R)
35	33, 34	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ (-1R ·R 0R) = 0R
36	32, 35	eqtr 1119	. . . . . . . . . . . . . 14 ⊢ (-1R ·R (0R ·R 1R)) = 0R
37	36	opreq2i 3010	. . . . . . . . . . . . 13 ⊢ (0R +R (-1R ·R (0R ·R 1R))) = (0R +R 0R)
38		0idsr 4000	. . . . . . . . . . . . . 14 ⊢ (0R ∈ R → (0R +R 0R) = 0R)
39	21, 38	ax-mp 6	. . . . . . . . . . . . 13 ⊢ (0R +R 0R) = 0R
40	37, 39	eqtr 1119	. . . . . . . . . . . 12 ⊢ (0R +R (-1R ·R (0R ·R 1R))) = 0R
41	29, 40	syl6eq 1140	. . . . . . . . . . 11 ⊢ (w ∈ R → ((w ·R 0R) +R (-1R ·R (0R ·R 1R))) = 0R)
42		1idsr 4001	. . . . . . . . . . . . 13 ⊢ (w ∈ R → (w ·R 1R) = w)
43	42	opreq2d 3013	. . . . . . . . . . . 12 ⊢ (w ∈ R → ((0R ·R 0R) +R (w ·R 1R)) = ((0R ·R 0R) +R w))
44		0idsr 4000	. . . . . . . . . . . . 13 ⊢ (w ∈ R → (w +R 0R) = w)
45		00sr 4002	. . . . . . . . . . . . . . . 16 ⊢ (0R ∈ R → (0R ·R 0R) = 0R)
46	21, 45	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ (0R ·R 0R) = 0R
47	46	opreq1i 3009	. . . . . . . . . . . . . 14 ⊢ ((0R ·R 0R) +R w) = (0R +R w)
48	21	elisseti 1355	. . . . . . . . . . . . . . 15 ⊢ 0R ∈ V
49		visset 1350	. . . . . . . . . . . . . . 15 ⊢ w ∈ V
50	48, 49	addcomsr 3990	. . . . . . . . . . . . . 14 ⊢ (0R +R w) = (w +R 0R)
51	eqtr 1119	. . . . . . . . . . . . 13 ⊢ ((0R ·R< 0R) +R w) = (w +R 0R)
52	44, 51	syl5eq 1136	. . . . . . . . . . . 12 ⊢ (w ∈ R → ((0R ·R 0R) +R w) = w)
53	43, 52	eqtrd 1128	. . . . . . . . . . 11 ⊢ (w ∈ R → ((0R ·R 0R) +R (w ·R 1R)) = w)
54	27, 41, 53	sylanc 361	. . . . . . . . . 10 ⊢ (w ∈ R → ⟨((w ·R 0R) +R (-1R ·R (0R ·R 1R))), ((0R ·R 0R) +R (w ·R 1R))⟩ = ⟨0R, w⟩)
55	26, 54	eqtrd 1128	. . . . . . . . 9 ⊢ (w ∈ R → (⟨w, 0R⟩ · ⟨0R, 1R⟩) = ⟨0R, w⟩)
56		df-i 4037	. . . . . . . . . 10 ⊢ i = ⟨0R, 1R⟩
57	56	opreq2i 3010	. . . . . . . . 9 ⊢ (⟨w, 0R⟩ · i) = (⟨w, 0R⟩ · ⟨0R, 1R⟩)
58	55, 57	syl5eq 1136	. . . . . . . 8 ⊢ (w ∈ R → (⟨w, 0R⟩ · i) = ⟨0R, w⟩)
59	58	opreq2d 3013	. . . . . . 7 ⊢ (w ∈ R → (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)) = (⟨z, 0R⟩ + ⟨0R, w⟩))
60	59	adantl 305	. . . . . 6 ⊢ ((z ∈ R ∧ w ∈ R) → (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)) = (⟨z, 0R⟩ + ⟨0R, w⟩))
61		addcnsr 4047	. . . . . . . 8 ⊢ (((z ∈ R ∧ 0R ∈ R) ∧ (0R ∈ R ∧ w ∈ R)) → (⟨z, 0R⟩ + ⟨0R, w⟩) = ⟨(z +R 0R), (0R +R w)⟩)
62	21, 61	mpan12 530	. . . . . . 7 ⊢ ((z ∈ R ∧ (0R ∈ R ∧ w ∈ R)) → (⟨z, 0R⟩ + ⟨0R, w⟩) = ⟨(z +R 0R), (0R +R w)⟩)
63	21, 62	mpan21 531	. . . . . 6 ⊢ ((z ∈ R ∧ w ∈ R) → (⟨z, 0R⟩ + ⟨0R, w⟩) = ⟨(z +R 0R), (0R +R w)⟩)
64		opeq12 1878	. . . . . . 7 ⊢ (((z +R 0R) = z ∧ (0R +R w) = w) → &Êang;(z +R 0R), (0R +R w)⟩ = ⟨z, w⟩)
65		0idsr 4000	. . . . . . 7 ⊢ (z ∈ R → (z +R 0R) = z)
66	44, 50	syl5eq 1136	. . . . . . 7 ⊢ (w ∈ R → (0R +R w) = w)
67	64, 65, 66	syl2an 349	. . . . . 6 ⊢ ((z ∈ R ∧ w ∈ R) → ⟨(z +R 0R), (0R +R w)⟩ = ⟨z, w⟩)
68	60, 63, 67	3eqtrd 1132	. . . . 5 ⊢ ((z ∈ R ∧ w ∈ R) → (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)) = ⟨z, w⟩)
69	68	cleqcomd 1106	. . . 4 ⊢ ((z ∈ R ∧ w ∈ R) → ⟨z, w⟩ = (⟨z, 0R⟩ + (⟨w, 0R⟩ · i)))
70	16, 20, 69	sylanc 361	. . 3 ⊢ ((z ∈ R ∧ w ∈ R) → ∃x∃y((x ∈ ℝ ∧ y ∈ ℝ) ∧ ⟨z, w⟩ = (x + (y · i))))
71		r2ex 1241	. . 3 ⊢ (∃x ∈ ℝ ∃y ∈ ℝ ⟨z, w⟩ = (x + (y · i)) ↔ ∃x∃y((x ∈ ℝ ∧ y ∈ ℝ) ∧ ⟨z, w⟩ = (x + (y · i))))
72	70, 71	sylibr 175	. 2 ⊢ ((z ∈ R ∧ w ∈ R) → ∃x ∈ ℝ ∃y ∈ ℝ ⟨z, w⟩ = (x + (y · i)))
73	1, 4, 72	optocl 2469	1 ⊢ (A ∈ ℂ → ∃x ∈ ℝ ∃y ∈ ℝ A = (x + (y · i)))

Syntax hints:   → wi 2   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  ⟨cop 1810  (class class class)co 3001  Rcnr 3787  0_Rc0r 3788  1_Rc1r 3789  -1_Rcm1r 3790   +_R cplr 3791   ·_R cmr 3792  ℂcc 4026  ℝcr 4027  ici 4030   + caddc 4031   · cmulc 4032

This theorem is referenced by:  creur 4532  creui 4533

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-i 4037  df-r 4038  df-plus 4039  df-mul 4040

metamath.org