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 e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cc
 |-  CC
2 0 1 wcel
 |-  A e. CC
3 vx
 |-  x
4 cr
 |-  RR
5 vy
 |-  y
6 3 cv
 |-  x
7 caddc
 |-  +
8 ci
 |-  _i
9 cmul
 |-  x.
10 5 cv
 |-  y
11 8 10 9 co
 |-  ( _i x. y )
12 6 11 7 co
 |-  ( x + ( _i x. y ) )
13 0 12 wceq
 |-  A = ( x + ( _i x. y ) )
14 13 5 4 wrex
 |-  E. y e. RR A = ( x + ( _i x. y ) )
15 14 3 4 wrex
 |-  E. x e. RR E. y e. RR A = ( x + ( _i x. y ) )
16 2 15 wi
 |-  ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )