**Description:** Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017)

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

Hypothesis | lt0ne0d.1 | $${\u22a2}{\phi}\to {A}<0$$ | |

Assertion | lt0ne0d | $${\u22a2}{\phi}\to {A}\ne 0$$ |

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

1 | lt0ne0d.1 | $${\u22a2}{\phi}\to {A}<0$$ | |

2 | 0re | $${\u22a2}0\in \mathbb{R}$$ | |

3 | 2 | ltnri | $${\u22a2}\neg 0<0$$ |

4 | breq1 | $${\u22a2}{A}=0\to \left({A}<0\leftrightarrow 0<0\right)$$ | |

5 | 3 4 | mtbiri | $${\u22a2}{A}=0\to \neg {A}<0$$ |

6 | 5 | necon2ai | $${\u22a2}{A}<0\to {A}\ne 0$$ |

7 | 1 6 | syl | $${\u22a2}{\phi}\to {A}\ne 0$$ |