Metamath Proof Explorer


Theorem divgt1b

Description: The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020)

Ref Expression
Assertion divgt1b A + B A < B 1 < B A

Proof

Step Hyp Ref Expression
1 rpcn A + A
2 1 adantr A + B A
3 2 mulid2d A + B 1 A = A
4 3 eqcomd A + B A = 1 A
5 4 breq1d A + B A < B 1 A < B
6 1red A + B 1
7 simpr A + B B
8 rpregt0 A + A 0 < A
9 8 adantr A + B A 0 < A
10 ltmuldiv 1 B A 0 < A 1 A < B 1 < B A
11 6 7 9 10 syl3anc A + B 1 A < B 1 < B A
12 5 11 bitrd A + B A < B 1 < B A