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