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 | |- ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | absrpcl | |- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ ) |
|
| 2 | 1 | rpne0d | |- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 ) |
| 3 | 2 | ex | |- ( A e. CC -> ( A =/= 0 -> ( abs ` A ) =/= 0 ) ) |
| 4 | 3 | necon4d | |- ( A e. CC -> ( ( abs ` A ) = 0 -> A = 0 ) ) |
| 5 | fveq2 | |- ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) ) |
|
| 6 | abs0 | |- ( abs ` 0 ) = 0 |
|
| 7 | 5 6 | eqtrdi | |- ( A = 0 -> ( abs ` A ) = 0 ) |
| 8 | 4 7 | impbid1 | |- ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) ) |