Metamath Proof Explorer


Theorem divge1b

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

Ref Expression
Assertion divge1b A + B A B 1 B A

Proof

Step Hyp Ref Expression
1 rpcn A + A
2 1 mulid2d A + 1 A = A
3 2 eqcomd A + A = 1 A
4 3 adantr 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 lemuldiv 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