Metamath Proof Explorer

Theorem ltdivp1i

Description: Less-than 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 ltdivp1i 
|- ( ( 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 ltmul1 
 |-  ( ( 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 5 20 mpanr1 
 |-  ( ( ( B / ( C + 1 ) ) e. RR /\ 0 < ( C + 1 ) ) -> ( A < ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) < ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
22 18 21 mpancom 
 |-  ( 0 < ( C + 1 ) -> ( A < ( B / ( C + 1 ) ) <-> ( A x. ( C + 1 ) ) < ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
23 22 biimpd 
 |-  ( 0 < ( C + 1 ) -> ( A < ( B / ( C + 1 ) ) -> ( A x. ( C + 1 ) ) < ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
24 15 23 syl 
 |-  ( 0 <_ C -> ( A < ( B / ( C + 1 ) ) -> ( A x. ( C + 1 ) ) < ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) ) )
25 24 imp 
 |-  ( ( 0 <_ C /\ A < ( B / ( C + 1 ) ) ) -> ( A x. ( C + 1 ) ) < ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) )
26 2 recni 
 |-  B e. CC
27 5 recni 
 |-  ( C + 1 ) e. CC
28 26 27 divcan1zi 
 |-  ( ( C + 1 ) =/= 0 -> ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) = B )
29 15 16 28 3syl 
 |-  ( 0 <_ C -> ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) = B )
30 29 adantr 
 |-  ( ( 0 <_ C /\ A < ( B / ( C + 1 ) ) ) -> ( ( B / ( C + 1 ) ) x. ( C + 1 ) ) = B )
31 25 30 breqtrd 
 |-  ( ( 0 <_ C /\ A < ( B / ( C + 1 ) ) ) -> ( A x. ( C + 1 ) ) < B )
32 31 3adant1 
 |-  ( ( 0 <_ A /\ 0 <_ C /\ A < ( B / ( C + 1 ) ) ) -> ( A x. ( C + 1 ) ) < B )
33 1 3 remulcli 
 |-  ( A x. C ) e. RR
34 1 5 remulcli 
 |-  ( A x. ( C + 1 ) ) e. RR
35 33 34 2 lelttri 
 |-  ( ( ( A x. C ) <_ ( A x. ( C + 1 ) ) /\ ( A x. ( C + 1 ) ) < B ) -> ( A x. C ) < B )
36 12 32 35 syl2anc 
 |-  ( ( 0 <_ A /\ 0 <_ C /\ A < ( B / ( C + 1 ) ) ) -> ( A x. C ) < B )