Metamath Proof Explorer

Theorem ledivp1

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, 28-Sep-2005)

Ref Expression
Assertion ledivp1 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ A )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. RR )
2 peano2re 
 |-  ( B e. RR -> ( B + 1 ) e. RR )
3 2 ad2antrl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B + 1 ) e. RR )
4 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. RR )
5 ltp1 
 |-  ( B e. RR -> B < ( B + 1 ) )
6 0re 
 |-  0 e. RR
7 lelttr 
 |-  ( ( 0 e. RR /\ B e. RR /\ ( B + 1 ) e. RR ) -> ( ( 0 <_ B /\ B < ( B + 1 ) ) -> 0 < ( B + 1 ) ) )
8 6 7 mp3an1 
 |-  ( ( B e. RR /\ ( B + 1 ) e. RR ) -> ( ( 0 <_ B /\ B < ( B + 1 ) ) -> 0 < ( B + 1 ) ) )
9 2 8 mpdan 
 |-  ( B e. RR -> ( ( 0 <_ B /\ B < ( B + 1 ) ) -> 0 < ( B + 1 ) ) )
10 5 9 mpan2d 
 |-  ( B e. RR -> ( 0 <_ B -> 0 < ( B + 1 ) ) )
11 10 imp 
 |-  ( ( B e. RR /\ 0 <_ B ) -> 0 < ( B + 1 ) )
12 11 gt0ne0d 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( B + 1 ) =/= 0 )
13 12 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B + 1 ) =/= 0 )
14 4 3 13 redivcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A / ( B + 1 ) ) e. RR )
15 2 adantr 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( B + 1 ) e. RR )
16 15 11 jca 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( ( B + 1 ) e. RR /\ 0 < ( B + 1 ) ) )
17 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( B + 1 ) e. RR /\ 0 < ( B + 1 ) ) ) -> 0 <_ ( A / ( B + 1 ) ) )
18 16 17 sylan2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A / ( B + 1 ) ) )
19 14 18 jca 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) e. RR /\ 0 <_ ( A / ( B + 1 ) ) ) )
20 lep1 
 |-  ( B e. RR -> B <_ ( B + 1 ) )
21 20 ad2antrl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B <_ ( B + 1 ) )
22 lemul2a 
 |-  ( ( ( B e. RR /\ ( B + 1 ) e. RR /\ ( ( A / ( B + 1 ) ) e. RR /\ 0 <_ ( A / ( B + 1 ) ) ) ) /\ B <_ ( B + 1 ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ ( ( A / ( B + 1 ) ) x. ( B + 1 ) ) )
23 1 3 19 21 22 syl31anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ ( ( A / ( B + 1 ) ) x. ( B + 1 ) ) )
24 recn 
 |-  ( A e. RR -> A e. CC )
25 24 ad2antrr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. CC )
26 2 recnd 
 |-  ( B e. RR -> ( B + 1 ) e. CC )
27 26 ad2antrl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B + 1 ) e. CC )
28 25 27 13 divcan1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. ( B + 1 ) ) = A )
29 23 28 breqtrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ A )