Metamath Proof Explorer

Theorem ltsubpos

Description: Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion ltsubpos ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B − A < B

Proof

Step Hyp Ref Expression
1 ltaddpos ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B < B + A
2 ltsubadd ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → B − A < B ↔ B < B + A
3 2 3anidm13 ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A < B ↔ B < B + A
4 3 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A < B ↔ B < B + A
5 1 4 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B − A < B