Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . . . . . 10
β’ (π β β β
(1...π) β
Fin) |
2 | | dvdsssfz1 16207 |
. . . . . . . . . 10
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
3 | 1, 2 | ssfid 9218 |
. . . . . . . . 9
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β Fin) |
4 | | ssrab2 4042 |
. . . . . . . . . . . 12
β’ {π₯ β β β£ π₯ β₯ π} β β |
5 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β π β {π₯ β β β£ π₯ β₯ π}) |
6 | 4, 5 | sselid 3947 |
. . . . . . . . . . 11
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
7 | | vmacl 26483 |
. . . . . . . . . . 11
β’ (π β β β
(Ξβπ) β
β) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (Ξβπ) β β) |
9 | | dvdsdivcl 16205 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β {π₯ β β β£ π₯ β₯ π}) |
10 | 4, 9 | sselid 3947 |
. . . . . . . . . . 11
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β β) |
11 | | vmacl 26483 |
. . . . . . . . . . 11
β’ ((π / π) β β β
(Ξβ(π / π)) β
β) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (Ξβ(π / π)) β β) |
13 | 8, 12 | remulcld 11192 |
. . . . . . . . 9
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
14 | 3, 13 | fsumrecl 15626 |
. . . . . . . 8
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) β β) |
15 | | vmacl 26483 |
. . . . . . . . 9
β’ (π β β β
(Ξβπ) β
β) |
16 | | nnrp 12933 |
. . . . . . . . . 10
β’ (π β β β π β
β+) |
17 | 16 | relogcld 25994 |
. . . . . . . . 9
β’ (π β β β
(logβπ) β
β) |
18 | 15, 17 | remulcld 11192 |
. . . . . . . 8
β’ (π β β β
((Ξβπ)
Β· (logβπ))
β β) |
19 | 14, 18 | readdcld 11191 |
. . . . . . 7
β’ (π β β β
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) β β) |
20 | 19 | recnd 11190 |
. . . . . 6
β’ (π β β β
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) β β) |
21 | 20 | adantl 483 |
. . . . 5
β’ ((π β β β§ π β β) β
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) β β) |
22 | 21 | fmpttd 7068 |
. . . 4
β’ (π β β β (π β β β¦
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))):ββΆβ) |
23 | | ssrab2 4042 |
. . . . . . . . 9
β’ {π₯ β β β£ π₯ β₯ π} β β |
24 | | simpr 486 |
. . . . . . . . 9
β’ (((π β β β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β {π₯ β β β£ π₯ β₯ π}) |
25 | 23, 24 | sselid 3947 |
. . . . . . . 8
β’ (((π β β β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
26 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π = π β (π₯ β₯ π β π₯ β₯ π)) |
27 | 26 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π = π β {π₯ β β β£ π₯ β₯ π} = {π₯ β β β£ π₯ β₯ π}) |
28 | | fvoveq1 7385 |
. . . . . . . . . . . . 13
β’ (π = π β (Ξβ(π / π)) = (Ξβ(π / π))) |
29 | 28 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = π β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ(π / π)))) |
30 | 29 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = π β§ π β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ(π / π)))) |
31 | 27, 30 | sumeq12dv 15598 |
. . . . . . . . . 10
β’ (π = π β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) |
32 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (Ξβπ) = (Ξβπ)) |
33 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (logβπ) = (logβπ)) |
34 | 32, 33 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β ((Ξβπ) Β· (logβπ)) = ((Ξβπ) Β· (logβπ))) |
35 | 31, 34 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
36 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) = (π β β β¦ (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
37 | | ovex 7395 |
. . . . . . . . 9
β’
(Ξ£π β
{π₯ β β β£
π₯ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) β V |
38 | 35, 36, 37 | fvmpt3i 6958 |
. . . . . . . 8
β’ (π β β β ((π β β β¦
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
39 | 25, 38 | syl 17 |
. . . . . . 7
β’ (((π β β β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π β β β¦ (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
40 | 39 | sumeq2dv 15595 |
. . . . . 6
β’ ((π β β β§ π β β) β
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((π β β β¦ (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
41 | | logsqvma 26906 |
. . . . . . 7
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) = ((logβπ)β2)) |
42 | 41 | adantl 483 |
. . . . . 6
β’ ((π β β β§ π β β) β
Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) = ((logβπ)β2)) |
43 | 40, 42 | eqtr2d 2778 |
. . . . 5
β’ ((π β β β§ π β β) β
((logβπ)β2) =
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((π β β β¦ (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ)) |
44 | 43 | mpteq2dva 5210 |
. . . 4
β’ (π β β β (π β β β¦
((logβπ)β2)) =
(π β β β¦
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((π β β β¦ (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ))) |
45 | 22, 44 | muinv 26558 |
. . 3
β’ (π β β β (π β β β¦
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ ((logβπ)β2))β(π / π))))) |
46 | 45 | fveq1d 6849 |
. 2
β’ (π β β β ((π β β β¦
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ) = ((π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ ((logβπ)β2))β(π / π))))βπ)) |
47 | | breq2 5114 |
. . . . . 6
β’ (π = π β (π₯ β₯ π β π₯ β₯ π)) |
48 | 47 | rabbidv 3418 |
. . . . 5
β’ (π = π β {π₯ β β β£ π₯ β₯ π} = {π₯ β β β£ π₯ β₯ π}) |
49 | | fvoveq1 7385 |
. . . . . . 7
β’ (π = π β (Ξβ(π / π)) = (Ξβ(π / π))) |
50 | 49 | oveq2d 7378 |
. . . . . 6
β’ (π = π β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ(π / π)))) |
51 | 50 | adantr 482 |
. . . . 5
β’ ((π = π β§ π β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ(π / π)))) |
52 | 48, 51 | sumeq12dv 15598 |
. . . 4
β’ (π = π β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) |
53 | | fveq2 6847 |
. . . . 5
β’ (π = π β (Ξβπ) = (Ξβπ)) |
54 | | fveq2 6847 |
. . . . 5
β’ (π = π β (logβπ) = (logβπ)) |
55 | 53, 54 | oveq12d 7380 |
. . . 4
β’ (π = π β ((Ξβπ) Β· (logβπ)) = ((Ξβπ) Β· (logβπ))) |
56 | 52, 55 | oveq12d 7380 |
. . 3
β’ (π = π β (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
57 | 56, 36, 37 | fvmpt3i 6958 |
. 2
β’ (π β β β ((π β β β¦
(Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))))βπ) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
58 | | fveq2 6847 |
. . . . . 6
β’ (π = π β (ΞΌβπ) = (ΞΌβπ)) |
59 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (π / π) = (π / π)) |
60 | 59 | fveq2d 6851 |
. . . . . . 7
β’ (π = π β (logβ(π / π)) = (logβ(π / π))) |
61 | 60 | oveq1d 7377 |
. . . . . 6
β’ (π = π β ((logβ(π / π))β2) = ((logβ(π / π))β2)) |
62 | 58, 61 | oveq12d 7380 |
. . . . 5
β’ (π = π β ((ΞΌβπ) Β· ((logβ(π / π))β2)) = ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
63 | 62 | cbvsumv 15588 |
. . . 4
β’
Ξ£π β
{π₯ β β β£
π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) |
64 | | breq2 5114 |
. . . . . 6
β’ (π = π β (π₯ β₯ π β π₯ β₯ π)) |
65 | 64 | rabbidv 3418 |
. . . . 5
β’ (π = π β {π₯ β β β£ π₯ β₯ π} = {π₯ β β β£ π₯ β₯ π}) |
66 | | fvoveq1 7385 |
. . . . . . . 8
β’ (π = π β (logβ(π / π)) = (logβ(π / π))) |
67 | 66 | oveq1d 7377 |
. . . . . . 7
β’ (π = π β ((logβ(π / π))β2) = ((logβ(π / π))β2)) |
68 | 67 | oveq2d 7378 |
. . . . . 6
β’ (π = π β ((ΞΌβπ) Β· ((logβ(π / π))β2)) = ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
69 | 68 | adantr 482 |
. . . . 5
β’ ((π = π β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· ((logβ(π / π))β2)) = ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
70 | 65, 69 | sumeq12dv 15598 |
. . . 4
β’ (π = π β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
71 | 63, 70 | eqtrid 2789 |
. . 3
β’ (π = π β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
72 | | ssrab2 4042 |
. . . . . . . 8
β’ {π₯ β β β£ π₯ β₯ π} β β |
73 | | dvdsdivcl 16205 |
. . . . . . . 8
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β {π₯ β β β£ π₯ β₯ π}) |
74 | 72, 73 | sselid 3947 |
. . . . . . 7
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β β) |
75 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = (π / π) β (logβπ) = (logβ(π / π))) |
76 | 75 | oveq1d 7377 |
. . . . . . . 8
β’ (π = (π / π) β ((logβπ)β2) = ((logβ(π / π))β2)) |
77 | | eqid 2737 |
. . . . . . . 8
β’ (π β β β¦
((logβπ)β2)) =
(π β β β¦
((logβπ)β2)) |
78 | | ovex 7395 |
. . . . . . . 8
β’
((logβπ)β2) β V |
79 | 76, 77, 78 | fvmpt3i 6958 |
. . . . . . 7
β’ ((π / π) β β β ((π β β β¦ ((logβπ)β2))β(π / π)) = ((logβ(π / π))β2)) |
80 | 74, 79 | syl 17 |
. . . . . 6
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π β β β¦ ((logβπ)β2))β(π / π)) = ((logβ(π / π))β2)) |
81 | 80 | oveq2d 7378 |
. . . . 5
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· ((π β β β¦ ((logβπ)β2))β(π / π))) = ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
82 | 81 | sumeq2dv 15595 |
. . . 4
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ ((logβπ)β2))β(π / π))) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
83 | 82 | mpteq2ia 5213 |
. . 3
β’ (π β β β¦
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ ((logβπ)β2))β(π / π)))) = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
84 | | sumex 15579 |
. . 3
β’
Ξ£π β
{π₯ β β β£
π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) β V |
85 | 71, 83, 84 | fvmpt3i 6958 |
. 2
β’ (π β β β ((π β β β¦
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ ((logβπ)β2))β(π / π))))βπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
86 | 46, 57, 85 | 3eqtr3rd 2786 |
1
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |