**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 | $${\u22a2}{\phi}\to {A}\in \u2102$$ | |

absne0d.2 | $${\u22a2}{\phi}\to {A}\ne 0$$ | ||

Assertion | absne0d | $${\u22a2}{\phi}\to \left|{A}\right|\ne 0$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | abscld.1 | $${\u22a2}{\phi}\to {A}\in \u2102$$ | |

2 | absne0d.2 | $${\u22a2}{\phi}\to {A}\ne 0$$ | |

3 | 1 | abs00ad | $${\u22a2}{\phi}\to \left(\left|{A}\right|=0\leftrightarrow {A}=0\right)$$ |

4 | 3 | necon3bid | $${\u22a2}{\phi}\to \left(\left|{A}\right|\ne 0\leftrightarrow {A}\ne 0\right)$$ |

5 | 2 4 | mpbird | $${\u22a2}{\phi}\to \left|{A}\right|\ne 0$$ |