Metamath Proof Explorer

Theorem ledivp1i

Description: "Less than or equal to" and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005)

Ref Expression
Hypotheses ltplus1.1 
|- A e. RR
prodgt0.2 
|- B e. RR
ltmul1.3 
|- C e. RR
Assertion ledivp1i 
|- ( ( 0 <_ A /\ 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( A x. C ) <_ B )

Proof

Step Hyp Ref Expression
1 ltplus1.1 
 |-  A e. RR
2 prodgt0.2 
 |-  B e. RR
3 ltmul1.3 
 |-  C e. RR
4 1re 
 |-  1 e. RR
5 3 4 readdcli 
 |-  ( C + 1 ) e. RR
6 3 ltp1i 
 |-  C < ( C + 1 )
7 3 5 6 ltleii 
 |-  C <_ ( C + 1 )
8 lemul2a 
 |-  ( ( ( C e. RR /\ ( C + 1 ) e. RR /\ ( A e. RR /\ 0 <_ A ) ) /\ C <_ ( C + 1 ) ) -> ( A x. C ) <_ ( A x. ( C + 1 ) ) )
9 7 8 mpan2 
 |-  ( ( C e. RR /\ ( C + 1 ) e. RR /\ ( A e. RR /\ 0 <_ A ) ) -> ( A x. C ) <_ ( A x. ( C + 1 ) ) )
10 3 5 9 mp3an12 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( A x. C ) <_ ( A x. ( C + 1 ) ) )
11 1 10 mpan 
 |-  ( 0 <_ A -> ( A x. C ) <_ ( A x. ( C + 1 ) ) )
12 11 3ad2ant1 
 |-  ( ( 0 <_ A /\ 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( A x. C ) <_ ( A x. ( C + 1 ) ) )
13 0re 
 |-  0 e. RR
14 13 3 5 lelttri 
 |-  ( ( 0 <_ C /\ C < ( C + 1 ) ) -> 0 < ( C + 1 ) )
15 6 14 mpan2 
 |-  ( 0 <_ C -> 0 < ( C + 1 ) )
16 5 gt0ne0i 
 |-  ( 0 < ( C + 1 ) -> ( C + 1 ) =/= 0 )
17 2 5 redivclzi 
 |-  ( ( C + 1 ) =/= 0 -> ( B / ( C + 1 ) ) e. RR )
18 16 17 syl 
 |-  ( 0 < ( C + 1 ) -> ( B / ( C + 1 ) ) e. RR )
19 lemul1 
 |-  ( ( A e. RR /\ ( B / ( C + 1 ) ) e. RR /\ ( ( C + 1 ) e. RR /\ 0 < ( C + 1 ) ) ) -> ( A <_ ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
20 1 19 mp3an1 
 |-  ( ( ( B / ( C + 1 ) ) e. RR /\ ( ( C + 1 ) e. RR /\ 0 < ( C + 1 ) ) ) -> ( A <_ ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
21 20 ex 
 |-  ( ( B / ( C + 1 ) ) e. RR -> ( ( ( C + 1 ) e. RR /\ 0 < ( C + 1 ) ) -> ( A <_ ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) ) )
22 5 21 mpani 
 |-  ( ( B / ( C + 1 ) ) e. RR -> ( 0 < ( C + 1 ) -> ( A <_ ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) ) )
23 18 22 mpcom 
 |-  ( 0 < ( C + 1 ) -> ( A <_ ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
24 23 biimpd 
 |-  ( 0 < ( C + 1 ) -> ( A <_ ( B / ( C + 1 ) ) -> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
25 15 24 syl 
 |-  ( 0 <_ C -> ( A <_ ( B / ( C + 1 ) ) -> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
26 25 imp 
 |-  ( ( 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( A x. ( C + 1 ) ) <_ ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) )
27 2 recni 
 |-  B e. CC
28 5 recni 
 |-  ( C + 1 ) e. CC
29 27 28 divcan1zi 
 |-  ( ( C + 1 ) =/= 0 -> ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) = B )
30 15 16 29 3syl 
 |-  ( 0 <_ C -> ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) = B )
31 30 adantr 
 |-  ( ( 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) = B )
32 26 31 breqtrd 
 |-  ( ( 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( A x. ( C + 1 ) ) <_ B )
33 32 3adant1 
 |-  ( ( 0 <_ A /\ 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( A x. ( C + 1 ) ) <_ B )
34 1 3 remulcli 
 |-  ( A x. C ) e. RR
35 1 5 remulcli 
 |-  ( A x. ( C + 1 ) ) e. RR
36 34 35 2 letri 
 |-  ( ( ( A x. C ) <_ ( A x. ( C + 1 ) ) /\ ( A x. ( C + 1 ) ) <_ B ) -> ( A x. C ) <_ B )
37 12 33 36 syl2anc 
 |-  ( ( 0 <_ A /\ 0 <_ C /\ A <_ ( B / ( C + 1 ) ) ) -> ( A x. C ) <_ B )