Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p2.1 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
2 | 1 | nnred 12175 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
3 | | 2re 12234 |
. . . . . . . . . . . 12
โข 2 โ
โ |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
5 | | 2pos 12263 |
. . . . . . . . . . . 12
โข 0 <
2 |
6 | 5 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 0 < 2) |
7 | 1 | nngt0d 12209 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < ๐) |
8 | | 1red 11163 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 โ
โ) |
9 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . . 19
โข 1 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 < 2) |
11 | 8, 10 | ltned 11298 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โ 2) |
12 | 11 | necomd 3000 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ 1) |
13 | 4, 6, 2, 7, 12 | relogbcld 40459 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 logb ๐) โ
โ) |
14 | | 5nn0 12440 |
. . . . . . . . . . . . . . . 16
โข 5 โ
โ0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 5 โ
โ0) |
16 | 13, 15 | reexpcld 14075 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 logb ๐)โ5) โ
โ) |
17 | | ceilcl 13754 |
. . . . . . . . . . . . . 14
โข (((2
logb ๐)โ5)
โ โ โ (โโ((2 logb ๐)โ5)) โ โค) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โค) |
19 | 18 | zred 12614 |
. . . . . . . . . . . 12
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โ) |
20 | | aks4d1p1p2.3 |
. . . . . . . . . . . . . 14
โข ๐ต = (โโ((2
logb ๐)โ5)) |
21 | 20 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต = (โโ((2 logb ๐)โ5))) |
22 | 21 | eleq1d 2823 |
. . . . . . . . . . . 12
โข (๐ โ (๐ต โ โ โ (โโ((2
logb ๐)โ5))
โ โ)) |
23 | 19, 22 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
24 | | 0red 11165 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ
โ) |
25 | 15 | nn0zd 12532 |
. . . . . . . . . . . . . 14
โข (๐ โ 5 โ
โค) |
26 | | 3re 12240 |
. . . . . . . . . . . . . . . . 17
โข 3 โ
โ |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 3 โ
โ) |
28 | | 1lt3 12333 |
. . . . . . . . . . . . . . . . 17
โข 1 <
3 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 < 3) |
30 | | aks4d1p1p2.4 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 3 โค ๐) |
31 | 8, 27, 2, 29, 30 | ltletrd 11322 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 < ๐) |
32 | 2, 7 | elrpd 12961 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ
โ+) |
33 | | 2rp 12927 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โ+ |
34 | 33, 9 | pm3.2i 472 |
. . . . . . . . . . . . . . . . 17
โข (2 โ
โ+ โง 1 < 2) |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 โ
โ+ โง 1 < 2)) |
36 | | logbgt0b 26159 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ+
โง (2 โ โ+ โง 1 < 2)) โ (0 < (2
logb ๐) โ 1
< ๐)) |
37 | 32, 35, 36 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 < (2 logb
๐) โ 1 < ๐)) |
38 | 31, 37 | mpbird 257 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < (2 logb
๐)) |
39 | | expgt0 14008 |
. . . . . . . . . . . . . 14
โข (((2
logb ๐) โ
โ โง 5 โ โค โง 0 < (2 logb ๐)) โ 0 < ((2
logb ๐)โ5)) |
40 | 13, 25, 38, 39 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < ((2 logb
๐)โ5)) |
41 | | ceilge 13757 |
. . . . . . . . . . . . . 14
โข (((2
logb ๐)โ5)
โ โ โ ((2 logb ๐)โ5) โค (โโ((2
logb ๐)โ5))) |
42 | 16, 41 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 logb ๐)โ5) โค
(โโ((2 logb ๐)โ5))) |
43 | 24, 16, 19, 40, 42 | ltletrd 11322 |
. . . . . . . . . . . 12
โข (๐ โ 0 < (โโ((2
logb ๐)โ5))) |
44 | 21 | breq2d 5122 |
. . . . . . . . . . . 12
โข (๐ โ (0 < ๐ต โ 0 < (โโ((2
logb ๐)โ5)))) |
45 | 43, 44 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ 0 < ๐ต) |
46 | 4, 6, 23, 45, 12 | relogbcld 40459 |
. . . . . . . . . 10
โข (๐ โ (2 logb ๐ต) โ
โ) |
47 | 46 | flcld 13710 |
. . . . . . . . 9
โข (๐ โ (โโ(2
logb ๐ต)) โ
โค) |
48 | | 7re 12253 |
. . . . . . . . . . . . . . . 16
โข 7 โ
โ |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 7 โ
โ) |
50 | | 1lt7 12351 |
. . . . . . . . . . . . . . . 16
โข 1 <
7 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 < 7) |
52 | 2, 30 | 3lexlogpow5ineq3 40543 |
. . . . . . . . . . . . . . 15
โข (๐ โ 7 < ((2 logb
๐)โ5)) |
53 | 8, 49, 16, 51, 52 | lttrd 11323 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 < ((2 logb
๐)โ5)) |
54 | 8, 16, 19, 53, 42 | ltletrd 11322 |
. . . . . . . . . . . . 13
โข (๐ โ 1 < (โโ((2
logb ๐)โ5))) |
55 | 21 | breq2d 5122 |
. . . . . . . . . . . . 13
โข (๐ โ (1 < ๐ต โ 1 < (โโ((2
logb ๐)โ5)))) |
56 | 54, 55 | mpbird 257 |
. . . . . . . . . . . 12
โข (๐ โ 1 < ๐ต) |
57 | 23, 45 | elrpd 12961 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ
โ+) |
58 | | logbgt0b 26159 |
. . . . . . . . . . . . 13
โข ((๐ต โ โ+
โง (2 โ โ+ โง 1 < 2)) โ (0 < (2
logb ๐ต) โ 1
< ๐ต)) |
59 | 57, 35, 58 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ (0 < (2 logb
๐ต) โ 1 < ๐ต)) |
60 | 56, 59 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ 0 < (2 logb
๐ต)) |
61 | 24, 46, 60 | ltled 11310 |
. . . . . . . . . 10
โข (๐ โ 0 โค (2 logb
๐ต)) |
62 | | 0zd 12518 |
. . . . . . . . . . 11
โข (๐ โ 0 โ
โค) |
63 | | flge 13717 |
. . . . . . . . . . 11
โข (((2
logb ๐ต) โ
โ โง 0 โ โค) โ (0 โค (2 logb ๐ต) โ 0 โค
(โโ(2 logb ๐ต)))) |
64 | 46, 62, 63 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ โ (0 โค (2 logb
๐ต) โ 0 โค
(โโ(2 logb ๐ต)))) |
65 | 61, 64 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ 0 โค (โโ(2
logb ๐ต))) |
66 | 47, 65 | jca 513 |
. . . . . . . 8
โข (๐ โ ((โโ(2
logb ๐ต)) โ
โค โง 0 โค (โโ(2 logb ๐ต)))) |
67 | | elnn0z 12519 |
. . . . . . . 8
โข
((โโ(2 logb ๐ต)) โ โ0 โ
((โโ(2 logb ๐ต)) โ โค โง 0 โค
(โโ(2 logb ๐ต)))) |
68 | 66, 67 | sylibr 233 |
. . . . . . 7
โข (๐ โ (โโ(2
logb ๐ต)) โ
โ0) |
69 | 2, 68 | reexpcld 14075 |
. . . . . 6
โข (๐ โ (๐โ(โโ(2 logb
๐ต))) โ
โ) |
70 | | fzfid 13885 |
. . . . . . 7
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ Fin) |
71 | 2 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
72 | | elfznn 13477 |
. . . . . . . . . . 11
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ ๐ โ โ) |
73 | 72 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
74 | | nnnn0 12427 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ0) |
76 | 71, 75 | reexpcld 14075 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) โ โ) |
77 | | 1red 11163 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โ
โ) |
78 | 76, 77 | resubcld 11590 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 1) โ โ) |
79 | 70, 78 | fprodrecl 15843 |
. . . . . 6
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1) โ โ) |
80 | 69, 79 | remulcld 11192 |
. . . . 5
โข (๐ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โ
โ) |
81 | | aks4d1p1p2.2 |
. . . . . . 7
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
82 | 81 | a1i 11 |
. . . . . 6
โข (๐ โ ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
83 | 82 | eleq1d 2823 |
. . . . 5
โข (๐ โ (๐ด โ โ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โ
โ)) |
84 | 80, 83 | mpbird 257 |
. . . 4
โข (๐ โ ๐ด โ โ) |
85 | 1 | nnnn0d 12480 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
86 | 85 | nn0ge0d 12483 |
. . . . 5
โข (๐ โ 0 โค ๐) |
87 | 16, 8 | readdcld 11191 |
. . . . . . 7
โข (๐ โ (((2 logb ๐)โ5) + 1) โ
โ) |
88 | 16 | ltp1d 12092 |
. . . . . . . 8
โข (๐ โ ((2 logb ๐)โ5) < (((2
logb ๐)โ5)
+ 1)) |
89 | 24, 16, 87, 40, 88 | lttrd 11323 |
. . . . . . 7
โข (๐ โ 0 < (((2
logb ๐)โ5)
+ 1)) |
90 | 4, 6, 87, 89, 12 | relogbcld 40459 |
. . . . . 6
โข (๐ โ (2 logb (((2
logb ๐)โ5)
+ 1)) โ โ) |
91 | 13 | resqcld 14037 |
. . . . . . . . . . . 12
โข (๐ โ ((2 logb ๐)โ2) โ
โ) |
92 | 91 | flcld 13710 |
. . . . . . . . . . 11
โข (๐ โ (โโ((2
logb ๐)โ2))
โ โค) |
93 | 92 | zred 12614 |
. . . . . . . . . . . 12
โข (๐ โ (โโ((2
logb ๐)โ2))
โ โ) |
94 | | 0lt1 11684 |
. . . . . . . . . . . . 13
โข 0 <
1 |
95 | 94 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 0 < 1) |
96 | 4, 6, 4, 6, 12 | relogbcld 40459 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 logb 2)
โ โ) |
97 | 96 | resqcld 14037 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 logb
2)โ2) โ โ) |
98 | | 2nn0 12437 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ0 |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ
โ0) |
100 | 8 | leidd 11728 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 โค 1) |
101 | 4 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ
โ) |
102 | 24, 6 | gtned 11297 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ 0) |
103 | | logbid1 26134 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง 2 โ 0 โง 2 โ 1) โ (2 logb 2) =
1) |
104 | 101, 102,
12, 103 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 logb 2) =
1) |
105 | 104 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 = (2 logb
2)) |
106 | 100, 105 | breqtrd 5136 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โค (2 logb
2)) |
107 | 96, 99, 106 | expge1d 14077 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โค ((2 logb
2)โ2)) |
108 | 105 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 logb 2) =
1) |
109 | 108 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2 logb
2)โ2) = (1โ2)) |
110 | 99 | nn0zd 12532 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ
โค) |
111 | | 1exp 14004 |
. . . . . . . . . . . . . . . . 17
โข (2 โ
โค โ (1โ2) = 1) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1โ2) =
1) |
113 | 109, 112 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 logb
2)โ2) = 1) |
114 | 4 | leidd 11728 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โค 2) |
115 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 1 โ
โ0 |
116 | 3, 115 | nn0addge1i 12468 |
. . . . . . . . . . . . . . . . . . . . 21
โข 2 โค (2
+ 1) |
117 | | 2p1e3 12302 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2 + 1) =
3 |
118 | 116, 117 | breqtri 5135 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โค
3 |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 2 โค 3) |
120 | 4, 27, 2, 119, 30 | letrd 11319 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โค ๐) |
121 | 110, 114,
4, 6, 2, 7,
120 | logblebd 40462 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 logb 2) โค
(2 logb ๐)) |
122 | 8, 96, 13, 106, 121 | letrd 11319 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 1 โค (2 logb
๐)) |
123 | 13, 99, 122 | expge1d 14077 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 โค ((2 logb
๐)โ2)) |
124 | 113, 123 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 logb
2)โ2) โค ((2 logb ๐)โ2)) |
125 | | 1z 12540 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โค |
126 | | zsqcl 14041 |
. . . . . . . . . . . . . . . . . . 19
โข (1 โ
โค โ (1โ2) โ โค) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข
(1โ2) โ โค |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1โ2) โ
โค) |
129 | 109 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (((2 logb
2)โ2) โ โค โ (1โ2) โ โค)) |
130 | 128, 129 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2 logb
2)โ2) โ โค) |
131 | 91, 130 | jca 513 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 logb ๐)โ2) โ โ โง
((2 logb 2)โ2) โ โค)) |
132 | | flge 13717 |
. . . . . . . . . . . . . . 15
โข ((((2
logb ๐)โ2)
โ โ โง ((2 logb 2)โ2) โ โค) โ (((2
logb 2)โ2) โค ((2 logb ๐)โ2) โ ((2 logb
2)โ2) โค (โโ((2 logb ๐)โ2)))) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 logb
2)โ2) โค ((2 logb ๐)โ2) โ ((2 logb
2)โ2) โค (โโ((2 logb ๐)โ2)))) |
134 | 124, 133 | mpbid 231 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 logb
2)โ2) โค (โโ((2 logb ๐)โ2))) |
135 | 8, 97, 93, 107, 134 | letrd 11319 |
. . . . . . . . . . . 12
โข (๐ โ 1 โค (โโ((2
logb ๐)โ2))) |
136 | 24, 8, 93, 95, 135 | ltletrd 11322 |
. . . . . . . . . . 11
โข (๐ โ 0 < (โโ((2
logb ๐)โ2))) |
137 | 92, 136 | jca 513 |
. . . . . . . . . 10
โข (๐ โ ((โโ((2
logb ๐)โ2))
โ โค โง 0 < (โโ((2 logb ๐)โ2)))) |
138 | | elnnz 12516 |
. . . . . . . . . . . 12
โข
((โโ((2 logb ๐)โ2)) โ โ โ
((โโ((2 logb ๐)โ2)) โ โค โง 0 <
(โโ((2 logb ๐)โ2)))) |
139 | 138 | bicomi 223 |
. . . . . . . . . . 11
โข
(((โโ((2 logb ๐)โ2)) โ โค โง 0 <
(โโ((2 logb ๐)โ2))) โ (โโ((2
logb ๐)โ2))
โ โ) |
140 | 139 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ (((โโ((2
logb ๐)โ2))
โ โค โง 0 < (โโ((2 logb ๐)โ2))) โ
(โโ((2 logb ๐)โ2)) โ โ)) |
141 | 137, 140 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ (โโ((2
logb ๐)โ2))
โ โ) |
142 | 141 | nnnn0d 12480 |
. . . . . . . 8
โข (๐ โ (โโ((2
logb ๐)โ2))
โ โ0) |
143 | | arisum 15752 |
. . . . . . . 8
โข
((โโ((2 logb ๐)โ2)) โ โ0 โ
ฮฃ๐ โ
(1...(โโ((2 logb ๐)โ2)))๐ = ((((โโ((2 logb
๐)โ2))โ2) +
(โโ((2 logb ๐)โ2))) / 2)) |
144 | 142, 143 | syl 17 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐ = ((((โโ((2 logb
๐)โ2))โ2) +
(โโ((2 logb ๐)โ2))) / 2)) |
145 | 73 | nnred 12175 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
146 | 70, 145 | fsumrecl 15626 |
. . . . . . 7
โข (๐ โ ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐ โ โ) |
147 | 144, 146 | eqeltrrd 2839 |
. . . . . 6
โข (๐ โ ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2) โ
โ) |
148 | 90, 147 | readdcld 11191 |
. . . . 5
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((โโ((2 logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2)) โ
โ) |
149 | 2, 86, 148 | recxpcld 26094 |
. . . 4
โข (๐ โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2))) โ
โ) |
150 | | 4nn0 12439 |
. . . . . . . . . 10
โข 4 โ
โ0 |
151 | 150 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 4 โ
โ0) |
152 | 13, 151 | reexpcld 14075 |
. . . . . . . 8
โข (๐ โ ((2 logb ๐)โ4) โ
โ) |
153 | 152, 91 | readdcld 11191 |
. . . . . . 7
โข (๐ โ (((2 logb ๐)โ4) + ((2 logb
๐)โ2)) โ
โ) |
154 | 153 | rehalfcld 12407 |
. . . . . 6
โข (๐ โ ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2) โ โ) |
155 | 90, 154 | readdcld 11191 |
. . . . 5
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((2 logb ๐)โ4) + ((2 logb ๐)โ2)) / 2)) โ
โ) |
156 | 2, 86, 155 | recxpcld 26094 |
. . . 4
โข (๐ โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2))) โ โ) |
157 | | reflcl 13708 |
. . . . . . . . . . 11
โข ((2
logb ๐ต) โ
โ โ (โโ(2 logb ๐ต)) โ โ) |
158 | 46, 157 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โโ(2
logb ๐ต)) โ
โ) |
159 | 2, 86, 158 | recxpcld 26094 |
. . . . . . . . 9
โข (๐ โ (๐โ๐(โโ(2
logb ๐ต))) โ
โ) |
160 | 32, 146 | rpcxpcld 26103 |
. . . . . . . . . . . 12
โข (๐ โ (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐) โ
โ+) |
161 | 32, 141 | aks4d1p1p1 40549 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐) = (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐)) |
162 | 161 | eleq1d 2823 |
. . . . . . . . . . . 12
โข (๐ โ (โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐) โ โ+ โ (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐) โ
โ+)) |
163 | 160, 162 | mpbird 257 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐) โ
โ+) |
164 | 163 | rpregt0d 12970 |
. . . . . . . . . 10
โข (๐ โ (โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐) โ โ โง 0 < โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
165 | 164 | simpld 496 |
. . . . . . . . 9
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐) โ โ) |
166 | 159, 165 | remulcld 11192 |
. . . . . . . 8
โข (๐ โ ((๐โ๐(โโ(2
logb ๐ต)))
ยท โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐)) โ โ) |
167 | 2, 86, 90 | recxpcld 26094 |
. . . . . . . . 9
โข (๐ โ (๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) โ
โ) |
168 | 167, 165 | remulcld 11192 |
. . . . . . . 8
โข (๐ โ ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐)) โ โ) |
169 | 70, 76 | fprodrecl 15843 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐) โ โ) |
170 | 2, 68, 86 | expge0d 14076 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค (๐โ(โโ(2 logb
๐ต)))) |
171 | | nfv 1918 |
. . . . . . . . . . . . 13
โข
โฒ๐๐ |
172 | | 0red 11165 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 0 โ
โ) |
173 | 1 | nnge1d 12208 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โค ๐) |
174 | 173 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โค ๐) |
175 | 71, 75, 174 | expge1d 14077 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โค (๐โ๐)) |
176 | 76 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) โ โ) |
177 | 176 | subid1d 11508 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 0) = (๐โ๐)) |
178 | 177 | breq2d 5122 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (1 โค ((๐โ๐) โ 0) โ 1 โค (๐โ๐))) |
179 | 175, 178 | mpbird 257 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โค ((๐โ๐) โ 0)) |
180 | 77, 76, 172, 179 | lesubd 11766 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 0 โค ((๐โ๐) โ 1)) |
181 | 76 | lem1d 12095 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 1) โค (๐โ๐)) |
182 | 171, 70, 78, 180, 76, 181 | fprodle 15886 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1) โค โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐)) |
183 | 79, 169, 69, 170, 182 | lemul2ad 12102 |
. . . . . . . . . . 11
โข (๐ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โค ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐))) |
184 | 82 | breq1d 5120 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โค ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐)) โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) โค ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐)))) |
185 | 183, 184 | mpbird 257 |
. . . . . . . . . 10
โข (๐ โ ๐ด โค ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐))) |
186 | 71 | recnd 11190 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
187 | | cxpexp 26039 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐๐) = (๐โ๐)) |
188 | 186, 75, 187 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐๐) = (๐โ๐)) |
189 | 188 | eqcomd 2743 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) = (๐โ๐๐)) |
190 | 189 | prodeq2dv 15813 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐) = โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐)) |
191 | 190 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐)) = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
192 | 185, 191 | breqtrd 5136 |
. . . . . . . . 9
โข (๐ โ ๐ด โค ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
193 | 2 | recnd 11190 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
194 | | cxpexp 26039 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
(โโ(2 logb ๐ต)) โ โ0) โ (๐โ๐(โโ(2
logb ๐ต))) =
(๐โ(โโ(2
logb ๐ต)))) |
195 | 193, 68, 194 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐โ๐(โโ(2
logb ๐ต))) =
(๐โ(โโ(2
logb ๐ต)))) |
196 | 195 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ ((๐โ๐(โโ(2
logb ๐ต)))
ยท โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐)) = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
197 | 196 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐)) = ((๐โ๐(โโ(2
logb ๐ต)))
ยท โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐))) |
198 | 192, 197 | breqtrd 5136 |
. . . . . . . 8
โข (๐ โ ๐ด โค ((๐โ๐(โโ(2
logb ๐ต)))
ยท โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐))) |
199 | 159, 167,
164 | 3jca 1129 |
. . . . . . . . 9
โข (๐ โ ((๐โ๐(โโ(2
logb ๐ต))) โ
โ โง (๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) โ โ โง
(โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐) โ โ โง 0 < โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐)))) |
200 | 1, 20, 30 | aks4d1p1p3 40555 |
. . . . . . . . 9
โข (๐ โ (๐โ๐(โโ(2
logb ๐ต))) <
(๐โ๐(2 logb
(((2 logb ๐)โ5) + 1)))) |
201 | | ltmul1a 12011 |
. . . . . . . . 9
โข ((((๐โ๐(โโ(2
logb ๐ต))) โ
โ โง (๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) โ โ โง
(โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐) โ โ โง 0 < โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) โง (๐โ๐(โโ(2
logb ๐ต))) <
(๐โ๐(2 logb
(((2 logb ๐)โ5) + 1)))) โ ((๐โ๐(โโ(2
logb ๐ต)))
ยท โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐)) < ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
202 | 199, 200,
201 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ ((๐โ๐(โโ(2
logb ๐ต)))
ยท โ๐ โ
(1...(โโ((2 logb ๐)โ2)))(๐โ๐๐)) < ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
203 | 84, 166, 168, 198, 202 | lelttrd 11320 |
. . . . . . 7
โข (๐ โ ๐ด < ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐))) |
204 | 161 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))(๐โ๐๐)) = ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐))) |
205 | 203, 204 | breqtrd 5136 |
. . . . . 6
โข (๐ โ ๐ด < ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐))) |
206 | 144 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐) = (๐โ๐((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) /
2))) |
207 | 206 | oveq2d 7378 |
. . . . . 6
โข (๐ โ ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐ฮฃ๐ โ (1...(โโ((2
logb ๐)โ2)))๐)) = ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) /
2)))) |
208 | 205, 207 | breqtrd 5136 |
. . . . 5
โข (๐ โ ๐ด < ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) /
2)))) |
209 | 24, 7 | gtned 11297 |
. . . . . . 7
โข (๐ โ ๐ โ 0) |
210 | 90 | recnd 11190 |
. . . . . . 7
โข (๐ โ (2 logb (((2
logb ๐)โ5)
+ 1)) โ โ) |
211 | 141 | nncnd 12176 |
. . . . . . . . . 10
โข (๐ โ (โโ((2
logb ๐)โ2))
โ โ) |
212 | 211 | sqcld 14056 |
. . . . . . . . 9
โข (๐ โ ((โโ((2
logb ๐)โ2))โ2) โ
โ) |
213 | 212, 211 | addcld 11181 |
. . . . . . . 8
โข (๐ โ (((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) โ โ) |
214 | 213 | halfcld 12405 |
. . . . . . 7
โข (๐ โ ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2) โ
โ) |
215 | 193, 209,
210, 214 | cxpaddd 26088 |
. . . . . 6
โข (๐ โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2))) = ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) /
2)))) |
216 | 215 | eqcomd 2743 |
. . . . 5
โข (๐ โ ((๐โ๐(2 logb
(((2 logb ๐)โ5) + 1))) ยท (๐โ๐((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) /
2))) = (๐โ๐((2 logb
(((2 logb ๐)โ5) + 1)) + ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) /
2)))) |
217 | 208, 216 | breqtrd 5136 |
. . . 4
โข (๐ โ ๐ด < (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2)))) |
218 | | reflcl 13708 |
. . . . . . . . . 10
โข (((2
logb ๐)โ2)
โ โ โ (โโ((2 logb ๐)โ2)) โ โ) |
219 | 91, 218 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โโ((2
logb ๐)โ2))
โ โ) |
220 | 219 | resqcld 14037 |
. . . . . . . 8
โข (๐ โ ((โโ((2
logb ๐)โ2))โ2) โ
โ) |
221 | 220, 219 | readdcld 11191 |
. . . . . . 7
โข (๐ โ (((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) โ โ) |
222 | 33 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โ+) |
223 | 91, 99 | reexpcld 14075 |
. . . . . . . . 9
โข (๐ โ (((2 logb ๐)โ2)โ2) โ
โ) |
224 | | id 22 |
. . . . . . . . . 10
โข (๐ โ ๐) |
225 | 142 | nn0ge0d 12483 |
. . . . . . . . . . 11
โข (๐ โ 0 โค (โโ((2
logb ๐)โ2))) |
226 | | flle 13711 |
. . . . . . . . . . . 12
โข (((2
logb ๐)โ2)
โ โ โ (โโ((2 logb ๐)โ2)) โค ((2 logb ๐)โ2)) |
227 | 91, 226 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (โโ((2
logb ๐)โ2))
โค ((2 logb ๐)โ2)) |
228 | 219, 91, 99, 225, 227 | leexp1ad 40458 |
. . . . . . . . . 10
โข (๐ โ ((โโ((2
logb ๐)โ2))โ2) โค (((2 logb
๐)โ2)โ2)) |
229 | 224, 228 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((โโ((2
logb ๐)โ2))โ2) โค (((2 logb
๐)โ2)โ2)) |
230 | 13 | recnd 11190 |
. . . . . . . . . . . . 13
โข (๐ โ (2 logb ๐) โ
โ) |
231 | 230, 99, 99 | expmuld 14061 |
. . . . . . . . . . . 12
โข (๐ โ ((2 logb ๐)โ(2 ยท 2)) = (((2
logb ๐)โ2)โ2)) |
232 | 231 | eqcomd 2743 |
. . . . . . . . . . 11
โข (๐ โ (((2 logb ๐)โ2)โ2) = ((2
logb ๐)โ(2
ยท 2))) |
233 | | 2t2e4 12324 |
. . . . . . . . . . . . 13
โข (2
ยท 2) = 4 |
234 | 233 | oveq2i 7373 |
. . . . . . . . . . . 12
โข ((2
logb ๐)โ(2
ยท 2)) = ((2 logb ๐)โ4) |
235 | 234 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ((2 logb ๐)โ(2 ยท 2)) = ((2
logb ๐)โ4)) |
236 | 232, 235 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (((2 logb ๐)โ2)โ2) = ((2
logb ๐)โ4)) |
237 | 223, 236 | eqled 11265 |
. . . . . . . . 9
โข (๐ โ (((2 logb ๐)โ2)โ2) โค ((2
logb ๐)โ4)) |
238 | 220, 223,
152, 229, 237 | letrd 11319 |
. . . . . . . 8
โข (๐ โ ((โโ((2
logb ๐)โ2))โ2) โค ((2 logb
๐)โ4)) |
239 | 220, 219,
152, 91, 238, 227 | le2addd 11781 |
. . . . . . 7
โข (๐ โ (((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) โค (((2 logb ๐)โ4) + ((2 logb
๐)โ2))) |
240 | 221, 153,
222, 239 | lediv1dd 13022 |
. . . . . 6
โข (๐ โ ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2) โค ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2)) |
241 | 147, 154,
90, 240 | leadd2dd 11777 |
. . . . 5
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((โโ((2 logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2)) โค ((2 logb
(((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2))) |
242 | 2, 31, 148, 155 | cxpled 26091 |
. . . . 5
โข (๐ โ (((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((โโ((2 logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2)) โค ((2 logb
(((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2)) โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2))) โค (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2))))) |
243 | 241, 242 | mpbid 231 |
. . . 4
โข (๐ โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((โโ((2
logb ๐)โ2))โ2) + (โโ((2
logb ๐)โ2))) / 2))) โค (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2)))) |
244 | 84, 149, 156, 217, 243 | ltletrd 11322 |
. . 3
โข (๐ โ ๐ด < (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2)))) |
245 | 152 | recnd 11190 |
. . . . . 6
โข (๐ โ ((2 logb ๐)โ4) โ
โ) |
246 | 91 | recnd 11190 |
. . . . . 6
โข (๐ โ ((2 logb ๐)โ2) โ
โ) |
247 | 245, 246,
101, 102 | divdird 11976 |
. . . . 5
โข (๐ โ ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2) = ((((2 logb ๐)โ4) / 2) + (((2 logb ๐)โ2) /
2))) |
248 | 247 | oveq2d 7378 |
. . . 4
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((2 logb ๐)โ4) + ((2 logb ๐)โ2)) / 2)) = ((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) / 2) + (((2
logb ๐)โ2)
/ 2)))) |
249 | 248 | oveq2d 7378 |
. . 3
โข (๐ โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) + ((2
logb ๐)โ2))
/ 2))) = (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) / 2) + (((2
logb ๐)โ2)
/ 2))))) |
250 | 244, 249 | breqtrd 5136 |
. 2
โข (๐ โ ๐ด < (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) / 2) + (((2
logb ๐)โ2)
/ 2))))) |
251 | 245, 101,
102 | divcld 11938 |
. . . . . 6
โข (๐ โ (((2 logb ๐)โ4) / 2) โ
โ) |
252 | 246, 101,
102 | divcld 11938 |
. . . . . 6
โข (๐ โ (((2 logb ๐)โ2) / 2) โ
โ) |
253 | 251, 252 | addcomd 11364 |
. . . . 5
โข (๐ โ ((((2 logb
๐)โ4) / 2) + (((2
logb ๐)โ2)
/ 2)) = ((((2 logb ๐)โ2) / 2) + (((2 logb ๐)โ4) /
2))) |
254 | 253 | oveq2d 7378 |
. . . 4
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((2 logb ๐)โ4) / 2) + (((2 logb ๐)โ2) / 2))) = ((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ2) / 2) + (((2
logb ๐)โ4)
/ 2)))) |
255 | 210, 252,
251 | addassd 11184 |
. . . . 5
โข (๐ โ (((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
logb ๐)โ4)
/ 2)))) |
256 | 255 | eqcomd 2743 |
. . . 4
โข (๐ โ ((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
logb ๐)โ4)
/ 2))) |
257 | 254, 256 | eqtrd 2777 |
. . 3
โข (๐ โ ((2 logb (((2
logb ๐)โ5)
+ 1)) + ((((2 logb ๐)โ4) / 2) + (((2 logb ๐)โ2) / 2))) = (((2
logb (((2 logb ๐)โ5) + 1)) + (((2 logb ๐)โ2) / 2)) + (((2
logb ๐)โ4)
/ 2))) |
258 | 257 | oveq2d 7378 |
. 2
โข (๐ โ (๐โ๐((2
logb (((2 logb ๐)โ5) + 1)) + ((((2 logb
๐)โ4) / 2) + (((2
logb ๐)โ2)
/ 2)))) = (๐โ๐(((2
logb (((2 logb ๐)โ5) + 1)) + (((2 logb ๐)โ2) / 2)) + (((2
logb ๐)โ4)
/ 2)))) |
259 | 250, 258 | breqtrd 5136 |
1
โข (๐ โ ๐ด < (๐โ๐(((2
logb (((2 logb ๐)โ5) + 1)) + (((2 logb ๐)โ2) / 2)) + (((2
logb ๐)โ4)
/ 2)))) |