Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . 7
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
2 | | pntlem1.a |
. . . . . . 7
β’ (π β π΄ β
β+) |
3 | | pntlem1.b |
. . . . . . 7
β’ (π β π΅ β
β+) |
4 | | pntlem1.l |
. . . . . . 7
β’ (π β πΏ β (0(,)1)) |
5 | | pntlem1.d |
. . . . . . 7
β’ π· = (π΄ + 1) |
6 | | pntlem1.f |
. . . . . . 7
β’ πΉ = ((1 β (1 / π·)) Β· ((πΏ / (;32 Β· π΅)) / (π·β2))) |
7 | | pntlem1.u |
. . . . . . 7
β’ (π β π β
β+) |
8 | | pntlem1.u2 |
. . . . . . 7
β’ (π β π β€ π΄) |
9 | | pntlem1.e |
. . . . . . 7
β’ πΈ = (π / π·) |
10 | | pntlem1.k |
. . . . . . 7
β’ πΎ = (expβ(π΅ / πΈ)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 26959 |
. . . . . 6
β’ (π β (πΈ β β+ β§ πΎ β β+
β§ (πΈ β (0(,)1)
β§ 1 < πΎ β§ (π β πΈ) β
β+))) |
12 | 11 | simp3d 1145 |
. . . . 5
β’ (π β (πΈ β (0(,)1) β§ 1 < πΎ β§ (π β πΈ) β
β+)) |
13 | 12 | simp3d 1145 |
. . . 4
β’ (π β (π β πΈ) β
β+) |
14 | 1, 2, 3, 4, 5, 6 | pntlemd 26958 |
. . . . . . . 8
β’ (π β (πΏ β β+ β§ π· β β+
β§ πΉ β
β+)) |
15 | 14 | simp1d 1143 |
. . . . . . 7
β’ (π β πΏ β
β+) |
16 | 11 | simp1d 1143 |
. . . . . . . 8
β’ (π β πΈ β
β+) |
17 | | 2z 12542 |
. . . . . . . 8
β’ 2 β
β€ |
18 | | rpexpcl 13993 |
. . . . . . . 8
β’ ((πΈ β β+
β§ 2 β β€) β (πΈβ2) β
β+) |
19 | 16, 17, 18 | sylancl 587 |
. . . . . . 7
β’ (π β (πΈβ2) β
β+) |
20 | 15, 19 | rpmulcld 12980 |
. . . . . 6
β’ (π β (πΏ Β· (πΈβ2)) β
β+) |
21 | | 3nn0 12438 |
. . . . . . . . 9
β’ 3 β
β0 |
22 | | 2nn 12233 |
. . . . . . . . 9
β’ 2 β
β |
23 | 21, 22 | decnncl 12645 |
. . . . . . . 8
β’ ;32 β β |
24 | | nnrp 12933 |
. . . . . . . 8
β’ (;32 β β β ;32 β
β+) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
β’ ;32 β
β+ |
26 | | rpmulcl 12945 |
. . . . . . 7
β’ ((;32 β β+ β§
π΅ β
β+) β (;32
Β· π΅) β
β+) |
27 | 25, 3, 26 | sylancr 588 |
. . . . . 6
β’ (π β (;32 Β· π΅) β
β+) |
28 | 20, 27 | rpdivcld 12981 |
. . . . 5
β’ (π β ((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) β
β+) |
29 | | pntlem1.y |
. . . . . . . . . 10
β’ (π β (π β β+ β§ 1 β€
π)) |
30 | | pntlem1.x |
. . . . . . . . . 10
β’ (π β (π β β+ β§ π < π)) |
31 | | pntlem1.c |
. . . . . . . . . 10
β’ (π β πΆ β
β+) |
32 | | pntlem1.w |
. . . . . . . . . 10
β’ π = (((π + (4 / (πΏ Β· πΈ)))β2) + (((π Β· (πΎβ2))β4) + (expβ(((;32 Β· π΅) / ((π β πΈ) Β· (πΏ Β· (πΈβ2)))) Β· ((π Β· 3) + πΆ))))) |
33 | | pntlem1.z |
. . . . . . . . . 10
β’ (π β π β (π[,)+β)) |
34 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33 | pntlemb 26961 |
. . . . . . . . 9
β’ (π β (π β β+ β§ (1 <
π β§ e β€
(ββπ) β§
(ββπ) β€
(π / π)) β§ ((4 / (πΏ Β· πΈ)) β€ (ββπ) β§ (((logβπ) / (logβπΎ)) + 2) β€ (((logβπ) / (logβπΎ)) / 4) β§ ((π Β· 3) + πΆ) β€ (((π β πΈ) Β· ((πΏ Β· (πΈβ2)) / (;32 Β· π΅))) Β· (logβπ))))) |
35 | 34 | simp1d 1143 |
. . . . . . . 8
β’ (π β π β
β+) |
36 | 35 | rpred 12964 |
. . . . . . 7
β’ (π β π β β) |
37 | 34 | simp2d 1144 |
. . . . . . . 8
β’ (π β (1 < π β§ e β€ (ββπ) β§ (ββπ) β€ (π / π))) |
38 | 37 | simp1d 1143 |
. . . . . . 7
β’ (π β 1 < π) |
39 | 36, 38 | rplogcld 26000 |
. . . . . 6
β’ (π β (logβπ) β
β+) |
40 | | rpexpcl 13993 |
. . . . . 6
β’
(((logβπ)
β β+ β§ 2 β β€) β ((logβπ)β2) β
β+) |
41 | 39, 17, 40 | sylancl 587 |
. . . . 5
β’ (π β ((logβπ)β2) β
β+) |
42 | 28, 41 | rpmulcld 12980 |
. . . 4
β’ (π β (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2)) β
β+) |
43 | 13, 42 | rpmulcld 12980 |
. . 3
β’ (π β ((π β πΈ) Β· (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) β
β+) |
44 | 43 | rpred 12964 |
. 2
β’ (π β ((π β πΈ) Β· (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) β β) |
45 | 15, 16 | rpmulcld 12980 |
. . . . . . 7
β’ (π β (πΏ Β· πΈ) β
β+) |
46 | | 8re 12256 |
. . . . . . . 8
β’ 8 β
β |
47 | | 8pos 12272 |
. . . . . . . 8
β’ 0 <
8 |
48 | 46, 47 | elrpii 12925 |
. . . . . . 7
β’ 8 β
β+ |
49 | | rpdivcl 12947 |
. . . . . . 7
β’ (((πΏ Β· πΈ) β β+ β§ 8 β
β+) β ((πΏ Β· πΈ) / 8) β
β+) |
50 | 45, 48, 49 | sylancl 587 |
. . . . . 6
β’ (π β ((πΏ Β· πΈ) / 8) β
β+) |
51 | 50, 39 | rpmulcld 12980 |
. . . . 5
β’ (π β (((πΏ Β· πΈ) / 8) Β· (logβπ)) β
β+) |
52 | 13, 51 | rpmulcld 12980 |
. . . 4
β’ (π β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β
β+) |
53 | 52 | rpred 12964 |
. . 3
β’ (π β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β β) |
54 | | pntlem1.m |
. . . . . . . 8
β’ π =
((ββ((logβπ) / (logβπΎ))) + 1) |
55 | | pntlem1.n |
. . . . . . . 8
β’ π =
(ββ(((logβπ) / (logβπΎ)) / 2)) |
56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemg 26962 |
. . . . . . 7
β’ (π β (π β β β§ π β (β€β₯βπ) β§ (((logβπ) / (logβπΎ)) / 4) β€ (π β π))) |
57 | 56 | simp1d 1143 |
. . . . . 6
β’ (π β π β β) |
58 | 56 | simp2d 1144 |
. . . . . 6
β’ (π β π β (β€β₯βπ)) |
59 | | eluznn 12850 |
. . . . . 6
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
60 | 57, 58, 59 | syl2anc 585 |
. . . . 5
β’ (π β π β β) |
61 | 60 | nnred 12175 |
. . . 4
β’ (π β π β β) |
62 | 57 | nnred 12175 |
. . . 4
β’ (π β π β β) |
63 | 61, 62 | resubcld 11590 |
. . 3
β’ (π β (π β π) β β) |
64 | 53, 63 | remulcld 11192 |
. 2
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β β) |
65 | | fzfid 13885 |
. . 3
β’ (π β (1...(ββ(π / π))) β Fin) |
66 | 7 | rpred 12964 |
. . . . . 6
β’ (π β π β β) |
67 | | elfznn 13477 |
. . . . . 6
β’ (π β
(1...(ββ(π /
π))) β π β
β) |
68 | | nndivre 12201 |
. . . . . 6
β’ ((π β β β§ π β β) β (π / π) β β) |
69 | 66, 67, 68 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (1...(ββ(π / π)))) β (π / π) β β) |
70 | 35 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββ(π / π)))) β π β
β+) |
71 | 67 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(ββ(π / π)))) β π β β) |
72 | 71 | nnrpd 12962 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββ(π / π)))) β π β β+) |
73 | 70, 72 | rpdivcld 12981 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββ(π / π)))) β (π / π) β
β+) |
74 | 1 | pntrf 26927 |
. . . . . . . . . 10
β’ π
:β+βΆβ |
75 | 74 | ffvelcdmi 7039 |
. . . . . . . . 9
β’ ((π / π) β β+ β (π
β(π / π)) β β) |
76 | 73, 75 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββ(π / π)))) β (π
β(π / π)) β β) |
77 | 76, 70 | rerpdivcld 12995 |
. . . . . . 7
β’ ((π β§ π β (1...(ββ(π / π)))) β ((π
β(π / π)) / π) β β) |
78 | 77 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β (1...(ββ(π / π)))) β ((π
β(π / π)) / π) β β) |
79 | 78 | abscld 15328 |
. . . . 5
β’ ((π β§ π β (1...(ββ(π / π)))) β (absβ((π
β(π / π)) / π)) β β) |
80 | 69, 79 | resubcld 11590 |
. . . 4
β’ ((π β§ π β (1...(ββ(π / π)))) β ((π / π) β (absβ((π
β(π / π)) / π))) β β) |
81 | 72 | relogcld 25994 |
. . . 4
β’ ((π β§ π β (1...(ββ(π / π)))) β (logβπ) β β) |
82 | 80, 81 | remulcld 11192 |
. . 3
β’ ((π β§ π β (1...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
83 | 65, 82 | fsumrecl 15626 |
. 2
β’ (π β Ξ£π β (1...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
84 | 45 | rpcnd 12966 |
. . . . . . . . 9
β’ (π β (πΏ Β· πΈ) β β) |
85 | 11 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ (π β πΎ β
β+) |
86 | 85 | rpred 12964 |
. . . . . . . . . . . 12
β’ (π β πΎ β β) |
87 | 12 | simp2d 1144 |
. . . . . . . . . . . 12
β’ (π β 1 < πΎ) |
88 | 86, 87 | rplogcld 26000 |
. . . . . . . . . . 11
β’ (π β (logβπΎ) β
β+) |
89 | 39, 88 | rpdivcld 12981 |
. . . . . . . . . 10
β’ (π β ((logβπ) / (logβπΎ)) β
β+) |
90 | 89 | rpcnd 12966 |
. . . . . . . . 9
β’ (π β ((logβπ) / (logβπΎ)) β β) |
91 | | rpcnne0 12940 |
. . . . . . . . . 10
β’ (8 β
β+ β (8 β β β§ 8 β 0)) |
92 | 48, 91 | mp1i 13 |
. . . . . . . . 9
β’ (π β (8 β β β§ 8
β 0)) |
93 | | 4re 12244 |
. . . . . . . . . . 11
β’ 4 β
β |
94 | | 4pos 12267 |
. . . . . . . . . . 11
β’ 0 <
4 |
95 | 93, 94 | elrpii 12925 |
. . . . . . . . . 10
β’ 4 β
β+ |
96 | | rpcnne0 12940 |
. . . . . . . . . 10
β’ (4 β
β+ β (4 β β β§ 4 β 0)) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . 9
β’ (π β (4 β β β§ 4
β 0)) |
98 | | divmuldiv 11862 |
. . . . . . . . 9
β’ ((((πΏ Β· πΈ) β β β§ ((logβπ) / (logβπΎ)) β β) β§ ((8 β β
β§ 8 β 0) β§ (4 β β β§ 4 β 0))) β (((πΏ Β· πΈ) / 8) Β· (((logβπ) / (logβπΎ)) / 4)) = (((πΏ Β· πΈ) Β· ((logβπ) / (logβπΎ))) / (8 Β· 4))) |
99 | 84, 90, 92, 97, 98 | syl22anc 838 |
. . . . . . . 8
β’ (π β (((πΏ Β· πΈ) / 8) Β· (((logβπ) / (logβπΎ)) / 4)) = (((πΏ Β· πΈ) Β· ((logβπ) / (logβπΎ))) / (8 Β· 4))) |
100 | 10 | fveq2i 6850 |
. . . . . . . . . . . . . 14
β’
(logβπΎ) =
(logβ(expβ(π΅ /
πΈ))) |
101 | 3, 16 | rpdivcld 12981 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΅ / πΈ) β
β+) |
102 | 101 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ / πΈ) β β) |
103 | 102 | relogefd 25999 |
. . . . . . . . . . . . . 14
β’ (π β
(logβ(expβ(π΅ /
πΈ))) = (π΅ / πΈ)) |
104 | 100, 103 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ (π β (logβπΎ) = (π΅ / πΈ)) |
105 | 104 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π β ((logβπ) / (logβπΎ)) = ((logβπ) / (π΅ / πΈ))) |
106 | 39 | rpcnd 12966 |
. . . . . . . . . . . . 13
β’ (π β (logβπ) β
β) |
107 | 3 | rpcnne0d 12973 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β β β§ π΅ β 0)) |
108 | 16 | rpcnne0d 12973 |
. . . . . . . . . . . . 13
β’ (π β (πΈ β β β§ πΈ β 0)) |
109 | | divdiv2 11874 |
. . . . . . . . . . . . 13
β’
(((logβπ)
β β β§ (π΅
β β β§ π΅ β
0) β§ (πΈ β β
β§ πΈ β 0)) β
((logβπ) / (π΅ / πΈ)) = (((logβπ) Β· πΈ) / π΅)) |
110 | 106, 107,
108, 109 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β ((logβπ) / (π΅ / πΈ)) = (((logβπ) Β· πΈ) / π΅)) |
111 | 105, 110 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β ((logβπ) / (logβπΎ)) = (((logβπ) Β· πΈ) / π΅)) |
112 | 111 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β ((πΏ Β· πΈ) Β· ((logβπ) / (logβπΎ))) = ((πΏ Β· πΈ) Β· (((logβπ) Β· πΈ) / π΅))) |
113 | 16 | rpcnd 12966 |
. . . . . . . . . . . 12
β’ (π β πΈ β β) |
114 | 106, 113 | mulcld 11182 |
. . . . . . . . . . 11
β’ (π β ((logβπ) Β· πΈ) β β) |
115 | | divass 11838 |
. . . . . . . . . . 11
β’ (((πΏ Β· πΈ) β β β§ ((logβπ) Β· πΈ) β β β§ (π΅ β β β§ π΅ β 0)) β (((πΏ Β· πΈ) Β· ((logβπ) Β· πΈ)) / π΅) = ((πΏ Β· πΈ) Β· (((logβπ) Β· πΈ) / π΅))) |
116 | 84, 114, 107, 115 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (((πΏ Β· πΈ) Β· ((logβπ) Β· πΈ)) / π΅) = ((πΏ Β· πΈ) Β· (((logβπ) Β· πΈ) / π΅))) |
117 | 15 | rpcnd 12966 |
. . . . . . . . . . . . 13
β’ (π β πΏ β β) |
118 | 117, 113,
106, 113 | mul4d 11374 |
. . . . . . . . . . . 12
β’ (π β ((πΏ Β· πΈ) Β· ((logβπ) Β· πΈ)) = ((πΏ Β· (logβπ)) Β· (πΈ Β· πΈ))) |
119 | 113 | sqvald 14055 |
. . . . . . . . . . . . 13
β’ (π β (πΈβ2) = (πΈ Β· πΈ)) |
120 | 119 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π β ((πΏ Β· (logβπ)) Β· (πΈβ2)) = ((πΏ Β· (logβπ)) Β· (πΈ Β· πΈ))) |
121 | 113 | sqcld 14056 |
. . . . . . . . . . . . 13
β’ (π β (πΈβ2) β β) |
122 | 117, 106,
121 | mul32d 11372 |
. . . . . . . . . . . 12
β’ (π β ((πΏ Β· (logβπ)) Β· (πΈβ2)) = ((πΏ Β· (πΈβ2)) Β· (logβπ))) |
123 | 118, 120,
122 | 3eqtr2d 2783 |
. . . . . . . . . . 11
β’ (π β ((πΏ Β· πΈ) Β· ((logβπ) Β· πΈ)) = ((πΏ Β· (πΈβ2)) Β· (logβπ))) |
124 | 123 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β (((πΏ Β· πΈ) Β· ((logβπ) Β· πΈ)) / π΅) = (((πΏ Β· (πΈβ2)) Β· (logβπ)) / π΅)) |
125 | 112, 116,
124 | 3eqtr2d 2783 |
. . . . . . . . 9
β’ (π β ((πΏ Β· πΈ) Β· ((logβπ) / (logβπΎ))) = (((πΏ Β· (πΈβ2)) Β· (logβπ)) / π΅)) |
126 | | 8t4e32 12742 |
. . . . . . . . . 10
β’ (8
Β· 4) = ;32 |
127 | 126 | a1i 11 |
. . . . . . . . 9
β’ (π β (8 Β· 4) = ;32) |
128 | 125, 127 | oveq12d 7380 |
. . . . . . . 8
β’ (π β (((πΏ Β· πΈ) Β· ((logβπ) / (logβπΎ))) / (8 Β· 4)) = ((((πΏ Β· (πΈβ2)) Β· (logβπ)) / π΅) / ;32)) |
129 | 20 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (π β (πΏ Β· (πΈβ2)) β β) |
130 | 129, 106 | mulcld 11182 |
. . . . . . . . . 10
β’ (π β ((πΏ Β· (πΈβ2)) Β· (logβπ)) β
β) |
131 | | rpcnne0 12940 |
. . . . . . . . . . 11
β’ (;32 β β+ β
(;32 β β β§ ;32 β 0)) |
132 | 25, 131 | mp1i 13 |
. . . . . . . . . 10
β’ (π β (;32 β β β§ ;32 β 0)) |
133 | | divdiv1 11873 |
. . . . . . . . . 10
β’ ((((πΏ Β· (πΈβ2)) Β· (logβπ)) β β β§ (π΅ β β β§ π΅ β 0) β§ (;32 β β β§ ;32 β 0)) β ((((πΏ Β· (πΈβ2)) Β· (logβπ)) / π΅) / ;32) = (((πΏ Β· (πΈβ2)) Β· (logβπ)) / (π΅ Β· ;32))) |
134 | 130, 107,
132, 133 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β ((((πΏ Β· (πΈβ2)) Β· (logβπ)) / π΅) / ;32) = (((πΏ Β· (πΈβ2)) Β· (logβπ)) / (π΅ Β· ;32))) |
135 | 23 | nncni 12170 |
. . . . . . . . . . 11
β’ ;32 β β |
136 | 3 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
137 | | mulcom 11144 |
. . . . . . . . . . 11
β’ ((;32 β β β§ π΅ β β) β (;32 Β· π΅) = (π΅ Β· ;32)) |
138 | 135, 136,
137 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (;32 Β· π΅) = (π΅ Β· ;32)) |
139 | 138 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β (((πΏ Β· (πΈβ2)) Β· (logβπ)) / (;32 Β· π΅)) = (((πΏ Β· (πΈβ2)) Β· (logβπ)) / (π΅ Β· ;32))) |
140 | 27 | rpcnne0d 12973 |
. . . . . . . . . 10
β’ (π β ((;32 Β· π΅) β β β§ (;32 Β· π΅) β 0)) |
141 | | div23 11839 |
. . . . . . . . . 10
β’ (((πΏ Β· (πΈβ2)) β β β§
(logβπ) β
β β§ ((;32 Β· π΅) β β β§ (;32 Β· π΅) β 0)) β (((πΏ Β· (πΈβ2)) Β· (logβπ)) / (;32 Β· π΅)) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ))) |
142 | 129, 106,
140, 141 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (((πΏ Β· (πΈβ2)) Β· (logβπ)) / (;32 Β· π΅)) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ))) |
143 | 134, 139,
142 | 3eqtr2d 2783 |
. . . . . . . 8
β’ (π β ((((πΏ Β· (πΈβ2)) Β· (logβπ)) / π΅) / ;32) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ))) |
144 | 99, 128, 143 | 3eqtrd 2781 |
. . . . . . 7
β’ (π β (((πΏ Β· πΈ) / 8) Β· (((logβπ) / (logβπΎ)) / 4)) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ))) |
145 | 144 | oveq1d 7377 |
. . . . . 6
β’ (π β ((((πΏ Β· πΈ) / 8) Β· (((logβπ) / (logβπΎ)) / 4)) Β· (logβπ)) = ((((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ)) Β· (logβπ))) |
146 | 50 | rpcnd 12966 |
. . . . . . 7
β’ (π β ((πΏ Β· πΈ) / 8) β β) |
147 | 89 | rpred 12964 |
. . . . . . . . 9
β’ (π β ((logβπ) / (logβπΎ)) β β) |
148 | | 4nn 12243 |
. . . . . . . . 9
β’ 4 β
β |
149 | | nndivre 12201 |
. . . . . . . . 9
β’
((((logβπ) /
(logβπΎ)) β
β β§ 4 β β) β (((logβπ) / (logβπΎ)) / 4) β β) |
150 | 147, 148,
149 | sylancl 587 |
. . . . . . . 8
β’ (π β (((logβπ) / (logβπΎ)) / 4) β β) |
151 | 150 | recnd 11190 |
. . . . . . 7
β’ (π β (((logβπ) / (logβπΎ)) / 4) β β) |
152 | 146, 106,
151 | mul32d 11372 |
. . . . . 6
β’ (π β ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (((logβπ) / (logβπΎ)) / 4)) = ((((πΏ Β· πΈ) / 8) Β· (((logβπ) / (logβπΎ)) / 4)) Β· (logβπ))) |
153 | 106 | sqvald 14055 |
. . . . . . . 8
β’ (π β ((logβπ)β2) = ((logβπ) Β· (logβπ))) |
154 | 153 | oveq2d 7378 |
. . . . . . 7
β’ (π β (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2)) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ) Β· (logβπ)))) |
155 | 28 | rpcnd 12966 |
. . . . . . . 8
β’ (π β ((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) β β) |
156 | 155, 106,
106 | mulassd 11185 |
. . . . . . 7
β’ (π β ((((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ)) Β· (logβπ)) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ) Β· (logβπ)))) |
157 | 154, 156 | eqtr4d 2780 |
. . . . . 6
β’ (π β (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2)) = ((((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· (logβπ)) Β· (logβπ))) |
158 | 145, 152,
157 | 3eqtr4d 2787 |
. . . . 5
β’ (π β ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (((logβπ) / (logβπΎ)) / 4)) = (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) |
159 | 56 | simp3d 1145 |
. . . . . 6
β’ (π β (((logβπ) / (logβπΎ)) / 4) β€ (π β π)) |
160 | 150, 63, 51 | lemul2d 13008 |
. . . . . 6
β’ (π β ((((logβπ) / (logβπΎ)) / 4) β€ (π β π) β ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (((logβπ) / (logβπΎ)) / 4)) β€ ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π)))) |
161 | 159, 160 | mpbid 231 |
. . . . 5
β’ (π β ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (((logβπ) / (logβπΎ)) / 4)) β€ ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π))) |
162 | 158, 161 | eqbrtrrd 5134 |
. . . 4
β’ (π β (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2)) β€ ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π))) |
163 | 42 | rpred 12964 |
. . . . 5
β’ (π β (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2)) β β) |
164 | 51 | rpred 12964 |
. . . . . 6
β’ (π β (((πΏ Β· πΈ) / 8) Β· (logβπ)) β β) |
165 | 164, 63 | remulcld 11192 |
. . . . 5
β’ (π β ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π)) β β) |
166 | 163, 165,
13 | lemul2d 13008 |
. . . 4
β’ (π β ((((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2)) β€ ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π)) β ((π β πΈ) Β· (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) β€ ((π β πΈ) Β· ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π))))) |
167 | 162, 166 | mpbid 231 |
. . 3
β’ (π β ((π β πΈ) Β· (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) β€ ((π β πΈ) Β· ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π)))) |
168 | 13 | rpcnd 12966 |
. . . 4
β’ (π β (π β πΈ) β β) |
169 | 51 | rpcnd 12966 |
. . . 4
β’ (π β (((πΏ Β· πΈ) / 8) Β· (logβπ)) β β) |
170 | 63 | recnd 11190 |
. . . 4
β’ (π β (π β π) β β) |
171 | 168, 169,
170 | mulassd 11185 |
. . 3
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = ((π β πΈ) Β· ((((πΏ Β· πΈ) / 8) Β· (logβπ)) Β· (π β π)))) |
172 | 167, 171 | breqtrrd 5138 |
. 2
β’ (π β ((π β πΈ) Β· (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) β€ (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) |
173 | | fzfid 13885 |
. . . 4
β’ (π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β Fin) |
174 | 60 | nnzd 12533 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
175 | 85, 174 | rpexpcld 14157 |
. . . . . . . . . . 11
β’ (π β (πΎβπ) β
β+) |
176 | 35, 175 | rpdivcld 12981 |
. . . . . . . . . 10
β’ (π β (π / (πΎβπ)) β
β+) |
177 | 176 | rprege0d 12971 |
. . . . . . . . 9
β’ (π β ((π / (πΎβπ)) β β β§ 0 β€ (π / (πΎβπ)))) |
178 | | flge0nn0 13732 |
. . . . . . . . 9
β’ (((π / (πΎβπ)) β β β§ 0 β€ (π / (πΎβπ))) β (ββ(π / (πΎβπ))) β
β0) |
179 | | nn0p1nn 12459 |
. . . . . . . . 9
β’
((ββ(π /
(πΎβπ))) β β0 β
((ββ(π / (πΎβπ))) + 1) β β) |
180 | 177, 178,
179 | 3syl 18 |
. . . . . . . 8
β’ (π β ((ββ(π / (πΎβπ))) + 1) β β) |
181 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
182 | 180, 181 | eleqtrdi 2848 |
. . . . . . 7
β’ (π β ((ββ(π / (πΎβπ))) + 1) β
(β€β₯β1)) |
183 | | fzss1 13487 |
. . . . . . 7
β’
(((ββ(π
/ (πΎβπ))) + 1) β
(β€β₯β1) β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
184 | 182, 183 | syl 17 |
. . . . . 6
β’ (π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
185 | 184 | sselda 3949 |
. . . . 5
β’ ((π β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β π β (1...(ββ(π / π)))) |
186 | 185, 82 | syldan 592 |
. . . 4
β’ ((π β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
187 | 173, 186 | fsumrecl 15626 |
. . 3
β’ (π β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
188 | | eluzfz2 13456 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
189 | 58, 188 | syl 17 |
. . . 4
β’ (π β π β (π...π)) |
190 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
191 | 190 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) |
192 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (πΎβπ) = (πΎβπ)) |
193 | 192 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (π / (πΎβπ)) = (π / (πΎβπ))) |
194 | 193 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β (ββ(π / (πΎβπ))) = (ββ(π / (πΎβπ)))) |
195 | 194 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = π β ((ββ(π / (πΎβπ))) + 1) = ((ββ(π / (πΎβπ))) + 1)) |
196 | 195 | oveq1d 7377 |
. . . . . . . 8
β’ (π = π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) = (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) |
197 | 196 | sumeq1d 15593 |
. . . . . . 7
β’ (π = π β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) = Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
198 | 191, 197 | breq12d 5123 |
. . . . . 6
β’ (π = π β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
199 | 198 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
200 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
201 | 200 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) |
202 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (πΎβπ) = (πΎβπ)) |
203 | 202 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (π / (πΎβπ)) = (π / (πΎβπ))) |
204 | 203 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β (ββ(π / (πΎβπ))) = (ββ(π / (πΎβπ)))) |
205 | 204 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = π β ((ββ(π / (πΎβπ))) + 1) = ((ββ(π / (πΎβπ))) + 1)) |
206 | 205 | oveq1d 7377 |
. . . . . . . 8
β’ (π = π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) = (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) |
207 | 206 | sumeq1d 15593 |
. . . . . . 7
β’ (π = π β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) = Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
208 | 201, 207 | breq12d 5123 |
. . . . . 6
β’ (π = π β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
209 | 208 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
210 | | oveq1 7369 |
. . . . . . . 8
β’ (π = (π + 1) β (π β π) = ((π + 1) β π)) |
211 | 210 | oveq2d 7378 |
. . . . . . 7
β’ (π = (π + 1) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π))) |
212 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (πΎβπ) = (πΎβ(π + 1))) |
213 | 212 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (π / (πΎβπ)) = (π / (πΎβ(π + 1)))) |
214 | 213 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = (π + 1) β (ββ(π / (πΎβπ))) = (ββ(π / (πΎβ(π + 1))))) |
215 | 214 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = (π + 1) β ((ββ(π / (πΎβπ))) + 1) = ((ββ(π / (πΎβ(π + 1)))) + 1)) |
216 | 215 | oveq1d 7377 |
. . . . . . . 8
β’ (π = (π + 1) β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) = (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))) |
217 | 216 | sumeq1d 15593 |
. . . . . . 7
β’ (π = (π + 1) β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) = Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
218 | 211, 217 | breq12d 5123 |
. . . . . 6
β’ (π = (π + 1) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
219 | 218 | imbi2d 341 |
. . . . 5
β’ (π = (π + 1) β ((π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
220 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
221 | 220 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) |
222 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (πΎβπ) = (πΎβπ)) |
223 | 222 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (π / (πΎβπ)) = (π / (πΎβπ))) |
224 | 223 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β (ββ(π / (πΎβπ))) = (ββ(π / (πΎβπ)))) |
225 | 224 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = π β ((ββ(π / (πΎβπ))) + 1) = ((ββ(π / (πΎβπ))) + 1)) |
226 | 225 | oveq1d 7377 |
. . . . . . . 8
β’ (π = π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) = (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) |
227 | 226 | sumeq1d 15593 |
. . . . . . 7
β’ (π = π β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) = Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
228 | 221, 227 | breq12d 5123 |
. . . . . 6
β’ (π = π β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
229 | 228 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
230 | 57 | nncnd 12176 |
. . . . . . . . . 10
β’ (π β π β β) |
231 | 230 | subidd 11507 |
. . . . . . . . 9
β’ (π β (π β π) = 0) |
232 | 231 | oveq2d 7378 |
. . . . . . . 8
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· 0)) |
233 | 52 | rpcnd 12966 |
. . . . . . . . 9
β’ (π β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β β) |
234 | 233 | mul01d 11361 |
. . . . . . . 8
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· 0) = 0) |
235 | 232, 234 | eqtrd 2777 |
. . . . . . 7
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) = 0) |
236 | | fzfid 13885 |
. . . . . . . 8
β’ (π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β Fin) |
237 | 57 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β€) |
238 | 85, 237 | rpexpcld 14157 |
. . . . . . . . . . . . . . 15
β’ (π β (πΎβπ) β
β+) |
239 | 35, 238 | rpdivcld 12981 |
. . . . . . . . . . . . . 14
β’ (π β (π / (πΎβπ)) β
β+) |
240 | 239 | rprege0d 12971 |
. . . . . . . . . . . . 13
β’ (π β ((π / (πΎβπ)) β β β§ 0 β€ (π / (πΎβπ)))) |
241 | | flge0nn0 13732 |
. . . . . . . . . . . . 13
β’ (((π / (πΎβπ)) β β β§ 0 β€ (π / (πΎβπ))) β (ββ(π / (πΎβπ))) β
β0) |
242 | | nn0p1nn 12459 |
. . . . . . . . . . . . 13
β’
((ββ(π /
(πΎβπ))) β β0 β
((ββ(π / (πΎβπ))) + 1) β β) |
243 | 240, 241,
242 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β ((ββ(π / (πΎβπ))) + 1) β β) |
244 | 243, 181 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ (π β ((ββ(π / (πΎβπ))) + 1) β
(β€β₯β1)) |
245 | | fzss1 13487 |
. . . . . . . . . . 11
β’
(((ββ(π
/ (πΎβπ))) + 1) β
(β€β₯β1) β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
246 | 244, 245 | syl 17 |
. . . . . . . . . 10
β’ (π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
247 | 246 | sselda 3949 |
. . . . . . . . 9
β’ ((π β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β π β (1...(ββ(π / π)))) |
248 | 247, 82 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
249 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π β
(1...(ββ(π /
π))) β π β€ (ββ(π / π))) |
250 | 249 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(ββ(π / π)))) β π β€ (ββ(π / π))) |
251 | 29 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β+) |
252 | 35, 251 | rpdivcld 12981 |
. . . . . . . . . . . . . 14
β’ (π β (π / π) β
β+) |
253 | 252 | rpred 12964 |
. . . . . . . . . . . . 13
β’ (π β (π / π) β β) |
254 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β
(1...(ββ(π /
π))) β π β
β€) |
255 | | flge 13717 |
. . . . . . . . . . . . 13
β’ (((π / π) β β β§ π β β€) β (π β€ (π / π) β π β€ (ββ(π / π)))) |
256 | 253, 254,
255 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(ββ(π / π)))) β (π β€ (π / π) β π β€ (ββ(π / π)))) |
257 | 250, 256 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(ββ(π / π)))) β π β€ (π / π)) |
258 | 71, 257 | jca 513 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββ(π / π)))) β (π β β β§ π β€ (π / π))) |
259 | | pntlem1.U |
. . . . . . . . . . 11
β’ (π β βπ§ β (π[,)+β)(absβ((π
βπ§) / π§)) β€ π) |
260 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259 | pntlemn 26964 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§ π β€ (π / π))) β 0 β€ (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
261 | 258, 260 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββ(π / π)))) β 0 β€ (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
262 | 247, 261 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β 0 β€ (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
263 | 236, 248,
262 | fsumge0 15687 |
. . . . . . 7
β’ (π β 0 β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
264 | 235, 263 | eqbrtrd 5132 |
. . . . . 6
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
265 | 264 | a1i 11 |
. . . . 5
β’ (π β
(β€β₯βπ) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
266 | | pntlem1.K |
. . . . . . . . . 10
β’ (π β βπ¦ β (π(,)+β)βπ§ β β+ ((π¦ < π§ β§ ((1 + (πΏ Β· πΈ)) Β· π§) < (πΎ Β· π¦)) β§ βπ’ β (π§[,]((1 + (πΏ Β· πΈ)) Β· π§))(absβ((π
βπ’) / π’)) β€ πΈ)) |
267 | | eqid 2737 |
. . . . . . . . . 10
β’
(((ββ(π
/ (πΎβ(π + 1)))) +
1)...(ββ(π /
(πΎβπ)))) = (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) |
268 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55, 259, 266, 267 | pntlemi 26968 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
269 | 52 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β
β+) |
270 | 269 | rpred 12964 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β β) |
271 | | elfzoelz 13579 |
. . . . . . . . . . . . . 14
β’ (π β (π..^π) β π β β€) |
272 | 271 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β π β β€) |
273 | 272 | zred 12614 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β π β β) |
274 | 57 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β π β β) |
275 | 274 | nnred 12175 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β π β β) |
276 | 273, 275 | resubcld 11590 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π β π) β β) |
277 | 270, 276 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β β) |
278 | | fzfid 13885 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) β Fin) |
279 | | ssun1 4137 |
. . . . . . . . . . . . . . 15
β’
(((ββ(π
/ (πΎβ(π + 1)))) +
1)...(ββ(π /
(πΎβπ)))) β ((((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) βͺ (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) |
280 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β π β β) |
281 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β πΎ β
β+) |
282 | 272 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β (π + 1) β β€) |
283 | 281, 282 | rpexpcld 14157 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β (πΎβ(π + 1)) β
β+) |
284 | 280, 283 | rerpdivcld 12995 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π..^π)) β (π / (πΎβ(π + 1))) β β) |
285 | 281, 272 | rpexpcld 14157 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β (πΎβπ) β
β+) |
286 | 280, 285 | rerpdivcld 12995 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π..^π)) β (π / (πΎβπ)) β β) |
287 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β πΎ β β) |
288 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 β
β |
289 | | ltle 11250 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1
β β β§ πΎ
β β) β (1 < πΎ β 1 β€ πΎ)) |
290 | 288, 86, 289 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1 < πΎ β 1 β€ πΎ)) |
291 | 87, 290 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1 β€ πΎ) |
292 | 291 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β 1 β€ πΎ) |
293 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β€ β π β
(β€β₯βπ)) |
294 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
295 | 272, 293,
294 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β (π + 1) β
(β€β₯βπ)) |
296 | 287, 292,
295 | leexp2ad 14164 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β (πΎβπ) β€ (πΎβ(π + 1))) |
297 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β π β
β+) |
298 | 285, 283,
297 | lediv2d 12988 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β ((πΎβπ) β€ (πΎβ(π + 1)) β (π / (πΎβ(π + 1))) β€ (π / (πΎβπ)))) |
299 | 296, 298 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π..^π)) β (π / (πΎβ(π + 1))) β€ (π / (πΎβπ))) |
300 | | flword2 13725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π / (πΎβ(π + 1))) β β β§ (π / (πΎβπ)) β β β§ (π / (πΎβ(π + 1))) β€ (π / (πΎβπ))) β (ββ(π / (πΎβπ))) β
(β€β₯β(ββ(π / (πΎβ(π + 1)))))) |
301 | 284, 286,
299, 300 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π..^π)) β (ββ(π / (πΎβπ))) β
(β€β₯β(ββ(π / (πΎβ(π + 1)))))) |
302 | | eluzp1p1 12798 |
. . . . . . . . . . . . . . . . 17
β’
((ββ(π /
(πΎβπ))) β
(β€β₯β(ββ(π / (πΎβ(π + 1))))) β ((ββ(π / (πΎβπ))) + 1) β
(β€β₯β((ββ(π / (πΎβ(π + 1)))) + 1))) |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β ((ββ(π / (πΎβπ))) + 1) β
(β€β₯β((ββ(π / (πΎβ(π + 1)))) + 1))) |
304 | 286 | flcld 13710 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π..^π)) β (ββ(π / (πΎβπ))) β β€) |
305 | 252 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β (π / π) β
β+) |
306 | 305 | rpred 12964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π..^π)) β (π / π) β β) |
307 | 306 | flcld 13710 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π..^π)) β (ββ(π / π)) β β€) |
308 | 251 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π..^π)) β π β
β+) |
309 | 308 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β π β β) |
310 | 285 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β (πΎβπ) β β) |
311 | 30 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β
β+) |
312 | 311 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β) |
313 | 312 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π..^π)) β π β β) |
314 | 30 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π < π) |
315 | 314 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π..^π)) β π < π) |
316 | | elfzofz 13595 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π..^π) β π β (π...π)) |
317 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
29, 30, 31, 32, 33, 54, 55 | pntlemh 26963 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (π...π)) β (π < (πΎβπ) β§ (πΎβπ) β€ (ββπ))) |
318 | 316, 317 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (π..^π)) β (π < (πΎβπ) β§ (πΎβπ) β€ (ββπ))) |
319 | 318 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π..^π)) β π < (πΎβπ)) |
320 | 309, 313,
310, 315, 319 | lttrd 11323 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π..^π)) β π < (πΎβπ)) |
321 | 309, 310,
320 | ltled 11310 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β π β€ (πΎβπ)) |
322 | 308, 285,
297 | lediv2d 12988 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π..^π)) β (π β€ (πΎβπ) β (π / (πΎβπ)) β€ (π / π))) |
323 | 321, 322 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π..^π)) β (π / (πΎβπ)) β€ (π / π)) |
324 | | flwordi 13724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π / (πΎβπ)) β β β§ (π / π) β β β§ (π / (πΎβπ)) β€ (π / π)) β (ββ(π / (πΎβπ))) β€ (ββ(π / π))) |
325 | 286, 306,
323, 324 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π..^π)) β (ββ(π / (πΎβπ))) β€ (ββ(π / π))) |
326 | | eluz2 12776 |
. . . . . . . . . . . . . . . . 17
β’
((ββ(π /
π)) β
(β€β₯β(ββ(π / (πΎβπ)))) β ((ββ(π / (πΎβπ))) β β€ β§
(ββ(π / π)) β β€ β§
(ββ(π / (πΎβπ))) β€ (ββ(π / π)))) |
327 | 304, 307,
325, 326 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β (ββ(π / π)) β
(β€β₯β(ββ(π / (πΎβπ))))) |
328 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . 16
β’
((((ββ(π
/ (πΎβπ))) + 1) β
(β€β₯β((ββ(π / (πΎβ(π + 1)))) + 1)) β§ (ββ(π / π)) β
(β€β₯β(ββ(π / (πΎβπ))))) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π))) = ((((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) βͺ (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))))) |
329 | 303, 327,
328 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π))) = ((((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) βͺ (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))))) |
330 | 279, 329 | sseqtrrid 4002 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))) |
331 | 297, 283 | rpdivcld 12981 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π..^π)) β (π / (πΎβ(π + 1))) β
β+) |
332 | 331 | rprege0d 12971 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π..^π)) β ((π / (πΎβ(π + 1))) β β β§ 0 β€ (π / (πΎβ(π + 1))))) |
333 | | flge0nn0 13732 |
. . . . . . . . . . . . . . . . 17
β’ (((π / (πΎβ(π + 1))) β β β§ 0 β€ (π / (πΎβ(π + 1)))) β (ββ(π / (πΎβ(π + 1)))) β
β0) |
334 | | nn0p1nn 12459 |
. . . . . . . . . . . . . . . . 17
β’
((ββ(π /
(πΎβ(π + 1)))) β β0 β
((ββ(π / (πΎβ(π + 1)))) + 1) β
β) |
335 | 332, 333,
334 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β ((ββ(π / (πΎβ(π + 1)))) + 1) β
β) |
336 | 335, 181 | eleqtrdi 2848 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π..^π)) β ((ββ(π / (πΎβ(π + 1)))) + 1) β
(β€β₯β1)) |
337 | | fzss1 13487 |
. . . . . . . . . . . . . . 15
β’
(((ββ(π
/ (πΎβ(π + 1)))) + 1) β
(β€β₯β1) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
338 | 336, 337 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
339 | 330, 338 | sstrd 3959 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) β (1...(ββ(π / π)))) |
340 | 339 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))) β π β (1...(ββ(π / π)))) |
341 | 82 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π β (1...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
342 | 340, 341 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
343 | 278, 342 | fsumrecl 15626 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
344 | | fzfid 13885 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β Fin) |
345 | | ssun2 4138 |
. . . . . . . . . . . . . . 15
β’
(((ββ(π
/ (πΎβπ))) + 1)...(ββ(π / π))) β ((((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) βͺ (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) |
346 | 345, 329 | sseqtrrid 4002 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))) |
347 | 346, 338 | sstrd 3959 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π))) β (1...(ββ(π / π)))) |
348 | 347 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β π β (1...(ββ(π / π)))) |
349 | 348, 341 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
350 | 344, 349 | fsumrecl 15626 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
351 | | le2add 11644 |
. . . . . . . . . 10
β’
(((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β β β§ (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β β) β§ (Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β β§ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β)) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β§ (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) β€ (Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) + Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
352 | 270, 277,
343, 350, 351 | syl22anc 838 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β§ (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) β€ (Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) + Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
353 | 268, 352 | mpand 694 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) β€ (Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) + Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
354 | 233 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) β β) |
355 | | 1cnd 11157 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β 1 β β) |
356 | 272 | zcnd 12615 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β π β β) |
357 | 230 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β π β β) |
358 | 356, 357 | subcld 11519 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π β π) β β) |
359 | 354, 355,
358 | adddid 11186 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (1 + (π β π))) = ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· 1) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)))) |
360 | 355, 358 | addcomd 11364 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (1 + (π β π)) = ((π β π) + 1)) |
361 | 356, 355,
357 | addsubd 11540 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β ((π + 1) β π) = ((π β π) + 1)) |
362 | 360, 361 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (1 + (π β π)) = ((π + 1) β π)) |
363 | 362 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (1 + (π β π))) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π))) |
364 | 354 | mulid1d 11179 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· 1) = ((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ)))) |
365 | 364 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· 1) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)))) |
366 | 359, 363,
365 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) = (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)))) |
367 | | reflcl 13708 |
. . . . . . . . . . . . 13
β’ ((π / (πΎβπ)) β β β
(ββ(π / (πΎβπ))) β β) |
368 | 286, 367 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (ββ(π / (πΎβπ))) β β) |
369 | 368 | ltp1d 12092 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (ββ(π / (πΎβπ))) < ((ββ(π / (πΎβπ))) + 1)) |
370 | | fzdisj 13475 |
. . . . . . . . . . 11
β’
((ββ(π /
(πΎβπ))) < ((ββ(π / (πΎβπ))) + 1) β ((((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) β© (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) = β
) |
371 | 369, 370 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β ((((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ)))) β© (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))) = β
) |
372 | | fzfid 13885 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π))) β Fin) |
373 | 338 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))) β π β (1...(ββ(π / π)))) |
374 | 373, 341 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
375 | 374 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π β (π..^π)) β§ π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))) β (((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β β) |
376 | 371, 329,
372, 375 | fsumsplit 15633 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) = (Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) + Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
377 | 366, 376 | breq12d 5123 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) + (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π))) β€ (Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / (πΎβπ))))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) + Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
378 | 353, 377 | sylibrd 259 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
379 | 378 | expcom 415 |
. . . . . 6
β’ (π β (π..^π) β (π β ((((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
380 | 379 | a2d 29 |
. . . . 5
β’ (π β (π..^π) β ((π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· ((π + 1) β π)) β€ Ξ£π β (((ββ(π / (πΎβ(π + 1)))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))))) |
381 | 199, 209,
219, 229, 265, 380 | fzind2 13697 |
. . . 4
β’ (π β (π...π) β (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)))) |
382 | 189, 381 | mpcom 38 |
. . 3
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
383 | 65, 82, 261, 184 | fsumless 15688 |
. . 3
β’ (π β Ξ£π β (((ββ(π / (πΎβπ))) + 1)...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ)) β€ Ξ£π β (1...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
384 | 64, 187, 83, 382, 383 | letrd 11319 |
. 2
β’ (π β (((π β πΈ) Β· (((πΏ Β· πΈ) / 8) Β· (logβπ))) Β· (π β π)) β€ Ξ£π β (1...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |
385 | 44, 64, 83, 172, 384 | letrd 11319 |
1
β’ (π β ((π β πΈ) Β· (((πΏ Β· (πΈβ2)) / (;32 Β· π΅)) Β· ((logβπ)β2))) β€ Ξ£π β (1...(ββ(π / π)))(((π / π) β (absβ((π
β(π / π)) / π))) Β· (logβπ))) |