Axiom ax-cnre

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, justified by Theorem axcnre . For naming consistency, use cnre for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999)

	Ref	Expression
Assertion	ax-cnre	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cc	⊢ ℂ
2	0 1	wcel	⊢ 𝐴 ∈ ℂ
3		vx	⊢ 𝑥
4		cr	⊢ ℝ
5		vy	⊢ 𝑦
6	3	cv	⊢ 𝑥
7		caddc	⊢ +
8		ci	⊢ i
9		cmul	⊢ ·
10	5	cv	⊢ 𝑦
11	8 10 9	co	⊢ ( i · 𝑦 )
12	6 11 7	co	⊢ ( 𝑥 + ( i · 𝑦 ) )
13	0 12	wceq	⊢ 𝐴 = ( 𝑥 + ( i · 𝑦 ) )
14	13 5 4	wrex	⊢ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) )
15	14 3 4	wrex	⊢ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) )
16	2 15	wi	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )