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 ยท ๐‘ฆ ) ) )