Step | Hyp | Ref
| Expression |
1 | | fzfid 13938 |
. . . . . 6
β’ (π β (1...(ββπ΄)) β Fin) |
2 | | mulog2sumlem1.2 |
. . . . . . . . 9
β’ (π β π΄ β
β+) |
3 | | elfznn 13530 |
. . . . . . . . . 10
β’ (π β
(1...(ββπ΄))
β π β
β) |
4 | 3 | nnrpd 13014 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β π β
β+) |
5 | | rpdivcl 12999 |
. . . . . . . . 9
β’ ((π΄ β β+
β§ π β
β+) β (π΄ / π) β
β+) |
6 | 2, 4, 5 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (π΄ / π) β
β+) |
7 | 6 | relogcld 26131 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (logβ(π΄ / π)) β β) |
8 | 3 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
9 | 7, 8 | nndivred 12266 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((logβ(π΄ / π)) / π) β β) |
10 | 1, 9 | fsumrecl 15680 |
. . . . 5
β’ (π β Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) β β) |
11 | 2 | relogcld 26131 |
. . . . . . . 8
β’ (π β (logβπ΄) β
β) |
12 | 11 | resqcld 14090 |
. . . . . . 7
β’ (π β ((logβπ΄)β2) β
β) |
13 | 12 | rehalfcld 12459 |
. . . . . 6
β’ (π β (((logβπ΄)β2) / 2) β
β) |
14 | | emre 26510 |
. . . . . . . 8
β’ Ξ³
β β |
15 | | remulcl 11195 |
. . . . . . . 8
β’ ((Ξ³
β β β§ (logβπ΄) β β) β (Ξ³ Β·
(logβπ΄)) β
β) |
16 | 14, 11, 15 | sylancr 588 |
. . . . . . 7
β’ (π β (Ξ³ Β·
(logβπ΄)) β
β) |
17 | | rpsup 13831 |
. . . . . . . . 9
β’
sup(β+, β*, < ) =
+β |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ (π β sup(β+,
β*, < ) = +β) |
19 | | logdivsum.1 |
. . . . . . . . . . . . 13
β’ πΉ = (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))((logβπ) / π) β (((logβπ¦)β2) / 2))) |
20 | 19 | logdivsum 27036 |
. . . . . . . . . . . 12
β’ (πΉ:β+βΆβ β§
πΉ β dom
βπ β§ ((πΉ βπ πΏ β§ π΄ β β+ β§ e β€
π΄) β
(absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄))) |
21 | 20 | simp1i 1140 |
. . . . . . . . . . 11
β’ πΉ:β+βΆβ |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ (π β πΉ:β+βΆβ) |
23 | 22 | feqmptd 6961 |
. . . . . . . . 9
β’ (π β πΉ = (π₯ β β+ β¦ (πΉβπ₯))) |
24 | | mulog2sumlem.1 |
. . . . . . . . 9
β’ (π β πΉ βπ πΏ) |
25 | 23, 24 | eqbrtrrd 5173 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ (πΉβπ₯)) βπ πΏ) |
26 | 21 | ffvelcdmi 7086 |
. . . . . . . . 9
β’ (π₯ β β+
β (πΉβπ₯) β
β) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (πΉβπ₯) β β) |
28 | 18, 25, 27 | rlimrecl 15524 |
. . . . . . 7
β’ (π β πΏ β β) |
29 | 16, 28 | resubcld 11642 |
. . . . . 6
β’ (π β ((Ξ³ Β·
(logβπ΄)) β
πΏ) β
β) |
30 | 13, 29 | readdcld 11243 |
. . . . 5
β’ (π β ((((logβπ΄)β2) / 2) + ((Ξ³
Β· (logβπ΄))
β πΏ)) β
β) |
31 | 10, 30 | resubcld 11642 |
. . . 4
β’ (π β (Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ))) β
β) |
32 | 31 | recnd 11242 |
. . 3
β’ (π β (Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ))) β
β) |
33 | 32 | abscld 15383 |
. 2
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ)))) β
β) |
34 | | rerpdivcl 13004 |
. . . . . . . 8
β’
(((logβπ΄)
β β β§ π
β β+) β ((logβπ΄) / π) β β) |
35 | 11, 4, 34 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β ((logβπ΄) / π) β β) |
36 | 35 | recnd 11242 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((logβπ΄) / π) β β) |
37 | 1, 36 | fsumcl 15679 |
. . . . 5
β’ (π β Ξ£π β (1...(ββπ΄))((logβπ΄) / π) β β) |
38 | 11 | recnd 11242 |
. . . . . 6
β’ (π β (logβπ΄) β
β) |
39 | | readdcl 11193 |
. . . . . . . 8
β’
(((logβπ΄)
β β β§ Ξ³ β β) β ((logβπ΄) + Ξ³) β
β) |
40 | 11, 14, 39 | sylancl 587 |
. . . . . . 7
β’ (π β ((logβπ΄) + Ξ³) β
β) |
41 | 40 | recnd 11242 |
. . . . . 6
β’ (π β ((logβπ΄) + Ξ³) β
β) |
42 | 38, 41 | mulcld 11234 |
. . . . 5
β’ (π β ((logβπ΄) Β· ((logβπ΄) + Ξ³)) β
β) |
43 | 37, 42 | subcld 11571 |
. . . 4
β’ (π β (Ξ£π β (1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) β
β) |
44 | 43 | abscld 15383 |
. . 3
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) β
β) |
45 | 8 | nnrpd 13014 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β π β β+) |
46 | 45 | relogcld 26131 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (logβπ) β β) |
47 | 46, 8 | nndivred 12266 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β ((logβπ) / π) β β) |
48 | 47 | recnd 11242 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((logβπ) / π) β β) |
49 | 1, 48 | fsumcl 15679 |
. . . . 5
β’ (π β Ξ£π β (1...(ββπ΄))((logβπ) / π) β β) |
50 | 13 | recnd 11242 |
. . . . . 6
β’ (π β (((logβπ΄)β2) / 2) β
β) |
51 | 28 | recnd 11242 |
. . . . . 6
β’ (π β πΏ β β) |
52 | 50, 51 | addcld 11233 |
. . . . 5
β’ (π β ((((logβπ΄)β2) / 2) + πΏ) β
β) |
53 | 49, 52 | subcld 11571 |
. . . 4
β’ (π β (Ξ£π β (1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)) β β) |
54 | 53 | abscld 15383 |
. . 3
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))) β β) |
55 | 44, 54 | readdcld 11243 |
. 2
β’ (π β ((absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) + (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) β β) |
56 | | 2re 12286 |
. . 3
β’ 2 β
β |
57 | 11, 2 | rerpdivcld 13047 |
. . 3
β’ (π β ((logβπ΄) / π΄) β β) |
58 | | remulcl 11195 |
. . 3
β’ ((2
β β β§ ((logβπ΄) / π΄) β β) β (2 Β·
((logβπ΄) / π΄)) β
β) |
59 | 56, 57, 58 | sylancr 588 |
. 2
β’ (π β (2 Β·
((logβπ΄) / π΄)) β
β) |
60 | | relogdiv 26101 |
. . . . . . . . . . 11
β’ ((π΄ β β+
β§ π β
β+) β (logβ(π΄ / π)) = ((logβπ΄) β (logβπ))) |
61 | 2, 4, 60 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β (logβ(π΄ / π)) = ((logβπ΄) β (logβπ))) |
62 | 61 | oveq1d 7424 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β ((logβ(π΄ / π)) / π) = (((logβπ΄) β (logβπ)) / π)) |
63 | 38 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β (logβπ΄) β β) |
64 | 46 | recnd 11242 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β (logβπ) β β) |
65 | 45 | rpcnne0d 13025 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β (π β β β§ π β 0)) |
66 | | divsubdir 11908 |
. . . . . . . . . 10
β’
(((logβπ΄)
β β β§ (logβπ) β β β§ (π β β β§ π β 0)) β (((logβπ΄) β (logβπ)) / π) = (((logβπ΄) / π) β ((logβπ) / π))) |
67 | 63, 64, 65, 66 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β (((logβπ΄) β (logβπ)) / π) = (((logβπ΄) / π) β ((logβπ) / π))) |
68 | 62, 67 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β ((logβ(π΄ / π)) / π) = (((logβπ΄) / π) β ((logβπ) / π))) |
69 | 68 | sumeq2dv 15649 |
. . . . . . 7
β’ (π β Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) = Ξ£π β (1...(ββπ΄))(((logβπ΄) / π) β ((logβπ) / π))) |
70 | 1, 36, 48 | fsumsub 15734 |
. . . . . . 7
β’ (π β Ξ£π β (1...(ββπ΄))(((logβπ΄) / π) β ((logβπ) / π)) = (Ξ£π β (1...(ββπ΄))((logβπ΄) / π) β Ξ£π β (1...(ββπ΄))((logβπ) / π))) |
71 | 69, 70 | eqtrd 2773 |
. . . . . 6
β’ (π β Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) = (Ξ£π β (1...(ββπ΄))((logβπ΄) / π) β Ξ£π β (1...(ββπ΄))((logβπ) / π))) |
72 | | remulcl 11195 |
. . . . . . . . . . . . 13
β’
(((logβπ΄)
β β β§ Ξ³ β β) β ((logβπ΄) Β· Ξ³) β
β) |
73 | 11, 14, 72 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β ((logβπ΄) Β· Ξ³) β
β) |
74 | 13, 73 | readdcld 11243 |
. . . . . . . . . . 11
β’ (π β ((((logβπ΄)β2) / 2) +
((logβπ΄) Β·
Ξ³)) β β) |
75 | 74 | recnd 11242 |
. . . . . . . . . 10
β’ (π β ((((logβπ΄)β2) / 2) +
((logβπ΄) Β·
Ξ³)) β β) |
76 | 75, 50 | pncand 11572 |
. . . . . . . . 9
β’ (π β ((((((logβπ΄)β2) / 2) +
((logβπ΄) Β·
Ξ³)) + (((logβπ΄)β2) / 2)) β (((logβπ΄)β2) / 2)) =
((((logβπ΄)β2) /
2) + ((logβπ΄)
Β· Ξ³))) |
77 | 14 | recni 11228 |
. . . . . . . . . . . . 13
β’ Ξ³
β β |
78 | 77 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Ξ³ β
β) |
79 | 38, 38, 78 | adddid 11238 |
. . . . . . . . . . 11
β’ (π β ((logβπ΄) Β· ((logβπ΄) + Ξ³)) =
(((logβπ΄) Β·
(logβπ΄)) +
((logβπ΄) Β·
Ξ³))) |
80 | 12 | recnd 11242 |
. . . . . . . . . . . . . 14
β’ (π β ((logβπ΄)β2) β
β) |
81 | 80 | 2halvesd 12458 |
. . . . . . . . . . . . 13
β’ (π β ((((logβπ΄)β2) / 2) +
(((logβπ΄)β2) /
2)) = ((logβπ΄)β2)) |
82 | 38 | sqvald 14108 |
. . . . . . . . . . . . 13
β’ (π β ((logβπ΄)β2) = ((logβπ΄) Β· (logβπ΄))) |
83 | 81, 82 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β ((((logβπ΄)β2) / 2) +
(((logβπ΄)β2) /
2)) = ((logβπ΄)
Β· (logβπ΄))) |
84 | 83 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (π β (((((logβπ΄)β2) / 2) +
(((logβπ΄)β2) /
2)) + ((logβπ΄)
Β· Ξ³)) = (((logβπ΄) Β· (logβπ΄)) + ((logβπ΄) Β· Ξ³))) |
85 | 73 | recnd 11242 |
. . . . . . . . . . . 12
β’ (π β ((logβπ΄) Β· Ξ³) β
β) |
86 | 50, 50, 85 | add32d 11441 |
. . . . . . . . . . 11
β’ (π β (((((logβπ΄)β2) / 2) +
(((logβπ΄)β2) /
2)) + ((logβπ΄)
Β· Ξ³)) = (((((logβπ΄)β2) / 2) + ((logβπ΄) Β· Ξ³)) +
(((logβπ΄)β2) /
2))) |
87 | 79, 84, 86 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ (π β ((logβπ΄) Β· ((logβπ΄) + Ξ³)) =
(((((logβπ΄)β2) /
2) + ((logβπ΄)
Β· Ξ³)) + (((logβπ΄)β2) / 2))) |
88 | 87 | oveq1d 7424 |
. . . . . . . . 9
β’ (π β (((logβπ΄) Β· ((logβπ΄) + Ξ³)) β
(((logβπ΄)β2) /
2)) = ((((((logβπ΄)β2) / 2) + ((logβπ΄) Β· Ξ³)) +
(((logβπ΄)β2) /
2)) β (((logβπ΄)β2) / 2))) |
89 | | mulcom 11196 |
. . . . . . . . . . 11
β’ ((Ξ³
β β β§ (logβπ΄) β β) β (Ξ³ Β·
(logβπ΄)) =
((logβπ΄) Β·
Ξ³)) |
90 | 77, 38, 89 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (Ξ³ Β·
(logβπ΄)) =
((logβπ΄) Β·
Ξ³)) |
91 | 90 | oveq2d 7425 |
. . . . . . . . 9
β’ (π β ((((logβπ΄)β2) / 2) + (Ξ³
Β· (logβπ΄))) =
((((logβπ΄)β2) /
2) + ((logβπ΄)
Β· Ξ³))) |
92 | 76, 88, 91 | 3eqtr4rd 2784 |
. . . . . . . 8
β’ (π β ((((logβπ΄)β2) / 2) + (Ξ³
Β· (logβπ΄))) =
(((logβπ΄) Β·
((logβπ΄) + Ξ³))
β (((logβπ΄)β2) / 2))) |
93 | 92 | oveq1d 7424 |
. . . . . . 7
β’ (π β (((((logβπ΄)β2) / 2) + (Ξ³
Β· (logβπ΄)))
β πΏ) =
((((logβπ΄) Β·
((logβπ΄) + Ξ³))
β (((logβπ΄)β2) / 2)) β πΏ)) |
94 | 90, 85 | eqeltrd 2834 |
. . . . . . . 8
β’ (π β (Ξ³ Β·
(logβπ΄)) β
β) |
95 | 50, 94, 51 | addsubassd 11591 |
. . . . . . 7
β’ (π β (((((logβπ΄)β2) / 2) + (Ξ³
Β· (logβπ΄)))
β πΏ) =
((((logβπ΄)β2) /
2) + ((Ξ³ Β· (logβπ΄)) β πΏ))) |
96 | 42, 50, 51 | subsub4d 11602 |
. . . . . . 7
β’ (π β ((((logβπ΄) Β· ((logβπ΄) + Ξ³)) β
(((logβπ΄)β2) /
2)) β πΏ) =
(((logβπ΄) Β·
((logβπ΄) + Ξ³))
β ((((logβπ΄)β2) / 2) + πΏ))) |
97 | 93, 95, 96 | 3eqtr3d 2781 |
. . . . . 6
β’ (π β ((((logβπ΄)β2) / 2) + ((Ξ³
Β· (logβπ΄))
β πΏ)) =
(((logβπ΄) Β·
((logβπ΄) + Ξ³))
β ((((logβπ΄)β2) / 2) + πΏ))) |
98 | 71, 97 | oveq12d 7427 |
. . . . 5
β’ (π β (Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ))) = ((Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β Ξ£π β (1...(ββπ΄))((logβπ) / π)) β (((logβπ΄) Β· ((logβπ΄) + Ξ³)) β ((((logβπ΄)β2) / 2) + πΏ)))) |
99 | 37, 49, 42, 52 | sub4d 11620 |
. . . . 5
β’ (π β ((Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β Ξ£π β (1...(ββπ΄))((logβπ) / π)) β (((logβπ΄) Β· ((logβπ΄) + Ξ³)) β ((((logβπ΄)β2) / 2) + πΏ))) = ((Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) β (Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) |
100 | 98, 99 | eqtrd 2773 |
. . . 4
β’ (π β (Ξ£π β (1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ))) = ((Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) β (Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) |
101 | 100 | fveq2d 6896 |
. . 3
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ)))) =
(absβ((Ξ£π
β (1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) β (Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))))) |
102 | 43, 53 | abs2dif2d 15405 |
. . 3
β’ (π β (absβ((Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) β (Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) β€ ((absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) + (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))))) |
103 | 101, 102 | eqbrtrd 5171 |
. 2
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ)))) β€
((absβ(Ξ£π
β (1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) + (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))))) |
104 | | harmonicbnd4 26515 |
. . . . . . 7
β’ (π΄ β β+
β (absβ(Ξ£π
β (1...(ββπ΄))(1 / π) β ((logβπ΄) + Ξ³))) β€ (1 / π΄)) |
105 | 2, 104 | syl 17 |
. . . . . 6
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) + Ξ³)))
β€ (1 / π΄)) |
106 | 8 | nnrecred 12263 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(ββπ΄))) β (1 / π) β β) |
107 | 1, 106 | fsumrecl 15680 |
. . . . . . . . . 10
β’ (π β Ξ£π β (1...(ββπ΄))(1 / π) β β) |
108 | 107, 40 | resubcld 11642 |
. . . . . . . . 9
β’ (π β (Ξ£π β (1...(ββπ΄))(1 / π) β ((logβπ΄) + Ξ³)) β
β) |
109 | 108 | recnd 11242 |
. . . . . . . 8
β’ (π β (Ξ£π β (1...(ββπ΄))(1 / π) β ((logβπ΄) + Ξ³)) β
β) |
110 | 109 | abscld 15383 |
. . . . . . 7
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) + Ξ³)))
β β) |
111 | 2 | rprecred 13027 |
. . . . . . 7
β’ (π β (1 / π΄) β β) |
112 | | 0red 11217 |
. . . . . . . 8
β’ (π β 0 β
β) |
113 | | 1red 11215 |
. . . . . . . 8
β’ (π β 1 β
β) |
114 | | 0lt1 11736 |
. . . . . . . . 9
β’ 0 <
1 |
115 | 114 | a1i 11 |
. . . . . . . 8
β’ (π β 0 < 1) |
116 | | loge 26095 |
. . . . . . . . 9
β’
(logβe) = 1 |
117 | | mulog2sumlem1.3 |
. . . . . . . . . 10
β’ (π β e β€ π΄) |
118 | | epr 16151 |
. . . . . . . . . . 11
β’ e β
β+ |
119 | | logleb 26111 |
. . . . . . . . . . 11
β’ ((e
β β+ β§ π΄ β β+) β (e β€
π΄ β (logβe) β€
(logβπ΄))) |
120 | 118, 2, 119 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (e β€ π΄ β (logβe) β€ (logβπ΄))) |
121 | 117, 120 | mpbid 231 |
. . . . . . . . 9
β’ (π β (logβe) β€
(logβπ΄)) |
122 | 116, 121 | eqbrtrrid 5185 |
. . . . . . . 8
β’ (π β 1 β€ (logβπ΄)) |
123 | 112, 113,
11, 115, 122 | ltletrd 11374 |
. . . . . . 7
β’ (π β 0 < (logβπ΄)) |
124 | | lemul2 12067 |
. . . . . . 7
β’
(((absβ(Ξ£π β (1...(ββπ΄))(1 / π) β ((logβπ΄) + Ξ³))) β β β§ (1 /
π΄) β β β§
((logβπ΄) β
β β§ 0 < (logβπ΄))) β ((absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) + Ξ³)))
β€ (1 / π΄) β
((logβπ΄) Β·
(absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³)))) β€ ((logβπ΄) Β· (1 / π΄)))) |
125 | 110, 111,
11, 123, 124 | syl112anc 1375 |
. . . . . 6
β’ (π β ((absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) + Ξ³)))
β€ (1 / π΄) β
((logβπ΄) Β·
(absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³)))) β€ ((logβπ΄) Β· (1 / π΄)))) |
126 | 105, 125 | mpbid 231 |
. . . . 5
β’ (π β ((logβπ΄) Β·
(absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³)))) β€ ((logβπ΄) Β· (1 / π΄))) |
127 | 45 | rpcnd 13018 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
128 | 45 | rpne0d 13021 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(ββπ΄))) β π β 0) |
129 | 63, 127, 128 | divrecd 11993 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(ββπ΄))) β ((logβπ΄) / π) = ((logβπ΄) Β· (1 / π))) |
130 | 129 | sumeq2dv 15649 |
. . . . . . . . . 10
β’ (π β Ξ£π β (1...(ββπ΄))((logβπ΄) / π) = Ξ£π β (1...(ββπ΄))((logβπ΄) Β· (1 / π))) |
131 | 106 | recnd 11242 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(ββπ΄))) β (1 / π) β β) |
132 | 1, 38, 131 | fsummulc2 15730 |
. . . . . . . . . 10
β’ (π β ((logβπ΄) Β· Ξ£π β
(1...(ββπ΄))(1 /
π)) = Ξ£π β
(1...(ββπ΄))((logβπ΄) Β· (1 / π))) |
133 | 130, 132 | eqtr4d 2776 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...(ββπ΄))((logβπ΄) / π) = ((logβπ΄) Β· Ξ£π β (1...(ββπ΄))(1 / π))) |
134 | 133 | oveq1d 7424 |
. . . . . . . 8
β’ (π β (Ξ£π β (1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) = (((logβπ΄) Β· Ξ£π β
(1...(ββπ΄))(1 /
π)) β
((logβπ΄) Β·
((logβπ΄) +
Ξ³)))) |
135 | 1, 131 | fsumcl 15679 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...(ββπ΄))(1 / π) β β) |
136 | 38, 135, 41 | subdid 11670 |
. . . . . . . 8
β’ (π β ((logβπ΄) Β· (Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) + Ξ³)))
= (((logβπ΄) Β·
Ξ£π β
(1...(ββπ΄))(1 /
π)) β
((logβπ΄) Β·
((logβπ΄) +
Ξ³)))) |
137 | 134, 136 | eqtr4d 2776 |
. . . . . . 7
β’ (π β (Ξ£π β (1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³))) = ((logβπ΄) Β· (Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³)))) |
138 | 137 | fveq2d 6896 |
. . . . . 6
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) =
(absβ((logβπ΄)
Β· (Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³))))) |
139 | 135, 41 | subcld 11571 |
. . . . . . 7
β’ (π β (Ξ£π β (1...(ββπ΄))(1 / π) β ((logβπ΄) + Ξ³)) β
β) |
140 | 38, 139 | absmuld 15401 |
. . . . . 6
β’ (π β
(absβ((logβπ΄)
Β· (Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³)))) = ((absβ(logβπ΄)) Β· (absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³))))) |
141 | 112, 11, 123 | ltled 11362 |
. . . . . . . 8
β’ (π β 0 β€ (logβπ΄)) |
142 | 11, 141 | absidd 15369 |
. . . . . . 7
β’ (π β
(absβ(logβπ΄)) =
(logβπ΄)) |
143 | 142 | oveq1d 7424 |
. . . . . 6
β’ (π β
((absβ(logβπ΄))
Β· (absβ(Ξ£π β (1...(ββπ΄))(1 / π) β ((logβπ΄) + Ξ³)))) = ((logβπ΄) Β·
(absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³))))) |
144 | 138, 140,
143 | 3eqtrd 2777 |
. . . . 5
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) = ((logβπ΄) Β·
(absβ(Ξ£π β
(1...(ββπ΄))(1 /
π) β
((logβπ΄) +
Ξ³))))) |
145 | 2 | rpcnd 13018 |
. . . . . 6
β’ (π β π΄ β β) |
146 | 2 | rpne0d 13021 |
. . . . . 6
β’ (π β π΄ β 0) |
147 | 38, 145, 146 | divrecd 11993 |
. . . . 5
β’ (π β ((logβπ΄) / π΄) = ((logβπ΄) Β· (1 / π΄))) |
148 | 126, 144,
147 | 3brtr4d 5181 |
. . . 4
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) β€ ((logβπ΄) / π΄)) |
149 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = π β (logβπ) = (logβπ)) |
150 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
151 | 149, 150 | oveq12d 7427 |
. . . . . . . . . . . . 13
β’ (π = π β ((logβπ) / π) = ((logβπ) / π)) |
152 | 151 | cbvsumv 15642 |
. . . . . . . . . . . 12
β’
Ξ£π β
(1...(ββπ¦))((logβπ) / π) = Ξ£π β (1...(ββπ¦))((logβπ) / π) |
153 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π¦ = π΄ β (ββπ¦) = (ββπ΄)) |
154 | 153 | oveq2d 7425 |
. . . . . . . . . . . . 13
β’ (π¦ = π΄ β (1...(ββπ¦)) = (1...(ββπ΄))) |
155 | 154 | sumeq1d 15647 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β Ξ£π β (1...(ββπ¦))((logβπ) / π) = Ξ£π β (1...(ββπ΄))((logβπ) / π)) |
156 | 152, 155 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β Ξ£π β (1...(ββπ¦))((logβπ) / π) = Ξ£π β (1...(ββπ΄))((logβπ) / π)) |
157 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π¦ = π΄ β (logβπ¦) = (logβπ΄)) |
158 | 157 | oveq1d 7424 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β ((logβπ¦)β2) = ((logβπ΄)β2)) |
159 | 158 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β (((logβπ¦)β2) / 2) = (((logβπ΄)β2) / 2)) |
160 | 156, 159 | oveq12d 7427 |
. . . . . . . . . 10
β’ (π¦ = π΄ β (Ξ£π β (1...(ββπ¦))((logβπ) / π) β (((logβπ¦)β2) / 2)) = (Ξ£π β (1...(ββπ΄))((logβπ) / π) β (((logβπ΄)β2) / 2))) |
161 | | ovex 7442 |
. . . . . . . . . 10
β’
(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β (((logβπ΄)β2) / 2)) β V |
162 | 160, 19, 161 | fvmpt 6999 |
. . . . . . . . 9
β’ (π΄ β β+
β (πΉβπ΄) = (Ξ£π β (1...(ββπ΄))((logβπ) / π) β (((logβπ΄)β2) / 2))) |
163 | 2, 162 | syl 17 |
. . . . . . . 8
β’ (π β (πΉβπ΄) = (Ξ£π β (1...(ββπ΄))((logβπ) / π) β (((logβπ΄)β2) / 2))) |
164 | 163 | oveq1d 7424 |
. . . . . . 7
β’ (π β ((πΉβπ΄) β πΏ) = ((Ξ£π β (1...(ββπ΄))((logβπ) / π) β (((logβπ΄)β2) / 2)) β πΏ)) |
165 | 49, 50, 51 | subsub4d 11602 |
. . . . . . 7
β’ (π β ((Ξ£π β
(1...(ββπ΄))((logβπ) / π) β (((logβπ΄)β2) / 2)) β πΏ) = (Ξ£π β (1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))) |
166 | 164, 165 | eqtrd 2773 |
. . . . . 6
β’ (π β ((πΉβπ΄) β πΏ) = (Ξ£π β (1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))) |
167 | 166 | fveq2d 6896 |
. . . . 5
β’ (π β (absβ((πΉβπ΄) β πΏ)) = (absβ(Ξ£π β (1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) |
168 | 20 | simp3i 1142 |
. . . . . 6
β’ ((πΉ βπ
πΏ β§ π΄ β β+ β§ e β€
π΄) β
(absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄)) |
169 | 24, 2, 117, 168 | syl3anc 1372 |
. . . . 5
β’ (π β (absβ((πΉβπ΄) β πΏ)) β€ ((logβπ΄) / π΄)) |
170 | 167, 169 | eqbrtrrd 5173 |
. . . 4
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ))) β€ ((logβπ΄) / π΄)) |
171 | 44, 54, 57, 57, 148, 170 | le2addd 11833 |
. . 3
β’ (π β ((absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) + (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) β€ (((logβπ΄) / π΄) + ((logβπ΄) / π΄))) |
172 | 57 | recnd 11242 |
. . . 4
β’ (π β ((logβπ΄) / π΄) β β) |
173 | 172 | 2timesd 12455 |
. . 3
β’ (π β (2 Β·
((logβπ΄) / π΄)) = (((logβπ΄) / π΄) + ((logβπ΄) / π΄))) |
174 | 171, 173 | breqtrrd 5177 |
. 2
β’ (π β ((absβ(Ξ£π β
(1...(ββπ΄))((logβπ΄) / π) β ((logβπ΄) Β· ((logβπ΄) + Ξ³)))) + (absβ(Ξ£π β
(1...(ββπ΄))((logβπ) / π) β ((((logβπ΄)β2) / 2) + πΏ)))) β€ (2 Β· ((logβπ΄) / π΄))) |
175 | 33, 55, 59, 103, 174 | letrd 11371 |
1
β’ (π β (absβ(Ξ£π β
(1...(ββπ΄))((logβ(π΄ / π)) / π) β ((((logβπ΄)β2) / 2) + ((Ξ³ Β·
(logβπ΄)) β
πΏ)))) β€ (2 Β·
((logβπ΄) / π΄))) |