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	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$

Proof

Step	Hyp	Ref	Expression
1		df-c	$$⊢ℂ=𝑹\times 𝑹$$
2		eqeq1	$$⊢⟨z,w⟩=A\to \left(⟨z,w⟩=x+\mathrm{i}y\leftrightarrow A=x+\mathrm{i}y\right)$$
3	2	2rexbidv	$$⊢⟨z,w⟩=A\to \left(\exists x\in ℝ\exists y\in ℝ⟨z,w⟩=x+\mathrm{i}y\leftrightarrow \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\right)$$
4		opelreal	$$⊢⟨z,0_{𝑹}⟩\in ℝ\leftrightarrow z\in 𝑹$$
5		opelreal	$$⊢⟨w,0_{𝑹}⟩\in ℝ\leftrightarrow w\in 𝑹$$
6	4 5	anbi12i	$$⊢\left(⟨z,0_{𝑹}⟩\in ℝ\wedge ⟨w,0_{𝑹}⟩\in ℝ\right)\leftrightarrow \left(z\in 𝑹\wedge w\in 𝑹\right)$$
7	6	biimpri	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to \left(⟨z,0_{𝑹}⟩\in ℝ\wedge ⟨w,0_{𝑹}⟩\in ℝ\right)$$
8		df-i	$$⊢\mathrm{i}=⟨0_{𝑹},1_{𝑹}⟩$$
9	8	oveq1i	$$⊢\mathrm{i}⟨w,0_{𝑹}⟩=⟨0_{𝑹},1_{𝑹}⟩⟨w,0_{𝑹}⟩$$
10		0r	$$⊢0_{𝑹}\in 𝑹$$
11		1sr	$$⊢1_{𝑹}\in 𝑹$$
12		mulcnsr	$$⊢\left(\left(0_{𝑹}\in 𝑹\wedge 1_{𝑹}\in 𝑹\right)\wedge \left(w\in 𝑹\wedge 0_{𝑹}\in 𝑹\right)\right)\to ⟨0_{𝑹},1_{𝑹}⟩⟨w,0_{𝑹}⟩=⟨\left(0_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)⟩$$
13	10 11 12	mpanl12	$$⊢\left(w\in 𝑹\wedge 0_{𝑹}\in 𝑹\right)\to ⟨0_{𝑹},1_{𝑹}⟩⟨w,0_{𝑹}⟩=⟨\left(0_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)⟩$$
14	10 13	mpan2	$$⊢w\in 𝑹\to ⟨0_{𝑹},1_{𝑹}⟩⟨w,0_{𝑹}⟩=⟨\left(0_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)⟩$$
15		mulcomsr	$$⊢0_{𝑹}{\cdot }_{𝑹}w=w{\cdot }_{𝑹}{0}_{𝑹}$$
16		00sr	$$⊢w\in 𝑹\to w{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
17	15 16	syl5eq	$$⊢w\in 𝑹\to 0_{𝑹}{\cdot }_{𝑹}w=0_{𝑹}$$
18	17	oveq1d	$$⊢w\in 𝑹\to \left(0_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right)=0_{𝑹}{+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right)$$
19		00sr	$$⊢1_{𝑹}\in 𝑹\to 1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
20	11 19	ax-mp	$$⊢1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
21	20	oveq2i	$$⊢{-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)={-1}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}$$
22		m1r	$$⊢{-1}_{𝑹}\in 𝑹$$
23		00sr	$$⊢{-1}_{𝑹}\in 𝑹\to {-1}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
24	22 23	ax-mp	$$⊢{-1}_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
25	21 24	eqtri	$$⊢{-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)=0_{𝑹}$$
26	25	oveq2i	$$⊢0_{𝑹}{+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right)=0_{𝑹}{+}_{𝑹}{0}_{𝑹}$$
27		0idsr	$$⊢0_{𝑹}\in 𝑹\to 0_{𝑹}{+}_{𝑹}{0}_{𝑹}=0_{𝑹}$$
28	10 27	ax-mp	$$⊢0_{𝑹}{+}_{𝑹}{0}_{𝑹}=0_{𝑹}$$
29	26 28	eqtri	$$⊢0_{𝑹}{+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right)=0_{𝑹}$$
30	18 29	syl6eq	$$⊢w\in 𝑹\to \left(0_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right)=0_{𝑹}$$
31		mulcomsr	$$⊢1_{𝑹}{\cdot }_{𝑹}w=w{\cdot }_{𝑹}{1}_{𝑹}$$
32		1idsr	$$⊢w\in 𝑹\to w{\cdot }_{𝑹}{1}_{𝑹}=w$$
33	31 32	syl5eq	$$⊢w\in 𝑹\to 1_{𝑹}{\cdot }_{𝑹}w=w$$
34	33	oveq1d	$$⊢w\in 𝑹\to \left(1_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)=w{+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)$$
35		00sr	$$⊢0_{𝑹}\in 𝑹\to 0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
36	10 35	ax-mp	$$⊢0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
37	36	oveq2i	$$⊢w{+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)=w{+}_{𝑹}{0}_{𝑹}$$
38		0idsr	$$⊢w\in 𝑹\to w{+}_{𝑹}{0}_{𝑹}=w$$
39	37 38	syl5eq	$$⊢w\in 𝑹\to w{+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)=w$$
40	34 39	eqtrd	$$⊢w\in 𝑹\to \left(1_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)=w$$
41	30 40	opeq12d	$$⊢w\in 𝑹\to ⟨\left(0_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}w\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right)⟩=⟨0_{𝑹},w⟩$$
42	14 41	eqtrd	$$⊢w\in 𝑹\to ⟨0_{𝑹},1_{𝑹}⟩⟨w,0_{𝑹}⟩=⟨0_{𝑹},w⟩$$
43	9 42	syl5eq	$$⊢w\in 𝑹\to \mathrm{i}⟨w,0_{𝑹}⟩=⟨0_{𝑹},w⟩$$
44	43	oveq2d	$$⊢w\in 𝑹\to ⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩=⟨z,0_{𝑹}⟩+⟨0_{𝑹},w⟩$$
45	44	adantl	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to ⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩=⟨z,0_{𝑹}⟩+⟨0_{𝑹},w⟩$$
46		addcnsr	$$⊢\left(\left(z\in 𝑹\wedge 0_{𝑹}\in 𝑹\right)\wedge \left(0_{𝑹}\in 𝑹\wedge w\in 𝑹\right)\right)\to ⟨z,0_{𝑹}⟩+⟨0_{𝑹},w⟩=⟨z{+}_{𝑹}{0}_{𝑹},0_{𝑹}{+}_{𝑹}w⟩$$
47	10 46	mpanl2	$$⊢\left(z\in 𝑹\wedge \left(0_{𝑹}\in 𝑹\wedge w\in 𝑹\right)\right)\to ⟨z,0_{𝑹}⟩+⟨0_{𝑹},w⟩=⟨z{+}_{𝑹}{0}_{𝑹},0_{𝑹}{+}_{𝑹}w⟩$$
48	10 47	mpanr1	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to ⟨z,0_{𝑹}⟩+⟨0_{𝑹},w⟩=⟨z{+}_{𝑹}{0}_{𝑹},0_{𝑹}{+}_{𝑹}w⟩$$
49		0idsr	$$⊢z\in 𝑹\to z{+}_{𝑹}{0}_{𝑹}=z$$
50		addcomsr	$$⊢0_{𝑹}{+}_{𝑹}w=w{+}_{𝑹}{0}_{𝑹}$$
51	50 38	syl5eq	$$⊢w\in 𝑹\to 0_{𝑹}{+}_{𝑹}w=w$$
52		opeq12	$$⊢\left(z{+}_{𝑹}{0}_{𝑹}=z\wedge 0_{𝑹}{+}_{𝑹}w=w\right)\to ⟨z{+}_{𝑹}{0}_{𝑹},0_{𝑹}{+}_{𝑹}w⟩=⟨z,w⟩$$
53	49 51 52	syl2an	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to ⟨z{+}_{𝑹}{0}_{𝑹},0_{𝑹}{+}_{𝑹}w⟩=⟨z,w⟩$$
54	45 48 53	3eqtrrd	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to ⟨z,w⟩=⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩$$
55		opex	$$⊢⟨z,0_{𝑹}⟩\in \mathrm{V}$$
56		opex	$$⊢⟨w,0_{𝑹}⟩\in \mathrm{V}$$
57		eleq1	$$⊢x=⟨z,0_{𝑹}⟩\to \left(x\in ℝ\leftrightarrow ⟨z,0_{𝑹}⟩\in ℝ\right)$$
58		eleq1	$$⊢y=⟨w,0_{𝑹}⟩\to \left(y\in ℝ\leftrightarrow ⟨w,0_{𝑹}⟩\in ℝ\right)$$
59	57 58	bi2anan9	$$⊢\left(x=⟨z,0_{𝑹}⟩\wedge y=⟨w,0_{𝑹}⟩\right)\to \left(\left(x\in ℝ\wedge y\in ℝ\right)\leftrightarrow \left(⟨z,0_{𝑹}⟩\in ℝ\wedge ⟨w,0_{𝑹}⟩\in ℝ\right)\right)$$
60		oveq1	$$⊢x=⟨z,0_{𝑹}⟩\to x+\mathrm{i}y=⟨z,0_{𝑹}⟩+\mathrm{i}y$$
61		oveq2	$$⊢y=⟨w,0_{𝑹}⟩\to \mathrm{i}y=\mathrm{i}⟨w,0_{𝑹}⟩$$
62	61	oveq2d	$$⊢y=⟨w,0_{𝑹}⟩\to ⟨z,0_{𝑹}⟩+\mathrm{i}y=⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩$$
63	60 62	sylan9eq	$$⊢\left(x=⟨z,0_{𝑹}⟩\wedge y=⟨w,0_{𝑹}⟩\right)\to x+\mathrm{i}y=⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩$$
64	63	eqeq2d	$$⊢\left(x=⟨z,0_{𝑹}⟩\wedge y=⟨w,0_{𝑹}⟩\right)\to \left(⟨z,w⟩=x+\mathrm{i}y\leftrightarrow ⟨z,w⟩=⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩\right)$$
65	59 64	anbi12d	$$⊢\left(x=⟨z,0_{𝑹}⟩\wedge y=⟨w,0_{𝑹}⟩\right)\to \left(\left(\left(x\in ℝ\wedge y\in ℝ\right)\wedge ⟨z,w⟩=x+\mathrm{i}y\right)\leftrightarrow \left(\left(⟨z,0_{𝑹}⟩\in ℝ\wedge ⟨w,0_{𝑹}⟩\in ℝ\right)\wedge ⟨z,w⟩=⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩\right)\right)$$
66	55 56 65	spc2ev	$$⊢\left(\left(⟨z,0_{𝑹}⟩\in ℝ\wedge ⟨w,0_{𝑹}⟩\in ℝ\right)\wedge ⟨z,w⟩=⟨z,0_{𝑹}⟩+\mathrm{i}⟨w,0_{𝑹}⟩\right)\to \exists x\exists y\left(\left(x\in ℝ\wedge y\in ℝ\right)\wedge ⟨z,w⟩=x+\mathrm{i}y\right)$$
67	7 54 66	syl2anc	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to \exists x\exists y\left(\left(x\in ℝ\wedge y\in ℝ\right)\wedge ⟨z,w⟩=x+\mathrm{i}y\right)$$
68		r2ex	$$⊢\exists x\in ℝ\exists y\in ℝ⟨z,w⟩=x+\mathrm{i}y\leftrightarrow \exists x\exists y\left(\left(x\in ℝ\wedge y\in ℝ\right)\wedge ⟨z,w⟩=x+\mathrm{i}y\right)$$
69	67 68	sylibr	$$⊢\left(z\in 𝑹\wedge w\in 𝑹\right)\to \exists x\in ℝ\exists y\in ℝ⟨z,w⟩=x+\mathrm{i}y$$
70	1 3 69	optocl	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$