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 A A = 0 A = 0

Proof

Step Hyp Ref Expression
1 absrpcl A A 0 A +
2 1 rpne0d A A 0 A 0
3 2 ex A A 0 A 0
4 3 necon4d A A = 0 A = 0
5 fveq2 A = 0 A = 0
6 abs0 0 = 0
7 5 6 syl6eq A = 0 A = 0
8 4 7 impbid1 A A = 0 A = 0