Step | Hyp | Ref
| Expression |
1 | | elioore 13354 |
. . . . . . . . . . . . 13
β’ (π₯ β (1(,)+β) β
π₯ β
β) |
2 | 1 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β π₯ β
β) |
3 | | 1rp 12978 |
. . . . . . . . . . . . 13
β’ 1 β
β+ |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β 1 β
β+) |
5 | | 1red 11215 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β 1 β
β) |
6 | | eliooord 13383 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (1(,)+β) β (1
< π₯ β§ π₯ <
+β)) |
7 | 6 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1(,)+β)) β (1 < π₯ β§ π₯ < +β)) |
8 | 7 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β 1 < π₯) |
9 | 5, 2, 8 | ltled 11362 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β 1 β€ π₯) |
10 | 2, 4, 9 | rpgecld 13055 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β π₯ β
β+) |
11 | | pntrlog2bnd.r |
. . . . . . . . . . . . 13
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
12 | 11 | pntrf 27066 |
. . . . . . . . . . . 12
β’ π
:β+βΆβ |
13 | 12 | ffvelcdmi 7086 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π
βπ₯) β
β) |
14 | 10, 13 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β (π
βπ₯) β β) |
15 | 14 | recnd 11242 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β (π
βπ₯) β β) |
16 | 15 | abscld 15383 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β
(absβ(π
βπ₯)) β
β) |
17 | 10 | relogcld 26131 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β
(logβπ₯) β
β) |
18 | 16, 17 | remulcld 11244 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β
((absβ(π
βπ₯)) Β· (logβπ₯)) β
β) |
19 | | 2re 12286 |
. . . . . . . . . 10
β’ 2 β
β |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β 2 β
β) |
21 | 2, 8 | rplogcld 26137 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β
(logβπ₯) β
β+) |
22 | 20, 21 | rerpdivcld 13047 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β (2 /
(logβπ₯)) β
β) |
23 | | fzfid 13938 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β
(1...(ββπ₯))
β Fin) |
24 | 10 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β π₯ β
β+) |
25 | | elfznn 13530 |
. . . . . . . . . . . . . . . 16
β’ (π β
(1...(ββπ₯))
β π β
β) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β π β
β) |
27 | 26 | nnrpd 13014 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β π β
β+) |
28 | 24, 27 | rpdivcld 13033 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
29 | 12 | ffvelcdmi 7086 |
. . . . . . . . . . . . 13
β’ ((π₯ / π) β β+ β (π
β(π₯ / π)) β β) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (π
β(π₯ / π)) β β) |
31 | 30 | recnd 11242 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (π
β(π₯ / π)) β β) |
32 | 31 | abscld 15383 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (absβ(π
β(π₯ / π))) β β) |
33 | 27 | relogcld 26131 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (logβπ) β
β) |
34 | 32, 33 | remulcld 11244 |
. . . . . . . . 9
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β ((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
35 | 23, 34 | fsumrecl 15680 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
36 | 22, 35 | remulcld 11244 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β β) |
37 | 18, 36 | resubcld 11642 |
. . . . . 6
β’ ((π β§ π₯ β (1(,)+β)) β
(((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) β β) |
38 | 37 | recnd 11242 |
. . . . 5
β’ ((π β§ π₯ β (1(,)+β)) β
(((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) β β) |
39 | | fzfid 13938 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯)) β Fin) |
40 | | ssun2 4174 |
. . . . . . . . . . 11
β’
(((ββ(π₯
/ π΄)) +
1)...(ββπ₯))
β ((1...(ββ(π₯ / π΄))) βͺ (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) |
41 | | pntsval.1 |
. . . . . . . . . . . 12
β’ π = (π β β β¦ Ξ£π β
(1...(ββπ))((Ξβπ) Β· ((logβπ) + (Οβ(π / π))))) |
42 | | pntrlog2bnd.t |
. . . . . . . . . . . 12
β’ π = (π β β β¦ if(π β β+, (π Β· (logβπ)), 0)) |
43 | | pntrlog2bndlem5.1 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β+) |
44 | | pntrlog2bndlem5.2 |
. . . . . . . . . . . 12
β’ (π β βπ¦ β β+
(absβ((π
βπ¦) / π¦)) β€ π΅) |
45 | | pntrlog2bndlem6.1 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
46 | | pntrlog2bndlem6.2 |
. . . . . . . . . . . 12
β’ (π β 1 β€ π΄) |
47 | 41, 11, 42, 43, 44, 45, 46 | pntrlog2bndlem6a 27085 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β
(1...(ββπ₯)) =
((1...(ββ(π₯ /
π΄))) βͺ
(((ββ(π₯ / π΄)) + 1)...(ββπ₯)))) |
48 | 40, 47 | sseqtrrid 4036 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯)) β
(1...(ββπ₯))) |
49 | 48 | sselda 3983 |
. . . . . . . . 9
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β (1...(ββπ₯))) |
50 | 49, 34 | syldan 592 |
. . . . . . . 8
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
51 | 39, 50 | fsumrecl 15680 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
52 | 22, 51 | remulcld 11244 |
. . . . . 6
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β β) |
53 | 52 | recnd 11242 |
. . . . 5
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β β) |
54 | 2 | recnd 11242 |
. . . . 5
β’ ((π β§ π₯ β (1(,)+β)) β π₯ β
β) |
55 | 10 | rpne0d 13021 |
. . . . 5
β’ ((π β§ π₯ β (1(,)+β)) β π₯ β 0) |
56 | 38, 53, 54, 55 | divdird 12028 |
. . . 4
β’ ((π β§ π₯ β (1(,)+β)) β
(((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) + ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) = (((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) + (((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯))) |
57 | 18 | recnd 11242 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β
((absβ(π
βπ₯)) Β· (logβπ₯)) β
β) |
58 | 36 | recnd 11242 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β β) |
59 | 57, 58, 53 | subsubd 11599 |
. . . . . 6
β’ ((π β§ π₯ β (1(,)+β)) β
(((absβ(π
βπ₯)) Β· (logβπ₯)) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))))) = ((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) + ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))))) |
60 | 22 | recnd 11242 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β (2 /
(logβπ₯)) β
β) |
61 | 35 | recnd 11242 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
62 | 51 | recnd 11242 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
63 | 60, 61, 62 | subdid 11670 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
(Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) = (((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))))) |
64 | | fzfid 13938 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β
(1...(ββ(π₯ /
π΄))) β
Fin) |
65 | | ssun1 4173 |
. . . . . . . . . . . . . . 15
β’
(1...(ββ(π₯ / π΄))) β ((1...(ββ(π₯ / π΄))) βͺ (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) |
66 | 65, 47 | sseqtrrid 4036 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1(,)+β)) β
(1...(ββ(π₯ /
π΄))) β
(1...(ββπ₯))) |
67 | 66 | sselda 3983 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββ(π₯ /
π΄)))) β π β
(1...(ββπ₯))) |
68 | 67, 34 | syldan 592 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββ(π₯ /
π΄)))) β
((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
69 | 64, 68 | fsumrecl 15680 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
70 | 69 | recnd 11242 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
71 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β+) |
72 | 45, 71, 46 | rpgecld 13055 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β
β+) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1(,)+β)) β π΄ β
β+) |
74 | 2, 73 | rerpdivcld 13047 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1(,)+β)) β (π₯ / π΄) β β) |
75 | | reflcl 13761 |
. . . . . . . . . . . . . 14
β’ ((π₯ / π΄) β β β
(ββ(π₯ / π΄)) β
β) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β
(ββ(π₯ / π΄)) β
β) |
77 | 76 | ltp1d 12144 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β
(ββ(π₯ / π΄)) < ((ββ(π₯ / π΄)) + 1)) |
78 | | fzdisj 13528 |
. . . . . . . . . . . 12
β’
((ββ(π₯ /
π΄)) <
((ββ(π₯ / π΄)) + 1) β
((1...(ββ(π₯ /
π΄))) β©
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))) = β
) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β
((1...(ββ(π₯ /
π΄))) β©
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))) = β
) |
80 | 34 | recnd 11242 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β ((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
81 | 79, 47, 23, 80 | fsumsplit 15687 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) = (Ξ£π β (1...(ββ(π₯ / π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)) + Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) |
82 | 70, 62, 81 | mvrraddd 11626 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) = Ξ£π β (1...(ββ(π₯ / π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ))) |
83 | 82 | oveq2d 7425 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
(Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) = ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββ(π₯ / π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)))) |
84 | 63, 83 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) = ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββ(π₯ / π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)))) |
85 | 84 | oveq2d 7425 |
. . . . . 6
β’ ((π β§ π₯ β (1(,)+β)) β
(((absβ(π
βπ₯)) Β· (logβπ₯)) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))))) = (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ))))) |
86 | 59, 85 | eqtr3d 2775 |
. . . . 5
β’ ((π β§ π₯ β (1(,)+β)) β
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) + ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) = (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ))))) |
87 | 86 | oveq1d 7424 |
. . . 4
β’ ((π β§ π₯ β (1(,)+β)) β
(((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) + ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) = ((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯)) |
88 | 56, 87 | eqtr3d 2775 |
. . 3
β’ ((π β§ π₯ β (1(,)+β)) β
(((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) + (((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯)) = ((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯)) |
89 | 88 | mpteq2dva 5249 |
. 2
β’ (π β (π₯ β (1(,)+β) β¦
(((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) + (((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯))) = (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯))) |
90 | 37, 10 | rerpdivcld 13047 |
. . 3
β’ ((π β§ π₯ β (1(,)+β)) β
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) β β) |
91 | 52, 10 | rerpdivcld 13047 |
. . 3
β’ ((π β§ π₯ β (1(,)+β)) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯) β β) |
92 | 41, 11, 42, 43, 44 | pntrlog2bndlem5 27084 |
. . 3
β’ (π β (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯)) β β€π(1)) |
93 | | ioossre 13385 |
. . . . 5
β’
(1(,)+β) β β |
94 | 93 | a1i 11 |
. . . 4
β’ (π β (1(,)+β) β
β) |
95 | | 1red 11215 |
. . . 4
β’ (π β 1 β
β) |
96 | 19 | a1i 11 |
. . . . 5
β’ (π β 2 β
β) |
97 | 43 | rpred 13016 |
. . . . . 6
β’ (π β π΅ β β) |
98 | 72 | relogcld 26131 |
. . . . . . 7
β’ (π β (logβπ΄) β
β) |
99 | 98, 95 | readdcld 11243 |
. . . . . 6
β’ (π β ((logβπ΄) + 1) β
β) |
100 | 97, 99 | remulcld 11244 |
. . . . 5
β’ (π β (π΅ Β· ((logβπ΄) + 1)) β β) |
101 | 96, 100 | remulcld 11244 |
. . . 4
β’ (π β (2 Β· (π΅ Β· ((logβπ΄) + 1))) β
β) |
102 | 51, 21 | rerpdivcld 13047 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β β) |
103 | 97 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β π΅ β
β) |
104 | 73 | relogcld 26131 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β
(logβπ΄) β
β) |
105 | 104, 5 | readdcld 11243 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β
((logβπ΄) + 1) β
β) |
106 | 103, 105 | remulcld 11244 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β (π΅ Β· ((logβπ΄) + 1)) β
β) |
107 | 2, 106 | remulcld 11244 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β (π₯ Β· (π΅ Β· ((logβπ΄) + 1))) β β) |
108 | | 2rp 12979 |
. . . . . . . . . 10
β’ 2 β
β+ |
109 | 108 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β 2 β
β+) |
110 | 109 | rpge0d 13020 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β 0 β€
2) |
111 | 103, 2 | remulcld 11244 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β (π΅ Β· π₯) β β) |
112 | 49, 25 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β β) |
113 | 112 | nnrecred 12263 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (1 / π) β β) |
114 | 39, 113 | fsumrecl 15680 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π) β β) |
115 | 111, 114 | remulcld 11244 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β ((π΅ Β· π₯) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π)) β β) |
116 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (logβπ₯) β
β+) |
117 | 50, 116 | rerpdivcld 13047 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β β) |
118 | 103 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π΅ β β) |
119 | 2 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π₯ β β) |
120 | 118, 119 | remulcld 11244 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π΅ Β· π₯) β β) |
121 | 120, 113 | remulcld 11244 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((π΅ Β· π₯) Β· (1 / π)) β β) |
122 | 49, 32 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (absβ(π
β(π₯ / π))) β β) |
123 | 119, 112 | nndivred 12266 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π₯ / π) β β) |
124 | 118, 123 | remulcld 11244 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π΅ Β· (π₯ / π)) β β) |
125 | 49, 27 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β β+) |
126 | 125 | relogcld 26131 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (logβπ) β β) |
127 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π₯ β β+) |
128 | 127 | relogcld 26131 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (logβπ₯) β β) |
129 | 49, 31 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π
β(π₯ / π)) β β) |
130 | 129 | absge0d 15391 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β 0 β€ (absβ(π
β(π₯ / π)))) |
131 | | elfzle2 13505 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯)) β π β€ (ββπ₯)) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β€ (ββπ₯)) |
133 | 112 | nnzd 12585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β β€) |
134 | | flge 13770 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π β β€) β (π β€ π₯ β π β€ (ββπ₯))) |
135 | 119, 133,
134 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π β€ π₯ β π β€ (ββπ₯))) |
136 | 132, 135 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β€ π₯) |
137 | 125, 127 | logled 26135 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π β€ π₯ β (logβπ) β€ (logβπ₯))) |
138 | 136, 137 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (logβπ) β€ (logβπ₯)) |
139 | 126, 128,
122, 130, 138 | lemul2ad 12154 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (logβπ)) β€ ((absβ(π
β(π₯ / π))) Β· (logβπ₯))) |
140 | 50, 122, 116 | ledivmul2d 13070 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ (absβ(π
β(π₯ / π))) β ((absβ(π
β(π₯ / π))) Β· (logβπ)) β€ ((absβ(π
β(π₯ / π))) Β· (logβπ₯)))) |
141 | 139, 140 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ (absβ(π
β(π₯ / π)))) |
142 | 123 | recnd 11242 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π₯ / π) β β) |
143 | 49, 28 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π₯ / π) β
β+) |
144 | 143 | rpne0d 13021 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π₯ / π) β 0) |
145 | 129, 142,
144 | absdivd 15402 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (absβ((π
β(π₯ / π)) / (π₯ / π))) = ((absβ(π
β(π₯ / π))) / (absβ(π₯ / π)))) |
146 | 10 | rpge0d 13020 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (1(,)+β)) β 0 β€ π₯) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β 0 β€ π₯) |
148 | 119, 125,
147 | divge0d 13056 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β 0 β€ (π₯ / π)) |
149 | 123, 148 | absidd 15369 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (absβ(π₯ / π)) = (π₯ / π)) |
150 | 149 | oveq2d 7425 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((absβ(π
β(π₯ / π))) / (absβ(π₯ / π))) = ((absβ(π
β(π₯ / π))) / (π₯ / π))) |
151 | 145, 150 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (absβ((π
β(π₯ / π)) / (π₯ / π))) = ((absβ(π
β(π₯ / π))) / (π₯ / π))) |
152 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π₯ / π) β (π
βπ¦) = (π
β(π₯ / π))) |
153 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π₯ / π) β π¦ = (π₯ / π)) |
154 | 152, 153 | oveq12d 7427 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (π₯ / π) β ((π
βπ¦) / π¦) = ((π
β(π₯ / π)) / (π₯ / π))) |
155 | 154 | fveq2d 6896 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (π₯ / π) β (absβ((π
βπ¦) / π¦)) = (absβ((π
β(π₯ / π)) / (π₯ / π)))) |
156 | 155 | breq1d 5159 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (π₯ / π) β ((absβ((π
βπ¦) / π¦)) β€ π΅ β (absβ((π
β(π₯ / π)) / (π₯ / π))) β€ π΅)) |
157 | 44 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β βπ¦ β β+
(absβ((π
βπ¦) / π¦)) β€ π΅) |
158 | 156, 157,
143 | rspcdva 3614 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (absβ((π
β(π₯ / π)) / (π₯ / π))) β€ π΅) |
159 | 151, 158 | eqbrtrrd 5173 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((absβ(π
β(π₯ / π))) / (π₯ / π)) β€ π΅) |
160 | 122, 118,
143 | ledivmul2d 13070 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (((absβ(π
β(π₯ / π))) / (π₯ / π)) β€ π΅ β (absβ(π
β(π₯ / π))) β€ (π΅ Β· (π₯ / π)))) |
161 | 159, 160 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (absβ(π
β(π₯ / π))) β€ (π΅ Β· (π₯ / π))) |
162 | 117, 122,
124, 141, 161 | letrd 11371 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ (π΅ Β· (π₯ / π))) |
163 | 118 | recnd 11242 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π΅ β β) |
164 | 54 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π₯ β β) |
165 | 112 | nncnd 12228 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β β) |
166 | 112 | nnne0d 12262 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β π β 0) |
167 | 163, 164,
165, 166 | divassd 12025 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((π΅ Β· π₯) / π) = (π΅ Β· (π₯ / π))) |
168 | 163, 164 | mulcld 11234 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π΅ Β· π₯) β β) |
169 | 168, 165,
166 | divrecd 11993 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((π΅ Β· π₯) / π) = ((π΅ Β· π₯) Β· (1 / π))) |
170 | 167, 169 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (π΅ Β· (π₯ / π)) = ((π΅ Β· π₯) Β· (1 / π))) |
171 | 162, 170 | breqtrd 5175 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ ((π΅ Β· π₯) Β· (1 / π))) |
172 | 39, 117, 121, 171 | fsumle 15745 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((π΅ Β· π₯) Β· (1 / π))) |
173 | 17 | recnd 11242 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β
(logβπ₯) β
β) |
174 | 49, 80 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (logβπ)) β β) |
175 | 21 | rpne0d 13021 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β
(logβπ₯) β
0) |
176 | 39, 173, 174, 175 | fsumdivc 15732 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) = Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯))) |
177 | 103 | recnd 11242 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β π΅ β
β) |
178 | 177, 54 | mulcld 11234 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β (π΅ Β· π₯) β β) |
179 | 113 | recnd 11242 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β (1(,)+β)) β§ π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))) β (1 / π) β β) |
180 | 39, 178, 179 | fsummulc2 15730 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β ((π΅ Β· π₯) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π)) = Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((π΅ Β· π₯) Β· (1 / π))) |
181 | 172, 176,
180 | 3brtr4d 5181 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ ((π΅ Β· π₯) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π))) |
182 | 43 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β π΅ β
β+) |
183 | 182 | rpge0d 13020 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β 0 β€ π΅) |
184 | 103, 2, 183, 146 | mulge0d 11791 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β 0 β€ (π΅ Β· π₯)) |
185 | 26 | nnrecred 12263 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
186 | 23, 185 | fsumrecl 15680 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββπ₯))(1 /
π) β
β) |
187 | 17, 104 | resubcld 11642 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β
((logβπ₯) β
(logβπ΄)) β
β) |
188 | 17, 5 | readdcld 11243 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β
((logβπ₯) + 1) β
β) |
189 | 67, 185 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββ(π₯ /
π΄)))) β (1 / π) β
β) |
190 | 64, 189 | fsumrecl 15680 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π) β β) |
191 | | harmonicubnd 26514 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ 1 β€
π₯) β Ξ£π β
(1...(ββπ₯))(1 /
π) β€ ((logβπ₯) + 1)) |
192 | 2, 9, 191 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββπ₯))(1 /
π) β€ ((logβπ₯) + 1)) |
193 | 10, 73 | relogdivd 26134 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1(,)+β)) β
(logβ(π₯ / π΄)) = ((logβπ₯) β (logβπ΄))) |
194 | 10, 73 | rpdivcld 13033 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (1(,)+β)) β (π₯ / π΄) β
β+) |
195 | | harmoniclbnd 26513 |
. . . . . . . . . . . . . . 15
β’ ((π₯ / π΄) β β+ β
(logβ(π₯ / π΄)) β€ Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π)) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1(,)+β)) β
(logβ(π₯ / π΄)) β€ Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π)) |
197 | 193, 196 | eqbrtrrd 5173 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β
((logβπ₯) β
(logβπ΄)) β€
Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π)) |
198 | 186, 187,
188, 190, 192, 197 | le2subd 11834 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β
(1...(ββπ₯))(1 /
π) β Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π)) β€ (((logβπ₯) + 1) β ((logβπ₯) β (logβπ΄)))) |
199 | 67, 25 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββ(π₯ /
π΄)))) β π β
β) |
200 | 199 | nnrecred 12263 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββ(π₯ /
π΄)))) β (1 / π) β
β) |
201 | 64, 200 | fsumrecl 15680 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π) β β) |
202 | 201 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π) β β) |
203 | 114 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π) β β) |
204 | 26 | nncnd 12228 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β π β
β) |
205 | 26 | nnne0d 12262 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β π β
0) |
206 | 204, 205 | reccld 11983 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β (1(,)+β)) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
207 | 79, 47, 23, 206 | fsumsplit 15687 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β
(1...(ββπ₯))(1 /
π) = (Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π) + Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π))) |
208 | 202, 203,
207 | mvrladdd 11627 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β
(1...(ββπ₯))(1 /
π) β Ξ£π β
(1...(ββ(π₯ /
π΄)))(1 / π)) = Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π)) |
209 | | 1cnd 11209 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β 1 β
β) |
210 | 104 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β
(logβπ΄) β
β) |
211 | 173, 209,
210 | pnncand 11610 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (1(,)+β)) β
(((logβπ₯) + 1)
β ((logβπ₯)
β (logβπ΄))) =
(1 + (logβπ΄))) |
212 | 209, 210,
211 | comraddd 11428 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β
(((logβπ₯) + 1)
β ((logβπ₯)
β (logβπ΄))) =
((logβπ΄) +
1)) |
213 | 198, 208,
212 | 3brtr3d 5180 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π) β€ ((logβπ΄) + 1)) |
214 | 114, 105,
111, 184, 213 | lemul2ad 12154 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β ((π΅ Β· π₯) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π)) β€ ((π΅ Β· π₯) Β· ((logβπ΄) + 1))) |
215 | 105 | recnd 11242 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (1(,)+β)) β
((logβπ΄) + 1) β
β) |
216 | 177, 54, 215 | mulassd 11237 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β ((π΅ Β· π₯) Β· ((logβπ΄) + 1)) = (π΅ Β· (π₯ Β· ((logβπ΄) + 1)))) |
217 | 177, 54, 215 | mul12d 11423 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (1(,)+β)) β (π΅ Β· (π₯ Β· ((logβπ΄) + 1))) = (π₯ Β· (π΅ Β· ((logβπ΄) + 1)))) |
218 | 216, 217 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (1(,)+β)) β ((π΅ Β· π₯) Β· ((logβπ΄) + 1)) = (π₯ Β· (π΅ Β· ((logβπ΄) + 1)))) |
219 | 214, 218 | breqtrd 5175 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β ((π΅ Β· π₯) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))(1 / π)) β€ (π₯ Β· (π΅ Β· ((logβπ΄) + 1)))) |
220 | 102, 115,
107, 181, 219 | letrd 11371 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β (Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)) β€ (π₯ Β· (π΅ Β· ((logβπ΄) + 1)))) |
221 | 102, 107,
20, 110, 220 | lemul2ad 12154 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β (2 Β·
(Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯))) β€ (2 Β· (π₯ Β· (π΅ Β· ((logβπ΄) + 1))))) |
222 | | 2cnd 12290 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β 2 β
β) |
223 | 222, 173,
62, 175 | div32d 12013 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) = (2 Β· (Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)) / (logβπ₯)))) |
224 | 210, 209 | addcld 11233 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1(,)+β)) β
((logβπ΄) + 1) β
β) |
225 | 177, 224 | mulcld 11234 |
. . . . . . . 8
β’ ((π β§ π₯ β (1(,)+β)) β (π΅ Β· ((logβπ΄) + 1)) β
β) |
226 | 54, 222, 225 | mul12d 11423 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β (π₯ Β· (2 Β· (π΅ Β· ((logβπ΄) + 1)))) = (2 Β· (π₯ Β· (π΅ Β· ((logβπ΄) + 1))))) |
227 | 221, 223,
226 | 3brtr4d 5181 |
. . . . . 6
β’ ((π β§ π₯ β (1(,)+β)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β€ (π₯ Β· (2 Β· (π΅ Β· ((logβπ΄) + 1))))) |
228 | 101 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (1(,)+β)) β (2 Β·
(π΅ Β·
((logβπ΄) + 1)))
β β) |
229 | 52, 228, 10 | ledivmuld 13069 |
. . . . . 6
β’ ((π β§ π₯ β (1(,)+β)) β ((((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯) β€ (2 Β· (π΅ Β· ((logβπ΄) + 1))) β ((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) β€ (π₯ Β· (2 Β· (π΅ Β· ((logβπ΄) + 1)))))) |
230 | 227, 229 | mpbird 257 |
. . . . 5
β’ ((π β§ π₯ β (1(,)+β)) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯) β€ (2 Β· (π΅ Β· ((logβπ΄) + 1)))) |
231 | 230 | adantrr 716 |
. . . 4
β’ ((π β§ (π₯ β (1(,)+β) β§ 1 β€ π₯)) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯) β€ (2 Β· (π΅ Β· ((logβπ΄) + 1)))) |
232 | 94, 91, 95, 101, 231 | ello1d 15467 |
. . 3
β’ (π β (π₯ β (1(,)+β) β¦ (((2 /
(logβπ₯)) Β·
Ξ£π β
(((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯)) β β€π(1)) |
233 | 90, 91, 92, 232 | lo1add 15571 |
. 2
β’ (π β (π₯ β (1(,)+β) β¦
(((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯) + (((2 / (logβπ₯)) Β· Ξ£π β (((ββ(π₯ / π΄)) + 1)...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (logβπ))) / π₯))) β β€π(1)) |
234 | 89, 233 | eqeltrrd 2835 |
1
β’ (π β (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββ(π₯ /
π΄)))((absβ(π
β(π₯ / π))) Β· (logβπ)))) / π₯)) β β€π(1)) |