Database
REAL AND COMPLEX NUMBERS
Construction and axiomatization of real and complex numbers
Real and complex number postulates restated as axioms
ax-cnre
Metamath Proof Explorer
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 ยท ๐ฆ ) ) )