Metamath Proof Explorer

Theorem ledivge1le

Description: If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021)

Ref Expression
Assertion ledivge1le 
|- ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( A <_ B -> ( A / C ) <_ B ) )

Proof

Step Hyp Ref Expression
1 divle1le 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) <_ 1 <-> A <_ B ) )
2 1 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( ( A / B ) <_ 1 <-> A <_ B ) )
3 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
4 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( A / B ) e. RR )
5 1red 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> 1 e. RR )
6 rpre 
 |-  ( C e. RR+ -> C e. RR )
7 6 adantl 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> C e. RR )
8 letr 
 |-  ( ( ( A / B ) e. RR /\ 1 e. RR /\ C e. RR ) -> ( ( ( A / B ) <_ 1 /\ 1 <_ C ) -> ( A / B ) <_ C ) )
9 4 5 7 8 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( ( ( A / B ) <_ 1 /\ 1 <_ C ) -> ( A / B ) <_ C ) )
10 9 expd 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( ( A / B ) <_ 1 -> ( 1 <_ C -> ( A / B ) <_ C ) ) )
11 2 10 sylbird 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( A <_ B -> ( 1 <_ C -> ( A / B ) <_ C ) ) )
12 11 com23 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ C e. RR+ ) -> ( 1 <_ C -> ( A <_ B -> ( A / B ) <_ C ) ) )
13 12 expimpd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( C e. RR+ /\ 1 <_ C ) -> ( A <_ B -> ( A / B ) <_ C ) ) )
14 13 ex 
 |-  ( A e. RR -> ( B e. RR+ -> ( ( C e. RR+ /\ 1 <_ C ) -> ( A <_ B -> ( A / B ) <_ C ) ) ) )
15 14 3imp1 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) /\ A <_ B ) -> ( A / B ) <_ C )
16 simp1 
 |-  ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> A e. RR )
17 6 adantr 
 |-  ( ( C e. RR+ /\ 1 <_ C ) -> C e. RR )
18 0lt1 
 |-  0 < 1
19 0red 
 |-  ( C e. RR+ -> 0 e. RR )
20 1red 
 |-  ( C e. RR+ -> 1 e. RR )
21 ltletr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ C e. RR ) -> ( ( 0 < 1 /\ 1 <_ C ) -> 0 < C ) )
22 19 20 6 21 syl3anc 
 |-  ( C e. RR+ -> ( ( 0 < 1 /\ 1 <_ C ) -> 0 < C ) )
23 18 22 mpani 
 |-  ( C e. RR+ -> ( 1 <_ C -> 0 < C ) )
24 23 imp 
 |-  ( ( C e. RR+ /\ 1 <_ C ) -> 0 < C )
25 17 24 jca 
 |-  ( ( C e. RR+ /\ 1 <_ C ) -> ( C e. RR /\ 0 < C ) )
26 25 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( C e. RR /\ 0 < C ) )
27 rpregt0 
 |-  ( B e. RR+ -> ( B e. RR /\ 0 < B ) )
28 27 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( B e. RR /\ 0 < B ) )
29 16 26 28 3jca 
 |-  ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( A e. RR /\ ( C e. RR /\ 0 < C ) /\ ( B e. RR /\ 0 < B ) ) )
30 29 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) /\ A <_ B ) -> ( A e. RR /\ ( C e. RR /\ 0 < C ) /\ ( B e. RR /\ 0 < B ) ) )
31 lediv23 
 |-  ( ( A e. RR /\ ( C e. RR /\ 0 < C ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / C ) <_ B <-> ( A / B ) <_ C ) )
32 30 31 syl 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) /\ A <_ B ) -> ( ( A / C ) <_ B <-> ( A / B ) <_ C ) )
33 15 32 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) /\ A <_ B ) -> ( A / C ) <_ B )
34 33 ex 
 |-  ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( A <_ B -> ( A / C ) <_ B ) )