This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lt0ne0d

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

Ref Expression
Hypothesis lt0ne0d.1 ⊢ ( 𝜑 → 𝐴 < 0 )
Assertion lt0ne0d ( 𝜑 → 𝐴 ≠ 0 )

Proof

Step Hyp Ref Expression
1 lt0ne0d.1 ⊢ ( 𝜑 → 𝐴 < 0 )
2 0re ⊢ 0 ∈ ℝ
3 2 ltnri ⊢ ¬ 0 < 0
4 breq1 ⊢ ( 𝐴 = 0 → ( 𝐴 < 0 ↔ 0 < 0 ) )
5 3 4 mtbiri ⊢ ( 𝐴 = 0 → ¬ 𝐴 < 0 )
6 5 necon2ai ⊢ ( 𝐴 < 0 → 𝐴 ≠ 0 )
7 1 6 syl ⊢ ( 𝜑 → 𝐴 ≠ 0 )