Step | Hyp | Ref
| Expression |
1 | | fzfid 13956 |
. . . . . 6
β’ (π₯ β β+
β (1...(ββπ₯)) β Fin) |
2 | | elfznn 13548 |
. . . . . . . . . . 11
β’ (π β
(1...(ββπ₯))
β π β
β) |
3 | 2 | adantl 481 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β) |
4 | | mucl 27047 |
. . . . . . . . . 10
β’ (π β β β
(ΞΌβπ) β
β€) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
6 | 5 | zred 12682 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
7 | 6, 3 | nndivred 12282 |
. . . . . . 7
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
8 | 7 | recnd 11258 |
. . . . . 6
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
9 | 1, 8 | fsumcl 15697 |
. . . . 5
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) β β) |
10 | 9 | adantl 481 |
. . . 4
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) β β) |
11 | | emre 26912 |
. . . . . 6
β’ Ξ³
β β |
12 | 11 | recni 11244 |
. . . . 5
β’ Ξ³
β β |
13 | 12 | a1i 11 |
. . . 4
β’
((β€ β§ π₯
β β+) β Ξ³ β β) |
14 | | mudivsum 27437 |
. . . . 5
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) β π(1) |
15 | 14 | a1i 11 |
. . . 4
β’ (β€
β (π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π)) β π(1)) |
16 | | rpssre 12999 |
. . . . . 6
β’
β+ β β |
17 | | o1const 15582 |
. . . . . 6
β’
((β+ β β β§ Ξ³ β β)
β (π₯ β
β+ β¦ Ξ³) β π(1)) |
18 | 16, 12, 17 | mp2an 691 |
. . . . 5
β’ (π₯ β β+
β¦ Ξ³) β π(1) |
19 | 18 | a1i 11 |
. . . 4
β’ (β€
β (π₯ β
β+ β¦ Ξ³) β π(1)) |
20 | 10, 13, 15, 19 | o1mul2 15587 |
. . 3
β’ (β€
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³)) β
π(1)) |
21 | | fzfid 13956 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1...(ββ(π₯ / π))) β Fin) |
22 | | elfznn 13548 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
23 | 22 | adantl 481 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
24 | 23 | nnrecred 12279 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (1 / π) β
β) |
25 | 21, 24 | fsumrecl 15698 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β β) |
26 | 2 | nnrpd 13032 |
. . . . . . . . . . 11
β’ (π β
(1...(ββπ₯))
β π β
β+) |
27 | | rpdivcl 13017 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
28 | 26, 27 | sylan2 592 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
29 | 28 | relogcld 26531 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
30 | 25, 29 | resubcld 11658 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β β) |
31 | 7, 30 | remulcld 11260 |
. . . . . . 7
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) β β) |
32 | 1, 31 | fsumrecl 15698 |
. . . . . 6
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β β) |
33 | 32 | recnd 11258 |
. . . . 5
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β β) |
34 | 33 | adantl 481 |
. . . 4
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β β) |
35 | | mulcl 11208 |
. . . . . 6
β’
((Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) β β β§ Ξ³ β
β) β (Ξ£π
β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³) β
β) |
36 | 9, 12, 35 | sylancl 585 |
. . . . 5
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³) β
β) |
37 | 36 | adantl 481 |
. . . 4
β’
((β€ β§ π₯
β β+) β (Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³) β
β) |
38 | | nnrecre 12270 |
. . . . . . . . . . . . 13
β’ (π β β β (1 /
π) β
β) |
39 | 38 | recnd 11258 |
. . . . . . . . . . . 12
β’ (π β β β (1 /
π) β
β) |
40 | 23, 39 | syl 17 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (1 / π) β
β) |
41 | 21, 40 | fsumcl 15697 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β β) |
42 | 29 | recnd 11258 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
43 | 41, 42 | subcld 11587 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β β) |
44 | 8, 43 | mulcld 11250 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) β β) |
45 | | mulcl 11208 |
. . . . . . . . 9
β’
((((ΞΌβπ) /
π) β β β§
Ξ³ β β) β (((ΞΌβπ) / π) Β· Ξ³) β
β) |
46 | 8, 12, 45 | sylancl 585 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· Ξ³) β
β) |
47 | 1, 44, 46 | fsumsub 15752 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (((ΞΌβπ) / π) Β· Ξ³)) = (Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ³))) |
48 | 12 | a1i 11 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ³ β β) |
49 | 41, 42, 48 | subsub4d 11618 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β Ξ³) = (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) |
50 | 49 | oveq2d 7430 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· ((Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β Ξ³)) = (((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) |
51 | 8, 43, 48 | subdid 11686 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· ((Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β Ξ³)) = ((((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (((ΞΌβπ) / π) Β· Ξ³))) |
52 | 50, 51 | eqtr3d 2769 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) = ((((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (((ΞΌβπ) / π) Β· Ξ³))) |
53 | 52 | sumeq2dv 15667 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) = Ξ£π β (1...(ββπ₯))((((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (((ΞΌβπ) / π) Β· Ξ³))) |
54 | 12 | a1i 11 |
. . . . . . . . 9
β’ (π₯ β β+
β Ξ³ β β) |
55 | 1, 54, 8 | fsummulc1 15749 |
. . . . . . . 8
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³) = Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ³)) |
56 | 55 | oveq2d 7430 |
. . . . . . 7
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³)) = (Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ³))) |
57 | 47, 53, 56 | 3eqtr4d 2777 |
. . . . . 6
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³))) |
58 | 57 | mpteq2ia 5245 |
. . . . 5
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³))) |
59 | 16 | a1i 11 |
. . . . . 6
β’ (β€
β β+ β β) |
60 | 42, 48 | addcld 11249 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) + Ξ³) β
β) |
61 | 41, 60 | subcld 11587 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)) β
β) |
62 | 8, 61 | mulcld 11250 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β
β) |
63 | 1, 62 | fsumcl 15697 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β
β) |
64 | 63 | adantl 481 |
. . . . . 6
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β
β) |
65 | | 1red 11231 |
. . . . . 6
β’ (β€
β 1 β β) |
66 | 63 | abscld 15401 |
. . . . . . . 8
β’ (π₯ β β+
β (absβΞ£π
β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β
β) |
67 | 62 | abscld 15401 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β
β) |
68 | 1, 67 | fsumrecl 15698 |
. . . . . . . 8
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β
β) |
69 | | 1red 11231 |
. . . . . . . 8
β’ (π₯ β β+
β 1 β β) |
70 | 1, 62 | fsumabs 15765 |
. . . . . . . 8
β’ (π₯ β β+
β (absβΞ£π
β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ Ξ£π β
(1...(ββπ₯))(absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))))) |
71 | | rprege0 13007 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (π₯ β β
β§ 0 β€ π₯)) |
72 | | flge0nn0 13803 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β0) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (ββπ₯)
β β0) |
74 | 73 | nn0red 12549 |
. . . . . . . . . 10
β’ (π₯ β β+
β (ββπ₯)
β β) |
75 | | rerpdivcl 13022 |
. . . . . . . . . 10
β’
(((ββπ₯)
β β β§ π₯
β β+) β ((ββπ₯) / π₯) β β) |
76 | 74, 75 | mpancom 687 |
. . . . . . . . 9
β’ (π₯ β β+
β ((ββπ₯) /
π₯) β
β) |
77 | | rpreccl 13018 |
. . . . . . . . . . . . 13
β’ (π₯ β β+
β (1 / π₯) β
β+) |
78 | 77 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1 / π₯) β
β+) |
79 | 78 | rpred 13034 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1 / π₯) β
β) |
80 | 8 | abscld 15401 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) β β) |
81 | 3 | nnrecred 12279 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
82 | 61 | abscld 15401 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(Ξ£π
β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β
β) |
83 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β π₯ β
β+) |
84 | | rpdivcl 13017 |
. . . . . . . . . . . . . . 15
β’ ((π β β+
β§ π₯ β
β+) β (π / π₯) β
β+) |
85 | 26, 83, 84 | syl2anr 596 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π / π₯) β
β+) |
86 | 85 | rpred 13034 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π / π₯) β
β) |
87 | 8 | absge0d 15409 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((ΞΌβπ) / π))) |
88 | 61 | absge0d 15409 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) |
89 | 6 | recnd 11258 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
90 | 3 | nncnd 12244 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β) |
91 | 3 | nnne0d 12278 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
0) |
92 | 89, 90, 91 | absdivd 15420 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) = ((absβ(ΞΌβπ)) / (absβπ))) |
93 | 3 | nnrpd 13032 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β+) |
94 | | rprege0 13007 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β (π β β
β§ 0 β€ π)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π β β
β§ 0 β€ π)) |
96 | | absid 15261 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 0 β€
π) β (absβπ) = π) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβπ) =
π) |
98 | 97 | oveq2d 7430 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) / (absβπ)) = ((absβ(ΞΌβπ)) / π)) |
99 | 92, 98 | eqtrd 2767 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) = ((absβ(ΞΌβπ)) / π)) |
100 | 89 | abscld 15401 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β β) |
101 | | 1red 11231 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β 1 β β) |
102 | | mule1 27054 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(absβ(ΞΌβπ))
β€ 1) |
103 | 3, 102 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β€ 1) |
104 | 100, 101,
93, 103 | lediv1dd 13092 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) / π) β€ (1 / π)) |
105 | 99, 104 | eqbrtrd 5164 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) β€ (1 / π)) |
106 | | harmonicbnd4 26917 |
. . . . . . . . . . . . . . 15
β’ ((π₯ / π) β β+ β
(absβ(Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β€ (1 / (π₯ / π))) |
107 | 28, 106 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(Ξ£π
β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β€ (1 / (π₯ / π))) |
108 | | rpcnne0 13010 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β (π₯ β β
β§ π₯ β
0)) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ π₯ β
0)) |
110 | | rpcnne0 13010 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β (π β β
β§ π β
0)) |
111 | 93, 110 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π β β
β§ π β
0)) |
112 | | recdiv 11936 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π₯ β 0) β§ (π β β β§ π β 0)) β (1 / (π₯ / π)) = (π / π₯)) |
113 | 109, 111,
112 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1 / (π₯ / π)) = (π / π₯)) |
114 | 107, 113 | breqtrd 5168 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(Ξ£π
β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))) β€ (π / π₯)) |
115 | 80, 81, 82, 86, 87, 88, 105, 114 | lemul12ad 12172 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((absβ((ΞΌβπ) / π)) Β· (absβ(Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ ((1 / π) Β· (π / π₯))) |
116 | 8, 61 | absmuld 15419 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) =
((absβ((ΞΌβπ)
/ π)) Β·
(absβ(Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³))))) |
117 | | 1cnd 11225 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β 1 β β) |
118 | | dmdcan 11940 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β 0) β§ (π₯ β β β§ π₯ β 0) β§ 1 β β)
β ((π / π₯) Β· (1 / π)) = (1 / π₯)) |
119 | 111, 109,
117, 118 | syl3anc 1369 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((π / π₯) Β· (1 / π)) = (1 / π₯)) |
120 | 85 | rpcnd 13036 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π / π₯) β
β) |
121 | 81 | recnd 11258 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
122 | 120, 121 | mulcomd 11251 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((π / π₯) Β· (1 / π)) = ((1 / π) Β· (π / π₯))) |
123 | 119, 122 | eqtr3d 2769 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1 / π₯) = ((1 /
π) Β· (π / π₯))) |
124 | 115, 116,
123 | 3brtr4d 5174 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ (1 / π₯)) |
125 | 1, 67, 79, 124 | fsumle 15763 |
. . . . . . . . . 10
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ Ξ£π β
(1...(ββπ₯))(1 /
π₯)) |
126 | | hashfz1 14323 |
. . . . . . . . . . . . 13
β’
((ββπ₯)
β β0 β (β―β(1...(ββπ₯))) = (ββπ₯)) |
127 | 73, 126 | syl 17 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (β―β(1...(ββπ₯))) = (ββπ₯)) |
128 | 127 | oveq1d 7429 |
. . . . . . . . . . 11
β’ (π₯ β β+
β ((β―β(1...(ββπ₯))) Β· (1 / π₯)) = ((ββπ₯) Β· (1 / π₯))) |
129 | 77 | rpcnd 13036 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (1 / π₯) β
β) |
130 | | fsumconst 15754 |
. . . . . . . . . . . 12
β’
(((1...(ββπ₯)) β Fin β§ (1 / π₯) β β) β Ξ£π β
(1...(ββπ₯))(1 /
π₯) =
((β―β(1...(ββπ₯))) Β· (1 / π₯))) |
131 | 1, 129, 130 | syl2anc 583 |
. . . . . . . . . . 11
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(1 /
π₯) =
((β―β(1...(ββπ₯))) Β· (1 / π₯))) |
132 | 73 | nn0cnd 12550 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (ββπ₯)
β β) |
133 | | rpcn 13002 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β) |
134 | | rpne0 13008 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
0) |
135 | 132, 133,
134 | divrecd 12009 |
. . . . . . . . . . 11
β’ (π₯ β β+
β ((ββπ₯) /
π₯) = ((ββπ₯) Β· (1 / π₯))) |
136 | 128, 131,
135 | 3eqtr4d 2777 |
. . . . . . . . . 10
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(1 /
π₯) = ((ββπ₯) / π₯)) |
137 | 125, 136 | breqtrd 5168 |
. . . . . . . . 9
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ ((ββπ₯) / π₯)) |
138 | | rpre 13000 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β) |
139 | | flle 13782 |
. . . . . . . . . . . 12
β’ (π₯ β β β
(ββπ₯) β€
π₯) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (ββπ₯)
β€ π₯) |
141 | 133 | mulridd 11247 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ Β· 1) =
π₯) |
142 | 140, 141 | breqtrrd 5170 |
. . . . . . . . . 10
β’ (π₯ β β+
β (ββπ₯)
β€ (π₯ Β·
1)) |
143 | | reflcl 13779 |
. . . . . . . . . . . 12
β’ (π₯ β β β
(ββπ₯) β
β) |
144 | 138, 143 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (ββπ₯)
β β) |
145 | | rpregt0 13006 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
146 | | ledivmul 12106 |
. . . . . . . . . . 11
β’
(((ββπ₯)
β β β§ 1 β β β§ (π₯ β β β§ 0 < π₯)) β (((ββπ₯) / π₯) β€ 1 β (ββπ₯) β€ (π₯ Β· 1))) |
147 | 144, 69, 145, 146 | syl3anc 1369 |
. . . . . . . . . 10
β’ (π₯ β β+
β (((ββπ₯)
/ π₯) β€ 1 β
(ββπ₯) β€
(π₯ Β·
1))) |
148 | 142, 147 | mpbird 257 |
. . . . . . . . 9
β’ (π₯ β β+
β ((ββπ₯) /
π₯) β€ 1) |
149 | 68, 76, 69, 137, 148 | letrd 11387 |
. . . . . . . 8
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(absβ(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ 1) |
150 | 66, 68, 69, 70, 149 | letrd 11387 |
. . . . . . 7
β’ (π₯ β β+
β (absβΞ£π
β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ 1) |
151 | 150 | ad2antrl 727 |
. . . . . 6
β’
((β€ β§ (π₯
β β+ β§ 1 β€ π₯)) β (absβΞ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β€ 1) |
152 | 59, 64, 65, 65, 151 | elo1d 15498 |
. . . . 5
β’ (β€
β (π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β ((logβ(π₯ / π)) + Ξ³)))) β
π(1)) |
153 | 58, 152 | eqeltrrid 2833 |
. . . 4
β’ (β€
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β (Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³))) β
π(1)) |
154 | 34, 37, 153 | o1dif 15592 |
. . 3
β’ (β€
β ((π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) β π(1) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) Β· Ξ³)) β
π(1))) |
155 | 20, 154 | mpbird 257 |
. 2
β’ (β€
β (π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) β π(1)) |
156 | 155 | mptru 1541 |
1
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) β π(1) |