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

Proof

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