Step | Hyp | Ref
| Expression |
1 | | elfznn 13477 |
. . . . . . 7
โข (๐ท โ
(1...(โโ๐))
โ ๐ท โ
โ) |
2 | 1 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ท โ
โ) |
3 | 2 | nnred 12175 |
. . . . 5
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ท โ
โ) |
4 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ+) โ ๐ โ
โ+) |
5 | 4 | rpregt0d 12970 |
. . . . . . 7
โข ((๐ โง ๐ โ โ+) โ (๐ โ โ โง 0 <
๐)) |
6 | 5 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (๐ โ โ
โง 0 < ๐)) |
7 | 6 | simpld 496 |
. . . . 5
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ โ
โ) |
8 | 4 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ โ
โ+) |
9 | 8 | rpge0d 12968 |
. . . . 5
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ 0 โค ๐) |
10 | 4 | rpred 12964 |
. . . . . . 7
โข ((๐ โง ๐ โ โ+) โ ๐ โ
โ) |
11 | | fznnfl 13774 |
. . . . . . 7
โข (๐ โ โ โ (๐ท โ
(1...(โโ๐))
โ (๐ท โ โ
โง ๐ท โค ๐))) |
12 | 10, 11 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ โ+) โ (๐ท โ
(1...(โโ๐))
โ (๐ท โ โ
โง ๐ท โค ๐))) |
13 | 12 | simplbda 501 |
. . . . 5
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ท โค ๐) |
14 | 3, 7, 7, 9, 13 | lemul2ad 12102 |
. . . 4
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (๐ ยท ๐ท) โค (๐ ยท ๐)) |
15 | | rpcn 12932 |
. . . . . . 7
โข (๐ โ โ+
โ ๐ โ
โ) |
16 | 15 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ+) โ ๐ โ
โ) |
17 | 16 | sqvald 14055 |
. . . . 5
โข ((๐ โง ๐ โ โ+) โ (๐โ2) = (๐ ยท ๐)) |
18 | 17 | adantr 482 |
. . . 4
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (๐โ2) = (๐ ยท ๐)) |
19 | 14, 18 | breqtrrd 5138 |
. . 3
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (๐ ยท ๐ท) โค (๐โ2)) |
20 | | 2z 12542 |
. . . . . . 7
โข 2 โ
โค |
21 | | rpexpcl 13993 |
. . . . . . 7
โข ((๐ โ โ+
โง 2 โ โค) โ (๐โ2) โ
โ+) |
22 | 4, 20, 21 | sylancl 587 |
. . . . . 6
โข ((๐ โง ๐ โ โ+) โ (๐โ2) โ
โ+) |
23 | 22 | rpred 12964 |
. . . . 5
โข ((๐ โง ๐ โ โ+) โ (๐โ2) โ
โ) |
24 | 23 | adantr 482 |
. . . 4
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (๐โ2) โ
โ) |
25 | 2 | nnrpd 12962 |
. . . 4
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ท โ
โ+) |
26 | 7, 24, 25 | lemuldivd 13013 |
. . 3
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ((๐ ยท ๐ท) โค (๐โ2) โ ๐ โค ((๐โ2) / ๐ท))) |
27 | 19, 26 | mpbid 231 |
. 2
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ๐ โค ((๐โ2) / ๐ท)) |
28 | | nndivre 12201 |
. . . 4
โข (((๐โ2) โ โ โง
๐ท โ โ) โ
((๐โ2) / ๐ท) โ
โ) |
29 | 23, 1, 28 | syl2an 597 |
. . 3
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ ((๐โ2) / ๐ท) โ
โ) |
30 | | flword2 13725 |
. . 3
โข ((๐ โ โ โง ((๐โ2) / ๐ท) โ โ โง ๐ โค ((๐โ2) / ๐ท)) โ (โโ((๐โ2) / ๐ท)) โ
(โคโฅโ(โโ๐))) |
31 | 7, 29, 27, 30 | syl3anc 1372 |
. 2
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (โโ((๐โ2) / ๐ท)) โ
(โคโฅโ(โโ๐))) |
32 | 27, 31 | jca 513 |
1
โข (((๐ โง ๐ โ โ+) โง ๐ท โ
(1...(โโ๐)))
โ (๐ โค ((๐โ2) / ๐ท) โง (โโ((๐โ2) / ๐ท)) โ
(โคโฅโ(โโ๐)))) |