Step | Hyp | Ref
| Expression |
1 | | aks4d1p6.7 |
. . . . . . 7
โข ๐พ = (๐ pCnt ๐
) |
2 | 1 | a1i 11 |
. . . . . 6
โข (๐ โ ๐พ = (๐ pCnt ๐
)) |
3 | | aks4d1p6.5 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
4 | | aks4d1p6.1 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
(โคโฅโ3)) |
5 | | aks4d1p6.2 |
. . . . . . . . . 10
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
6 | | aks4d1p6.3 |
. . . . . . . . . 10
โข ๐ต = (โโ((2
logb ๐)โ5)) |
7 | | aks4d1p6.4 |
. . . . . . . . . 10
โข ๐
= inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) |
8 | 4, 5, 6, 7 | aks4d1p4 40582 |
. . . . . . . . 9
โข (๐ โ (๐
โ (1...๐ต) โง ยฌ ๐
โฅ ๐ด)) |
9 | 8 | simpld 496 |
. . . . . . . 8
โข (๐ โ ๐
โ (1...๐ต)) |
10 | | elfznn 13476 |
. . . . . . . 8
โข (๐
โ (1...๐ต) โ ๐
โ โ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
โข (๐ โ ๐
โ โ) |
12 | 3, 11 | pccld 16727 |
. . . . . 6
โข (๐ โ (๐ pCnt ๐
) โ
โ0) |
13 | 2, 12 | eqeltrd 2834 |
. . . . 5
โข (๐ โ ๐พ โ
โ0) |
14 | 13 | nn0zd 12530 |
. . . 4
โข (๐ โ ๐พ โ โค) |
15 | 14 | zred 12612 |
. . 3
โข (๐ โ ๐พ โ โ) |
16 | | prmnn 16555 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
17 | 3, 16 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โ) |
18 | 17 | nnred 12173 |
. . . 4
โข (๐ โ ๐ โ โ) |
19 | 17 | nngt0d 12207 |
. . . 4
โข (๐ โ 0 < ๐) |
20 | 6 | a1i 11 |
. . . . . . . 8
โข (๐ โ ๐ต = (โโ((2 logb ๐)โ5))) |
21 | | 2re 12232 |
. . . . . . . . . . . 12
โข 2 โ
โ |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
23 | | 2pos 12261 |
. . . . . . . . . . . 12
โข 0 <
2 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 0 < 2) |
25 | | eluzelz 12778 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ3) โ ๐ โ โค) |
26 | 4, 25 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
27 | 26 | zred 12612 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
28 | | 0red 11163 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ
โ) |
29 | | 3re 12238 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 3 โ
โ) |
31 | | 3pos 12263 |
. . . . . . . . . . . . 13
โข 0 <
3 |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 0 < 3) |
33 | | eluzle 12781 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ3) โ 3 โค ๐) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ 3 โค ๐) |
35 | 28, 30, 27, 32, 34 | ltletrd 11320 |
. . . . . . . . . . 11
โข (๐ โ 0 < ๐) |
36 | | 1red 11161 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โ
โ) |
37 | | 1lt2 12329 |
. . . . . . . . . . . . . 14
โข 1 <
2 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 1 < 2) |
39 | 36, 38 | ltned 11296 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ 2) |
40 | 39 | necomd 2996 |
. . . . . . . . . . 11
โข (๐ โ 2 โ 1) |
41 | 22, 24, 27, 35, 40 | relogbcld 40476 |
. . . . . . . . . 10
โข (๐ โ (2 logb ๐) โ
โ) |
42 | | 5nn0 12438 |
. . . . . . . . . . 11
โข 5 โ
โ0 |
43 | 42 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 5 โ
โ0) |
44 | 41, 43 | reexpcld 14074 |
. . . . . . . . 9
โข (๐ โ ((2 logb ๐)โ5) โ
โ) |
45 | | ceilcl 13753 |
. . . . . . . . 9
โข (((2
logb ๐)โ5)
โ โ โ (โโ((2 logb ๐)โ5)) โ โค) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โค) |
47 | 20, 46 | eqeltrd 2834 |
. . . . . . 7
โข (๐ โ ๐ต โ โค) |
48 | 47 | zred 12612 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
49 | | 9re 12257 |
. . . . . . . . . 10
โข 9 โ
โ |
50 | 49 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 9 โ
โ) |
51 | | 9pos 12271 |
. . . . . . . . . 10
โข 0 <
9 |
52 | 51 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 < 9) |
53 | 27, 34 | 3lexlogpow5ineq4 40559 |
. . . . . . . . 9
โข (๐ โ 9 < ((2 logb
๐)โ5)) |
54 | 28, 50, 44, 52, 53 | lttrd 11321 |
. . . . . . . 8
โข (๐ โ 0 < ((2 logb
๐)โ5)) |
55 | | ceilge 13756 |
. . . . . . . . . 10
โข (((2
logb ๐)โ5)
โ โ โ ((2 logb ๐)โ5) โค (โโ((2
logb ๐)โ5))) |
56 | 44, 55 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((2 logb ๐)โ5) โค
(โโ((2 logb ๐)โ5))) |
57 | 56, 20 | breqtrrd 5134 |
. . . . . . . 8
โข (๐ โ ((2 logb ๐)โ5) โค ๐ต) |
58 | 28, 44, 48, 54, 57 | ltletrd 11320 |
. . . . . . 7
โข (๐ โ 0 < ๐ต) |
59 | 47, 58 | jca 513 |
. . . . . 6
โข (๐ โ (๐ต โ โค โง 0 < ๐ต)) |
60 | | elnnz 12514 |
. . . . . 6
โข (๐ต โ โ โ (๐ต โ โค โง 0 <
๐ต)) |
61 | 59, 60 | sylibr 233 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
62 | 61 | nnred 12173 |
. . . 4
โข (๐ โ ๐ต โ โ) |
63 | 61 | nngt0d 12207 |
. . . 4
โข (๐ โ 0 < ๐ต) |
64 | | 2z 12540 |
. . . . . . . . 9
โข 2 โ
โค |
65 | 64 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ
โค) |
66 | 65 | zred 12612 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
67 | | prmuz2 16577 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
68 | 3, 67 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ2)) |
69 | | eluzle 12781 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ 2 โค ๐) |
70 | 68, 69 | syl 17 |
. . . . . . 7
โข (๐ โ 2 โค ๐) |
71 | 36, 66, 18, 38, 70 | ltletrd 11320 |
. . . . . 6
โข (๐ โ 1 < ๐) |
72 | 36, 71 | ltned 11296 |
. . . . 5
โข (๐ โ 1 โ ๐) |
73 | 72 | necomd 2996 |
. . . 4
โข (๐ โ ๐ โ 1) |
74 | 18, 19, 62, 63, 73 | relogbcld 40476 |
. . 3
โข (๐ โ (๐ logb ๐ต) โ โ) |
75 | 66, 24, 62, 63, 40 | relogbcld 40476 |
. . 3
โข (๐ โ (2 logb ๐ต) โ
โ) |
76 | 17 | nnrpd 12960 |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
77 | 76 | rpcnd 12964 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
78 | 76 | rpne0d 12967 |
. . . . . 6
โข (๐ โ ๐ โ 0) |
79 | 77, 78, 14 | cxpexpzd 26082 |
. . . . 5
โข (๐ โ (๐โ๐๐พ) = (๐โ๐พ)) |
80 | 18, 13 | reexpcld 14074 |
. . . . . . 7
โข (๐ โ (๐โ๐พ) โ โ) |
81 | 11 | nnred 12173 |
. . . . . . 7
โข (๐ โ ๐
โ โ) |
82 | 2 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ (๐โ๐พ) = (๐โ(๐ pCnt ๐
))) |
83 | | pcdvds 16741 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐
โ โ) โ (๐โ(๐ pCnt ๐
)) โฅ ๐
) |
84 | 3, 11, 83 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐โ(๐ pCnt ๐
)) โฅ ๐
) |
85 | 17 | nnzd 12531 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
86 | | zexpcl 13988 |
. . . . . . . . . . 11
โข ((๐ โ โค โง (๐ pCnt ๐
) โ โ0) โ (๐โ(๐ pCnt ๐
)) โ โค) |
87 | 85, 12, 86 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ (๐โ(๐ pCnt ๐
)) โ โค) |
88 | | dvdsle 16197 |
. . . . . . . . . 10
โข (((๐โ(๐ pCnt ๐
)) โ โค โง ๐
โ โ) โ ((๐โ(๐ pCnt ๐
)) โฅ ๐
โ (๐โ(๐ pCnt ๐
)) โค ๐
)) |
89 | 87, 11, 88 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((๐โ(๐ pCnt ๐
)) โฅ ๐
โ (๐โ(๐ pCnt ๐
)) โค ๐
)) |
90 | 84, 89 | mpd 15 |
. . . . . . . 8
โข (๐ โ (๐โ(๐ pCnt ๐
)) โค ๐
) |
91 | 82, 90 | eqbrtrd 5128 |
. . . . . . 7
โข (๐ โ (๐โ๐พ) โค ๐
) |
92 | | elfzle2 13451 |
. . . . . . . 8
โข (๐
โ (1...๐ต) โ ๐
โค ๐ต) |
93 | 9, 92 | syl 17 |
. . . . . . 7
โข (๐ โ ๐
โค ๐ต) |
94 | 80, 81, 62, 91, 93 | letrd 11317 |
. . . . . 6
โข (๐ โ (๐โ๐พ) โค ๐ต) |
95 | 78, 73 | nelprd 4618 |
. . . . . . . 8
โข (๐ โ ยฌ ๐ โ {0, 1}) |
96 | 77, 95 | eldifd 3922 |
. . . . . . 7
โข (๐ โ ๐ โ (โ โ {0,
1})) |
97 | 62 | recnd 11188 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
98 | 28, 63 | ltned 11296 |
. . . . . . . . . . 11
โข (๐ โ 0 โ ๐ต) |
99 | 98 | necomd 2996 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ 0) |
100 | 99 | neneqd 2945 |
. . . . . . . . 9
โข (๐ โ ยฌ ๐ต = 0) |
101 | | elsng 4601 |
. . . . . . . . . 10
โข (๐ต โ โ โ (๐ต โ {0} โ ๐ต = 0)) |
102 | 61, 101 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ต โ {0} โ ๐ต = 0)) |
103 | 100, 102 | mtbird 325 |
. . . . . . . 8
โข (๐ โ ยฌ ๐ต โ {0}) |
104 | 97, 103 | eldifd 3922 |
. . . . . . 7
โข (๐ โ ๐ต โ (โ โ
{0})) |
105 | | cxplogb 26152 |
. . . . . . 7
โข ((๐ โ (โ โ {0, 1})
โง ๐ต โ (โ
โ {0})) โ (๐โ๐(๐ logb ๐ต)) = ๐ต) |
106 | 96, 104, 105 | syl2anc 585 |
. . . . . 6
โข (๐ โ (๐โ๐(๐ logb ๐ต)) = ๐ต) |
107 | 94, 106 | breqtrrd 5134 |
. . . . 5
โข (๐ โ (๐โ๐พ) โค (๐โ๐(๐ logb ๐ต))) |
108 | 79, 107 | eqbrtrd 5128 |
. . . 4
โข (๐ โ (๐โ๐๐พ) โค (๐โ๐(๐ logb ๐ต))) |
109 | 76 | rpred 12962 |
. . . . 5
โข (๐ โ ๐ โ โ) |
110 | 36, 66, 109, 38, 70 | ltletrd 11320 |
. . . . 5
โข (๐ โ 1 < ๐) |
111 | 109, 110,
15, 74 | cxpled 26091 |
. . . 4
โข (๐ โ (๐พ โค (๐ logb ๐ต) โ (๐โ๐๐พ) โค (๐โ๐(๐ logb ๐ต)))) |
112 | 108, 111 | mpbird 257 |
. . 3
โข (๐ โ ๐พ โค (๐ logb ๐ต)) |
113 | 22, 38 | rplogcld 26000 |
. . . . 5
โข (๐ โ (logโ2) โ
โ+) |
114 | 109, 110 | rplogcld 26000 |
. . . . 5
โข (๐ โ (logโ๐) โ
โ+) |
115 | 61 | nnrpd 12960 |
. . . . . 6
โข (๐ โ ๐ต โ
โ+) |
116 | 115 | relogcld 25994 |
. . . . 5
โข (๐ โ (logโ๐ต) โ
โ) |
117 | 61 | nnge1d 12206 |
. . . . . 6
โข (๐ โ 1 โค ๐ต) |
118 | 62, 117 | logge0d 26001 |
. . . . 5
โข (๐ โ 0 โค (logโ๐ต)) |
119 | | 2rp 12925 |
. . . . . . . 8
โข 2 โ
โ+ |
120 | 119 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โ+) |
121 | 120, 76 | logled 25998 |
. . . . . 6
โข (๐ โ (2 โค ๐ โ (logโ2) โค (logโ๐))) |
122 | 70, 121 | mpbid 231 |
. . . . 5
โข (๐ โ (logโ2) โค
(logโ๐)) |
123 | 113, 114,
116, 118, 122 | lediv2ad 12984 |
. . . 4
โข (๐ โ ((logโ๐ต) / (logโ๐)) โค ((logโ๐ต) / (logโ2))) |
124 | | relogbval 26138 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง ๐ต โ โ+) โ (๐ logb ๐ต) = ((logโ๐ต) / (logโ๐))) |
125 | 68, 115, 124 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ logb ๐ต) = ((logโ๐ต) / (logโ๐))) |
126 | 125 | eqcomd 2739 |
. . . 4
โข (๐ โ ((logโ๐ต) / (logโ๐)) = (๐ logb ๐ต)) |
127 | 65 | uzidd 12784 |
. . . . . 6
โข (๐ โ 2 โ
(โคโฅโ2)) |
128 | | relogbval 26138 |
. . . . . 6
โข ((2
โ (โคโฅโ2) โง ๐ต โ โ+) โ (2
logb ๐ต) =
((logโ๐ต) /
(logโ2))) |
129 | 127, 115,
128 | syl2anc 585 |
. . . . 5
โข (๐ โ (2 logb ๐ต) = ((logโ๐ต) /
(logโ2))) |
130 | 129 | eqcomd 2739 |
. . . 4
โข (๐ โ ((logโ๐ต) / (logโ2)) = (2
logb ๐ต)) |
131 | 123, 126,
130 | 3brtr3d 5137 |
. . 3
โข (๐ โ (๐ logb ๐ต) โค (2 logb ๐ต)) |
132 | 15, 74, 75, 112, 131 | letrd 11317 |
. 2
โข (๐ โ ๐พ โค (2 logb ๐ต)) |
133 | | flge 13716 |
. . 3
โข (((2
logb ๐ต) โ
โ โง ๐พ โ
โค) โ (๐พ โค (2
logb ๐ต) โ
๐พ โค (โโ(2
logb ๐ต)))) |
134 | 75, 14, 133 | syl2anc 585 |
. 2
โข (๐ โ (๐พ โค (2 logb ๐ต) โ ๐พ โค (โโ(2 logb
๐ต)))) |
135 | 132, 134 | mpbid 231 |
1
โข (๐ โ ๐พ โค (โโ(2 logb
๐ต))) |