Step | Hyp | Ref
| Expression |
1 | | ltplus1.1 |
. . . 4
โข ๐ด โ โ |
2 | | ltmul1.3 |
. . . . 5
โข ๐ถ โ โ |
3 | | 1re 11113 |
. . . . . 6
โข 1 โ
โ |
4 | 2, 3 | readdcli 11128 |
. . . . 5
โข (๐ถ + 1) โ
โ |
5 | 2 | ltp1i 12017 |
. . . . . . 7
โข ๐ถ < (๐ถ + 1) |
6 | 2, 4, 5 | ltleii 11236 |
. . . . . 6
โข ๐ถ โค (๐ถ + 1) |
7 | | lemul2a 11968 |
. . . . . 6
โข (((๐ถ โ โ โง (๐ถ + 1) โ โ โง
(๐ด โ โ โง 0
โค ๐ด)) โง ๐ถ โค (๐ถ + 1)) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
8 | 6, 7 | mpan2 689 |
. . . . 5
โข ((๐ถ โ โ โง (๐ถ + 1) โ โ โง
(๐ด โ โ โง 0
โค ๐ด)) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
9 | 2, 4, 8 | mp3an12 1451 |
. . . 4
โข ((๐ด โ โ โง 0 โค
๐ด) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
10 | 1, 9 | mpan 688 |
. . 3
โข (0 โค
๐ด โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
11 | 10 | 3ad2ant1 1133 |
. 2
โข ((0 โค
๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1))) |
12 | | 0re 11115 |
. . . . . . . 8
โข 0 โ
โ |
13 | 12, 2, 4 | lelttri 11240 |
. . . . . . 7
โข ((0 โค
๐ถ โง ๐ถ < (๐ถ + 1)) โ 0 < (๐ถ + 1)) |
14 | 5, 13 | mpan2 689 |
. . . . . 6
โข (0 โค
๐ถ โ 0 < (๐ถ + 1)) |
15 | 4 | gt0ne0i 11648 |
. . . . . . . . 9
โข (0 <
(๐ถ + 1) โ (๐ถ + 1) โ 0) |
16 | | prodgt0.2 |
. . . . . . . . . 10
โข ๐ต โ โ |
17 | 16, 4 | redivclzi 11879 |
. . . . . . . . 9
โข ((๐ถ + 1) โ 0 โ (๐ต / (๐ถ + 1)) โ โ) |
18 | 15, 17 | syl 17 |
. . . . . . . 8
โข (0 <
(๐ถ + 1) โ (๐ต / (๐ถ + 1)) โ โ) |
19 | | ltmul1 11963 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ต / (๐ถ + 1)) โ โ โง ((๐ถ + 1) โ โ โง 0
< (๐ถ + 1))) โ
(๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
20 | 1, 19 | mp3an1 1448 |
. . . . . . . . 9
โข (((๐ต / (๐ถ + 1)) โ โ โง ((๐ถ + 1) โ โ โง 0
< (๐ถ + 1))) โ
(๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
21 | 4, 20 | mpanr1 701 |
. . . . . . . 8
โข (((๐ต / (๐ถ + 1)) โ โ โง 0 < (๐ถ + 1)) โ (๐ด < (๐ต / (๐ถ + 1)) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)))) |
22 | 18, 21 | mpancom 686 |
. . . . . . 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 407 |
. . . 4
โข ((0 โค
๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท (๐ถ + 1)) < ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1))) |
26 | 16 | recni 11127 |
. . . . . . 7
โข ๐ต โ โ |
27 | 4 | recni 11127 |
. . . . . . 7
โข (๐ถ + 1) โ
โ |
28 | 26, 27 | divcan1zi 11849 |
. . . . . 6
โข ((๐ถ + 1) โ 0 โ ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)) = ๐ต) |
29 | 14, 15, 28 | 3syl 18 |
. . . . 5
โข (0 โค
๐ถ โ ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)) = ๐ต) |
30 | 29 | adantr 481 |
. . . 4
โข ((0 โค
๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ ((๐ต / (๐ถ + 1)) ยท (๐ถ + 1)) = ๐ต) |
31 | 25, 30 | breqtrd 5129 |
. . 3
โข ((0 โค
๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท (๐ถ + 1)) < ๐ต) |
32 | 31 | 3adant1 1130 |
. 2
โข ((0 โค
๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท (๐ถ + 1)) < ๐ต) |
33 | 1, 2 | remulcli 11129 |
. . 3
โข (๐ด ยท ๐ถ) โ โ |
34 | 1, 4 | remulcli 11129 |
. . 3
โข (๐ด ยท (๐ถ + 1)) โ โ |
35 | 33, 34, 16 | lelttri 11240 |
. 2
โข (((๐ด ยท ๐ถ) โค (๐ด ยท (๐ถ + 1)) โง (๐ด ยท (๐ถ + 1)) < ๐ต) โ (๐ด ยท ๐ถ) < ๐ต) |
36 | 11, 32, 35 | syl2anc 584 |
1
โข ((0 โค
๐ด โง 0 โค ๐ถ โง ๐ด < (๐ต / (๐ถ + 1))) โ (๐ด ยท ๐ถ) < ๐ต) |