Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p5.1 |
. 2
β’ (π β π β β) |
2 | | aks4d1p1p5.2 |
. 2
β’ π΄ = ((πβ(ββ(2 logb
π΅))) Β· βπ β (1...(ββ((2
logb π)β2)))((πβπ) β 1)) |
3 | | aks4d1p1p5.3 |
. 2
β’ π΅ = (ββ((2
logb π)β5)) |
4 | | 3re 12240 |
. . . 4
β’ 3 β
β |
5 | 4 | a1i 11 |
. . 3
β’ (π β 3 β
β) |
6 | | 4re 12244 |
. . . 4
β’ 4 β
β |
7 | 6 | a1i 11 |
. . 3
β’ (π β 4 β
β) |
8 | 1 | nnred 12175 |
. . 3
β’ (π β π β β) |
9 | 5 | lep1d 12093 |
. . . 4
β’ (π β 3 β€ (3 +
1)) |
10 | | 3p1e4 12305 |
. . . 4
β’ (3 + 1) =
4 |
11 | 9, 10 | breqtrdi 5151 |
. . 3
β’ (π β 3 β€ 4) |
12 | | aks4d1p1p5.4 |
. . 3
β’ (π β 4 β€ π) |
13 | 5, 7, 8, 11, 12 | letrd 11319 |
. 2
β’ (π β 3 β€ π) |
14 | | aks4d1p1p5.5 |
. 2
β’ πΆ = (2 logb (((2
logb π)β5)
+ 1)) |
15 | | aks4d1p1p5.6 |
. 2
β’ π· = ((2 logb π)β2) |
16 | | aks4d1p1p5.7 |
. 2
β’ πΈ = ((2 logb π)β4) |
17 | | 2re 12234 |
. . . . . . . 8
β’ 2 β
β |
18 | 17 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β (4[,]π)) β 2 β β) |
19 | | 2pos 12263 |
. . . . . . . . 9
β’ 0 <
2 |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β (4[,]π)) β 0 < 2) |
21 | | elicc2 13336 |
. . . . . . . . . . . . . . 15
β’ ((4
β β β§ π
β β) β (π₯
β (4[,]π) β
(π₯ β β β§ 4
β€ π₯ β§ π₯ β€ π))) |
22 | 7, 8, 21 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β (4[,]π) β (π₯ β β β§ 4 β€ π₯ β§ π₯ β€ π))) |
23 | 22 | biimpd 228 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β (4[,]π) β (π₯ β β β§ 4 β€ π₯ β§ π₯ β€ π))) |
24 | 23 | imp 408 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β (π₯ β β β§ 4 β€ π₯ β§ π₯ β€ π)) |
25 | 24 | simp1d 1143 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β π₯ β β) |
26 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ (π β 0 β
β) |
27 | 26 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β 0 β β) |
28 | 6 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β 4 β β) |
29 | | 4pos 12267 |
. . . . . . . . . . . . 13
β’ 0 <
4 |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β 0 < 4) |
31 | 24 | simp2d 1144 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β 4 β€ π₯) |
32 | 27, 28, 25, 30, 31 | ltletrd 11322 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β 0 < π₯) |
33 | | 1red 11163 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
34 | | 1lt2 12331 |
. . . . . . . . . . . . . . 15
β’ 1 <
2 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 1 < 2) |
36 | 33, 35 | ltned 11298 |
. . . . . . . . . . . . 13
β’ (π β 1 β 2) |
37 | 36 | necomd 3000 |
. . . . . . . . . . . 12
β’ (π β 2 β 1) |
38 | 37 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β 2 β 1) |
39 | 18, 20, 25, 32, 38 | relogbcld 40459 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (4[,]π)) β (2 logb π₯) β
β) |
40 | | 5nn0 12440 |
. . . . . . . . . . 11
β’ 5 β
β0 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (4[,]π)) β 5 β
β0) |
42 | 39, 41 | reexpcld 14075 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β ((2 logb π₯)β5) β
β) |
43 | | 1red 11163 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β 1 β β) |
44 | 42, 43 | readdcld 11191 |
. . . . . . . 8
β’ ((π β§ π₯ β (4[,]π)) β (((2 logb π₯)β5) + 1) β
β) |
45 | 27, 43 | readdcld 11191 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β (0 + 1) β
β) |
46 | 27 | ltp1d 12092 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β 0 < (0 + 1)) |
47 | 41 | nn0zd 12532 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β 5 β β€) |
48 | | ax-resscn 11115 |
. . . . . . . . . . . . . 14
β’ β
β β |
49 | 48, 18 | sselid 3947 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (4[,]π)) β 2 β β) |
50 | 27, 20 | gtned 11297 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (4[,]π)) β 2 β 0) |
51 | | logb1 26135 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ 2 β 0 β§ 2 β 1) β (2 logb 1) =
0) |
52 | 49, 50, 38, 51 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β (2 logb 1) =
0) |
53 | | 1lt4 12336 |
. . . . . . . . . . . . . . 15
β’ 1 <
4 |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (4[,]π)) β 1 < 4) |
55 | 43, 28, 25, 54, 31 | ltletrd 11322 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (4[,]π)) β 1 < π₯) |
56 | | 2z 12542 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β€ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (4[,]π)) β 2 β β€) |
58 | 57 | uzidd 12786 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (4[,]π)) β 2 β
(β€β₯β2)) |
59 | | 1rp 12926 |
. . . . . . . . . . . . . . 15
β’ 1 β
β+ |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (4[,]π)) β 1 β
β+) |
61 | 25, 32 | elrpd 12961 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (4[,]π)) β π₯ β β+) |
62 | | logblt 26150 |
. . . . . . . . . . . . . 14
β’ ((2
β (β€β₯β2) β§ 1 β β+
β§ π₯ β
β+) β (1 < π₯ β (2 logb 1) < (2
logb π₯))) |
63 | 58, 60, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (4[,]π)) β (1 < π₯ β (2 logb 1) < (2
logb π₯))) |
64 | 55, 63 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β (2 logb 1) < (2
logb π₯)) |
65 | 52, 64 | eqbrtrrd 5134 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β 0 < (2 logb π₯)) |
66 | | expgt0 14008 |
. . . . . . . . . . 11
β’ (((2
logb π₯) β
β β§ 5 β β€ β§ 0 < (2 logb π₯)) β 0 < ((2
logb π₯)β5)) |
67 | 39, 47, 65, 66 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (4[,]π)) β 0 < ((2 logb π₯)β5)) |
68 | 27, 42, 43, 67 | ltadd1dd 11773 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β (0 + 1) < (((2 logb
π₯)β5) +
1)) |
69 | 27, 45, 44, 46, 68 | lttrd 11323 |
. . . . . . . 8
β’ ((π β§ π₯ β (4[,]π)) β 0 < (((2 logb π₯)β5) + 1)) |
70 | 18, 20, 44, 69, 38 | relogbcld 40459 |
. . . . . . 7
β’ ((π β§ π₯ β (4[,]π)) β (2 logb (((2
logb π₯)β5)
+ 1)) β β) |
71 | 18, 70 | remulcld 11192 |
. . . . . 6
β’ ((π β§ π₯ β (4[,]π)) β (2 Β· (2 logb
(((2 logb π₯)β5) + 1))) β
β) |
72 | | 0red 11165 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β 0 β β) |
73 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β π₯ β (4[,]π)) |
74 | 7, 8 | jca 513 |
. . . . . . . . . . . . 13
β’ (π β (4 β β β§
π β
β)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (4[,]π)) β (4 β β β§ π β
β)) |
76 | 75, 21 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (4[,]π)) β (π₯ β (4[,]π) β (π₯ β β β§ 4 β€ π₯ β§ π₯ β€ π))) |
77 | 73, 76 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (4[,]π)) β (π₯ β β β§ 4 β€ π₯ β§ π₯ β€ π)) |
78 | 77 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ π₯ β (4[,]π)) β 4 β€ π₯) |
79 | 72, 28, 25, 30, 78 | ltletrd 11322 |
. . . . . . . 8
β’ ((π β§ π₯ β (4[,]π)) β 0 < π₯) |
80 | 18, 20, 25, 79, 38 | relogbcld 40459 |
. . . . . . 7
β’ ((π β§ π₯ β (4[,]π)) β (2 logb π₯) β
β) |
81 | 80 | resqcld 14037 |
. . . . . 6
β’ ((π β§ π₯ β (4[,]π)) β ((2 logb π₯)β2) β
β) |
82 | 71, 81 | readdcld 11191 |
. . . . 5
β’ ((π β§ π₯ β (4[,]π)) β ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)) β
β) |
83 | 82 | fmpttd 7068 |
. . . 4
β’ (π β (π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))):(4[,]π)βΆβ) |
84 | 48 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
85 | | 3lt4 12334 |
. . . . . . . . . . 11
β’ 3 <
4 |
86 | 85 | a1i 11 |
. . . . . . . . . 10
β’ (π β 3 < 4) |
87 | 8, 33 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β (π + 1) β β) |
88 | 8 | ltp1d 12092 |
. . . . . . . . . . 11
β’ (π β π < (π + 1)) |
89 | 7, 8, 87, 12, 88 | lelttrd 11320 |
. . . . . . . . . 10
β’ (π β 4 < (π + 1)) |
90 | 86, 89 | jca 513 |
. . . . . . . . 9
β’ (π β (3 < 4 β§ 4 <
(π + 1))) |
91 | 5 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β 3 β
β*) |
92 | 87 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β (π + 1) β
β*) |
93 | 7 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β 4 β
β*) |
94 | | elioo5 13328 |
. . . . . . . . . 10
β’ ((3
β β* β§ (π + 1) β β* β§ 4
β β*) β (4 β (3(,)(π + 1)) β (3 < 4 β§ 4 < (π + 1)))) |
95 | 91, 92, 93, 94 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (4 β (3(,)(π + 1)) β (3 < 4 β§ 4
< (π +
1)))) |
96 | 90, 95 | mpbird 257 |
. . . . . . . 8
β’ (π β 4 β (3(,)(π + 1))) |
97 | 5, 7, 8, 86, 12 | ltletrd 11322 |
. . . . . . . . . 10
β’ (π β 3 < π) |
98 | 97, 88 | jca 513 |
. . . . . . . . 9
β’ (π β (3 < π β§ π < (π + 1))) |
99 | 8 | rexrd 11212 |
. . . . . . . . . 10
β’ (π β π β
β*) |
100 | | elioo5 13328 |
. . . . . . . . . 10
β’ ((3
β β* β§ (π + 1) β β* β§ π β β*)
β (π β
(3(,)(π + 1)) β (3
< π β§ π < (π + 1)))) |
101 | 91, 92, 99, 100 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π β (3(,)(π + 1)) β (3 < π β§ π < (π + 1)))) |
102 | 98, 101 | mpbird 257 |
. . . . . . . 8
β’ (π β π β (3(,)(π + 1))) |
103 | | iccssioo2 13344 |
. . . . . . . 8
β’ ((4
β (3(,)(π + 1)) β§
π β (3(,)(π + 1))) β (4[,]π) β (3(,)(π + 1))) |
104 | 96, 102, 103 | syl2anc 585 |
. . . . . . 7
β’ (π β (4[,]π) β (3(,)(π + 1))) |
105 | 104 | resmptd 5999 |
. . . . . 6
β’ (π β ((π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) βΎ (4[,]π)) = (π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) |
106 | | 2cnd 12238 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β
β) |
107 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β
β) |
108 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < 2) |
109 | | elioore 13301 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (3(,)(π + 1)) β π₯ β β) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β π₯ β β) |
111 | | 0red 11165 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 β
β) |
112 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 3 β
β) |
113 | | 3pos 12265 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 <
3 |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < 3) |
115 | | eliooord 13330 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (3(,)(π + 1)) β (3 < π₯ β§ π₯ < (π + 1))) |
116 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((3 <
π₯ β§ π₯ < (π + 1)) β 3 < π₯) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (3(,)(π + 1)) β 3 < π₯) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 3 < π₯) |
119 | 111, 112,
110, 114, 118 | lttrd 11323 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < π₯) |
120 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β 1) |
121 | 107, 108,
110, 119, 120 | relogbcld 40459 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 logb π₯) β
β) |
122 | 40 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β 5 β
β0) |
123 | 121, 122 | reexpcld 14075 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 logb π₯)β5) β
β) |
124 | | 1red 11163 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β 1 β
β) |
125 | 123, 124 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β (((2 logb π₯)β5) + 1) β
β) |
126 | 111, 124 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β (0 + 1) β
β) |
127 | 111 | ltp1d 12092 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < (0 +
1)) |
128 | 122 | nn0zd 12532 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β 5 β
β€) |
129 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (3(,)(π + 1))) β 1 < 2) |
130 | | 2lt3 12332 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 <
3 |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 < 3) |
132 | 124, 107,
112, 129, 131 | lttrd 11323 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (3(,)(π + 1))) β 1 < 3) |
133 | 124, 112,
110, 132, 118 | lttrd 11323 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 1 < π₯) |
134 | 110, 119 | elrpd 12961 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (3(,)(π + 1))) β π₯ β β+) |
135 | | 2rp 12927 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
β+ |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β
β+) |
137 | 134, 136,
129 | jca32 517 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (3(,)(π + 1))) β (π₯ β β+ β§ (2 β
β+ β§ 1 < 2))) |
138 | | logbgt0b 26159 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β β+
β§ (2 β β+ β§ 1 < 2)) β (0 < (2
logb π₯) β 1
< π₯)) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β (0 < (2 logb
π₯) β 1 < π₯)) |
140 | 133, 139 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < (2 logb
π₯)) |
141 | 121, 128,
140, 66 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < ((2 logb
π₯)β5)) |
142 | 111, 123,
124, 141 | ltadd1dd 11773 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β (0 + 1) < (((2
logb π₯)β5)
+ 1)) |
143 | 111, 126,
125, 127, 142 | lttrd 11323 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β 0 < (((2 logb
π₯)β5) +
1)) |
144 | 124, 129 | ltned 11298 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β 1 β 2) |
145 | 144 | necomd 3000 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β 1) |
146 | 107, 108,
125, 143, 145 | relogbcld 40459 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 logb (((2
logb π₯)β5)
+ 1)) β β) |
147 | 146 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 logb (((2
logb π₯)β5)
+ 1)) β β) |
148 | 106, 147 | mulcld 11182 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 Β· (2
logb (((2 logb π₯)β5) + 1))) β
β) |
149 | 48, 121 | sselid 3947 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 logb π₯) β
β) |
150 | 149 | sqcld 14056 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 logb π₯)β2) β
β) |
151 | 148, 150 | addcld 11181 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)) β
β) |
152 | 151 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))):(3(,)(π +
1))βΆβ) |
153 | | ioossre 13332 |
. . . . . . . . . 10
β’
(3(,)(π + 1))
β β |
154 | 153 | a1i 11 |
. . . . . . . . 9
β’ (π β (3(,)(π + 1)) β β) |
155 | 84, 152, 154 | 3jca 1129 |
. . . . . . . 8
β’ (π β (β β β
β§ (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))):(3(,)(π + 1))βΆβ β§
(3(,)(π + 1)) β
β)) |
156 | 136 | relogcld 25994 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (logβ2) β
β) |
157 | 125, 156 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((((2 logb π₯)β5) + 1) Β·
(logβ2)) β β) |
158 | 48, 123 | sselid 3947 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 logb π₯)β5) β
β) |
159 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 1 β
β) |
160 | 158, 159 | addcld 11181 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (((2 logb π₯)β5) + 1) β
β) |
161 | 111, 108 | gtned 11297 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β 0) |
162 | 106, 161 | logcld 25942 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (logβ2) β
β) |
163 | 111, 143 | gtned 11297 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (((2 logb π₯)β5) + 1) β
0) |
164 | | loggt0b 26003 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (2 β
β+ β (0 < (logβ2) β 1 <
2)) |
165 | 135, 164 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 <
(logβ2) β 1 < 2) |
166 | 35, 165 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 <
(logβ2)) |
167 | 26, 166 | ltned 11298 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 0 β
(logβ2)) |
168 | 167 | necomd 3000 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (logβ2) β
0) |
169 | 168 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (logβ2) β
0) |
170 | 160, 162,
163, 169 | mulne0d 11814 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((((2 logb π₯)β5) + 1) Β·
(logβ2)) β 0) |
171 | 124, 157,
170 | redivcld 11990 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β (1 / ((((2 logb
π₯)β5) + 1) Β·
(logβ2))) β β) |
172 | | 5re 12247 |
. . . . . . . . . . . . . . . . . . 19
β’ 5 β
β |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β 5 β
β) |
174 | | 4nn0 12439 |
. . . . . . . . . . . . . . . . . . . 20
β’ 4 β
β0 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (3(,)(π + 1))) β 4 β
β0) |
176 | 121, 175 | reexpcld 14075 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 logb π₯)β4) β
β) |
177 | 173, 176 | remulcld 11192 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (5 Β· ((2
logb π₯)β4))
β β) |
178 | 110, 156 | remulcld 11192 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β (π₯ Β· (logβ2)) β
β) |
179 | 48, 110 | sselid 3947 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (3(,)(π + 1))) β π₯ β β) |
180 | 111, 119 | gtned 11297 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (3(,)(π + 1))) β π₯ β 0) |
181 | 179, 162,
180, 169 | mulne0d 11814 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (3(,)(π + 1))) β (π₯ Β· (logβ2)) β
0) |
182 | 124, 178,
181 | redivcld 11990 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (3(,)(π + 1))) β (1 / (π₯ Β· (logβ2))) β
β) |
183 | 177, 182 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((5 Β· ((2
logb π₯)β4))
Β· (1 / (π₯ Β·
(logβ2)))) β β) |
184 | 183, 111 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β (((5 Β· ((2
logb π₯)β4))
Β· (1 / (π₯ Β·
(logβ2)))) + 0) β β) |
185 | 171, 184 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((1 / ((((2 logb
π₯)β5) + 1) Β·
(logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) + 0)) β
β) |
186 | 107, 185 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) β β) |
187 | 156 | resqcld 14037 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((logβ2)β2) β
β) |
188 | 56 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β 2 β
β€) |
189 | 162, 169,
188 | expne0d 14064 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((logβ2)β2) β
0) |
190 | 107, 187,
189 | redivcld 11990 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 / ((logβ2)β2))
β β) |
191 | 134 | relogcld 25994 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β (logβπ₯) β β) |
192 | | 2m1e1 12286 |
. . . . . . . . . . . . . . . . . 18
β’ (2
β 1) = 1 |
193 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β0 |
194 | 192, 193 | eqeltri 2834 |
. . . . . . . . . . . . . . . . 17
β’ (2
β 1) β β0 |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (3(,)(π + 1))) β (2 β 1) β
β0) |
196 | 191, 195 | reexpcld 14075 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((logβπ₯)β(2 β 1)) β
β) |
197 | 196, 110,
180 | redivcld 11990 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β (((logβπ₯)β(2 β 1)) / π₯) β
β) |
198 | 190, 197 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 / ((logβ2)β2))
Β· (((logβπ₯)β(2 β 1)) / π₯)) β β) |
199 | 186, 198 | readdcld 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯))) β β) |
200 | 199 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π β βπ₯ β (3(,)(π + 1))((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯))) β β) |
201 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π₯(3(,)(π + 1)) |
202 | 201 | fnmptf 6642 |
. . . . . . . . . . 11
β’
(βπ₯ β
(3(,)(π + 1))((2 Β·
((1 / ((((2 logb π₯)β5) + 1) Β· (logβ2)))
Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) + 0))) + ((2 /
((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯))) β β β (π₯ β (3(,)(π + 1)) β¦ ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯)))) Fn (3(,)(π + 1))) |
203 | 200, 202 | syl 17 |
. . . . . . . . . 10
β’ (π β (π₯ β (3(,)(π + 1)) β¦ ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯)))) Fn (3(,)(π + 1))) |
204 | 5 | leidd 11728 |
. . . . . . . . . . . 12
β’ (π β 3 β€ 3) |
205 | 8 | lep1d 12093 |
. . . . . . . . . . . . 13
β’ (π β π β€ (π + 1)) |
206 | 5, 8, 87, 13, 205 | letrd 11319 |
. . . . . . . . . . . 12
β’ (π β 3 β€ (π + 1)) |
207 | 5, 87, 204, 206 | aks4d1p1p6 40559 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) = (π₯ β (3(,)(π + 1)) β¦ ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯))))) |
208 | 207 | fneq1d 6600 |
. . . . . . . . . 10
β’ (π β ((β D (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) Fn (3(,)(π + 1)) β (π₯ β (3(,)(π + 1)) β¦ ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯)))) Fn (3(,)(π + 1)))) |
209 | 203, 208 | mpbird 257 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) Fn (3(,)(π + 1))) |
210 | 209 | fndmd 6612 |
. . . . . . . 8
β’ (π β dom (β D (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) = (3(,)(π + 1))) |
211 | | dvcn 25301 |
. . . . . . . 8
β’
(((β β β β§ (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))):(3(,)(π + 1))βΆβ β§
(3(,)(π + 1)) β
β) β§ dom (β D (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) = (3(,)(π + 1))) β (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((3(,)(π + 1))βcnββ)) |
212 | 155, 210,
211 | syl2anc 585 |
. . . . . . 7
β’ (π β (π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((3(,)(π + 1))βcnββ)) |
213 | | rescncf 24276 |
. . . . . . . 8
β’
((4[,]π) β
(3(,)(π + 1)) β
((π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((3(,)(π + 1))βcnββ) β ((π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) βΎ (4[,]π)) β ((4[,]π)βcnββ))) |
214 | 104, 213 | syl 17 |
. . . . . . 7
β’ (π β ((π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((3(,)(π + 1))βcnββ) β ((π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) βΎ (4[,]π)) β ((4[,]π)βcnββ))) |
215 | 212, 214 | mpd 15 |
. . . . . 6
β’ (π β ((π₯ β (3(,)(π + 1)) β¦ ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) βΎ (4[,]π)) β ((4[,]π)βcnββ)) |
216 | 105, 215 | eqeltrrd 2839 |
. . . . 5
β’ (π β (π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((4[,]π)βcnββ)) |
217 | | cncfcdm 24277 |
. . . . 5
β’ ((β
β β β§ (π₯
β (4[,]π) β¦ ((2
Β· (2 logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((4[,]π)βcnββ)) β ((π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((4[,]π)βcnββ) β (π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))):(4[,]π)βΆβ)) |
218 | 84, 216, 217 | syl2anc 585 |
. . . 4
β’ (π β ((π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((4[,]π)βcnββ) β (π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))):(4[,]π)βΆβ)) |
219 | 83, 218 | mpbird 257 |
. . 3
β’ (π β (π₯ β (4[,]π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2))) β ((4[,]π)βcnββ)) |
220 | 174 | a1i 11 |
. . . . . 6
β’ ((π β§ π₯ β (4[,]π)) β 4 β
β0) |
221 | 39, 220 | reexpcld 14075 |
. . . . 5
β’ ((π β§ π₯ β (4[,]π)) β ((2 logb π₯)β4) β
β) |
222 | 221 | fmpttd 7068 |
. . . 4
β’ (π β (π₯ β (4[,]π) β¦ ((2 logb π₯)β4)):(4[,]π)βΆβ) |
223 | 104 | resmptd 5999 |
. . . . . 6
β’ (π β ((π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) βΎ (4[,]π)) = (π₯ β (4[,]π) β¦ ((2 logb π₯)β4))) |
224 | 48, 176 | sselid 3947 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((2 logb π₯)β4) β
β) |
225 | 224 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)):(3(,)(π +
1))βΆβ) |
226 | 84, 225, 154 | 3jca 1129 |
. . . . . . . 8
β’ (π β (β β β
β§ (π₯ β (3(,)(π + 1)) β¦ ((2
logb π₯)β4)):(3(,)(π + 1))βΆβ β§ (3(,)(π + 1)) β
β)) |
227 | 6 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β 4 β
β) |
228 | 156, 175 | reexpcld 14075 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((logβ2)β4) β
β) |
229 | | 4z 12544 |
. . . . . . . . . . . . . . . 16
β’ 4 β
β€ |
230 | 229 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β 4 β
β€) |
231 | 162, 169,
230 | expne0d 14064 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((logβ2)β4) β
0) |
232 | 227, 228,
231 | redivcld 11990 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (3(,)(π + 1))) β (4 / ((logβ2)β4))
β β) |
233 | | 4m1e3 12289 |
. . . . . . . . . . . . . . . . 17
β’ (4
β 1) = 3 |
234 | | 3nn0 12438 |
. . . . . . . . . . . . . . . . 17
β’ 3 β
β0 |
235 | 233, 234 | eqeltri 2834 |
. . . . . . . . . . . . . . . 16
β’ (4
β 1) β β0 |
236 | 235 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (3(,)(π + 1))) β (4 β 1) β
β0) |
237 | 191, 236 | reexpcld 14075 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((logβπ₯)β(4 β 1)) β
β) |
238 | 237, 110,
180 | redivcld 11990 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (3(,)(π + 1))) β (((logβπ₯)β(4 β 1)) / π₯) β
β) |
239 | 232, 238 | remulcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (3(,)(π + 1))) β ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯)) β β) |
240 | 239 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π β βπ₯ β (3(,)(π + 1))((4 / ((logβ2)β4)) Β·
(((logβπ₯)β(4
β 1)) / π₯)) β
β) |
241 | 201 | fnmptf 6642 |
. . . . . . . . . . 11
β’
(βπ₯ β
(3(,)(π + 1))((4 /
((logβ2)β4)) Β· (((logβπ₯)β(4 β 1)) / π₯)) β β β (π₯ β (3(,)(π + 1)) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) Fn (3(,)(π + 1))) |
242 | 240, 241 | syl 17 |
. . . . . . . . . 10
β’ (π β (π₯ β (3(,)(π + 1)) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) Fn (3(,)(π + 1))) |
243 | 113 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 0 < 3) |
244 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) = (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) |
245 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π₯ β (3(,)(π + 1)) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) = (π₯ β (3(,)(π + 1)) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) |
246 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (4 /
((logβ2)β4)) = (4 / ((logβ2)β4)) |
247 | | 4nn 12243 |
. . . . . . . . . . . . 13
β’ 4 β
β |
248 | 247 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 4 β
β) |
249 | 5, 87, 243, 206, 244, 245, 246, 248 | dvrelogpow2b 40554 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4))) = (π₯ β (3(,)(π + 1)) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯)))) |
250 | 249 | fneq1d 6600 |
. . . . . . . . . 10
β’ (π β ((β D (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4))) Fn (3(,)(π + 1)) β (π₯ β (3(,)(π + 1)) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) Fn (3(,)(π + 1)))) |
251 | 242, 250 | mpbird 257 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4))) Fn (3(,)(π + 1))) |
252 | 251 | fndmd 6612 |
. . . . . . . 8
β’ (π β dom (β D (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4))) = (3(,)(π + 1))) |
253 | | dvcn 25301 |
. . . . . . . 8
β’
(((β β β β§ (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)):(3(,)(π + 1))βΆβ β§
(3(,)(π + 1)) β
β) β§ dom (β D (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4))) = (3(,)(π + 1))) β (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) β ((3(,)(π + 1))βcnββ)) |
254 | 226, 252,
253 | syl2anc 585 |
. . . . . . 7
β’ (π β (π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) β ((3(,)(π + 1))βcnββ)) |
255 | | rescncf 24276 |
. . . . . . . 8
β’
((4[,]π) β
(3(,)(π + 1)) β
((π₯ β (3(,)(π + 1)) β¦ ((2
logb π₯)β4))
β ((3(,)(π +
1))βcnββ) β ((π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) βΎ (4[,]π)) β ((4[,]π)βcnββ))) |
256 | 104, 255 | syl 17 |
. . . . . . 7
β’ (π β ((π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) β ((3(,)(π + 1))βcnββ) β ((π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) βΎ (4[,]π)) β ((4[,]π)βcnββ))) |
257 | 254, 256 | mpd 15 |
. . . . . 6
β’ (π β ((π₯ β (3(,)(π + 1)) β¦ ((2 logb π₯)β4)) βΎ (4[,]π)) β ((4[,]π)βcnββ)) |
258 | 223, 257 | eqeltrrd 2839 |
. . . . 5
β’ (π β (π₯ β (4[,]π) β¦ ((2 logb π₯)β4)) β ((4[,]π)βcnββ)) |
259 | | cncfcdm 24277 |
. . . . 5
β’ ((β
β β β§ (π₯
β (4[,]π) β¦ ((2
logb π₯)β4))
β ((4[,]π)βcnββ)) β ((π₯ β (4[,]π) β¦ ((2 logb π₯)β4)) β ((4[,]π)βcnββ) β (π₯ β (4[,]π) β¦ ((2 logb π₯)β4)):(4[,]π)βΆβ)) |
260 | 84, 258, 259 | syl2anc 585 |
. . . 4
β’ (π β ((π₯ β (4[,]π) β¦ ((2 logb π₯)β4)) β ((4[,]π)βcnββ) β (π₯ β (4[,]π) β¦ ((2 logb π₯)β4)):(4[,]π)βΆβ)) |
261 | 222, 260 | mpbird 257 |
. . 3
β’ (π β (π₯ β (4[,]π) β¦ ((2 logb π₯)β4)) β ((4[,]π)βcnββ)) |
262 | 7, 8, 11, 12 | aks4d1p1p6 40559 |
. . 3
β’ (π β (β D (π₯ β (4(,)π) β¦ ((2 Β· (2 logb
(((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)))) = (π₯ β (4(,)π) β¦ ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯))))) |
263 | 29 | a1i 11 |
. . . . 5
β’ (π β 0 < 4) |
264 | | eqid 2737 |
. . . . 5
β’ (π₯ β (4(,)π) β¦ ((2 logb π₯)β4)) = (π₯ β (4(,)π) β¦ ((2 logb π₯)β4)) |
265 | | eqid 2737 |
. . . . 5
β’ (π₯ β (4(,)π) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) = (π₯ β (4(,)π) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) |
266 | 7, 8, 263, 12, 264, 265, 246, 248 | dvrelogpow2b 40554 |
. . . 4
β’ (π β (β D (π₯ β (4(,)π) β¦ ((2 logb π₯)β4))) = (π₯ β (4(,)π) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯)))) |
267 | 233 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β (4(,)π)) β (4 β 1) =
3) |
268 | 267 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ π₯ β (4(,)π)) β ((logβπ₯)β(4 β 1)) = ((logβπ₯)β3)) |
269 | 268 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π₯ β (4(,)π)) β (((logβπ₯)β(4 β 1)) / π₯) = (((logβπ₯)β3) / π₯)) |
270 | 269 | oveq2d 7378 |
. . . . 5
β’ ((π β§ π₯ β (4(,)π)) β ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯)) = ((4 / ((logβ2)β4)) Β·
(((logβπ₯)β3) /
π₯))) |
271 | 270 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β (4(,)π) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β(4 β 1)) / π₯))) = (π₯ β (4(,)π) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β3) / π₯)))) |
272 | 266, 271 | eqtrd 2777 |
. . 3
β’ (π β (β D (π₯ β (4(,)π) β¦ ((2 logb π₯)β4))) = (π₯ β (4(,)π) β¦ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β3) / π₯)))) |
273 | | elioore 13301 |
. . . . 5
β’ (π₯ β (4(,)π) β π₯ β β) |
274 | 273 | adantl 483 |
. . . 4
β’ ((π β§ π₯ β (4(,)π)) β π₯ β β) |
275 | 6 | a1i 11 |
. . . . 5
β’ ((π β§ π₯ β (4(,)π)) β 4 β β) |
276 | | eliooord 13330 |
. . . . . . 7
β’ (π₯ β (4(,)π) β (4 < π₯ β§ π₯ < π)) |
277 | 276 | simpld 496 |
. . . . . 6
β’ (π₯ β (4(,)π) β 4 < π₯) |
278 | 277 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β (4(,)π)) β 4 < π₯) |
279 | 275, 274,
278 | ltled 11310 |
. . . 4
β’ ((π β§ π₯ β (4(,)π)) β 4 β€ π₯) |
280 | 274, 279 | aks4d1p1p7 40560 |
. . 3
β’ ((π β§ π₯ β (4(,)π)) β ((2 Β· ((1 / ((((2
logb π₯)β5)
+ 1) Β· (logβ2))) Β· (((5 Β· ((2 logb π₯)β4)) Β· (1 / (π₯ Β· (logβ2)))) +
0))) + ((2 / ((logβ2)β2)) Β· (((logβπ₯)β(2 β 1)) / π₯))) β€ ((4 / ((logβ2)β4))
Β· (((logβπ₯)β3) / π₯))) |
281 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = 4 β (2 logb
π₯) = (2 logb
4)) |
282 | 281 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = 4 β ((2 logb
π₯)β5) = ((2
logb 4)β5)) |
283 | 282 | oveq1d 7377 |
. . . . . 6
β’ (π₯ = 4 β (((2 logb
π₯)β5) + 1) = (((2
logb 4)β5) + 1)) |
284 | 283 | oveq2d 7378 |
. . . . 5
β’ (π₯ = 4 β (2 logb
(((2 logb π₯)β5) + 1)) = (2 logb (((2
logb 4)β5) + 1))) |
285 | 284 | oveq2d 7378 |
. . . 4
β’ (π₯ = 4 β (2 Β· (2
logb (((2 logb π₯)β5) + 1))) = (2 Β· (2
logb (((2 logb 4)β5) + 1)))) |
286 | 281 | oveq1d 7377 |
. . . 4
β’ (π₯ = 4 β ((2 logb
π₯)β2) = ((2
logb 4)β2)) |
287 | 285, 286 | oveq12d 7380 |
. . 3
β’ (π₯ = 4 β ((2 Β· (2
logb (((2 logb π₯)β5) + 1))) + ((2 logb π₯)β2)) = ((2 Β· (2
logb (((2 logb 4)β5) + 1))) + ((2 logb
4)β2))) |
288 | 281 | oveq1d 7377 |
. . 3
β’ (π₯ = 4 β ((2 logb
π₯)β4) = ((2
logb 4)β4)) |
289 | | oveq2 7370 |
. . . . . . . . 9
β’ (π₯ = π β (2 logb π₯) = (2 logb π)) |
290 | 289 | oveq1d 7377 |
. . . . . . . 8
β’ (π₯ = π β ((2 logb π₯)β5) = ((2 logb
π)β5)) |
291 | 290 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = π β (((2 logb π₯)β5) + 1) = (((2
logb π)β5)
+ 1)) |
292 | 291 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = π β (2 logb (((2
logb π₯)β5)
+ 1)) = (2 logb (((2 logb π)β5) + 1))) |
293 | 292 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π β (2 Β· (2 logb (((2
logb π₯)β5)
+ 1))) = (2 Β· (2 logb (((2 logb π)β5) + 1)))) |
294 | 14 | a1i 11 |
. . . . . . 7
β’ (π₯ = π β πΆ = (2 logb (((2 logb
π)β5) +
1))) |
295 | 294 | oveq2d 7378 |
. . . . . 6
β’ (π₯ = π β (2 Β· πΆ) = (2 Β· (2 logb (((2
logb π)β5)
+ 1)))) |
296 | 295 | eqcomd 2743 |
. . . . 5
β’ (π₯ = π β (2 Β· (2 logb (((2
logb π)β5)
+ 1))) = (2 Β· πΆ)) |
297 | 293, 296 | eqtrd 2777 |
. . . 4
β’ (π₯ = π β (2 Β· (2 logb (((2
logb π₯)β5)
+ 1))) = (2 Β· πΆ)) |
298 | 289 | oveq1d 7377 |
. . . . 5
β’ (π₯ = π β ((2 logb π₯)β2) = ((2 logb
π)β2)) |
299 | 15 | a1i 11 |
. . . . . 6
β’ (π₯ = π β π· = ((2 logb π)β2)) |
300 | 299 | eqcomd 2743 |
. . . . 5
β’ (π₯ = π β ((2 logb π)β2) = π·) |
301 | 298, 300 | eqtrd 2777 |
. . . 4
β’ (π₯ = π β ((2 logb π₯)β2) = π·) |
302 | 297, 301 | oveq12d 7380 |
. . 3
β’ (π₯ = π β ((2 Β· (2 logb (((2
logb π₯)β5)
+ 1))) + ((2 logb π₯)β2)) = ((2 Β· πΆ) + π·)) |
303 | 289 | oveq1d 7377 |
. . . 4
β’ (π₯ = π β ((2 logb π₯)β4) = ((2 logb
π)β4)) |
304 | 16 | a1i 11 |
. . . . 5
β’ (π₯ = π β πΈ = ((2 logb π)β4)) |
305 | 304 | eqcomd 2743 |
. . . 4
β’ (π₯ = π β ((2 logb π)β4) = πΈ) |
306 | 303, 305 | eqtrd 2777 |
. . 3
β’ (π₯ = π β ((2 logb π₯)β4) = πΈ) |
307 | | sq2 14108 |
. . . . . . . . . . . . . . . 16
β’
(2β2) = 4 |
308 | 307 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
β’ (2
logb (2β2)) = (2 logb 4) |
309 | 308 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (2 logb
(2β2)) = (2 logb 4)) |
310 | 309 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π β (2 logb 4) = (2
logb (2β2))) |
311 | 135 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β
β+) |
312 | 56 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β
β€) |
313 | | relogbexp 26146 |
. . . . . . . . . . . . . 14
β’ ((2
β β+ β§ 2 β 1 β§ 2 β β€) β (2
logb (2β2)) = 2) |
314 | 311, 37, 312, 313 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (2 logb
(2β2)) = 2) |
315 | 310, 314 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (2 logb 4) =
2) |
316 | 315 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β ((2 logb
4)β5) = (2β5)) |
317 | 316 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β (((2 logb
4)β5) + 1) = ((2β5) + 1)) |
318 | 317 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β (2 logb (((2
logb 4)β5) + 1)) = (2 logb ((2β5) +
1))) |
319 | 17 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 2 β
β) |
320 | 319 | leidd 11728 |
. . . . . . . . . . 11
β’ (π β 2 β€ 2) |
321 | 315, 319 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ (π β (2 logb 4)
β β) |
322 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 5 β
β0) |
323 | 321, 322 | reexpcld 14075 |
. . . . . . . . . . . . 13
β’ (π β ((2 logb
4)β5) β β) |
324 | 316, 323 | eqeltrrd 2839 |
. . . . . . . . . . . 12
β’ (π β (2β5) β
β) |
325 | 324, 33 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β ((2β5) + 1) β
β) |
326 | 322 | nn0zd 12532 |
. . . . . . . . . . . . . . 15
β’ (π β 5 β
β€) |
327 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 < 2) |
328 | 327, 315 | breqtrrd 5138 |
. . . . . . . . . . . . . . 15
β’ (π β 0 < (2 logb
4)) |
329 | 321, 326,
328 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (π β ((2 logb 4)
β β β§ 5 β β€ β§ 0 < (2 logb
4))) |
330 | | expgt0 14008 |
. . . . . . . . . . . . . 14
β’ (((2
logb 4) β β β§ 5 β β€ β§ 0 < (2
logb 4)) β 0 < ((2 logb
4)β5)) |
331 | 329, 330 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 0 < ((2 logb
4)β5)) |
332 | 331, 316 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (π β 0 <
(2β5)) |
333 | 324 | ltp1d 12092 |
. . . . . . . . . . . 12
β’ (π β (2β5) <
((2β5) + 1)) |
334 | 26, 324, 325, 332, 333 | lttrd 11323 |
. . . . . . . . . . 11
β’ (π β 0 < ((2β5) +
1)) |
335 | | 6nn0 12441 |
. . . . . . . . . . . . 13
β’ 6 β
β0 |
336 | 335 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 6 β
β0) |
337 | 319, 336 | reexpcld 14075 |
. . . . . . . . . . 11
β’ (π β (2β6) β
β) |
338 | 336 | nn0zd 12532 |
. . . . . . . . . . . 12
β’ (π β 6 β
β€) |
339 | | expgt0 14008 |
. . . . . . . . . . . 12
β’ ((2
β β β§ 6 β β€ β§ 0 < 2) β 0 <
(2β6)) |
340 | 319, 338,
327, 339 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β 0 <
(2β6)) |
341 | 324, 324 | readdcld 11191 |
. . . . . . . . . . . 12
β’ (π β ((2β5) + (2β5))
β β) |
342 | 33, 319, 35 | ltled 11310 |
. . . . . . . . . . . . . 14
β’ (π β 1 β€ 2) |
343 | 319, 322,
342 | expge1d 14077 |
. . . . . . . . . . . . 13
β’ (π β 1 β€
(2β5)) |
344 | 33, 324, 324, 343 | leadd2dd 11777 |
. . . . . . . . . . . 12
β’ (π β ((2β5) + 1) β€
((2β5) + (2β5))) |
345 | 341 | leidd 11728 |
. . . . . . . . . . . . 13
β’ (π β ((2β5) + (2β5))
β€ ((2β5) + (2β5))) |
346 | | df-6 12227 |
. . . . . . . . . . . . . . . . . . 19
β’ 6 = (5 +
1) |
347 | 346 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 6 = (5 +
1)) |
348 | 347 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2β6) = (2β(5 +
1))) |
349 | | 2cn 12235 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β |
350 | 349 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 2 β
β) |
351 | 193 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 1 β
β0) |
352 | 350, 351,
322 | expaddd 14060 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2β(5 + 1)) =
((2β5) Β· (2β1))) |
353 | 348, 352 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β (2β6) = ((2β5)
Β· (2β1))) |
354 | 350 | exp1d 14053 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2β1) =
2) |
355 | 354 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π β ((2β5) Β·
(2β1)) = ((2β5) Β· 2)) |
356 | 353, 355 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (π β (2β6) = ((2β5)
Β· 2)) |
357 | 48, 324 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ (π β (2β5) β
β) |
358 | 357 | times2d 12404 |
. . . . . . . . . . . . . . 15
β’ (π β ((2β5) Β· 2) =
((2β5) + (2β5))) |
359 | 356, 358 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (π β (2β6) = ((2β5) +
(2β5))) |
360 | 359 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π β ((2β5) + (2β5))
= (2β6)) |
361 | 345, 360 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (π β ((2β5) + (2β5))
β€ (2β6)) |
362 | 325, 341,
337, 344, 361 | letrd 11319 |
. . . . . . . . . . 11
β’ (π β ((2β5) + 1) β€
(2β6)) |
363 | 312, 320,
325, 334, 337, 340, 362 | logblebd 40462 |
. . . . . . . . . 10
β’ (π β (2 logb
((2β5) + 1)) β€ (2 logb (2β6))) |
364 | 311, 37, 338 | relogbexpd 40460 |
. . . . . . . . . 10
β’ (π β (2 logb
(2β6)) = 6) |
365 | 363, 364 | breqtrd 5136 |
. . . . . . . . 9
β’ (π β (2 logb
((2β5) + 1)) β€ 6) |
366 | 318, 365 | eqbrtrd 5132 |
. . . . . . . 8
β’ (π β (2 logb (((2
logb 4)β5) + 1)) β€ 6) |
367 | | 6t2e12 12729 |
. . . . . . . . 9
β’ (6
Β· 2) = ;12 |
368 | | 6cn 12251 |
. . . . . . . . . . 11
β’ 6 β
β |
369 | 368 | a1i 11 |
. . . . . . . . . 10
β’ (π β 6 β
β) |
370 | | 2nn 12233 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
371 | 193, 370 | decnncl 12645 |
. . . . . . . . . . . . 13
β’ ;12 β β |
372 | 371 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β ;12 β β) |
373 | 372 | nnred 12175 |
. . . . . . . . . . 11
β’ (π β ;12 β β) |
374 | 373 | recnd 11190 |
. . . . . . . . . 10
β’ (π β ;12 β β) |
375 | 26, 327 | gtned 11297 |
. . . . . . . . . 10
β’ (π β 2 β 0) |
376 | 369, 350,
374, 375 | ldiv 11996 |
. . . . . . . . 9
β’ (π β ((6 Β· 2) = ;12 β 6 = (;12 / 2))) |
377 | 367, 376 | mpbii 232 |
. . . . . . . 8
β’ (π β 6 = (;12 / 2)) |
378 | 366, 377 | breqtrd 5136 |
. . . . . . 7
β’ (π β (2 logb (((2
logb 4)β5) + 1)) β€ (;12 / 2)) |
379 | 323, 33 | readdcld 11191 |
. . . . . . . . 9
β’ (π β (((2 logb
4)β5) + 1) β β) |
380 | 26, 33 | readdcld 11191 |
. . . . . . . . . 10
β’ (π β (0 + 1) β
β) |
381 | 26 | ltp1d 12092 |
. . . . . . . . . 10
β’ (π β 0 < (0 +
1)) |
382 | 26, 323, 33, 331 | ltadd1dd 11773 |
. . . . . . . . . 10
β’ (π β (0 + 1) < (((2
logb 4)β5) + 1)) |
383 | 26, 380, 379, 381, 382 | lttrd 11323 |
. . . . . . . . 9
β’ (π β 0 < (((2
logb 4)β5) + 1)) |
384 | 319, 327,
379, 383, 37 | relogbcld 40459 |
. . . . . . . 8
β’ (π β (2 logb (((2
logb 4)β5) + 1)) β β) |
385 | 384, 373,
311 | lemuldiv2d 13014 |
. . . . . . 7
β’ (π β ((2 Β· (2
logb (((2 logb 4)β5) + 1))) β€ ;12 β (2 logb (((2 logb
4)β5) + 1)) β€ (;12 /
2))) |
386 | 378, 385 | mpbird 257 |
. . . . . 6
β’ (π β (2 Β· (2
logb (((2 logb 4)β5) + 1))) β€ ;12) |
387 | 315 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β ((2 logb
4)β2) = (2β2)) |
388 | 387, 307 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π β ((2 logb
4)β2) = 4) |
389 | 388 | oveq2d 7378 |
. . . . . . . 8
β’ (π β (;16 β ((2 logb 4)β2)) = (;16 β 4)) |
390 | | 2nn0 12437 |
. . . . . . . . . 10
β’ 2 β
β0 |
391 | | eqid 2737 |
. . . . . . . . . 10
β’ ;12 = ;12 |
392 | | 4cn 12245 |
. . . . . . . . . . 11
β’ 4 β
β |
393 | | 4p2e6 12313 |
. . . . . . . . . . 11
β’ (4 + 2) =
6 |
394 | 392, 349,
393 | addcomli 11354 |
. . . . . . . . . 10
β’ (2 + 4) =
6 |
395 | 193, 390,
174, 391, 394 | decaddi 12685 |
. . . . . . . . 9
β’ (;12 + 4) = ;16 |
396 | 392 | a1i 11 |
. . . . . . . . . 10
β’ (π β 4 β
β) |
397 | | 6nn 12249 |
. . . . . . . . . . . . . 14
β’ 6 β
β |
398 | 193, 397 | decnncl 12645 |
. . . . . . . . . . . . 13
β’ ;16 β β |
399 | 398 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β ;16 β β) |
400 | 399 | nnred 12175 |
. . . . . . . . . . 11
β’ (π β ;16 β β) |
401 | 48, 400 | sselid 3947 |
. . . . . . . . . 10
β’ (π β ;16 β β) |
402 | 374, 396,
401 | addlsub 11578 |
. . . . . . . . 9
β’ (π β ((;12 + 4) = ;16 β ;12 = (;16 β 4))) |
403 | 395, 402 | mpbii 232 |
. . . . . . . 8
β’ (π β ;12 = (;16 β 4)) |
404 | 389, 403 | eqtr4d 2780 |
. . . . . . 7
β’ (π β (;16 β ((2 logb 4)β2)) = ;12) |
405 | 404 | eqcomd 2743 |
. . . . . 6
β’ (π β ;12 = (;16 β ((2 logb
4)β2))) |
406 | 386, 405 | breqtrd 5136 |
. . . . 5
β’ (π β (2 Β· (2
logb (((2 logb 4)β5) + 1))) β€ (;16 β ((2 logb
4)β2))) |
407 | 319, 384 | remulcld 11192 |
. . . . . 6
β’ (π β (2 Β· (2
logb (((2 logb 4)β5) + 1))) β
β) |
408 | 321 | resqcld 14037 |
. . . . . 6
β’ (π β ((2 logb
4)β2) β β) |
409 | | leaddsub 11638 |
. . . . . 6
β’ (((2
Β· (2 logb (((2 logb 4)β5) + 1))) β
β β§ ((2 logb 4)β2) β β β§ ;16 β β) β (((2 Β·
(2 logb (((2 logb 4)β5) + 1))) + ((2 logb
4)β2)) β€ ;16 β (2
Β· (2 logb (((2 logb 4)β5) + 1))) β€ (;16 β ((2 logb
4)β2)))) |
410 | 407, 408,
400, 409 | syl3anc 1372 |
. . . . 5
β’ (π β (((2 Β· (2
logb (((2 logb 4)β5) + 1))) + ((2 logb
4)β2)) β€ ;16 β (2
Β· (2 logb (((2 logb 4)β5) + 1))) β€ (;16 β ((2 logb
4)β2)))) |
411 | 406, 410 | mpbird 257 |
. . . 4
β’ (π β ((2 Β· (2
logb (((2 logb 4)β5) + 1))) + ((2 logb
4)β2)) β€ ;16) |
412 | 315 | oveq1d 7377 |
. . . . . 6
β’ (π β ((2 logb
4)β4) = (2β4)) |
413 | | 2exp4 16964 |
. . . . . 6
β’
(2β4) = ;16 |
414 | 412, 413 | eqtrdi 2793 |
. . . . 5
β’ (π β ((2 logb
4)β4) = ;16) |
415 | 414 | eqcomd 2743 |
. . . 4
β’ (π β ;16 = ((2 logb
4)β4)) |
416 | 411, 415 | breqtrd 5136 |
. . 3
β’ (π β ((2 Β· (2
logb (((2 logb 4)β5) + 1))) + ((2 logb
4)β2)) β€ ((2 logb 4)β4)) |
417 | 7, 8, 219, 261, 262, 272, 280, 287, 288, 302, 306, 416, 12 | dvle2 40558 |
. 2
β’ (π β ((2 Β· πΆ) + π·) β€ πΈ) |
418 | 1, 2, 3, 13, 14, 15, 16, 417 | aks4d1p1p4 40557 |
1
β’ (π β π΄ < (2βπ΅)) |