This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary real and complex functions Square root; absolute value absne0d
Description: The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of Gleason p. 133. (Contributed by Mario
Carneiro , 29-May-2016)
Ref
Expression
Hypotheses
abscld.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
absne0d.2 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion
absne0d ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≠ 0 )
Proof
Step
Hyp
Ref
Expression
1
abscld.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2
absne0d.2 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3
1
abs00ad ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
4
3
necon3bid ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
5
2 4
mpbird ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≠ 0 )