This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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