Metamath Proof Explorer


Theorem reposdif

Description: Comparison of two numbers whose difference is positive. Compare posdif . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion reposdif A B A < B 0 < B - A

Proof

Step Hyp Ref Expression
1 reltsub1 A B A A < B A - A < B - A
2 1 3anidm13 A B A < B A - A < B - A
3 resubid A A - A = 0
4 3 adantr A B A - A = 0
5 4 breq1d A B A - A < B - A 0 < B - A
6 2 5 bitrd A B A < B 0 < B - A