Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
2 | 1 | a1i 11 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β β) |
3 | | elioore 13301 |
. . . . . . . . . . . . 13
β’ (π₯ β (1(,)+β) β
π₯ β
β) |
4 | 3 | adantl 483 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
5 | | 1rp 12926 |
. . . . . . . . . . . . 13
β’ 1 β
β+ |
6 | 5 | a1i 11 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β+) |
7 | | 1red 11163 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β) |
8 | | eliooord 13330 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (1(,)+β) β (1
< π₯ β§ π₯ <
+β)) |
9 | 8 | adantl 483 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (1 < π₯ β§ π₯ < +β)) |
10 | 9 | simpld 496 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β 1 < π₯) |
11 | 7, 4, 10 | ltled 11310 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β€ π₯) |
12 | 4, 6, 11 | rpgecld 13003 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β+) |
13 | | pntrval.r |
. . . . . . . . . . . . 13
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
14 | 13 | pntrf 26927 |
. . . . . . . . . . . 12
β’ π
:β+βΆβ |
15 | 14 | ffvelcdmi 7039 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π
βπ₯) β
β) |
16 | 12, 15 | syl 17 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (π
βπ₯) β β) |
17 | 12 | relogcld 25994 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
18 | 16, 17 | remulcld 11192 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((π
βπ₯) Β· (logβπ₯)) β β) |
19 | 2, 18 | remulcld 11192 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· ((π
βπ₯) Β· (logβπ₯))) β β) |
20 | 19 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· ((π
βπ₯) Β· (logβπ₯))) β β) |
21 | 4, 10 | rplogcld 26000 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β
β+) |
22 | 2, 21 | rerpdivcld 12995 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (2 / (logβπ₯)) β β) |
23 | 22 | recnd 11190 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (2 / (logβπ₯)) β β) |
24 | | fzfid 13885 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (1...(ββπ₯)) β Fin) |
25 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π₯ β β+) |
26 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β
(1...(ββπ₯))
β π β
β) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
28 | 27 | nnrpd 12962 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β+) |
29 | 25, 28 | rpdivcld 12981 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π₯ / π) β
β+) |
30 | 14 | ffvelcdmi 7039 |
. . . . . . . . . . . 12
β’ ((π₯ / π) β β+ β (π
β(π₯ / π)) β β) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / π)) β β) |
32 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (1...π) β Fin) |
33 | | dvdsssfz1 16207 |
. . . . . . . . . . . . . . 15
β’ (π β β β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
35 | 32, 34 | ssfid 9218 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β {π¦ β β β£ π¦ β₯ π} β Fin) |
36 | | ssrab2 4042 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β β β£ π¦ β₯ π} β β |
37 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β π β {π¦ β β β£ π¦ β₯ π}) |
38 | 36, 37 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β π β β) |
39 | | vmacl 26483 |
. . . . . . . . . . . . . . 15
β’ (π β β β
(Ξβπ) β
β) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβπ) β β) |
41 | | dvdsdivcl 16205 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
42 | 27, 41 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
43 | 36, 42 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β β) |
44 | | vmacl 26483 |
. . . . . . . . . . . . . . 15
β’ ((π / π) β β β
(Ξβ(π / π)) β
β) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβ(π / π)) β β) |
46 | 40, 45 | remulcld 11192 |
. . . . . . . . . . . . 13
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
47 | 35, 46 | fsumrecl 15626 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β β) |
48 | | vmacl 26483 |
. . . . . . . . . . . . . 14
β’ (π β β β
(Ξβπ) β
β) |
49 | 27, 48 | syl 17 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
50 | 28 | relogcld 25994 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβπ) β
β) |
51 | 49, 50 | remulcld 11192 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· (logβπ))
β β) |
52 | 47, 51 | resubcld 11590 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))) β
β) |
53 | 31, 52 | remulcld 11192 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
54 | 24, 53 | fsumrecl 15626 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
55 | 54 | recnd 11190 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) β
β) |
56 | 23, 55 | mulcld 11182 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β
β) |
57 | 20, 56 | subcld 11519 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) β
β) |
58 | 4 | recnd 11190 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
59 | | 2cnd 12238 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β β) |
60 | 12 | rpne0d 12969 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β 0) |
61 | | 2ne0 12264 |
. . . . . . 7
β’ 2 β
0 |
62 | 61 | a1i 11 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β 0) |
63 | 57, 58, 59, 60, 62 | divdiv32d 11963 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) / 2) = ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / 2) / π₯)) |
64 | 57, 58, 60 | divcld 11938 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) β β) |
65 | 64, 59, 62 | divrecd 11941 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) / 2) = ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) Β· (1 / 2))) |
66 | 20, 56, 59, 62 | divsubdird 11977 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / 2) = (((2 Β·
((π
βπ₯) Β· (logβπ₯))) / 2) β (((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / 2))) |
67 | 18 | recnd 11190 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((π
βπ₯) Β· (logβπ₯)) β β) |
68 | 67, 59, 62 | divcan3d 11943 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) / 2) = ((π
βπ₯) Β· (logβπ₯))) |
69 | 21 | rpcnd 12966 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
70 | 21 | rpne0d 12969 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β 0) |
71 | 59, 69, 55, 70 | div32d 11961 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) = (2 Β·
(Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) |
72 | 71 | oveq1d 7377 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / 2) = ((2 Β·
(Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / 2)) |
73 | 54, 21 | rerpdivcld 12995 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)) β
β) |
74 | 73 | recnd 11190 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)) β
β) |
75 | 74, 59, 62 | divcan3d 11943 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / 2) = (Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) |
76 | 72, 75 | eqtrd 2777 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / 2) = (Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) |
77 | 68, 76 | oveq12d 7380 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) / 2) β (((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) / 2)) = (((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) |
78 | 66, 77 | eqtrd 2777 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / 2) = (((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯)))) |
79 | 78 | oveq1d 7377 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / 2) / π₯) = ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) |
80 | 63, 65, 79 | 3eqtr3d 2785 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) Β· (1 / 2)) = ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) |
81 | 80 | mpteq2dva 5210 |
. . 3
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) Β· (1 / 2))) = (π₯ β (1(,)+β) β¦ ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯))) |
82 | 22, 54 | remulcld 11192 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) β
β) |
83 | 19, 82 | resubcld 11590 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) β
β) |
84 | 83, 12 | rerpdivcld 12995 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) β β) |
85 | 7 | rehalfcld 12407 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β (1 / 2) β β) |
86 | 31 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / π)) β β) |
87 | 47 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β β) |
88 | 49 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
89 | 50 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβπ) β
β) |
90 | 88, 89 | mulcld 11182 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· (logβπ))
β β) |
91 | 86, 87, 90 | subdid 11618 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) = (((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β· (logβπ))))) |
92 | 86, 88, 89 | mul12d 11371 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β· (logβπ))) = ((Ξβπ) Β· ((π
β(π₯ / π)) Β· (logβπ)))) |
93 | 88, 86, 89 | mulassd 11185 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ)
Β· (π
β(π₯ / π))) Β· (logβπ)) = ((Ξβπ) Β· ((π
β(π₯ / π)) Β· (logβπ)))) |
94 | 92, 93 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β· (logβπ))) = (((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))) |
95 | 94 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β· (logβπ)))) = (((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β (((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) |
96 | 91, 95 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) = (((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β (((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) |
97 | 96 | sumeq2dv 15595 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) = Ξ£π β (1...(ββπ₯))(((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β (((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) |
98 | 86, 87 | mulcld 11182 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β β) |
99 | 88, 86 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· (π
β(π₯ / π))) β β) |
100 | 99, 89 | mulcld 11182 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ)
Β· (π
β(π₯ / π))) Β· (logβπ)) β β) |
101 | 24, 98, 100 | fsumsub 15680 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β (((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))) = (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) |
102 | 46 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
103 | 35, 86, 102 | fsummulc2 15676 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = Ξ£π β {π¦ β β β£ π¦ β₯ π} ((π
β(π₯ / π)) Β· ((Ξβπ) Β·
(Ξβ(π / π))))) |
104 | 103 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((π
β(π₯ / π)) Β· ((Ξβπ) Β·
(Ξβ(π / π))))) |
105 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π Β· π) β (π₯ / π) = (π₯ / (π Β· π))) |
106 | 105 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π Β· π) β (π
β(π₯ / π)) = (π
β(π₯ / (π Β· π)))) |
107 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π Β· π) β (Ξβ(π / π)) = (Ξβ((π Β· π) / π))) |
108 | 107 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π Β· π) β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ((π Β· π) / π)))) |
109 | 106, 108 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π Β· π) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β·
(Ξβ(π / π)))) = ((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π))))) |
110 | 31 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β (π
β(π₯ / π)) β β) |
111 | 40 | anasss 468 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β (Ξβπ) β β) |
112 | 45 | anasss 468 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β (Ξβ(π / π)) β β) |
113 | 111, 112 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β ((Ξβπ) Β·
(Ξβ(π / π))) β
β) |
114 | 110, 113 | remulcld 11192 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β·
(Ξβ(π / π)))) β
β) |
115 | 114 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β ((π
β(π₯ / π)) Β· ((Ξβπ) Β·
(Ξβ(π / π)))) β
β) |
116 | 109, 4, 115 | dvdsflsumcom 26553 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((π
β(π₯ / π)) Β· ((Ξβπ) Β·
(Ξβ(π / π)))) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π))))) |
117 | 58 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π₯ β β) |
118 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β
(1...(ββπ₯))
β π β
β) |
119 | 118 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
120 | 119 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β+) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β+) |
122 | 121 | rpcnd 12966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
123 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
125 | 124 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
126 | 121 | rpne0d 12969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β 0) |
127 | 124 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β 0) |
128 | 117, 122,
125, 126, 127 | divdiv1d 11969 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((π₯ / π) / π) = (π₯ / (π Β· π))) |
129 | 128 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (π₯ / (π Β· π)) = ((π₯ / π) / π)) |
130 | 129 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (π
β(π₯ / (π Β· π))) = (π
β((π₯ / π) / π))) |
131 | 125, 122,
126 | divcan3d 11943 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((π Β· π) / π) = π) |
132 | 131 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (Ξβ((π Β· π) / π)) = (Ξβπ)) |
133 | 132 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) Β·
(Ξβ((π
Β· π) / π))) = ((Ξβπ) Β· (Ξβπ))) |
134 | 130, 133 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π)))) = ((π
β((π₯ / π) / π)) Β· ((Ξβπ) Β· (Ξβπ)))) |
135 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π₯ β β+) |
136 | 135, 121 | rpdivcld 12981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (π₯ / π) β
β+) |
137 | 124 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β+) |
138 | 136, 137 | rpdivcld 12981 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((π₯ / π) / π) β
β+) |
139 | 14 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ / π) / π) β β+ β (π
β((π₯ / π) / π)) β β) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (π
β((π₯ / π) / π)) β β) |
141 | 140 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (π
β((π₯ / π) / π)) β β) |
142 | 119, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
143 | 142 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (Ξβπ) β
β) |
145 | | vmacl 26483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β
(Ξβπ) β
β) |
146 | 124, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (Ξβπ) β
β) |
147 | 146 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (Ξβπ) β
β) |
148 | 144, 147 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) Β· (Ξβπ)) β
β) |
149 | 141, 148 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((π
β((π₯ / π) / π)) Β· ((Ξβπ) Β· (Ξβπ))) = (((Ξβπ) Β· (Ξβπ)) Β· (π
β((π₯ / π) / π)))) |
150 | 144, 147,
141 | mulassd 11185 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (((Ξβπ) Β· (Ξβπ)) Β· (π
β((π₯ / π) / π))) = ((Ξβπ) Β· ((Ξβπ) Β· (π
β((π₯ / π) / π))))) |
151 | 134, 149,
150 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . 19
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π)))) = ((Ξβπ) Β·
((Ξβπ)
Β· (π
β((π₯ / π) / π))))) |
152 | 151 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π)))) = Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· ((Ξβπ) Β· (π
β((π₯ / π) / π))))) |
153 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(1...(ββ(π₯ /
π))) β
Fin) |
154 | 146, 140 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) Β· (π
β((π₯ / π) / π))) β β) |
155 | 154 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) Β· (π
β((π₯ / π) / π))) β β) |
156 | 153, 143,
155 | fsummulc2 15676 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) = Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· ((Ξβπ) Β· (π
β((π₯ / π) / π))))) |
157 | 152, 156 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π)))) = ((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) |
158 | 157 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((π
β(π₯ / (π Β· π))) Β· ((Ξβπ) Β·
(Ξβ((π
Β· π) / π)))) = Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) |
159 | 104, 116,
158 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) |
160 | 159 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))) = (Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) |
161 | 97, 101, 160 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) = (Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) |
162 | 161 | oveq2d 7378 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) = ((2 / (logβπ₯)) Β· (Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))))) |
163 | 153, 154 | fsumrecl 15626 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))) β β) |
164 | 142, 163 | remulcld 11192 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β β) |
165 | 24, 164 | fsumrecl 15626 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β β) |
166 | 165 | recnd 11190 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β β) |
167 | 49, 31 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ)
Β· (π
β(π₯ / π))) β β) |
168 | 167, 50 | remulcld 11192 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ)
Β· (π
β(π₯ / π))) Β· (logβπ)) β β) |
169 | 24, 168 | fsumrecl 15626 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)) β β) |
170 | 169 | recnd 11190 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)) β β) |
171 | 23, 166, 170 | subdid 11618 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· (Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))) β Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) = (((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))))) |
172 | 162, 171 | eqtrd 2777 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ))))) = (((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))))) |
173 | 172 | oveq2d 7378 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) = ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β (((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))))) |
174 | 23, 166 | mulcld 11182 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) β β) |
175 | 22, 169 | remulcld 11192 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))) β β) |
176 | 175 | recnd 11190 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))) β β) |
177 | 20, 174, 176 | subsub3d 11549 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β (((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))))) = (((2 Β· ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))))) |
178 | 173, 177 | eqtrd 2777 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) = (((2 Β· ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))))) |
179 | 67 | 2timesd 12403 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· ((π
βπ₯) Β· (logβπ₯))) = (((π
βπ₯) Β· (logβπ₯)) + ((π
βπ₯) Β· (logβπ₯)))) |
180 | 179 | oveq1d 7377 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) = ((((π
βπ₯) Β· (logβπ₯)) + ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))))) |
181 | 67, 176, 67 | add32d 11389 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + ((π
βπ₯) Β· (logβπ₯))) = ((((π
βπ₯) Β· (logβπ₯)) + ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ))))) |
182 | 180, 181 | eqtr4d 2780 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) = ((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + ((π
βπ₯) Β· (logβπ₯)))) |
183 | 182 | oveq1d 7377 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) = (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))))) |
184 | 18, 175 | readdcld 11191 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) β β) |
185 | 184 | recnd 11190 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) β β) |
186 | 185, 67, 174 | addsubassd 11539 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) = ((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + (((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))))) |
187 | 178, 183,
186 | 3eqtrd 2781 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) = ((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + (((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))))) |
188 | 187 | oveq1d 7377 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) = (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + (((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))))) / π₯)) |
189 | 67, 174 | subcld 11519 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) β β) |
190 | 185, 189,
58, 60 | divdird 11976 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) + (((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))))) / π₯) = (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯) + ((((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯))) |
191 | 188, 190 | eqtrd 2777 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) = (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯) + ((((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯))) |
192 | 191 | mpteq2dva 5210 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯)) = (π₯ β (1(,)+β) β¦ (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯) + ((((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯)))) |
193 | 184, 12 | rerpdivcld 12995 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯) β β) |
194 | 22, 165 | remulcld 11192 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))((Ξβπ) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β· (π
β((π₯ / π) / π))))) β β) |
195 | 18, 194 | resubcld 11590 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) β β) |
196 | 195, 12 | rerpdivcld 12995 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯) β β) |
197 | 13 | selberg3r 26933 |
. . . . . . 7
β’ (π₯ β (1(,)+β) β¦
((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯)) β π(1) |
198 | 197 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯)) β π(1)) |
199 | 13 | selberg4r 26934 |
. . . . . . 7
β’ (π₯ β (1(,)+β) β¦
((((π
βπ₯) Β· (logβπ₯)) β ((2 /
(logβπ₯)) Β·
Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯)) β π(1) |
200 | 199 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯)) β π(1)) |
201 | 193, 196,
198, 200 | o1add2 15513 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((((π
βπ₯) Β· (logβπ₯)) + ((2 / (logβπ₯)) Β· Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (π
β(π₯ / π))) Β· (logβπ)))) / π₯) + ((((π
βπ₯) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (π
β((π₯ / π) / π)))))) / π₯))) β π(1)) |
202 | 192, 201 | eqeltrd 2838 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯)) β π(1)) |
203 | | ioossre 13332 |
. . . . 5
β’
(1(,)+β) β β |
204 | | 1cnd 11157 |
. . . . . 6
β’ (β€
β 1 β β) |
205 | 204 | halfcld 12405 |
. . . . 5
β’ (β€
β (1 / 2) β β) |
206 | | o1const 15509 |
. . . . 5
β’
(((1(,)+β) β β β§ (1 / 2) β β) β
(π₯ β (1(,)+β)
β¦ (1 / 2)) β π(1)) |
207 | 203, 205,
206 | sylancr 588 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ (1 / 2)) β π(1)) |
208 | 84, 85, 202, 207 | o1mul2 15514 |
. . 3
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((2 Β· ((π
βπ₯) Β· (logβπ₯))) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))))) / π₯) Β· (1 / 2))) β
π(1)) |
209 | 81, 208 | eqeltrrd 2839 |
. 2
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) β π(1)) |
210 | 209 | mptru 1549 |
1
β’ (π₯ β (1(,)+β) β¦
((((π
βπ₯) Β· (logβπ₯)) β (Ξ£π β
(1...(ββπ₯))((π
β(π₯ / π)) Β· (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β ((Ξβπ) Β· (logβπ)))) / (logβπ₯))) / π₯)) β π(1) |