Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Division
recne0zi
Next ⟩
recidzi
Metamath Proof Explorer
Ascii
Unicode
Theorem
recne0zi
Description:
The reciprocal of a nonzero number is nonzero.
(Contributed by
NM
, 14-May-1999)
Ref
Expression
Hypothesis
divclz.1
⊢
A
∈
ℂ
Assertion
recne0zi
⊢
A
≠
0
→
1
A
≠
0
Proof
Step
Hyp
Ref
Expression
1
divclz.1
⊢
A
∈
ℂ
2
recne0
⊢
A
∈
ℂ
∧
A
≠
0
→
1
A
≠
0
3
1
2
mpan
⊢
A
≠
0
→
1
A
≠
0