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

Metamath Proof Explorer

Theorem posdif

Description: Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
2 1 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ
3 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
4 ltaddpos ⊢ B − A ∈ ℝ ∧ A ∈ ℝ → 0 < B − A ↔ A < A + B - A
5 2 3 4 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < B − A ↔ A < A + B - A
6 recn ⊢ A ∈ ℝ → A ∈ ℂ
7 recn ⊢ B ∈ ℝ → B ∈ ℂ
8 pncan3 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A = B
9 6 7 8 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B - A = B
10 9 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < A + B - A ↔ A < B
11 5 10 bitr2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ 0 < B − A