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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 ↔ ( 𝐵 − 𝐴 ) < 𝐵 ) )

Proof

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