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

Metamath Proof Explorer

Theorem ltsubrp

Description: Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007)

Ref Expression
Assertion ltsubrp ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A − B < A

Proof

Step Hyp Ref Expression
1 elrp ⊢ B ∈ ℝ + ↔ B ∈ ℝ ∧ 0 < B
2 ltsubpos ⊢ B ∈ ℝ ∧ A ∈ ℝ → 0 < B ↔ A − B < A
3 2 biimpd ⊢ B ∈ ℝ ∧ A ∈ ℝ → 0 < B → A − B < A
4 3 expcom ⊢ A ∈ ℝ → B ∈ ℝ → 0 < B → A − B < A
5 4 imp32 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → A − B < A
6 1 5 sylan2b ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A − B < A