Metamath Proof Explorer


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 · 𝑦 ) ) )