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 )