Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (1...(2
ยท ๐)) โ
Fin) |
2 | | 2nn 12233 |
. . . . . . . . . . 11
โข 2 โ
โ |
3 | | nnmulcl 12184 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
4 | 2, 3 | mpan 689 |
. . . . . . . . . 10
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
5 | 4 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท ๐) โ
โ) |
6 | | prmnn 16557 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
7 | 6 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ) |
8 | | elfznn 13477 |
. . . . . . . . . . . 12
โข (๐ โ (1...(2 ยท ๐)) โ ๐ โ โ) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ) |
10 | 9 | nnnn0d 12480 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ0) |
11 | 7, 10 | nnexpcld 14155 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐โ๐) โ โ) |
12 | | nnrp 12933 |
. . . . . . . . . 10
โข ((2
ยท ๐) โ โ
โ (2 ยท ๐)
โ โ+) |
13 | | nnrp 12933 |
. . . . . . . . . 10
โข ((๐โ๐) โ โ โ (๐โ๐) โ
โ+) |
14 | | rpdivcl 12947 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ
โ+ โง (๐โ๐) โ โ+) โ ((2
ยท ๐) / (๐โ๐)) โ
โ+) |
15 | 12, 13, 14 | syl2an 597 |
. . . . . . . . 9
โข (((2
ยท ๐) โ โ
โง (๐โ๐) โ โ) โ ((2
ยท ๐) / (๐โ๐)) โ
โ+) |
16 | 5, 11, 15 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) / (๐โ๐)) โ
โ+) |
17 | 16 | rpred 12964 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) / (๐โ๐)) โ โ) |
18 | 17 | flcld 13710 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ((2
ยท ๐) / (๐โ๐))) โ โค) |
19 | | 2z 12542 |
. . . . . . 7
โข 2 โ
โค |
20 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ) |
21 | | nnrp 12933 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ+) |
22 | | rpdivcl 12947 |
. . . . . . . . . . 11
โข ((๐ โ โ+
โง (๐โ๐) โ โ+)
โ (๐ / (๐โ๐)) โ
โ+) |
23 | 21, 13, 22 | syl2an 597 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐โ๐) โ โ) โ (๐ / (๐โ๐)) โ
โ+) |
24 | 20, 11, 23 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ / (๐โ๐)) โ
โ+) |
25 | 24 | rpred 12964 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ / (๐โ๐)) โ โ) |
26 | 25 | flcld 13710 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ(๐ / (๐โ๐))) โ โค) |
27 | | zmulcl 12559 |
. . . . . . 7
โข ((2
โ โค โง (โโ(๐ / (๐โ๐))) โ โค) โ (2 ยท
(โโ(๐ / (๐โ๐)))) โ โค) |
28 | 19, 26, 27 | sylancr 588 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท
(โโ(๐ / (๐โ๐)))) โ โค) |
29 | 18, 28 | zsubcld 12619 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โ โค) |
30 | 29 | zred 12614 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โ โ) |
31 | | 1re 11162 |
. . . . . 6
โข 1 โ
โ |
32 | | 0re 11164 |
. . . . . 6
โข 0 โ
โ |
33 | 31, 32 | ifcli 4538 |
. . . . 5
โข if(๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))), 1, 0) โ โ |
34 | 33 | a1i 11 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1, 0)
โ โ) |
35 | 28 | zred 12614 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท
(โโ(๐ / (๐โ๐)))) โ โ) |
36 | 17, 35 | resubcld 11590 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) โ (2 ยท (โโ(๐ / (๐โ๐))))) โ โ) |
37 | | 2re 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
38 | 37 | a1i 11 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 2 โ
โ) |
39 | 18 | zred 12614 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ((2
ยท ๐) / (๐โ๐))) โ โ) |
40 | | flle 13711 |
. . . . . . . . . . 11
โข (((2
ยท ๐) / (๐โ๐)) โ โ โ (โโ((2
ยท ๐) / (๐โ๐))) โค ((2 ยท ๐) / (๐โ๐))) |
41 | 17, 40 | syl 17 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ((2
ยท ๐) / (๐โ๐))) โค ((2 ยท ๐) / (๐โ๐))) |
42 | 39, 17, 35, 41 | lesub1dd 11778 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค (((2 ยท ๐) / (๐โ๐)) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |
43 | | resubcl 11472 |
. . . . . . . . . . . . 13
โข (((๐ / (๐โ๐)) โ โ โง 1 โ โ)
โ ((๐ / (๐โ๐)) โ 1) โ
โ) |
44 | 25, 31, 43 | sylancl 587 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐ / (๐โ๐)) โ 1) โ
โ) |
45 | | remulcl 11143 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ((๐ /
(๐โ๐)) โ 1) โ โ) โ (2
ยท ((๐ / (๐โ๐)) โ 1)) โ
โ) |
46 | 37, 44, 45 | sylancr 588 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท ((๐ / (๐โ๐)) โ 1)) โ
โ) |
47 | | flltp1 13712 |
. . . . . . . . . . . . . 14
โข ((๐ / (๐โ๐)) โ โ โ (๐ / (๐โ๐)) < ((โโ(๐ / (๐โ๐))) + 1)) |
48 | 25, 47 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ / (๐โ๐)) < ((โโ(๐ / (๐โ๐))) + 1)) |
49 | | 1red 11163 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 1 โ
โ) |
50 | 26 | zred 12614 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ(๐ / (๐โ๐))) โ โ) |
51 | 25, 49, 50 | ltsubaddd 11758 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((๐ / (๐โ๐)) โ 1) < (โโ(๐ / (๐โ๐))) โ (๐ / (๐โ๐)) < ((โโ(๐ / (๐โ๐))) + 1))) |
52 | 48, 51 | mpbird 257 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐ / (๐โ๐)) โ 1) < (โโ(๐ / (๐โ๐)))) |
53 | | 2pos 12263 |
. . . . . . . . . . . . . . 15
โข 0 <
2 |
54 | 37, 53 | pm3.2i 472 |
. . . . . . . . . . . . . 14
โข (2 โ
โ โง 0 < 2) |
55 | | ltmul2 12013 |
. . . . . . . . . . . . . 14
โข ((((๐ / (๐โ๐)) โ 1) โ โ โง
(โโ(๐ / (๐โ๐))) โ โ โง (2 โ โ
โง 0 < 2)) โ (((๐ / (๐โ๐)) โ 1) < (โโ(๐ / (๐โ๐))) โ (2 ยท ((๐ / (๐โ๐)) โ 1)) < (2 ยท
(โโ(๐ / (๐โ๐)))))) |
56 | 54, 55 | mp3an3 1451 |
. . . . . . . . . . . . 13
โข ((((๐ / (๐โ๐)) โ 1) โ โ โง
(โโ(๐ / (๐โ๐))) โ โ) โ (((๐ / (๐โ๐)) โ 1) < (โโ(๐ / (๐โ๐))) โ (2 ยท ((๐ / (๐โ๐)) โ 1)) < (2 ยท
(โโ(๐ / (๐โ๐)))))) |
57 | 44, 50, 56 | syl2anc 585 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((๐ / (๐โ๐)) โ 1) < (โโ(๐ / (๐โ๐))) โ (2 ยท ((๐ / (๐โ๐)) โ 1)) < (2 ยท
(โโ(๐ / (๐โ๐)))))) |
58 | 52, 57 | mpbid 231 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท ((๐ / (๐โ๐)) โ 1)) < (2 ยท
(โโ(๐ / (๐โ๐))))) |
59 | 46, 35, 17, 58 | ltsub2dd 11775 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) โ (2 ยท (โโ(๐ / (๐โ๐))))) < (((2 ยท ๐) / (๐โ๐)) โ (2 ยท ((๐ / (๐โ๐)) โ 1)))) |
60 | | 2cnd 12238 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 2 โ
โ) |
61 | | nncn 12168 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ) |
63 | 11 | nncnd 12176 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐โ๐) โ โ) |
64 | 11 | nnne0d 12210 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐โ๐) โ 0) |
65 | 60, 62, 63, 64 | divassd 11973 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) / (๐โ๐)) = (2 ยท (๐ / (๐โ๐)))) |
66 | 25 | recnd 11190 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ / (๐โ๐)) โ โ) |
67 | 60, 66 | muls1d 11622 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท ((๐ / (๐โ๐)) โ 1)) = ((2 ยท (๐ / (๐โ๐))) โ 2)) |
68 | 65, 67 | oveq12d 7380 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) โ (2 ยท ((๐ / (๐โ๐)) โ 1))) = ((2 ยท (๐ / (๐โ๐))) โ ((2 ยท (๐ / (๐โ๐))) โ 2))) |
69 | | remulcl 11143 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง (๐ /
(๐โ๐)) โ โ) โ (2 ยท (๐ / (๐โ๐))) โ โ) |
70 | 37, 25, 69 | sylancr 588 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท (๐ / (๐โ๐))) โ โ) |
71 | 70 | recnd 11190 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท (๐ / (๐โ๐))) โ โ) |
72 | | 2cn 12235 |
. . . . . . . . . . . 12
โข 2 โ
โ |
73 | | nncan 11437 |
. . . . . . . . . . . 12
โข (((2
ยท (๐ / (๐โ๐))) โ โ โง 2 โ โ)
โ ((2 ยท (๐ /
(๐โ๐))) โ ((2 ยท (๐ / (๐โ๐))) โ 2)) = 2) |
74 | 71, 72, 73 | sylancl 587 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท (๐ / (๐โ๐))) โ ((2 ยท (๐ / (๐โ๐))) โ 2)) = 2) |
75 | 68, 74 | eqtrd 2777 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) โ (2 ยท ((๐ / (๐โ๐)) โ 1))) = 2) |
76 | 59, 75 | breqtrd 5136 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) โ (2 ยท (โโ(๐ / (๐โ๐))))) < 2) |
77 | 30, 36, 38, 42, 76 | lelttrd 11320 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) < 2) |
78 | | df-2 12223 |
. . . . . . . 8
โข 2 = (1 +
1) |
79 | 77, 78 | breqtrdi 5151 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) < (1 + 1)) |
80 | | 1z 12540 |
. . . . . . . 8
โข 1 โ
โค |
81 | | zleltp1 12561 |
. . . . . . . 8
โข
((((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โ โค โง 1 โ โค)
โ (((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 1 โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) < (1 + 1))) |
82 | 29, 80, 81 | sylancl 587 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 1 โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) < (1 + 1))) |
83 | 79, 82 | mpbird 257 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 1) |
84 | | iftrue 4497 |
. . . . . . 7
โข (๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1, 0) =
1) |
85 | 84 | breq2d 5122 |
. . . . . 6
โข (๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1, 0)
โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 1)) |
86 | 83, 85 | syl5ibrcom 247 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))) โ
((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0))) |
87 | 9 | nnge1d 12208 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 1 โค ๐) |
88 | 87 | biantrurd 534 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ โค (โโ((logโ(2 ยท
๐)) / (logโ๐))) โ (1 โค ๐ โง ๐ โค (โโ((logโ(2 ยท
๐)) / (logโ๐)))))) |
89 | 6 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
90 | 89 | nnred 12175 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
91 | | prmuz2 16579 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
92 | 91 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
(โคโฅโ2)) |
93 | | eluz2gt1 12852 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ 1 <
๐) |
95 | 90, 94 | jca 513 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โ โ โง 1 <
๐)) |
96 | 95 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ โ โ โง 1 < ๐)) |
97 | | elfzelz 13448 |
. . . . . . . . . . . 12
โข (๐ โ (1...(2 ยท ๐)) โ ๐ โ โค) |
98 | 97 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โค) |
99 | 4 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ) |
100 | 99 | nnrpd 12962 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ+) |
101 | 100 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท ๐) โ
โ+) |
102 | | efexple 26645 |
. . . . . . . . . . 11
โข (((๐ โ โ โง 1 <
๐) โง ๐ โ โค โง (2 ยท ๐) โ โ+)
โ ((๐โ๐) โค (2 ยท ๐) โ ๐ โค (โโ((logโ(2 ยท
๐)) / (logโ๐))))) |
103 | 96, 98, 101, 102 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐โ๐) โค (2 ยท ๐) โ ๐ โค (โโ((logโ(2 ยท
๐)) / (logโ๐))))) |
104 | 9 | nnzd 12533 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โค) |
105 | 80 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 1 โ
โค) |
106 | 99 | nnred 12175 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ) |
107 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ 1 โ
โ) |
108 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ 2 โ
โ) |
109 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . 18
โข 1 <
2 |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ 1 <
2) |
111 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . . 18
โข (2
ยท 1) = 2 |
112 | | nnre 12167 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
113 | 112 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
114 | | 0le2 12262 |
. . . . . . . . . . . . . . . . . . . . 21
โข 0 โค
2 |
115 | 37, 114 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . 20
โข (2 โ
โ โง 0 โค 2) |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (2
โ โ โง 0 โค 2)) |
117 | | nnge1 12188 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 1 โค
๐) |
118 | 117 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ 1 โค
๐) |
119 | | lemul2a 12017 |
. . . . . . . . . . . . . . . . . . 19
โข (((1
โ โ โง ๐
โ โ โง (2 โ โ โง 0 โค 2)) โง 1 โค ๐) โ (2 ยท 1) โค (2
ยท ๐)) |
120 | 107, 113,
116, 118, 119 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท 1) โค (2 ยท ๐)) |
121 | 111, 120 | eqbrtrrid 5146 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ 2 โค
(2 ยท ๐)) |
122 | 107, 108,
106, 110, 121 | ltletrd 11322 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ) โ 1 <
(2 ยท ๐)) |
123 | 106, 122 | rplogcld 26000 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ) โ
(logโ(2 ยท ๐))
โ โ+) |
124 | 90, 94 | rplogcld 26000 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ) โ
(logโ๐) โ
โ+) |
125 | 123, 124 | rpdivcld 12981 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ
((logโ(2 ยท ๐))
/ (logโ๐)) โ
โ+) |
126 | 125 | rpred 12964 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ
((logโ(2 ยท ๐))
/ (logโ๐)) โ
โ) |
127 | 126 | flcld 13710 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โ โค) |
128 | 127 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โ โค) |
129 | | elfz 13437 |
. . . . . . . . . . 11
โข ((๐ โ โค โง 1 โ
โค โง (โโ((logโ(2 ยท ๐)) / (logโ๐))) โ โค) โ (๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (1 โค ๐ โง ๐ โค (โโ((logโ(2 ยท
๐)) / (logโ๐)))))) |
130 | 104, 105,
128, 129 | syl3anc 1372 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))) โ (1
โค ๐ โง ๐ โค
(โโ((logโ(2 ยท ๐)) / (logโ๐)))))) |
131 | 88, 103, 130 | 3bitr4rd 312 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))) โ
(๐โ๐) โค (2 ยท ๐))) |
132 | 131 | notbid 318 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (ยฌ ๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ ยฌ (๐โ๐) โค (2 ยท ๐))) |
133 | 106 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท ๐) โ
โ) |
134 | 11 | nnred 12175 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐โ๐) โ โ) |
135 | 133, 134 | ltnled 11309 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) < (๐โ๐) โ ยฌ (๐โ๐) โค (2 ยท ๐))) |
136 | 132, 135 | bitr4d 282 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (ยฌ ๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (2 ยท ๐) < (๐โ๐))) |
137 | 16 | rpge0d 12968 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 0 โค ((2 ยท
๐) / (๐โ๐))) |
138 | 137 | adantrr 716 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ 0 โค ((2 ยท ๐) / (๐โ๐))) |
139 | 11 | nngt0d 12209 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 0 < (๐โ๐)) |
140 | | ltdivmul 12037 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง ((๐โ๐) โ โ โง 0 < (๐โ๐))) โ (((2 ยท ๐) / (๐โ๐)) < 1 โ (2 ยท ๐) < ((๐โ๐) ยท 1))) |
141 | 133, 49, 134, 139, 140 | syl112anc 1375 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) < 1 โ (2 ยท ๐) < ((๐โ๐) ยท 1))) |
142 | 63 | mulid1d 11179 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐โ๐) ยท 1) = (๐โ๐)) |
143 | 142 | breq2d 5122 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) < ((๐โ๐) ยท 1) โ (2 ยท ๐) < (๐โ๐))) |
144 | 141, 143 | bitrd 279 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (((2 ยท ๐) / (๐โ๐)) < 1 โ (2 ยท ๐) < (๐โ๐))) |
145 | 144 | biimprd 248 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) < (๐โ๐) โ ((2 ยท ๐) / (๐โ๐)) < 1)) |
146 | 145 | impr 456 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((2 ยท ๐) / (๐โ๐)) < 1) |
147 | | 0p1e1 12282 |
. . . . . . . . . . . . 13
โข (0 + 1) =
1 |
148 | 146, 147 | breqtrrdi 5152 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((2 ยท ๐) / (๐โ๐)) < (0 + 1)) |
149 | 17 | adantrr 716 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((2 ยท ๐) / (๐โ๐)) โ โ) |
150 | | 0z 12517 |
. . . . . . . . . . . . 13
โข 0 โ
โค |
151 | | flbi 13728 |
. . . . . . . . . . . . 13
โข ((((2
ยท ๐) / (๐โ๐)) โ โ โง 0 โ โค)
โ ((โโ((2 ยท ๐) / (๐โ๐))) = 0 โ (0 โค ((2 ยท ๐) / (๐โ๐)) โง ((2 ยท ๐) / (๐โ๐)) < (0 + 1)))) |
152 | 149, 150,
151 | sylancl 587 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((โโ((2 ยท ๐) / (๐โ๐))) = 0 โ (0 โค ((2 ยท ๐) / (๐โ๐)) โง ((2 ยท ๐) / (๐โ๐)) < (0 + 1)))) |
153 | 138, 148,
152 | mpbir2and 712 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (โโ((2 ยท ๐) / (๐โ๐))) = 0) |
154 | 24 | rpge0d 12968 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ 0 โค (๐ / (๐โ๐))) |
155 | 154 | adantrr 716 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ 0 โค (๐ / (๐โ๐))) |
156 | 112, 21 | ltaddrp2d 12998 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ < (๐ + ๐)) |
157 | 61 | 2timesd 12403 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (2
ยท ๐) = (๐ + ๐)) |
158 | 156, 157 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ < (2 ยท ๐)) |
159 | 158 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ < (2 ยท ๐)) |
160 | 112 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ) |
161 | | lttr 11238 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง (2
ยท ๐) โ โ
โง (๐โ๐) โ โ) โ ((๐ < (2 ยท ๐) โง (2 ยท ๐) < (๐โ๐)) โ ๐ < (๐โ๐))) |
162 | 160, 133,
134, 161 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐ < (2 ยท ๐) โง (2 ยท ๐) < (๐โ๐)) โ ๐ < (๐โ๐))) |
163 | 159, 162 | mpand 694 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) < (๐โ๐) โ ๐ < (๐โ๐))) |
164 | | ltdivmul 12037 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง 1 โ
โ โง ((๐โ๐) โ โ โง 0 < (๐โ๐))) โ ((๐ / (๐โ๐)) < 1 โ ๐ < ((๐โ๐) ยท 1))) |
165 | 160, 49, 134, 139, 164 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐ / (๐โ๐)) < 1 โ ๐ < ((๐โ๐) ยท 1))) |
166 | 142 | breq2d 5122 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ < ((๐โ๐) ยท 1) โ ๐ < (๐โ๐))) |
167 | 165, 166 | bitrd 279 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((๐ / (๐โ๐)) < 1 โ ๐ < (๐โ๐))) |
168 | 163, 167 | sylibrd 259 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) < (๐โ๐) โ (๐ / (๐โ๐)) < 1)) |
169 | 168 | impr 456 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (๐ / (๐โ๐)) < 1) |
170 | 169, 147 | breqtrrdi 5152 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (๐ / (๐โ๐)) < (0 + 1)) |
171 | 25 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (๐ / (๐โ๐)) โ โ) |
172 | | flbi 13728 |
. . . . . . . . . . . . . . 15
โข (((๐ / (๐โ๐)) โ โ โง 0 โ โค)
โ ((โโ(๐ /
(๐โ๐))) = 0 โ (0 โค (๐ / (๐โ๐)) โง (๐ / (๐โ๐)) < (0 + 1)))) |
173 | 171, 150,
172 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((โโ(๐ / (๐โ๐))) = 0 โ (0 โค (๐ / (๐โ๐)) โง (๐ / (๐โ๐)) < (0 + 1)))) |
174 | 155, 170,
173 | mpbir2and 712 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (โโ(๐ / (๐โ๐))) = 0) |
175 | 174 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))) = (2 ยท 0)) |
176 | | 2t0e0 12329 |
. . . . . . . . . . . 12
โข (2
ยท 0) = 0 |
177 | 175, 176 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))) = 0) |
178 | 153, 177 | oveq12d 7380 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = (0 โ 0)) |
179 | | 0m0e0 12280 |
. . . . . . . . . 10
โข (0
โ 0) = 0 |
180 | 178, 179 | eqtrdi 2793 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) = 0) |
181 | | 0le0 12261 |
. . . . . . . . 9
โข 0 โค
0 |
182 | 180, 181 | eqbrtrdi 5149 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง (๐ โ (1...(2 ยท ๐)) โง (2 ยท ๐) < (๐โ๐))) โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 0) |
183 | 182 | expr 458 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((2 ยท ๐) < (๐โ๐) โ ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 0)) |
184 | 136, 183 | sylbid 239 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (ยฌ ๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ ((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 0)) |
185 | | iffalse 4500 |
. . . . . . . 8
โข (ยฌ
๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1, 0) =
0) |
186 | 185 | eqcomd 2743 |
. . . . . . 7
โข (ยฌ
๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ 0 = if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0)) |
187 | 186 | breq2d 5122 |
. . . . . 6
โข (ยฌ
๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค 0 โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0))) |
188 | 184, 187 | mpbidi 240 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (ยฌ ๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ ((โโ((2 ยท
๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0))) |
189 | 86, 188 | pm2.61d 179 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0)) |
190 | 1, 30, 34, 189 | fsumle 15691 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
ฮฃ๐ โ (1...(2
ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐))))) โค ฮฃ๐ โ (1...(2 ยท ๐))if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0)) |
191 | | pcbcctr 26640 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |
192 | 127 | zred 12614 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โ โ) |
193 | | flle 13711 |
. . . . . . . . 9
โข
(((logโ(2 ยท ๐)) / (logโ๐)) โ โ โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โค ((logโ(2 ยท ๐)) / (logโ๐))) |
194 | 126, 193 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โค ((logโ(2 ยท ๐)) / (logโ๐))) |
195 | 99 | nnnn0d 12480 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ0) |
196 | 89, 195 | nnexpcld 14155 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ(2 ยท ๐)) โ
โ) |
197 | 196 | nnred 12175 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ(2 ยท ๐)) โ
โ) |
198 | | bernneq3 14141 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (2 ยท ๐) โ โ0) โ (2
ยท ๐) < (๐โ(2 ยท ๐))) |
199 | 92, 195, 198 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) < (๐โ(2 ยท ๐))) |
200 | 106, 197,
199 | ltled 11310 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โค (๐โ(2 ยท ๐))) |
201 | 100 | reeflogd 25995 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ
(expโ(logโ(2 ยท ๐))) = (2 ยท ๐)) |
202 | 89 | nnrpd 12962 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ+) |
203 | 99 | nnzd 12533 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โค) |
204 | | reexplog 25966 |
. . . . . . . . . . . . 13
โข ((๐ โ โ+
โง (2 ยท ๐) โ
โค) โ (๐โ(2
ยท ๐)) =
(expโ((2 ยท ๐)
ยท (logโ๐)))) |
205 | 202, 203,
204 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ(2 ยท ๐)) = (expโ((2 ยท
๐) ยท
(logโ๐)))) |
206 | 205 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ
(expโ((2 ยท ๐)
ยท (logโ๐))) =
(๐โ(2 ยท ๐))) |
207 | 200, 201,
206 | 3brtr4d 5142 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ
(expโ(logโ(2 ยท ๐))) โค (expโ((2 ยท ๐) ยท (logโ๐)))) |
208 | 100 | relogcld 25994 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ
(logโ(2 ยท ๐))
โ โ) |
209 | 124 | rpred 12964 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ
(logโ๐) โ
โ) |
210 | 106, 209 | remulcld 11192 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ ((2
ยท ๐) ยท
(logโ๐)) โ
โ) |
211 | | efle 16007 |
. . . . . . . . . . 11
โข
(((logโ(2 ยท ๐)) โ โ โง ((2 ยท ๐) ยท (logโ๐)) โ โ) โ
((logโ(2 ยท ๐))
โค ((2 ยท ๐)
ยท (logโ๐))
โ (expโ(logโ(2 ยท ๐))) โค (expโ((2 ยท ๐) ยท (logโ๐))))) |
212 | 208, 210,
211 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ
((logโ(2 ยท ๐))
โค ((2 ยท ๐)
ยท (logโ๐))
โ (expโ(logโ(2 ยท ๐))) โค (expโ((2 ยท ๐) ยท (logโ๐))))) |
213 | 207, 212 | mpbird 257 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ
(logโ(2 ยท ๐))
โค ((2 ยท ๐)
ยท (logโ๐))) |
214 | 208, 106,
124 | ledivmul2d 13018 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ
(((logโ(2 ยท ๐)) / (logโ๐)) โค (2 ยท ๐) โ (logโ(2 ยท ๐)) โค ((2 ยท ๐) ยท (logโ๐)))) |
215 | 213, 214 | mpbird 257 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ
((logโ(2 ยท ๐))
/ (logโ๐)) โค (2
ยท ๐)) |
216 | 192, 126,
106, 194, 215 | letrd 11319 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โค (2 ยท ๐)) |
217 | | eluz 12784 |
. . . . . . . 8
โข
(((โโ((logโ(2 ยท ๐)) / (logโ๐))) โ โค โง (2 ยท ๐) โ โค) โ ((2
ยท ๐) โ
(โคโฅโ(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โค (2 ยท ๐))) |
218 | 127, 203,
217 | syl2anc 585 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((2
ยท ๐) โ
(โคโฅโ(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โค (2 ยท ๐))) |
219 | 216, 218 | mpbird 257 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
(โคโฅโ(โโ((logโ(2 ยท ๐)) / (logโ๐))))) |
220 | | fzss2 13488 |
. . . . . 6
โข ((2
ยท ๐) โ
(โคโฅโ(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (1...(2 ยท ๐))) |
221 | 219, 220 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (1...(2 ยท ๐))) |
222 | | sumhash 16775 |
. . . . 5
โข (((1...(2
ยท ๐)) โ Fin
โง (1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))) โ (1...(2 ยท ๐))) โ ฮฃ๐ โ (1...(2 ยท ๐))if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1, 0) =
(โฏโ(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))))) |
223 | 1, 221, 222 | syl2anc 585 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ
ฮฃ๐ โ (1...(2
ยท ๐))if(๐ โ
(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))), 1, 0) =
(โฏโ(1...(โโ((logโ(2 ยท ๐)) / (logโ๐)))))) |
224 | 125 | rprege0d 12971 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ
(((logโ(2 ยท ๐)) / (logโ๐)) โ โ โง 0 โค
((logโ(2 ยท ๐))
/ (logโ๐)))) |
225 | | flge0nn0 13732 |
. . . . 5
โข
((((logโ(2 ยท ๐)) / (logโ๐)) โ โ โง 0 โค
((logโ(2 ยท ๐))
/ (logโ๐))) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) โ
โ0) |
226 | | hashfz1 14253 |
. . . . 5
โข
((โโ((logโ(2 ยท ๐)) / (logโ๐))) โ โ0 โ
(โฏโ(1...(โโ((logโ(2 ยท ๐)) / (logโ๐))))) = (โโ((logโ(2
ยท ๐)) /
(logโ๐)))) |
227 | 224, 225,
226 | 3syl 18 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ
(โฏโ(1...(โโ((logโ(2 ยท ๐)) / (logโ๐))))) = (โโ((logโ(2
ยท ๐)) /
(logโ๐)))) |
228 | 223, 227 | eqtr2d 2778 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ((logโ(2 ยท ๐)) / (logโ๐))) = ฮฃ๐ โ (1...(2 ยท ๐))if(๐ โ (1...(โโ((logโ(2
ยท ๐)) /
(logโ๐)))), 1,
0)) |
229 | 190, 191,
228 | 3brtr4d 5142 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) โค (โโ((logโ(2
ยท ๐)) /
(logโ๐)))) |
230 | | simpr 486 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
231 | | nnnn0 12427 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ0) |
232 | | fzctr 13560 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ (0...(2
ยท ๐))) |
233 | | bccl2 14230 |
. . . . . . 7
โข (๐ โ (0...(2 ยท ๐)) โ ((2 ยท ๐)C๐) โ โ) |
234 | 231, 232,
233 | 3syl 18 |
. . . . . 6
โข (๐ โ โ โ ((2
ยท ๐)C๐) โ
โ) |
235 | 234 | adantr 482 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((2
ยท ๐)C๐) โ
โ) |
236 | 230, 235 | pccld 16729 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) โ
โ0) |
237 | 236 | nn0zd 12532 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) โ โค) |
238 | | efexple 26645 |
. . 3
โข (((๐ โ โ โง 1 <
๐) โง (๐ pCnt ((2 ยท ๐)C๐)) โ โค โง (2 ยท ๐) โ โ+)
โ ((๐โ(๐ pCnt ((2 ยท ๐)C๐))) โค (2 ยท ๐) โ (๐ pCnt ((2 ยท ๐)C๐)) โค (โโ((logโ(2
ยท ๐)) /
(logโ๐))))) |
239 | 90, 94, 237, 100, 238 | syl211anc 1377 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ ((๐โ(๐ pCnt ((2 ยท ๐)C๐))) โค (2 ยท ๐) โ (๐ pCnt ((2 ยท ๐)C๐)) โค (โโ((logโ(2
ยท ๐)) /
(logโ๐))))) |
240 | 229, 239 | mpbird 257 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ(๐ pCnt ((2 ยท ๐)C๐))) โค (2 ยท ๐)) |