Metamath Proof Explorer


Theorem abs00

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 NM, 26-Sep-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abs00 ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step Hyp Ref Expression
1 absrpcl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
2 1 rpne0d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
3 2 ex ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 → ( abs ‘ 𝐴 ) ≠ 0 ) )
4 3 necon4d ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 → 𝐴 = 0 ) )
5 fveq2 ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
6 abs0 ( abs ‘ 0 ) = 0
7 5 6 eqtrdi ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
8 4 7 impbid1 ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )