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 e. CC -> E.x e. RR E.y e. RR A = (x + (y x. i)))

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

Proof of Theorem axcnre

Step	Hyp	Ref	Expression
1		df-c 4034	. 2 |- CC = (R. X. R.)
2		cleq1 1107	. . . 4 |- (<.z, w>. = A -> (<.z, w>. = (x + (y x. i)) <-> A = (x + (y x. i))))
3	2	birexdv 1220	. . 3 |- (<.z, w>. = A -> (E.y e. RR <.z, w>. = (x + (y x. i)) <-> E.y e. RR A = (x + (y x. i))))
4	3	birexdv 1220	. 2 |- (<.z, w>. = A -> (E.x e. RR E.y e. RR <.z, w>. = (x + (y x. i)) <-> E.x e. RR E.y e. RR A = (x + (y x. i))))
5		opex 1893	. . . . 5 |- <.z, 0R>. e. V
6		opex 1893	. . . . 5 |- <.w, 0R>. e. V
7		eleq1 1149	. . . . . . 7 |- (x = <.z, 0R>. -> (x e. RR <-> <.z, 0R>. e. RR))
8		eleq1 1149	. . . . . . 7 |- (y = <.w, 0R>. -> (y e. RR <-> <.w, 0R>. e. RR))
9	7, 8	bi2anan9 478	. . . . . 6 |- ((x = <.z, 0R>. /\ y = <.w, 0R>.) -> ((x e. RR /\ y e. RR) <-> (<.z, 0R>. e. RR /\ <.w, 0R>. e. RR)))
10		opreq1 3006	. . . . . . . 8 |- (x = <.z, 0R>. -> (x + (y x. i)) = (<.z, 0R>. + (y x. i)))
11		opreq1 3006	. . . . . . . . 9 |- (y = <.w, 0R>. -> (y x. i) = (<.w, 0R>. x. i))
12	11	opreq2d 3013	. . . . . . . 8 |- (y = <.w, 0R>. -> (<.z, 0R>. + (y x. i)) = (<.z, 0R>. + (<.w, 0R>. x. i)))
13	10, 12	sylan9eq 1144	. . . . . . 7 |- ((x = <.z, 0R>. /\ y = <.w, 0R>.) -> (x + (y x. i)) = (<.z, 0R>. + (<.w, 0R>. x. i)))
14	13	cleq2d 1112	. . . . . 6 |- ((x = <.z, 0R>. /\ y = <.w, 0R>.) -> (<.z, w>. = (x + (y x. i)) <-> <.z, w>. = (<.z, 0R>. + (<.w, 0R>. x. i))))
15	9, 14	anbi12d 476	. . . . 5 |- ((x = <.z, 0R>. /\ y = <.w, 0R>.) -> (((x e. RR /\ y e. RR) /\ <.z, w>. = (x + (y x. i))) <-> ((<.z, 0R>. e. RR /\ <.w, 0R>. e. RR) /\ <.z, w>. = (<.z, 0R>. + (<.w, 0R>. x. i)))))
16	5, 6, 15	cla4e2v 1406	. . . 4 |- (((<.z, 0R>. e. RR /\ <.w, 0R>. e. RR) /\ <.z, w>. = (<.z, 0R>. + (<.w, 0R>. x. i))) -> E.xE.y((x e. RR /\ y e. RR) /\ <.z, w>. = (x + (y x. i))))
17		opelreal 4043	. . . . . 6 |- (<.z, 0R>. e. RR <-> z e. R.)
18		opelreal 4043	. . . . . 6 |- (<.w, 0R>. e. RR <-> w e. R.)
19	17, 18	anbi12i 369	. . . . 5 |- ((<.z, 0R>. e. RR /\ <.w, 0R>. e. RR) <-> (z e. R. /\ w e. R.))
20	19	biimpr 134	. . . 4 |- ((z e. R. /\ w e. R.) -> (<.z, 0R>. e. RR /\ <.w, 0R>. e. RR))
21		0r 3983	. . . . . . . . . . 11 |- 0R e. R.
22		1r 3984	. . . . . . . . . . . . 13 |- 1R e. R.
23	21, 22	pm3.2i 234	. . . . . . . . . . . 12 |- (0R e. R. /\ 1R e. R.)
24		mulcnsr 4048	. . . . . . . . . . . 12 |- (((w e. R. /\ 0R e. R.) /\ (0R e. R. /\ 1R e. R.)) -> (<.w, 0R>. x. <.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 e. R. /\ 0R e. R.) -> (<.w, 0R>. x. <.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 e. R. -> (<.w, 0R>. x. <.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 e. R. -> (w .R 0R) = 0R)
29	28	opreq1d 3012	. . . . . . . . . . . 12 |- (w e. R. -> ((w .R 0R) +R (-1R .R (0R .R 1R))) = (0R +R (-1R .R (0R .R 1R))))
30		1idsr 4001	. . . . . . . . . . . . . . . . 17 |- (0R e. 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 e. R.
34		00sr 4002	. . . . . . . . . . . . . . . 16 |- (-1R e. 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 e. 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 e. R. -> ((w .R 0R) +R (-1R .R (0R .R 1R))) = 0R)
42		1idsr 4001	. . . . . . . . . . . . 13 |- (w e. R. -> (w .R 1R) = w)
43	42	opreq2d 3013	. . . . . . . . . . . 12 |- (w e. R. -> ((0R .R 0R) +R (w .R 1R)) = ((0R .R 0R) +R w))
44		0idsr 4000	. . . . . . . . . . . . 13 |- (w e. R. -> (w +R 0R) = w)
45		00sr 4002	. . . . . . . . . . . . . . . 16 |- (0R e. 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 e. V
49		visset 1350	. . . . . . . . . . . . . . 15 |- w e. V
50	48, 49	addcomsr 3990	. . . . . . . . . . . . . 14 |- (0R +R w) = (w +R 0R)
51	47, 50	eqtr 1119	. . . . . . . . . . . . 13 |- ((0R .R 0R) +R w) = (w +R 0R)
52	44, 51	syl5eq 1136	. . . . . . . . . . . 12 |- (w e. R. -> ((0R .R 0R) +R w) = w)
53	43, 52	eqtrd 1128	. . . . . . . . . . 11 |- (w e. R. -> ((0R .R 0R) +R (w .R 1R)) = w)
54	27, 41, 53	sylanc 361	. . . . . . . . . 10 |- (w e. 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 e. R. -> (<.w, 0R>. x. <.0R, 1R>.) = <.0R, w>.)
56		df-i 4037	. . . . . . . . . 10 |- i = <.0R, 1R>.
57	56	opreq2i 3010	. . . . . . . . 9 |- (<.w, 0R>. x. i) = (<.w, 0R>. x. <.0R, 1R>.)
58	55, 57	syl5eq 1136	. . . . . . . 8 |- (w e. R. -> (<.w, 0R>. x. i) = <.0R, w>.)
59	58	opreq2d 3013	. . . . . . 7 |- (w e. R. -> (<.z, 0R>. + (<.w, 0R>. x. i)) = (<.z, 0R>. + <.0R, w>.))
60	59	adantl 305	. . . . . 6 |- ((z e. R. /\ w e. R.) -> (<.z, 0R>. + (<.w, 0R>. x. i)) = (<.z, 0R>. + <.0R, w>.))
61		addcnsr 4047	. . . . . . . 8 |- (((z e. R. /\ 0R e. R.) /\ (0R e. R. /\ w e. R.)) -> (<.z, 0R>. + <.0R, w>.) = <.(z +R 0R), (0R +R w)>.)
62	21, 61	mpan12 530	. . . . . . 7 |- ((z e. R. /\ (0R e. R. /\ w e. R.)) -> (<.z, 0R>. + <.0R, w>.) = <.(z +R 0R), (0R +R w)>.)
63	21, 62	mpan21 531	. . . . . 6 |- ((z e. R. /\ w e. R.) -> (<.z, 0R>. + <.0R, w>.) = <.(z +R 0R), (0R +R w)>.)
64		opeq12 1878	. . . . . . 7 |- (((z +R 0R) = z /\ (0R +R w) = w) -> <.(z +R 0R), (0R +R w)>. = <.z, w>.)
65		0idsr 4000	. . . . . . 7 |- (z e. R. -> (z +R 0R) = z)
66	44, 50	syl5eq 1136	. . . . . . 7 |- (w e. R. -> (0R +R w) = w)
67	64, 65, 66	syl2an 349	. . . . . 6 |- ((z e. R. /\ w e. R.) -> <.(z +R 0R), (0R +R w)>. = <.z, w>.)
68	60, 63, 67	3eqtrd 1132	. . . . 5 |- ((z e. R. /\ w e. R.) -> (<.z, 0R>. + (<.w, 0R>. x. i)) = <.z, w>.)
69	68	cleqcomd 1106	. . . 4 |- ((z e. R. /\ w e. R.) -> <.z, w>. = (<.z, 0R>. + (<.w, 0R>. x. i)))
70	16, 20, 69	sylanc 361	. . 3 |- ((z e. R. /\ w e. R.) -> E.xE.y((x e. RR /\ y e. RR) /\ <.z, w>. = (x + (y x. i))))
71		r2ex 1241	. . 3 |- (E.x e. RR E.y e. RR <.z, w>.