Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p4.1 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
2 | 1 | nnred 12175 |
. . . . 5
โข (๐ โ ๐ โ โ) |
3 | | 2re 12234 |
. . . . . . . . . 10
โข 2 โ
โ |
4 | 3 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
5 | | 2pos 12263 |
. . . . . . . . . 10
โข 0 <
2 |
6 | 5 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 < 2) |
7 | 1 | nngt0d 12209 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < ๐) |
8 | | 1red 11163 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โ
โ) |
9 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . 17
โข 1 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 < 2) |
11 | 8, 10 | ltned 11298 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 โ 2) |
12 | 11 | necomd 3000 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ 1) |
13 | 4, 6, 2, 7, 12 | relogbcld 40459 |
. . . . . . . . . . . . 13
โข (๐ โ (2 logb ๐) โ
โ) |
14 | | 5nn0 12440 |
. . . . . . . . . . . . . 14
โข 5 โ
โ0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 5 โ
โ0) |
16 | 13, 15 | reexpcld 14075 |
. . . . . . . . . . . 12
โข (๐ โ ((2 logb ๐)โ5) โ
โ) |
17 | | ceilcl 13754 |
. . . . . . . . . . . 12
โข (((2
logb ๐)โ5)
โ โ โ (โโ((2 logb ๐)โ5)) โ โค) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โค) |
19 | 18 | zred 12614 |
. . . . . . . . . 10
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โ) |
20 | | aks4d1p1p4.3 |
. . . . . . . . . . . 12
โข ๐ต = (โโ((2
logb ๐)โ5)) |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ๐ต = (โโ((2 logb ๐)โ5))) |
22 | 21 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ โ โ (โโ((2
logb ๐)โ5))
โ โ)) |
23 | 19, 22 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
24 | | 0red 11165 |
. . . . . . . . . 10
โข (๐ โ 0 โ
โ) |
25 | | 7re 12253 |
. . . . . . . . . . 11
โข 7 โ
โ |
26 | 25 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 7 โ
โ) |
27 | | 7pos 12271 |
. . . . . . . . . . 11
โข 0 <
7 |
28 | 27 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 0 < 7) |
29 | | aks4d1p1p4.4 |
. . . . . . . . . . . . 13
โข (๐ โ 3 โค ๐) |
30 | 2, 29 | 3lexlogpow5ineq3 40543 |
. . . . . . . . . . . 12
โข (๐ โ 7 < ((2 logb
๐)โ5)) |
31 | 26, 16, 30 | ltled 11310 |
. . . . . . . . . . 11
โข (๐ โ 7 โค ((2 logb
๐)โ5)) |
32 | | ceilge 13757 |
. . . . . . . . . . . . 13
โข (((2
logb ๐)โ5)
โ โ โ ((2 logb ๐)โ5) โค (โโ((2
logb ๐)โ5))) |
33 | 16, 32 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ((2 logb ๐)โ5) โค
(โโ((2 logb ๐)โ5))) |
34 | 33, 21 | breqtrrd 5138 |
. . . . . . . . . . 11
โข (๐ โ ((2 logb ๐)โ5) โค ๐ต) |
35 | 26, 16, 23, 31, 34 | letrd 11319 |
. . . . . . . . . 10
โข (๐ โ 7 โค ๐ต) |
36 | 24, 26, 23, 28, 35 | ltletrd 11322 |
. . . . . . . . 9
โข (๐ โ 0 < ๐ต) |
37 | 4, 6, 23, 36, 12 | relogbcld 40459 |
. . . . . . . 8
โข (๐ โ (2 logb ๐ต) โ
โ) |
38 | 37 | flcld 13710 |
. . . . . . 7
โข (๐ โ (โโ(2
logb ๐ต)) โ
โค) |
39 | 24, 8 | readdcld 11191 |
. . . . . . . . 9
โข (๐ โ (0 + 1) โ
โ) |
40 | 38 | zred 12614 |
. . . . . . . . . 10
โข (๐ โ (โโ(2
logb ๐ต)) โ
โ) |
41 | 40, 8 | readdcld 11191 |
. . . . . . . . 9
โข (๐ โ ((โโ(2
logb ๐ต)) + 1)
โ โ) |
42 | 4, 6, 4, 6, 12 | relogbcld 40459 |
. . . . . . . . . 10
โข (๐ โ (2 logb 2)
โ โ) |
43 | 8 | leidd 11728 |
. . . . . . . . . . 11
โข (๐ โ 1 โค 1) |
44 | | 1cnd 11157 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โ
โ) |
45 | 44 | addid2d 11363 |
. . . . . . . . . . . 12
โข (๐ โ (0 + 1) =
1) |
46 | 4 | recnd 11190 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ) |
47 | 24, 6 | gtned 11297 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ 0) |
48 | | logbid1 26134 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ โง 2 โ 0 โง 2 โ 1) โ (2 logb 2) =
1) |
49 | 46, 47, 12, 48 | syl3anc 1372 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 logb 2) =
1) |
50 | 49 | eqcomd 2743 |
. . . . . . . . . . . . 13
โข (๐ โ 1 = (2 logb
2)) |
51 | 50 | eqcomd 2743 |
. . . . . . . . . . . 12
โข (๐ โ (2 logb 2) =
1) |
52 | 45, 51 | breq12d 5123 |
. . . . . . . . . . 11
โข (๐ โ ((0 + 1) โค (2
logb 2) โ 1 โค 1)) |
53 | 43, 52 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ (0 + 1) โค (2
logb 2)) |
54 | | 5re 12247 |
. . . . . . . . . . . . . . 15
โข 5 โ
โ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 5 โ
โ) |
56 | 4, 55 | readdcld 11191 |
. . . . . . . . . . . . 13
โข (๐ โ (2 + 5) โ
โ) |
57 | 3, 14 | nn0addge1i 12468 |
. . . . . . . . . . . . . 14
โข 2 โค (2
+ 5) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โค (2 +
5)) |
59 | 3 | recni 11176 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
60 | | 5cn 12248 |
. . . . . . . . . . . . . . . . 17
โข 5 โ
โ |
61 | 59, 60 | addcomi 11353 |
. . . . . . . . . . . . . . . 16
โข (2 + 5) =
(5 + 2) |
62 | | 5p2e7 12316 |
. . . . . . . . . . . . . . . 16
โข (5 + 2) =
7 |
63 | 61, 62 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข (2 + 5) =
7 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 + 5) =
7) |
65 | 26 | leidd 11728 |
. . . . . . . . . . . . . 14
โข (๐ โ 7 โค 7) |
66 | 64, 65 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
โข (๐ โ (2 + 5) โค
7) |
67 | 4, 56, 26, 58, 66 | letrd 11319 |
. . . . . . . . . . . 12
โข (๐ โ 2 โค 7) |
68 | 4, 26, 23, 67, 35 | letrd 11319 |
. . . . . . . . . . 11
โข (๐ โ 2 โค ๐ต) |
69 | | 2z 12542 |
. . . . . . . . . . . . . 14
โข 2 โ
โค |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ
โค) |
71 | 70 | uzidd 12786 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
(โคโฅโ2)) |
72 | | 2rp 12927 |
. . . . . . . . . . . . 13
โข 2 โ
โ+ |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ+) |
74 | 23, 36 | elrpd 12961 |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ
โ+) |
75 | | logbleb 26149 |
. . . . . . . . . . . 12
โข ((2
โ (โคโฅโ2) โง 2 โ โ+
โง ๐ต โ
โ+) โ (2 โค ๐ต โ (2 logb 2) โค (2
logb ๐ต))) |
76 | 71, 73, 74, 75 | syl3anc 1372 |
. . . . . . . . . . 11
โข (๐ โ (2 โค ๐ต โ (2 logb 2) โค (2
logb ๐ต))) |
77 | 68, 76 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (2 logb 2) โค
(2 logb ๐ต)) |
78 | 39, 42, 37, 53, 77 | letrd 11319 |
. . . . . . . . 9
โข (๐ โ (0 + 1) โค (2
logb ๐ต)) |
79 | | fllep1 13713 |
. . . . . . . . . 10
โข ((2
logb ๐ต) โ
โ โ (2 logb ๐ต) โค ((โโ(2 logb
๐ต)) + 1)) |
80 | 37, 79 | syl 17 |
. . . . . . . . 9
โข (๐ โ (2 logb ๐ต) โค ((โโ(2
logb ๐ต)) +
1)) |
81 | 39, 37, 41, 78, 80 | letrd 11319 |
. . . . . . . 8
โข (๐ โ (0 + 1) โค
((โโ(2 logb ๐ต)) + 1)) |
82 | 24, 40, 8 | leadd1d 11756 |
. . . . . . . 8
โข (๐ โ (0 โค (โโ(2
logb ๐ต)) โ
(0 + 1) โค ((โโ(2 logb ๐ต)) + 1))) |
83 | 81, 82 | mpbird 257 |
. . . . . . 7
โข (๐ โ 0 โค (โโ(2
logb ๐ต))) |
84 | 38, 83 | jca 513 |
. . . . . 6
โข (๐ โ ((โโ(2
logb ๐ต)) โ
โค โง 0 โค (โโ(2 logb ๐ต)))) |
85 | | elnn0z 12519 |
. . . . . 6
โข
((โโ(2 logb ๐ต)) โ โ0 โ
((โโ(2 logb ๐ต)) โ โค โง 0 โค
(โโ(2 logb ๐ต)))) |
86 | 84, 85 | sylibr 233 |
. . . . 5
โข (๐ โ (โโ(2
logb ๐ต)) โ
โ0) |
87 | 2, 86 | reexpcld 14075 |
. . . 4
โข (๐ โ (๐โ(โโ(2 logb
๐ต))) โ
โ) |
88 | | fzfid 13885 |
. . . . 5
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ Fin) |
89 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
90 | | elfznn 13477 |
. . . . . . . . 9
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ ๐ โ โ) |
91 | 90 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
92 | 91 | nnnn0d 12480 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ0) |
93 | 89, 92 | reexpcld 14075 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) โ โ) |
94 | | 1red 11163 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โ
โ) |
95 | 93, 94 | resubcld 11590 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 1) โ โ) |
96 | 88, 95 | fprodrecl 15843 |
. . . 4
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1) โ โ) |
97 | 87, 96 | remulcld 11192 |
. . 3
โข (๐ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โ
โ) |
98 | | aks4d1p1p4.2 |
. . . . 5
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
99 | 98 | a1i 11 |
. . . 4
โข (๐ โ ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
100 | 99 | eleq1d 2823 |
. . 3
โข (๐ โ (๐ด โ โ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โ
โ)) |
101 | 97, 100 | mpbird 257 |
. 2
โข (๐ โ ๐ด โ โ) |
102 | | aks4d1p1p4.7 |
. . . . . . . . 9
โข ๐ธ = ((2 logb ๐)โ4) |
103 | 102 | a1i 11 |
. . . . . . . 8
โข (๐ โ ๐ธ = ((2 logb ๐)โ4)) |
104 | 103 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (๐โ๐๐ธ) = (๐โ๐((2
logb ๐)โ4))) |
105 | | 2cnd 12238 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ) |
106 | 73 | rpne0d 12969 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ 0) |
107 | 106, 12 | nelprd 4622 |
. . . . . . . . . . . 12
โข (๐ โ ยฌ 2 โ {0,
1}) |
108 | 105, 107 | eldifd 3926 |
. . . . . . . . . . 11
โข (๐ โ 2 โ (โ โ
{0, 1})) |
109 | 2 | recnd 11190 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
110 | 24, 7 | ltned 11298 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โ ๐) |
111 | | necom 2998 |
. . . . . . . . . . . . . . . 16
โข (0 โ
๐ โ ๐ โ 0) |
112 | 111 | imbi2i 336 |
. . . . . . . . . . . . . . 15
โข ((๐ โ 0 โ ๐) โ (๐ โ ๐ โ 0)) |
113 | 110, 112 | mpbi 229 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ 0) |
114 | 113 | neneqd 2949 |
. . . . . . . . . . . . 13
โข (๐ โ ยฌ ๐ = 0) |
115 | | c0ex 11156 |
. . . . . . . . . . . . . 14
โข 0 โ
V |
116 | 115 | elsn2 4630 |
. . . . . . . . . . . . 13
โข (๐ โ {0} โ ๐ = 0) |
117 | 114, 116 | sylnibr 329 |
. . . . . . . . . . . 12
โข (๐ โ ยฌ ๐ โ {0}) |
118 | 109, 117 | eldifd 3926 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ (โ โ
{0})) |
119 | | cxplogb 26152 |
. . . . . . . . . . 11
โข ((2
โ (โ โ {0, 1}) โง ๐ โ (โ โ {0})) โ
(2โ๐(2 logb ๐)) = ๐) |
120 | 108, 118,
119 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ
(2โ๐(2 logb ๐)) = ๐) |
121 | 120 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ ๐ = (2โ๐(2
logb ๐))) |
122 | 121 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ (๐โ๐((2
logb ๐)โ4))
= ((2โ๐(2 logb ๐))โ๐((2
logb ๐)โ4))) |
123 | | eqidd 2738 |
. . . . . . . 8
โข (๐ โ
((2โ๐(2 logb ๐))โ๐((2
logb ๐)โ4))
= ((2โ๐(2 logb ๐))โ๐((2
logb ๐)โ4))) |
124 | 122, 123 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (๐โ๐((2
logb ๐)โ4))
= ((2โ๐(2 logb ๐))โ๐((2
logb ๐)โ4))) |
125 | 104, 124 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (๐โ๐๐ธ) = ((2โ๐(2
logb ๐))โ๐((2
logb ๐)โ4))) |
126 | 103 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ ((2 logb ๐)โ4) = ๐ธ) |
127 | | 4nn0 12439 |
. . . . . . . . . . . . 13
โข 4 โ
โ0 |
128 | 127 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 4 โ
โ0) |
129 | 13, 128 | reexpcld 14075 |
. . . . . . . . . . 11
โข (๐ โ ((2 logb ๐)โ4) โ
โ) |
130 | 103 | eleq1d 2823 |
. . . . . . . . . . 11
โข (๐ โ (๐ธ โ โ โ ((2 logb
๐)โ4) โ
โ)) |
131 | 129, 130 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ ๐ธ โ โ) |
132 | 131 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ ๐ธ โ โ) |
133 | 126, 132 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ((2 logb ๐)โ4) โ
โ) |
134 | 73, 13, 133 | cxpmuld 26107 |
. . . . . . 7
โข (๐ โ
(2โ๐((2 logb ๐) ยท ((2 logb ๐)โ4))) =
((2โ๐(2 logb ๐))โ๐((2
logb ๐)โ4))) |
135 | 134 | eqcomd 2743 |
. . . . . 6
โข (๐ โ
((2โ๐(2 logb ๐))โ๐((2
logb ๐)โ4))
= (2โ๐((2 logb ๐) ยท ((2 logb ๐)โ4)))) |
136 | 125, 135 | eqtrd 2777 |
. . . . 5
โข (๐ โ (๐โ๐๐ธ) = (2โ๐((2
logb ๐) ยท
((2 logb ๐)โ4)))) |
137 | 13 | recnd 11190 |
. . . . . . . . . 10
โข (๐ โ (2 logb ๐) โ
โ) |
138 | 137 | exp1d 14053 |
. . . . . . . . 9
โข (๐ โ ((2 logb ๐)โ1) = (2 logb
๐)) |
139 | 138 | eqcomd 2743 |
. . . . . . . 8
โข (๐ โ (2 logb ๐) = ((2 logb ๐)โ1)) |
140 | 139 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((2 logb ๐) ยท ((2 logb
๐)โ4)) = (((2
logb ๐)โ1)
ยท ((2 logb ๐)โ4))) |
141 | | 1nn0 12436 |
. . . . . . . . . 10
โข 1 โ
โ0 |
142 | 141 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ0) |
143 | 137, 128,
142 | expaddd 14060 |
. . . . . . . 8
โข (๐ โ ((2 logb ๐)โ(1 + 4)) = (((2
logb ๐)โ1)
ยท ((2 logb ๐)โ4))) |
144 | 143 | eqcomd 2743 |
. . . . . . 7
โข (๐ โ (((2 logb ๐)โ1) ยท ((2
logb ๐)โ4))
= ((2 logb ๐)โ(1 + 4))) |
145 | 140, 144 | eqtrd 2777 |
. . . . . 6
โข (๐ โ ((2 logb ๐) ยท ((2 logb
๐)โ4)) = ((2
logb ๐)โ(1
+ 4))) |
146 | 145 | oveq2d 7378 |
. . . . 5
โข (๐ โ
(2โ๐((2 logb ๐) ยท ((2 logb ๐)โ4))) =
(2โ๐((2 logb ๐)โ(1 + 4)))) |
147 | 136, 146 | eqtrd 2777 |
. . . 4
โข (๐ โ (๐โ๐๐ธ) = (2โ๐((2
logb ๐)โ(1
+ 4)))) |
148 | | 4cn 12245 |
. . . . . . . 8
โข 4 โ
โ |
149 | | ax-1cn 11116 |
. . . . . . . 8
โข 1 โ
โ |
150 | | 4p1e5 12306 |
. . . . . . . 8
โข (4 + 1) =
5 |
151 | 148, 149,
150 | addcomli 11354 |
. . . . . . 7
โข (1 + 4) =
5 |
152 | 151 | a1i 11 |
. . . . . 6
โข (๐ โ (1 + 4) =
5) |
153 | 152 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((2 logb ๐)โ(1 + 4)) = ((2
logb ๐)โ5)) |
154 | 153 | oveq2d 7378 |
. . . 4
โข (๐ โ
(2โ๐((2 logb ๐)โ(1 + 4))) =
(2โ๐((2 logb ๐)โ5))) |
155 | 147, 154 | eqtrd 2777 |
. . 3
โข (๐ โ (๐โ๐๐ธ) = (2โ๐((2
logb ๐)โ5))) |
156 | | 3re 12240 |
. . . . . 6
โข 3 โ
โ |
157 | 156 | a1i 11 |
. . . . 5
โข (๐ โ 3 โ
โ) |
158 | | 0le1 11685 |
. . . . . . 7
โข 0 โค
1 |
159 | 158 | a1i 11 |
. . . . . 6
โข (๐ โ 0 โค 1) |
160 | | 1lt3 12333 |
. . . . . . . 8
โข 1 <
3 |
161 | 160 | a1i 11 |
. . . . . . 7
โข (๐ โ 1 < 3) |
162 | 8, 157, 161 | ltled 11310 |
. . . . . 6
โข (๐ โ 1 โค 3) |
163 | 24, 8, 157, 159, 162 | letrd 11319 |
. . . . 5
โข (๐ โ 0 โค 3) |
164 | 24, 157, 2, 163, 29 | letrd 11319 |
. . . 4
โข (๐ โ 0 โค ๐) |
165 | 2, 164, 131 | recxpcld 26094 |
. . 3
โข (๐ โ (๐โ๐๐ธ) โ โ) |
166 | 155, 165 | eqeltrrd 2839 |
. 2
โข (๐ โ
(2โ๐((2 logb ๐)โ5)) โ โ) |
167 | 21 | eleq1d 2823 |
. . . . . 6
โข (๐ โ (๐ต โ โค โ (โโ((2
logb ๐)โ5))
โ โค)) |
168 | 18, 167 | mpbird 257 |
. . . . 5
โข (๐ โ ๐ต โ โค) |
169 | 24, 23, 36 | ltled 11310 |
. . . . 5
โข (๐ โ 0 โค ๐ต) |
170 | 168, 169 | jca 513 |
. . . 4
โข (๐ โ (๐ต โ โค โง 0 โค ๐ต)) |
171 | | elnn0z 12519 |
. . . 4
โข (๐ต โ โ0
โ (๐ต โ โค
โง 0 โค ๐ต)) |
172 | 170, 171 | sylibr 233 |
. . 3
โข (๐ โ ๐ต โ
โ0) |
173 | 4, 172 | reexpcld 14075 |
. 2
โข (๐ โ (2โ๐ต) โ โ) |
174 | 2, 7 | elrpd 12961 |
. . . . . 6
โข (๐ โ ๐ โ
โ+) |
175 | 16, 8 | readdcld 11191 |
. . . . . . . . . 10
โข (๐ โ (((2 logb ๐)โ5) + 1) โ
โ) |
176 | 15 | nn0zd 12532 |
. . . . . . . . . . . . 13
โข (๐ โ 5 โ
โค) |
177 | | logb1 26135 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ โง 2 โ 0 โง 2 โ 1) โ (2 logb 1) =
0) |
178 | 46, 47, 12, 177 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 logb 1) =
0) |
179 | 178, 24 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 logb 1)
โ โ) |
180 | 24 | leidd 11728 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โค 0) |
181 | 178 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 = (2 logb
1)) |
182 | 180, 181 | breqtrd 5136 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 โค (2 logb
1)) |
183 | 8, 157, 2, 161, 29 | ltletrd 11322 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 < ๐) |
184 | | 1rp 12926 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
โ+ |
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โ
โ+) |
186 | | logblt 26150 |
. . . . . . . . . . . . . . . 16
โข ((2
โ (โคโฅโ2) โง 1 โ โ+
โง ๐ โ
โ+) โ (1 < ๐ โ (2 logb 1) < (2
logb ๐))) |
187 | 71, 185, 174, 186 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 < ๐ โ (2 logb 1) < (2
logb ๐))) |
188 | 183, 187 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 logb 1) <
(2 logb ๐)) |
189 | 24, 179, 13, 182, 188 | lelttrd 11320 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < (2 logb
๐)) |
190 | 13, 176, 189 | 3jca 1129 |
. . . . . . . . . . . 12
โข (๐ โ ((2 logb ๐) โ โ โง 5 โ
โค โง 0 < (2 logb ๐))) |
191 | | expgt0 14008 |
. . . . . . . . . . . 12
โข (((2
logb ๐) โ
โ โง 5 โ โค โง 0 < (2 logb ๐)) โ 0 < ((2
logb ๐)โ5)) |
192 | 190, 191 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ 0 < ((2 logb
๐)โ5)) |
193 | | ltp1 12002 |
. . . . . . . . . . . 12
โข (((2
logb ๐)โ5)
โ โ โ ((2 logb ๐)โ5) < (((2 logb ๐)โ5) + 1)) |
194 | 16, 193 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((2 logb ๐)โ5) < (((2
logb ๐)โ5)
+ 1)) |
195 | 24, 16, 175, 192, 194 | lttrd 11323 |
. . . . . . . . . 10
โข (๐ โ 0 < (((2
logb ๐)โ5)
+ 1)) |
196 | 4, 6, 175, 195, 12 | relogbcld 40459 |
. . . . . . . . 9
โข (๐ โ (2 logb (((2
logb ๐)โ5)
+ 1)) โ โ) |
197 | | aks4d1p1p4.5 |
. . . . . . . . . . 11
โข ๐ถ = (2 logb (((2
logb ๐)โ5)
+ 1)) |
198 | 197 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ ๐ถ = (2 logb (((2 logb
๐)โ5) +
1))) |
199 | 198 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ โ (๐ถ โ โ โ (2 logb
(((2 logb ๐)โ5) + 1)) โ
โ)) |
200 | 196, 199 | mpbird 257 |
. . . . . . . 8
โข (๐ โ ๐ถ โ โ) |
201 | 13 | resqcld 14037 |
. . . . . . . . . 10
โข (๐ โ ((2 logb ๐)โ2) โ
โ) |
202 | | aks4d1p1p4.6 |
. . . . . . . . . . . 12
โข ๐ท = ((2 logb ๐)โ2) |
203 | 202 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ๐ท = ((2 logb ๐)โ2)) |
204 | 203 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ โ (๐ท โ โ โ ((2 logb
๐)โ2) โ
โ)) |
205 | 201, 204 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ ๐ท โ โ) |
206 | 205 | rehalfcld 12407 |
. . . . . . . 8
โข (๐ โ (๐ท / 2) โ โ) |
207 | 200, 206 | readdcld 11191 |
. . . . . . 7
โข (๐ โ (๐ถ + (๐ท / 2)) โ โ) |
208 | 131, 4, 106 | redivcld 11990 |
. . . . . . 7
โข (๐ โ (๐ธ / 2) โ โ) |
209 | 207, 208 | readdcld 11191 |
. . . . . 6
โข (๐ โ ((๐ถ + (๐ท / 2)) + (๐ธ / 2)) โ โ) |
210 | 174, 209 | rpcxpcld 26103 |
. . . . 5
โข (๐ โ (๐โ๐((๐ถ + (๐ท / 2)) + (๐ธ / 2))) โ
โ+) |
211 | 210 | rpred 12964 |
. . . 4
โข (๐ โ (๐โ๐((๐ถ + (๐ท / 2)) + (๐ธ / 2))) โ โ) |
212 | 1, 98, 20, 29 | aks4d1p1p2 40556 |
. . . . 5
โข (๐ โ ๐ด < (๐โ๐(((2
logb (((2 logb ๐)โ5) + 1)) + (((2 logb ๐)โ2) / 2)) + (((2
logb ๐)โ4)
/ 2)))) |
213 | 126 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ (((2 logb ๐)โ4) / 2) = (๐ธ / 2)) |
214 | 213 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (((2 logb (((2
logb ๐)โ5)
+ 1)) + (((2 logb ๐)โ2) / 2)) + (((2 logb ๐)โ4) / 2)) = (((2
logb (((2 logb ๐)โ5) + 1)) + (((2 logb ๐)โ2) / 2)) + (๐ธ / 2))) |
215 | 198 | eqcomd 2743 |
. . . . . . . . . 10
โข (๐ โ (2 logb (((2
logb ๐)โ5)
+ 1)) = ๐ถ) |
216 | 215 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + (((2 logb ๐)โ2) / 2)) = (๐ถ + (((2 logb ๐)โ2) / 2))) |
217 | 203 | eqcomd 2743 |
. . . . . . . . . . 11
โข (๐ โ ((2 logb ๐)โ2) = ๐ท) |
218 | 217 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ (((2 logb ๐)โ2) / 2) = (๐ท / 2)) |
219 | 218 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ (๐ถ + (((2 logb ๐)โ2) / 2)) = (๐ถ + (๐ท / 2))) |
220 | 216, 219 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + (((2 logb ๐)โ2) / 2)) = (๐ถ + (๐ท / 2))) |
221 | 220 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (((2 logb (((2
logb ๐)โ5)
+ 1)) + (((2 logb ๐)โ2) / 2)) + (๐ธ / 2)) = ((๐ถ + (๐ท / 2)) + (๐ธ / 2))) |
222 | 214, 221 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (((2 logb (((2
logb ๐)โ5)
+ 1)) + (((2 logb ๐)โ2) / 2)) + (((2 logb ๐)โ4) / 2)) = ((๐ถ + (๐ท / 2)) + (๐ธ / 2))) |
223 | 222 | oveq2d 7378 |
. . . . 5
โข (๐ โ (๐โ๐(((2
logb (((2 logb ๐)โ5) + 1)) + (((2 logb ๐)โ2) / 2)) + (((2
logb ๐)โ4)
/ 2))) = (๐โ๐((๐ถ + (๐ท / 2)) + (๐ธ / 2)))) |
224 | 212, 223 | breqtrd 5136 |
. . . 4
โข (๐ โ ๐ด < (๐โ๐((๐ถ + (๐ท / 2)) + (๐ธ / 2)))) |
225 | 200 | recnd 11190 |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
226 | 225, 105,
106 | divcan3d 11943 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐ถ) / 2) = ๐ถ) |
227 | 226 | eqcomd 2743 |
. . . . . . . . . 10
โข (๐ โ ๐ถ = ((2 ยท ๐ถ) / 2)) |
228 | 227 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ (๐ถ + (๐ท / 2)) = (((2 ยท ๐ถ) / 2) + (๐ท / 2))) |
229 | 4, 200 | remulcld 11192 |
. . . . . . . . . . . 12
โข (๐ โ (2 ยท ๐ถ) โ
โ) |
230 | 229 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐ถ) โ
โ) |
231 | 205 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ ๐ท โ โ) |
232 | 230, 231,
46, 106 | divdird 11976 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐ถ) + ๐ท) / 2) = (((2 ยท ๐ถ) / 2) + (๐ท / 2))) |
233 | 232 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐ถ) / 2) + (๐ท / 2)) = (((2 ยท ๐ถ) + ๐ท) / 2)) |
234 | 228, 233 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (๐ถ + (๐ท / 2)) = (((2 ยท ๐ถ) + ๐ท) / 2)) |
235 | | aks4d1p1p4.8 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐ถ) + ๐ท) โค ๐ธ) |
236 | 229, 205 | readdcld 11191 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐ถ) + ๐ท) โ โ) |
237 | 236, 131,
73 | lediv1d 13010 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐ถ) + ๐ท) โค ๐ธ โ (((2 ยท ๐ถ) + ๐ท) / 2) โค (๐ธ / 2))) |
238 | 235, 237 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐ถ) + ๐ท) / 2) โค (๐ธ / 2)) |
239 | 234, 238 | eqbrtrd 5132 |
. . . . . . 7
โข (๐ โ (๐ถ + (๐ท / 2)) โค (๐ธ / 2)) |
240 | 207, 208,
208, 239 | leadd1dd 11776 |
. . . . . 6
โข (๐ โ ((๐ถ + (๐ท / 2)) + (๐ธ / 2)) โค ((๐ธ / 2) + (๐ธ / 2))) |
241 | 132 | 2halvesd 12406 |
. . . . . 6
โข (๐ โ ((๐ธ / 2) + (๐ธ / 2)) = ๐ธ) |
242 | 240, 241 | breqtrd 5136 |
. . . . 5
โข (๐ โ ((๐ถ + (๐ท / 2)) + (๐ธ / 2)) โค ๐ธ) |
243 | 2, 183, 209, 131 | cxpled 26091 |
. . . . 5
โข (๐ โ (((๐ถ + (๐ท / 2)) + (๐ธ / 2)) โค ๐ธ โ (๐โ๐((๐ถ + (๐ท / 2)) + (๐ธ / 2))) โค (๐โ๐๐ธ))) |
244 | 242, 243 | mpbid 231 |
. . . 4
โข (๐ โ (๐โ๐((๐ถ + (๐ท / 2)) + (๐ธ / 2))) โค (๐โ๐๐ธ)) |
245 | 101, 211,
165, 224, 244 | ltletrd 11322 |
. . 3
โข (๐ โ ๐ด < (๐โ๐๐ธ)) |
246 | 245, 155 | breqtrd 5136 |
. 2
โข (๐ โ ๐ด < (2โ๐((2
logb ๐)โ5))) |
247 | | 1le2 12369 |
. . . . 5
โข 1 โค
2 |
248 | 247 | a1i 11 |
. . . 4
โข (๐ โ 1 โค 2) |
249 | 172 | nn0red 12481 |
. . . 4
โข (๐ โ ๐ต โ โ) |
250 | 21 | eqcomd 2743 |
. . . . 5
โข (๐ โ (โโ((2
logb ๐)โ5))
= ๐ต) |
251 | 33, 250 | breqtrd 5136 |
. . . 4
โข (๐ โ ((2 logb ๐)โ5) โค ๐ต) |
252 | 4, 248, 16, 249, 251 | cxplead 26092 |
. . 3
โข (๐ โ
(2โ๐((2 logb ๐)โ5)) โค
(2โ๐๐ต)) |
253 | | cxpexp 26039 |
. . . 4
โข ((2
โ โ โง ๐ต
โ โ0) โ (2โ๐๐ต) = (2โ๐ต)) |
254 | 105, 172,
253 | syl2anc 585 |
. . 3
โข (๐ โ
(2โ๐๐ต) = (2โ๐ต)) |
255 | 252, 254 | breqtrd 5136 |
. 2
โข (๐ โ
(2โ๐((2 logb ๐)โ5)) โค (2โ๐ต)) |
256 | 101, 166,
173, 246, 255 | ltletrd 11322 |
1
โข (๐ โ ๐ด < (2โ๐ต)) |