**Description:** A complex number is zero iff its absolute value is zero. Deduction form
of abs00 . (Contributed by David Moews, 28-Feb-2017)

Ref | Expression | ||
---|---|---|---|

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

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

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

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

2 | abs00 | $${\u22a2}{A}\in \u2102\to \left(\left|{A}\right|=0\leftrightarrow {A}=0\right)$$ | |

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