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