**Description:** A negative number is the negative of its own absolute value.
(Contributed by NM, 2-Aug-1999)

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

Hypothesis | sqrtthi.1 | $${\u22a2}{A}\in \mathbb{R}$$ | |

Assertion | absnidi | $${\u22a2}{A}\le 0\to \left|{A}\right|=-{A}$$ |

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

1 | sqrtthi.1 | $${\u22a2}{A}\in \mathbb{R}$$ | |

2 | absnid | $${\u22a2}\left({A}\in \mathbb{R}\wedge {A}\le 0\right)\to \left|{A}\right|=-{A}$$ | |

3 | 1 2 | mpan | $${\u22a2}{A}\le 0\to \left|{A}\right|=-{A}$$ |