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 ⊢ A ∈ ℂ → ∃ x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cc class ℂ
2 0 1 wcel wff A ∈ ℂ
3 vx setvar x
4 cr class ℝ
5 vy setvar y
6 3 cv setvar x
7 caddc class +
8 ci class i
9 cmul class ×
10 5 cv setvar y
11 8 10 9 co class i ⁢ y
12 6 11 7 co class x + i ⁢ y
13 0 12 wceq wff A = x + i ⁢ y
14 13 5 4 wrex wff ∃ y ∈ ℝ A = x + i ⁢ y
15 14 3 4 wrex wff ∃ x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y
16 2 15 wi wff A ∈ ℂ → ∃ x ∈ ℝ ∃ y ∈ ℝ A = x + i ⁢ y