Step | Hyp | Ref
| Expression |
1 | | nn0re 12485 |
. . 3
โข (๐ โ โ0
โ ๐ โ
โ) |
2 | 1 | adantl 481 |
. 2
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ โ
โ) |
3 | | peano2re 11391 |
. . 3
โข (๐ โ โ โ (๐ + 1) โ
โ) |
4 | 2, 3 | syl 17 |
. 2
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (๐ + 1) โ
โ) |
5 | | eluzelre 12837 |
. . 3
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
6 | | reexpcl 14049 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
7 | 5, 6 | sylan 579 |
. 2
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (๐โ๐) โ โ) |
8 | 2 | ltp1d 12148 |
. 2
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ < (๐ + 1)) |
9 | | uz2m1nn 12911 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
10 | 9 | adantr 480 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (๐ โ 1) โ
โ) |
11 | 10 | nnred 12231 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (๐ โ 1) โ
โ) |
12 | 11, 2 | remulcld 11248 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ((๐ โ 1) ยท ๐) โ
โ) |
13 | | peano2re 11391 |
. . . 4
โข (((๐ โ 1) ยท ๐) โ โ โ (((๐ โ 1) ยท ๐) + 1) โ
โ) |
14 | 12, 13 | syl 17 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (((๐ โ 1) ยท ๐) + 1) โ
โ) |
15 | | 1red 11219 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ 1 โ
โ) |
16 | | nn0ge0 12501 |
. . . . . 6
โข (๐ โ โ0
โ 0 โค ๐) |
17 | 16 | adantl 481 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ 0 โค
๐) |
18 | 10 | nnge1d 12264 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ 1 โค
(๐ โ
1)) |
19 | 2, 11, 17, 18 | lemulge12d 12156 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ โค ((๐ โ 1) ยท ๐)) |
20 | 2, 12, 15, 19 | leadd1dd 11832 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (๐ + 1) โค (((๐ โ 1) ยท ๐) + 1)) |
21 | 5 | adantr 480 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ โ
โ) |
22 | | simpr 484 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ โ
โ0) |
23 | | eluzge2nn0 12875 |
. . . . . 6
โข (๐ โ
(โคโฅโ2) โ ๐ โ
โ0) |
24 | | nn0ge0 12501 |
. . . . . 6
โข (๐ โ โ0
โ 0 โค ๐) |
25 | 23, 24 | syl 17 |
. . . . 5
โข (๐ โ
(โคโฅโ2) โ 0 โค ๐) |
26 | 25 | adantr 480 |
. . . 4
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ 0 โค
๐) |
27 | | bernneq2 14198 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0
โง 0 โค ๐) โ
(((๐ โ 1) ยท
๐) + 1) โค (๐โ๐)) |
28 | 21, 22, 26, 27 | syl3anc 1368 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (((๐ โ 1) ยท ๐) + 1) โค (๐โ๐)) |
29 | 4, 14, 7, 20, 28 | letrd 11375 |
. 2
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ (๐ + 1) โค (๐โ๐)) |
30 | 2, 4, 7, 8, 29 | ltletrd 11378 |
1
โข ((๐ โ
(โคโฅโ2) โง ๐ โ โ0) โ ๐ < (๐โ๐)) |