Step | Hyp | Ref
| Expression |
1 | | ltplus1.1 |
. . . 4
โข ๐ด โ โ |
2 | | ltmul1.3 |
. . . . 5
โข ๐ถ โ โ |
3 | | 1re 11218 |
. . . . . 6
โข 1 โ
โ |
4 | 2, 3 | readdcli 11233 |
. . . . 5
โข (๐ถ + 1) โ
โ |
5 | 2 | ltp1i 12122 |
. . . . . . 7
โข ๐ถ < (๐ถ + 1) |
6 | 2, 4, 5 | ltleii 11341 |
. . . . . 6
โข ๐ถ โค (๐ถ + 1) |
7 | | lemul2a 12073 |
. . . . . 6
โข (((๐ถ โ โ โง (๐ถ + 1) โ โ โง
(๐ด โ โ โง 0
โค ๐ด)) โง ๐ถ โค (๐ถ + 1)) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
8 | 6, 7 | mpan2 688 |
. . . . 5
โข ((๐ถ โ โ โง (๐ถ + 1) โ โ โง
(๐ด โ โ โง 0
โค ๐ด)) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
9 | 2, 4, 8 | mp3an12 1447 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
10 | 1, 9 | mpan 687 |
. . 3
โข (0 โค
๐ด โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
11 | 10 | 3ad2ant1 1130 |
. 2
โข ((0 โค
๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
12 | | 0re 11220 |
. . . . . . . 8
โข 0 โ
โ |
13 | 12, 2, 4 | lelttri 11345 |
. . . . . . 7
โข ((0 โค
๐ถ โง ๐ถ < (๐ถ + 1)) โ 0 < (๐ถ + 1)) |
14 | 5, 13 | mpan2 688 |
. . . . . 6
โข (0 โค
๐ถ โ 0 < (๐ถ + 1)) |
15 | 4 | gt0ne0i 11753 |
. . . . . . . . 9
โข (0 <
(๐ถ + 1) โ (๐ถ + 1) โ 0) |
16 | | prodgt0.2 |
. . . . . . . . . 10
โข ๐ต โ โ |
17 | 16, 4 | redivclzi 11984 |
. . . . . . . . 9
โข ((๐ถ + 1) โ 0 โ (๐ต / (๐ถ + 1)) โ โ) |
18 | 15, 17 | syl 17 |
. . . . . . . 8
โข (0 <
(๐ถ + 1) โ (๐ต / (๐ถ + 1)) โ โ) |
19 | | ltmul1 12068 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ต / (๐ถ + 1)) โ โ โง ((๐ถ + 1) โ โ โง 0
< (๐ถ + 1))) โ
(๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
20 | 1, 19 | mp3an1 1444 |
. . . . . . . . 9
โข (((๐ต / (๐ถ + 1)) โ โ โง ((๐ถ + 1) โ โ โง 0
< (๐ถ + 1))) โ
(๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
21 | 4, 20 | mpanr1 700 |
. . . . . . . 8
โข (((๐ต / (๐ถ + 1)) โ โ โง 0 < (๐ถ + 1)) โ (๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
22 | 18, 21 | mpancom 685 |
. . . . . . 7
โข (0 <
(๐ถ + 1) โ (๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
23 | 22 | biimpd 228 |
. . . . . 6
โข (0 <
(๐ถ + 1) โ (๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
24 | 14, 23 | syl 17 |
. . . . 5
โข (0 โค
๐ถ โ (๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
25 | 24 | imp 406 |
. . . 4
โข ((0 โค
๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1))) |
26 | 16 | recni 11232 |
. . . . . . 7
โข ๐ต โ โ |
27 | 4 | recni 11232 |
. . . . . . 7
โข (๐ถ + 1) โ
โ |
28 | 26, 27 | divcan1zi 11954 |
. . . . . 6
โข ((๐ถ + 1) โ 0 โ ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)) = ๐ต) |
29 | 14, 15, 28 | 3syl 18 |
. . . . 5
โข (0 โค
๐ถ โ ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)) = ๐ต) |
30 | 29 | adantr 480 |
. . . 4
โข ((0 โค
๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)) = ๐ต) |
31 | 25, 30 | breqtrd 5167 |
. . 3
โข ((0 โค
๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท (๐ถ + 1)) < ๐ต) |
32 | 31 | 3adant1 1127 |
. 2
โข ((0 โค
๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท (๐ถ + 1)) < ๐ต) |
33 | 1, 2 | remulcli 11234 |
. . 3
โข (๐ด ยท ๐ถ) โ โ |
34 | 1, 4 | remulcli 11234 |
. . 3
โข (๐ด ยท (๐ถ + 1)) โ โ |
35 | 33, 34, 16 | lelttri 11345 |
. 2
โข (((๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1)) โง (๐ด ยท (๐ถ + 1)) < ๐ต) โ (๐ด ยท ๐ถ) < ๐ต) |
36 | 11, 32, 35 | syl2anc 583 |
1
โข ((0 โค
๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท ๐ถ) < ๐ต) |