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 ) |