Database
BASIC ALGEBRAIC STRUCTURES
The complex numbers as an algebraic extensible structure
Definition and basic properties
cndrng
Next ⟩
cnflddiv
Metamath Proof Explorer
Ascii
Unicode
Theorem
cndrng
Description:
The complex numbers form a division ring.
(Contributed by
Stefan O'Rear
, 27-Nov-2014)
Ref
Expression
Assertion
cndrng
⊢
ℂ
fld
∈
DivRing
Proof
Step
Hyp
Ref
Expression
1
cnfldbas
⊢
ℂ
=
Base
ℂ
fld
2
1
a1i
⊢
⊤
→
ℂ
=
Base
ℂ
fld
3
cnfldmul
⊢
×
=
⋅
ℂ
fld
4
3
a1i
⊢
⊤
→
×
=
⋅
ℂ
fld
5
cnfld0
⊢
0
=
0
ℂ
fld
6
5
a1i
⊢
⊤
→
0
=
0
ℂ
fld
7
cnfld1
⊢
1
=
1
ℂ
fld
8
7
a1i
⊢
⊤
→
1
=
1
ℂ
fld
9
cnring
⊢
ℂ
fld
∈
Ring
10
9
a1i
⊢
⊤
→
ℂ
fld
∈
Ring
11
mulne0
⊢
x
∈
ℂ
∧
x
≠
0
∧
y
∈
ℂ
∧
y
≠
0
→
x
⁢
y
≠
0
12
11
3adant1
⊢
⊤
∧
x
∈
ℂ
∧
x
≠
0
∧
y
∈
ℂ
∧
y
≠
0
→
x
⁢
y
≠
0
13
ax-1ne0
⊢
1
≠
0
14
13
a1i
⊢
⊤
→
1
≠
0
15
reccl
⊢
x
∈
ℂ
∧
x
≠
0
→
1
x
∈
ℂ
16
15
adantl
⊢
⊤
∧
x
∈
ℂ
∧
x
≠
0
→
1
x
∈
ℂ
17
recid2
⊢
x
∈
ℂ
∧
x
≠
0
→
1
x
⁢
x
=
1
18
17
adantl
⊢
⊤
∧
x
∈
ℂ
∧
x
≠
0
→
1
x
⁢
x
=
1
19
2
4
6
8
10
12
14
16
18
isdrngd
⊢
⊤
→
ℂ
fld
∈
DivRing
20
19
mptru
⊢
ℂ
fld
∈
DivRing