Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. . 3
β’ (β€
β 1 β β) |
2 | | pntrlog2bnd.r |
. . . . 5
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
3 | 2 | selberg34r 26935 |
. . . 4
β’ (π₯ β (1(,)+β) β¦
((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) β π(1) |
4 | | elioore 13301 |
. . . . . . . . . . . 12
β’ (π₯ β (1(,)+β) β
π₯ β
β) |
5 | 4 | adantl 483 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
6 | | 1rp 12926 |
. . . . . . . . . . . 12
β’ 1 β
β+ |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β+) |
8 | | 1red 11163 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β) |
9 | | eliooord 13330 |
. . . . . . . . . . . . . 14
β’ (π₯ β (1(,)+β) β (1
< π₯ β§ π₯ <
+β)) |
10 | 9 | adantl 483 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β (1 < π₯ β§ π₯ < +β)) |
11 | 10 | simpld 496 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 1 < π₯) |
12 | 8, 5, 11 | ltled 11310 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β€ π₯) |
13 | 5, 7, 12 | rpgecld 13003 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β+) |
14 | 2 | pntrf 26927 |
. . . . . . . . . . 11
β’ π
:β+βΆβ |
15 | 14 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π
βπ₯) β
β) |
16 | 13, 15 | syl 17 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (π
βπ₯) β β) |
17 | 13 | relogcld 25994 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
18 | 16, 17 | remulcld 11192 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((π
βπ₯) Β· (logβπ₯)) β β) |
19 | | fzfid 13885 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (1...(ββπ₯)) β Fin) |
20 | 13 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π₯ β β+) |
21 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β
(1...(ββπ₯))
β π β
β) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
23 | 22 | nnrpd 12962 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β+) |
24 | 20, 23 | rpdivcld 12981 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π₯ / π) β
β+) |
25 | 14 | ffvelcdmi 7039 |
. . . . . . . . . . . 12
β’ ((π₯ / π) β β+ β (π
β(π₯ / π)) β β) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / π)) β β) |
27 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (1...π) β Fin) |
28 | | dvdsssfz1 16207 |
. . . . . . . . . . . . . . 15
β’ (π β β β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
29 | 22, 28 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
30 | 27, 29 | ssfid 9218 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β {π¦ β β β£ π¦ β₯ π} β Fin) |
31 | | ssrab2 4042 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β β β£ π¦ β₯ π} β β |
32 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β π β {π¦ β β β£ π¦ β₯ π}) |
33 | 31, 32 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β π β β) |
34 | | vmacl 26483 |
. . . . . . . . . . . . . . 15
β’ (π β β β
(Ξβπ) β
β) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβπ) β β) |
36 | | dvdsdivcl 16205 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
37 | 22, 36 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
38 | 31, 37 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β β) |
39 | | vmacl 26483 |
. . . . . . . . . . . . . . 15
β’ ((π / π) β β β
(Ξβ(π / π)) β
β) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβ(π / π)) β β) |
41 | 35, 40 | remulcld 11192 |
. . . . . . . . . . . . 13
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
42 | 30, 41 | fsumrecl 15626 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β β) |
43 | | vmacl 26483 |
. . . . . . . . . . . . . 14
β’ (π β β β
(Ξβπ) β
β) |
44 | 22, 43 | syl 17 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
45 | 23 | relogcld 25994 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβπ) β
β) |
46 | 44, 45 | remulcld 11192 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· (logβπ))
β β) |
47 | 42, 46 | resubcld 11590 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))) β
β) |
48 | 26, 47 | remulcld 11192 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
49 | 19, 48 | fsumrecl 15626 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
50 | 5, 11 | rplogcld 26000 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β
β+) |
51 | 49, 50 | rerpdivcld 12995 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)) β
β) |
52 | 18, 51 | resubcld 11590 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) β
β) |
53 | 52, 13 | rerpdivcld 12995 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯) β β) |
54 | 53 | recnd 11190 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯) β β) |
55 | 54 | lo1o12 15422 |
. . . 4
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) β π(1) β (π₯ β (1(,)+β) β¦
(absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯))) β
β€π(1))) |
56 | 3, 55 | mpbii 232 |
. . 3
β’ (β€
β (π₯ β
(1(,)+β) β¦ (absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯))) β β€π(1)) |
57 | 54 | abscld 15328 |
. . 3
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) β β) |
58 | 16 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (π
βπ₯) β β) |
59 | 58 | abscld 15328 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(π
βπ₯)) β β) |
60 | 59, 17 | remulcld 11192 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(π
βπ₯)) Β· (logβπ₯)) β β) |
61 | 26 | recnd 11190 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / π)) β β) |
62 | 61 | abscld 15328 |
. . . . . . . 8
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ(π
β(π₯ / π))) β β) |
63 | 22 | nnred 12175 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
64 | | pntsval.1 |
. . . . . . . . . . . 12
β’ π = (π β β β¦ Ξ£π β
(1...(ββπ))((Ξβπ) Β· ((logβπ) + (Οβ(π / π))))) |
65 | 64 | pntsf 26937 |
. . . . . . . . . . 11
β’ π:ββΆβ |
66 | 65 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’ (π β β β (πβπ) β β) |
67 | 63, 66 | syl 17 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) β β) |
68 | | 1red 11163 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β
β) |
69 | 63, 68 | resubcld 11590 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π β 1) β β) |
70 | 65 | ffvelcdmi 7039 |
. . . . . . . . . 10
β’ ((π β 1) β β
β (πβ(π β 1)) β
β) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) β β) |
72 | 67, 71 | resubcld 11590 |
. . . . . . . 8
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) β
β) |
73 | 62, 72 | remulcld 11192 |
. . . . . . 7
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
74 | 19, 73 | fsumrecl 15626 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
75 | 74, 50 | rerpdivcld 12995 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β
β) |
76 | 60, 75 | resubcld 11590 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) β
β) |
77 | 76, 13 | rerpdivcld 12995 |
. . 3
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) β β) |
78 | 17 | recnd 11190 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
79 | 58, 78 | mulcld 11182 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((π
βπ₯) Β· (logβπ₯)) β β) |
80 | 49 | recnd 11190 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
81 | 50 | rpne0d 12969 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β 0) |
82 | 80, 78, 81 | divcld 11938 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)) β
β) |
83 | 79, 82 | subcld 11519 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) β
β) |
84 | 83 | abscld 15328 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) β
β) |
85 | 80 | abscld 15328 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (absβΞ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β
β) |
86 | 85, 50 | rerpdivcld 12995 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβΞ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯)) β
β) |
87 | 60, 86 | resubcld 11590 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((absβΞ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯))) β
β) |
88 | 48 | recnd 11190 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
89 | 88 | abscld 15328 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β
β) |
90 | 19, 89 | fsumrecl 15626 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(absβ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β
β) |
91 | 19, 88 | fsumabs 15693 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (absβΞ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β€ Ξ£π β
(1...(ββπ₯))(absβ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) |
92 | 47 | recnd 11190 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))) β
β) |
93 | 61, 92 | absmuld 15346 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) = ((absβ(π
β(π₯ / π))) Β· (absβ(Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) |
94 | 92 | abscld 15328 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(absβ(Ξ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π))) β
((Ξβπ)
Β· (logβπ))))
β β) |
95 | 61 | absge0d 15336 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
(absβ(π
β(π₯ / π)))) |
96 | 42 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β β) |
97 | 46 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· (logβπ))
β β) |
98 | 96, 97 | abs2dif2d 15350 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(absβ(Ξ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π))) β
((Ξβπ)
Β· (logβπ))))
β€ ((absβΞ£π
β {π¦ β β
β£ π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π)))) +
(absβ((Ξβπ) Β· (logβπ))))) |
99 | 71 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) β β) |
100 | 96, 97 | addcld 11181 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) β β) |
101 | 99, 100 | pncan2d 11521 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβ(π β 1)) + (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) β (πβ(π β 1))) = (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
102 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(1...(ββπ₯))
β π β
(β€β₯β1)) |
103 | 102 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β
(β€β₯β1)) |
104 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) β π β β) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β π β β) |
106 | | vmacl 26483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β
(Ξβπ) β
β) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β (Ξβπ) β β) |
108 | 105 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β π β β+) |
109 | 108 | relogcld 25994 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β (logβπ) β β) |
110 | 107, 109 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β ((Ξβπ) Β· (logβπ)) β β) |
111 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β (1...π) β Fin) |
112 | | dvdsssfz1 16207 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
113 | 105, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
114 | 111, 113 | ssfid 9218 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β {π¦ β β β£ π¦ β₯ π} β Fin) |
115 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ {π¦ β β β£ π¦ β₯ π} β β |
116 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β π β {π¦ β β β£ π¦ β₯ π}) |
117 | 115, 116 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β π β β) |
118 | 117, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβπ) β β) |
119 | | dvdsdivcl 16205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
120 | 105, 119 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
121 | 115, 120 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β β) |
122 | | vmacl 26483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π / π) β β β
(Ξβ(π / π)) β
β) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβ(π / π)) β β) |
124 | 118, 123 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((β€ β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β§ π β (1...π)) β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
125 | 114, 124 | fsumrecl 15626 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β β) |
126 | 110, 125 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . 19
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β β) |
127 | 126 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...π)) β (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β β) |
128 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (Ξβπ) = (Ξβπ)) |
129 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (logβπ) = (logβπ)) |
130 | 128, 129 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((Ξβπ) Β· (logβπ)) = ((Ξβπ) Β· (logβπ))) |
131 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π¦ β₯ π β π¦ β₯ π)) |
132 | 131 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β {π¦ β β β£ π¦ β₯ π} = {π¦ β β β£ π¦ β₯ π}) |
133 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (Ξβ(π / π)) = (Ξβ(π / π))) |
134 | 133 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ(π / π)))) |
135 | 134 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = π β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ(π / π)))) |
136 | 132, 135 | sumeq12rdv 15599 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) = Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) |
137 | 130, 136 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
138 | 103, 127,
137 | fsumm1 15643 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β (1...π)(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = (Ξ£π β (1...(π β 1))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) + (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))))) |
139 | 64 | pntsval2 26940 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (πβπ) = Ξ£π β (1...(ββπ))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
140 | 63, 139 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) = Ξ£π β (1...(ββπ))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
141 | 22 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β€) |
142 | | flid 13720 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β€ β
(ββπ) = π) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (ββπ) = π) |
144 | 143 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(1...(ββπ)) =
(1...π)) |
145 | 144 | sumeq1d 15593 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββπ))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = Ξ£π β (1...π)(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
146 | 140, 145 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) = Ξ£π β (1...π)(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
147 | 64 | pntsval2 26940 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β 1) β β
β (πβ(π β 1)) = Ξ£π β
(1...(ββ(π
β 1)))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
148 | 69, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) = Ξ£π β (1...(ββ(π β
1)))(((Ξβπ)
Β· (logβπ)) +
Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
149 | | 1zzd 12541 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β
β€) |
150 | 141, 149 | zsubcld 12619 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π β 1) β β€) |
151 | | flid 13720 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β 1) β β€
β (ββ(π
β 1)) = (π β
1)) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (ββ(π β 1)) = (π β 1)) |
153 | 152 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(1...(ββ(π
β 1))) = (1...(π
β 1))) |
154 | 153 | sumeq1d 15593 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π
β 1)))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = Ξ£π β (1...(π β 1))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
155 | 148, 154 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) = Ξ£π β (1...(π β 1))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
156 | 96, 97 | addcomd 11364 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) = (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
157 | 155, 156 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβ(π β 1)) + (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) = (Ξ£π β (1...(π β 1))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) + (((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))))) |
158 | 138, 146,
157 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) = ((πβ(π β 1)) + (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))) |
159 | 158 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) = (((πβ(π β 1)) + (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) β (πβ(π β 1)))) |
160 | | vmage0 26486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β 0 β€
(Ξβπ)) |
161 | 33, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β 0 β€ (Ξβπ)) |
162 | | vmage0 26486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π / π) β β β 0 β€
(Ξβ(π / π))) |
163 | 38, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β 0 β€ (Ξβ(π / π))) |
164 | 35, 40, 161, 163 | mulge0d 11739 |
. . . . . . . . . . . . . . . . . 18
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β 0 β€ ((Ξβπ) Β·
(Ξβ(π / π)))) |
165 | 30, 41, 164 | fsumge0 15687 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€ Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) |
166 | 42, 165 | absidd 15314 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(absβΞ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π)))) = Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) |
167 | | vmage0 26486 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β 0 β€
(Ξβπ)) |
168 | 22, 167 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
(Ξβπ)) |
169 | 22 | nnge1d 12208 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β€ π) |
170 | 63, 169 | logge0d 26001 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
(logβπ)) |
171 | 44, 45, 168, 170 | mulge0d 11739 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
((Ξβπ)
Β· (logβπ))) |
172 | 46, 171 | absidd 15314 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(absβ((Ξβπ) Β· (logβπ))) = ((Ξβπ) Β· (logβπ))) |
173 | 166, 172 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((absβΞ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π)))) +
(absβ((Ξβπ) Β· (logβπ)))) = (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
174 | 101, 159,
173 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) = ((absβΞ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) + (absβ((Ξβπ) Β· (logβπ))))) |
175 | 98, 174 | breqtrrd 5138 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(absβ(Ξ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π))) β
((Ξβπ)
Β· (logβπ))))
β€ ((πβπ) β (πβ(π β 1)))) |
176 | 94, 72, 62, 95, 175 | lemul2ad 12102 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (absβ(Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β€ ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) |
177 | 93, 176 | eqbrtrd 5132 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β€ ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) |
178 | 19, 89, 73, 177 | fsumle 15691 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(absβ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β€ Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) |
179 | 85, 90, 74, 91, 178 | letrd 11319 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (absβΞ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β€ Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) |
180 | 85, 74, 50, 179 | lediv1dd 13022 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβΞ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯)) β€ (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) |
181 | 86, 75, 60, 180 | lesub2dd 11779 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) β€ (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((absβΞ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯)))) |
182 | 58, 78 | absmuld 15346 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ((π
βπ₯) Β· (logβπ₯))) = ((absβ(π
βπ₯)) Β· (absβ(logβπ₯)))) |
183 | 5, 12 | logge0d 26001 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (logβπ₯)) |
184 | 17, 183 | absidd 15314 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(logβπ₯)) = (logβπ₯)) |
185 | 184 | oveq2d 7378 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(π
βπ₯)) Β· (absβ(logβπ₯))) = ((absβ(π
βπ₯)) Β· (logβπ₯))) |
186 | 182, 185 | eqtrd 2777 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ((π
βπ₯) Β· (logβπ₯))) = ((absβ(π
βπ₯)) Β· (logβπ₯))) |
187 | 80, 78, 81 | absdivd 15347 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) = ((absβΞ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) /
(absβ(logβπ₯)))) |
188 | 184 | oveq2d 7378 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβΞ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) /
(absβ(logβπ₯)))
= ((absβΞ£π
β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯))) |
189 | 187, 188 | eqtrd 2777 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) = ((absβΞ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯))) |
190 | 186, 189 | oveq12d 7380 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ((π
βπ₯) Β· (logβπ₯))) β (absβ(Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) = (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((absβΞ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯)))) |
191 | 79, 82 | abs2difd 15349 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ((π
βπ₯) Β· (logβπ₯))) β (absβ(Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) β€ (absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))))) |
192 | 190, 191 | eqbrtrrd 5134 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((absβΞ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / (logβπ₯))) β€ (absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))))) |
193 | 76, 87, 84, 181, 192 | letrd 11319 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) β€ (absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))))) |
194 | 76, 84, 13, 193 | lediv1dd 13022 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) β€ ((absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) / π₯)) |
195 | 52 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) β
β) |
196 | 5 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
197 | 13 | rpne0d 12969 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β 0) |
198 | 195, 196,
197 | absdivd 15347 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) = ((absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) / (absβπ₯))) |
199 | 13 | rpge0d 12968 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ π₯) |
200 | 5, 199 | absidd 15314 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (absβπ₯) = π₯) |
201 | 200 | oveq2d 7378 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) / (absβπ₯)) = ((absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) / π₯)) |
202 | 198, 201 | eqtrd 2777 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) = ((absβ(((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) / π₯)) |
203 | 194, 202 | breqtrrd 5138 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) β€ (absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯))) |
204 | 203 | adantrr 716 |
. . 3
β’
((β€ β§ (π₯
β (1(,)+β) β§ 1 β€ π₯)) β ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) β€ (absβ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯))) |
205 | 1, 56, 57, 77, 204 | lo1le 15543 |
. 2
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯)) β β€π(1)) |
206 | 205 | mptru 1549 |
1
β’ (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯)) β β€π(1) |