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

Metamath Proof Explorer

Theorem difrp

Description: Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014)

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

Proof

Step Hyp Ref Expression
1 posdif ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ 0 < B − A
2 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
3 2 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ
4 elrp ⊢ B − A ∈ ℝ + ↔ B − A ∈ ℝ ∧ 0 < B − A
5 4 baib ⊢ B − A ∈ ℝ → B − A ∈ ℝ + ↔ 0 < B − A
6 3 5 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ + ↔ 0 < B − A
7 1 6 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ B − A ∈ ℝ +