Metamath Proof Explorer

Theorem posdif

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

Ref Expression
Assertion posdif ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔0<{B}-{A}\right)$

Proof

Step Hyp Ref Expression
1 resubcl ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to {B}-{A}\in ℝ$
2 1 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}-{A}\in ℝ$
3 simpl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\in ℝ$
4 ltaddpos ${⊢}\left({B}-{A}\in ℝ\wedge {A}\in ℝ\right)\to \left(0<{B}-{A}↔{A}<{A}+{B}-{A}\right)$
5 2 3 4 syl2anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0<{B}-{A}↔{A}<{A}+{B}-{A}\right)$
6 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
7 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
8 pncan3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}-{A}={B}$
9 6 7 8 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}+{B}-{A}={B}$
10 9 breq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{A}+{B}-{A}↔{A}<{B}\right)$
11 5 10 bitr2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}↔0<{B}-{A}\right)$