Step | Hyp | Ref
| Expression |
1 | | fzfid 13944 |
. . . 4
β’ (π β β β
(1...π) β
Fin) |
2 | | dvdsssfz1 16268 |
. . . 4
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
3 | 1, 2 | ssfid 9269 |
. . 3
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β Fin) |
4 | | fzfid 13944 |
. . . . 5
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (1...π) β Fin) |
5 | | elrabi 3672 |
. . . . . . 7
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β β) |
6 | 5 | adantl 481 |
. . . . . 6
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
7 | | dvdsssfz1 16268 |
. . . . . 6
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
8 | 6, 7 | syl 17 |
. . . . 5
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
9 | 4, 8 | ssfid 9269 |
. . . 4
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ π} β Fin) |
10 | | elrabi 3672 |
. . . . . . . . 9
β’ (π’ β {π₯ β β β£ π₯ β₯ π} β π’ β β) |
11 | 10 | ad2antll 726 |
. . . . . . . 8
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β π’ β β) |
12 | | vmacl 27005 |
. . . . . . . 8
β’ (π’ β β β
(Ξβπ’) β
β) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β (Ξβπ’) β β) |
14 | | breq1 5144 |
. . . . . . . . . . . 12
β’ (π₯ = π’ β (π₯ β₯ π β π’ β₯ π)) |
15 | 14 | elrab 3678 |
. . . . . . . . . . 11
β’ (π’ β {π₯ β β β£ π₯ β₯ π} β (π’ β β β§ π’ β₯ π)) |
16 | 15 | simprbi 496 |
. . . . . . . . . 10
β’ (π’ β {π₯ β β β£ π₯ β₯ π} β π’ β₯ π) |
17 | 16 | ad2antll 726 |
. . . . . . . . 9
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β π’ β₯ π) |
18 | 5 | ad2antrl 725 |
. . . . . . . . . 10
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β π β β) |
19 | | nndivdvds 16213 |
. . . . . . . . . 10
β’ ((π β β β§ π’ β β) β (π’ β₯ π β (π / π’) β β)) |
20 | 18, 11, 19 | syl2anc 583 |
. . . . . . . . 9
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β (π’ β₯ π β (π / π’) β β)) |
21 | 17, 20 | mpbid 231 |
. . . . . . . 8
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β (π / π’) β β) |
22 | | vmacl 27005 |
. . . . . . . 8
β’ ((π / π’) β β β
(Ξβ(π / π’)) β
β) |
23 | 21, 22 | syl 17 |
. . . . . . 7
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β (Ξβ(π / π’)) β β) |
24 | 13, 23 | remulcld 11248 |
. . . . . 6
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β ((Ξβπ’) Β·
(Ξβ(π / π’))) β
β) |
25 | 24 | recnd 11246 |
. . . . 5
β’ ((π β β β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π’ β {π₯ β β β£ π₯ β₯ π})) β ((Ξβπ’) Β·
(Ξβ(π / π’))) β
β) |
26 | 25 | anassrs 467 |
. . . 4
β’ (((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β§ π’ β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ’) Β· (Ξβ(π / π’))) β β) |
27 | 9, 26 | fsumcl 15685 |
. . 3
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) β β) |
28 | | vmacl 27005 |
. . . . . 6
β’ (π β β β
(Ξβπ) β
β) |
29 | 6, 28 | syl 17 |
. . . . 5
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (Ξβπ) β β) |
30 | 6 | nnrpd 13020 |
. . . . . 6
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β+) |
31 | 30 | relogcld 26512 |
. . . . 5
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (logβπ) β β) |
32 | 29, 31 | remulcld 11248 |
. . . 4
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ) Β· (logβπ)) β
β) |
33 | 32 | recnd 11246 |
. . 3
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ) Β· (logβπ)) β
β) |
34 | 3, 27, 33 | fsumadd 15692 |
. 2
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) + ((Ξβπ) Β· (logβπ))) = (Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) + Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)))) |
35 | | id 22 |
. . . . 5
β’ (π β β β π β
β) |
36 | | fvoveq1 7428 |
. . . . . 6
β’ (π = (π’ Β· π) β (Ξβ(π / π’)) = (Ξβ((π’ Β· π) / π’))) |
37 | 36 | oveq2d 7421 |
. . . . 5
β’ (π = (π’ Β· π) β ((Ξβπ’) Β· (Ξβ(π / π’))) = ((Ξβπ’) Β· (Ξβ((π’ Β· π) / π’)))) |
38 | 35, 37, 25 | fsumdvdscom 27072 |
. . . 4
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) = Ξ£π’ β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} ((Ξβπ’) Β· (Ξβ((π’ Β· π) / π’)))) |
39 | | ssrab2 4072 |
. . . . . . . . . . . . 13
β’ {π₯ β β β£ π₯ β₯ (π / π’)} β β |
40 | | simpr 484 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β π β {π₯ β β β£ π₯ β₯ (π / π’)}) |
41 | 39, 40 | sselid 3975 |
. . . . . . . . . . . 12
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β π β β) |
42 | 41 | nncnd 12232 |
. . . . . . . . . . 11
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β π β β) |
43 | | ssrab2 4072 |
. . . . . . . . . . . . . 14
β’ {π₯ β β β£ π₯ β₯ π} β β |
44 | | simpr 484 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β π’ β {π₯ β β β£ π₯ β₯ π}) |
45 | 43, 44 | sselid 3975 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β π’ β β) |
46 | 45 | nncnd 12232 |
. . . . . . . . . . . 12
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β π’ β β) |
47 | 46 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β π’ β β) |
48 | 45 | nnne0d 12266 |
. . . . . . . . . . . 12
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β π’ β 0) |
49 | 48 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β π’ β 0) |
50 | 42, 47, 49 | divcan3d 11999 |
. . . . . . . . . 10
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β ((π’ Β· π) / π’) = π) |
51 | 50 | fveq2d 6889 |
. . . . . . . . 9
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β (Ξβ((π’ Β· π) / π’)) = (Ξβπ)) |
52 | 51 | sumeq2dv 15655 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβ((π’ Β· π) / π’)) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβπ)) |
53 | | dvdsdivcl 16266 |
. . . . . . . . . 10
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (π / π’) β {π₯ β β β£ π₯ β₯ π}) |
54 | 43, 53 | sselid 3975 |
. . . . . . . . 9
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (π / π’) β β) |
55 | | vmasum 27104 |
. . . . . . . . 9
β’ ((π / π’) β β β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβπ) = (logβ(π / π’))) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβπ) = (logβ(π / π’))) |
57 | | nnrp 12991 |
. . . . . . . . . 10
β’ (π β β β π β
β+) |
58 | 57 | adantr 480 |
. . . . . . . . 9
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β π β
β+) |
59 | 45 | nnrpd 13020 |
. . . . . . . . 9
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β π’ β β+) |
60 | 58, 59 | relogdivd 26515 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (logβ(π / π’)) = ((logβπ) β (logβπ’))) |
61 | 52, 56, 60 | 3eqtrd 2770 |
. . . . . . 7
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβ((π’ Β· π) / π’)) = ((logβπ) β (logβπ’))) |
62 | 61 | oveq2d 7421 |
. . . . . 6
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ’) Β· Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβ((π’ Β· π) / π’))) = ((Ξβπ’) Β· ((logβπ) β (logβπ’)))) |
63 | | fzfid 13944 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (1...(π / π’)) β Fin) |
64 | | dvdsssfz1 16268 |
. . . . . . . . 9
β’ ((π / π’) β β β {π₯ β β β£ π₯ β₯ (π / π’)} β (1...(π / π’))) |
65 | 54, 64 | syl 17 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ (π / π’)} β (1...(π / π’))) |
66 | 63, 65 | ssfid 9269 |
. . . . . . 7
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ (π / π’)} β Fin) |
67 | 45, 12 | syl 17 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (Ξβπ’) β β) |
68 | 67 | recnd 11246 |
. . . . . . 7
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (Ξβπ’) β β) |
69 | | vmacl 27005 |
. . . . . . . . . 10
β’ (π β β β
(Ξβπ) β
β) |
70 | 41, 69 | syl 17 |
. . . . . . . . 9
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β (Ξβπ) β β) |
71 | 70 | recnd 11246 |
. . . . . . . 8
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β (Ξβπ) β β) |
72 | 51, 71 | eqeltrd 2827 |
. . . . . . 7
β’ (((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π’)}) β (Ξβ((π’ Β· π) / π’)) β β) |
73 | 66, 68, 72 | fsummulc2 15736 |
. . . . . 6
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ’) Β· Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} (Ξβ((π’ Β· π) / π’))) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} ((Ξβπ’) Β· (Ξβ((π’ Β· π) / π’)))) |
74 | | relogcl 26464 |
. . . . . . . . 9
β’ (π β β+
β (logβπ) β
β) |
75 | 74 | recnd 11246 |
. . . . . . . 8
β’ (π β β+
β (logβπ) β
β) |
76 | 58, 75 | syl 17 |
. . . . . . 7
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (logβπ) β β) |
77 | 59 | relogcld 26512 |
. . . . . . . 8
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (logβπ’) β β) |
78 | 77 | recnd 11246 |
. . . . . . 7
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β (logβπ’) β β) |
79 | 68, 76, 78 | subdid 11674 |
. . . . . 6
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ’) Β· ((logβπ) β (logβπ’))) = (((Ξβπ’) Β· (logβπ)) β
((Ξβπ’)
Β· (logβπ’)))) |
80 | 62, 73, 79 | 3eqtr3d 2774 |
. . . . 5
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} ((Ξβπ’) Β· (Ξβ((π’ Β· π) / π’))) = (((Ξβπ’) Β· (logβπ)) β ((Ξβπ’) Β· (logβπ’)))) |
81 | 80 | sumeq2dv 15655 |
. . . 4
β’ (π β β β
Ξ£π’ β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π’)} ((Ξβπ’) Β· (Ξβ((π’ Β· π) / π’))) = Ξ£π’ β {π₯ β β β£ π₯ β₯ π} (((Ξβπ’) Β· (logβπ)) β ((Ξβπ’) Β· (logβπ’)))) |
82 | 68, 76 | mulcld 11238 |
. . . . . 6
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ’) Β· (logβπ)) β
β) |
83 | 68, 78 | mulcld 11238 |
. . . . . 6
β’ ((π β β β§ π’ β {π₯ β β β£ π₯ β₯ π}) β ((Ξβπ’) Β· (logβπ’)) β
β) |
84 | 3, 82, 83 | fsumsub 15740 |
. . . . 5
β’ (π β β β
Ξ£π’ β {π₯ β β β£ π₯ β₯ π} (((Ξβπ’) Β· (logβπ)) β ((Ξβπ’) Β· (logβπ’))) = (Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ)) β Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ’)))) |
85 | 57, 75 | syl 17 |
. . . . . . . 8
β’ (π β β β
(logβπ) β
β) |
86 | 85 | sqvald 14113 |
. . . . . . 7
β’ (π β β β
((logβπ)β2) =
((logβπ) Β·
(logβπ))) |
87 | | vmasum 27104 |
. . . . . . . 8
β’ (π β β β
Ξ£π’ β {π₯ β β β£ π₯ β₯ π} (Ξβπ’) = (logβπ)) |
88 | 87 | oveq1d 7420 |
. . . . . . 7
β’ (π β β β
(Ξ£π’ β {π₯ β β β£ π₯ β₯ π} (Ξβπ’) Β· (logβπ)) = ((logβπ) Β· (logβπ))) |
89 | 3, 85, 68 | fsummulc1 15737 |
. . . . . . 7
β’ (π β β β
(Ξ£π’ β {π₯ β β β£ π₯ β₯ π} (Ξβπ’) Β· (logβπ)) = Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ))) |
90 | 86, 88, 89 | 3eqtr2rd 2773 |
. . . . . 6
β’ (π β β β
Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ)) = ((logβπ)β2)) |
91 | | fveq2 6885 |
. . . . . . . . 9
β’ (π’ = π β (Ξβπ’) = (Ξβπ)) |
92 | | fveq2 6885 |
. . . . . . . . 9
β’ (π’ = π β (logβπ’) = (logβπ)) |
93 | 91, 92 | oveq12d 7423 |
. . . . . . . 8
β’ (π’ = π β ((Ξβπ’) Β· (logβπ’)) = ((Ξβπ) Β· (logβπ))) |
94 | 93 | cbvsumv 15648 |
. . . . . . 7
β’
Ξ£π’ β
{π₯ β β β£
π₯ β₯ π} ((Ξβπ’) Β· (logβπ’)) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)) |
95 | 94 | a1i 11 |
. . . . . 6
β’ (π β β β
Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ’)) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ))) |
96 | 90, 95 | oveq12d 7423 |
. . . . 5
β’ (π β β β
(Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ)) β Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (logβπ’))) = (((logβπ)β2) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)))) |
97 | 84, 96 | eqtrd 2766 |
. . . 4
β’ (π β β β
Ξ£π’ β {π₯ β β β£ π₯ β₯ π} (((Ξβπ’) Β· (logβπ)) β ((Ξβπ’) Β· (logβπ’))) = (((logβπ)β2) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)))) |
98 | 38, 81, 97 | 3eqtrd 2770 |
. . 3
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) = (((logβπ)β2) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)))) |
99 | 98 | oveq1d 7420 |
. 2
β’ (π β β β
(Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) + Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ))) = ((((logβπ)β2) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ))) + Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)))) |
100 | 85 | sqcld 14114 |
. . 3
β’ (π β β β
((logβπ)β2)
β β) |
101 | 3, 33 | fsumcl 15685 |
. . 3
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ)) β β) |
102 | 100, 101 | npcand 11579 |
. 2
β’ (π β β β
((((logβπ)β2)
β Ξ£π β
{π₯ β β β£
π₯ β₯ π} ((Ξβπ) Β· (logβπ))) + Ξ£π β {π₯ β β β£ π₯ β₯ π} ((Ξβπ) Β· (logβπ))) = ((logβπ)β2)) |
103 | 34, 99, 102 | 3eqtrd 2770 |
1
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξ£π’ β {π₯ β β β£ π₯ β₯ π} ((Ξβπ’) Β· (Ξβ(π / π’))) + ((Ξβπ) Β· (logβπ))) = ((logβπ)β2)) |