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 ) ) |
| 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 ) ) |