Metamath Proof Explorer


Theorem sublt0d

Description: When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sublt0d.1
|- ( ph -> A e. RR )
sublt0d.2
|- ( ph -> B e. RR )
Assertion sublt0d
|- ( ph -> ( ( A - B ) < 0 <-> A < B ) )

Proof

Step Hyp Ref Expression
1 sublt0d.1
 |-  ( ph -> A e. RR )
2 sublt0d.2
 |-  ( ph -> B e. RR )
3 0red
 |-  ( ph -> 0 e. RR )
4 1 2 3 ltsubaddd
 |-  ( ph -> ( ( A - B ) < 0 <-> A < ( 0 + B ) ) )
5 2 recnd
 |-  ( ph -> B e. CC )
6 5 addid2d
 |-  ( ph -> ( 0 + B ) = B )
7 6 breq2d
 |-  ( ph -> ( A < ( 0 + B ) <-> A < B ) )
8 4 7 bitrd
 |-  ( ph -> ( ( A - B ) < 0 <-> A < B ) )