Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
2cnne0
Next ⟩
2rene0
Metamath Proof Explorer
Ascii
Unicode
Theorem
2cnne0
Description:
2 is a nonzero complex number.
(Contributed by
David A. Wheeler
, 7-Dec-2018)
Ref
Expression
Assertion
2cnne0
⊢
2
∈
ℂ
∧
2
≠
0
Proof
Step
Hyp
Ref
Expression
1
2cn
⊢
2
∈
ℂ
2
2ne0
⊢
2
≠
0
3
1
2
pm3.2i
⊢
2
∈
ℂ
∧
2
≠
0