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

Metamath Proof Explorer

Theorem sublt0d

Description: When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sublt0d.1 ⊢ φ → A ∈ ℝ
sublt0d.2 ⊢ φ → B ∈ ℝ
Assertion sublt0d ⊢ φ → A − B < 0 ↔ A < B

Proof

Step Hyp Ref Expression
1 sublt0d.1 ⊢ φ → A ∈ ℝ
2 sublt0d.2 ⊢ φ → B ∈ ℝ
3 0red ⊢ φ → 0 ∈ ℝ
4 1 2 3 ltsubaddd ⊢ φ → A − B < 0 ↔ A < 0 + B
5 2 recnd ⊢ φ → B ∈ ℂ
6 5 addlidd ⊢ φ → 0 + B = B
7 6 breq2d ⊢ φ → A < 0 + B ↔ A < B
8 4 7 bitrd ⊢ φ → A − B < 0 ↔ A < B