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 + i y$

Proof

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

Metamath Proof Explorer

Theorem axcnre

Proof