Step | Hyp | Ref
| Expression |
1 | | dchrisum0fmul.a |
. . 3
β’ (π β π΄ β β) |
2 | | dchrisum0fmul.b |
. . 3
β’ (π β π΅ β β) |
3 | | dchrisum0fmul.m |
. . 3
β’ (π β (π΄ gcd π΅) = 1) |
4 | | eqid 2737 |
. . 3
β’ {π β β β£ π β₯ π΄} = {π β β β£ π β₯ π΄} |
5 | | eqid 2737 |
. . 3
β’ {π β β β£ π β₯ π΅} = {π β β β£ π β₯ π΅} |
6 | | eqid 2737 |
. . 3
β’ {π β β β£ π β₯ (π΄ Β· π΅)} = {π β β β£ π β₯ (π΄ Β· π΅)} |
7 | | rpvmasum2.g |
. . . 4
β’ πΊ = (DChrβπ) |
8 | | rpvmasum.z |
. . . 4
β’ π =
(β€/nβ€βπ) |
9 | | rpvmasum2.d |
. . . 4
β’ π· = (BaseβπΊ) |
10 | | rpvmasum.l |
. . . 4
β’ πΏ = (β€RHomβπ) |
11 | | dchrisum0f.x |
. . . . 5
β’ (π β π β π·) |
12 | 11 | adantr 482 |
. . . 4
β’ ((π β§ π β {π β β β£ π β₯ π΄}) β π β π·) |
13 | | elrabi 3644 |
. . . . . 6
β’ (π β {π β β β£ π β₯ π΄} β π β β) |
14 | 13 | nnzd 12533 |
. . . . 5
β’ (π β {π β β β£ π β₯ π΄} β π β β€) |
15 | 14 | adantl 483 |
. . . 4
β’ ((π β§ π β {π β β β£ π β₯ π΄}) β π β β€) |
16 | 7, 8, 9, 10, 12, 15 | dchrzrhcl 26609 |
. . 3
β’ ((π β§ π β {π β β β£ π β₯ π΄}) β (πβ(πΏβπ)) β β) |
17 | 11 | adantr 482 |
. . . 4
β’ ((π β§ π β {π β β β£ π β₯ π΅}) β π β π·) |
18 | | elrabi 3644 |
. . . . . 6
β’ (π β {π β β β£ π β₯ π΅} β π β β) |
19 | 18 | nnzd 12533 |
. . . . 5
β’ (π β {π β β β£ π β₯ π΅} β π β β€) |
20 | 19 | adantl 483 |
. . . 4
β’ ((π β§ π β {π β β β£ π β₯ π΅}) β π β β€) |
21 | 7, 8, 9, 10, 17, 20 | dchrzrhcl 26609 |
. . 3
β’ ((π β§ π β {π β β β£ π β₯ π΅}) β (πβ(πΏβπ)) β β) |
22 | 14, 19 | anim12i 614 |
. . . 4
β’ ((π β {π β β β£ π β₯ π΄} β§ π β {π β β β£ π β₯ π΅}) β (π β β€ β§ π β β€)) |
23 | 11 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β β€ β§ π β β€)) β π β π·) |
24 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β β€ β§ π β β€)) β π β β€) |
25 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π β β€ β§ π β β€)) β π β β€) |
26 | 7, 8, 9, 10, 23, 24, 25 | dchrzrhmul 26610 |
. . . . 5
β’ ((π β§ (π β β€ β§ π β β€)) β (πβ(πΏβ(π Β· π))) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ)))) |
27 | 26 | eqcomd 2743 |
. . . 4
β’ ((π β§ (π β β€ β§ π β β€)) β ((πβ(πΏβπ)) Β· (πβ(πΏβπ))) = (πβ(πΏβ(π Β· π)))) |
28 | 22, 27 | sylan2 594 |
. . 3
β’ ((π β§ (π β {π β β β£ π β₯ π΄} β§ π β {π β β β£ π β₯ π΅})) β ((πβ(πΏβπ)) Β· (πβ(πΏβπ))) = (πβ(πΏβ(π Β· π)))) |
29 | | 2fveq3 6852 |
. . 3
β’ (π = (π Β· π) β (πβ(πΏβπ)) = (πβ(πΏβ(π Β· π)))) |
30 | 1, 2, 3, 4, 5, 6, 16, 21, 28, 29 | fsumdvdsmul 26560 |
. 2
β’ (π β (Ξ£π β {π β β β£ π β₯ π΄} (πβ(πΏβπ)) Β· Ξ£π β {π β β β£ π β₯ π΅} (πβ(πΏβπ))) = Ξ£π β {π β β β£ π β₯ (π΄ Β· π΅)} (πβ(πΏβπ))) |
31 | | rpvmasum.a |
. . . . 5
β’ (π β π β β) |
32 | | rpvmasum2.1 |
. . . . 5
β’ 1 =
(0gβπΊ) |
33 | | dchrisum0f.f |
. . . . 5
β’ πΉ = (π β β β¦ Ξ£π£ β {π β β β£ π β₯ π} (πβ(πΏβπ£))) |
34 | 8, 10, 31, 7, 9, 32, 33 | dchrisum0fval 26869 |
. . . 4
β’ (π΄ β β β (πΉβπ΄) = Ξ£π β {π β β β£ π β₯ π΄} (πβ(πΏβπ))) |
35 | 1, 34 | syl 17 |
. . 3
β’ (π β (πΉβπ΄) = Ξ£π β {π β β β£ π β₯ π΄} (πβ(πΏβπ))) |
36 | 8, 10, 31, 7, 9, 32, 33 | dchrisum0fval 26869 |
. . . 4
β’ (π΅ β β β (πΉβπ΅) = Ξ£π β {π β β β£ π β₯ π΅} (πβ(πΏβπ))) |
37 | 2, 36 | syl 17 |
. . 3
β’ (π β (πΉβπ΅) = Ξ£π β {π β β β£ π β₯ π΅} (πβ(πΏβπ))) |
38 | 35, 37 | oveq12d 7380 |
. 2
β’ (π β ((πΉβπ΄) Β· (πΉβπ΅)) = (Ξ£π β {π β β β£ π β₯ π΄} (πβ(πΏβπ)) Β· Ξ£π β {π β β β£ π β₯ π΅} (πβ(πΏβπ)))) |
39 | 1, 2 | nnmulcld 12213 |
. . 3
β’ (π β (π΄ Β· π΅) β β) |
40 | 8, 10, 31, 7, 9, 32, 33 | dchrisum0fval 26869 |
. . 3
β’ ((π΄ Β· π΅) β β β (πΉβ(π΄ Β· π΅)) = Ξ£π β {π β β β£ π β₯ (π΄ Β· π΅)} (πβ(πΏβπ))) |
41 | 39, 40 | syl 17 |
. 2
β’ (π β (πΉβ(π΄ Β· π΅)) = Ξ£π β {π β β β£ π β₯ (π΄ Β· π΅)} (πβ(πΏβπ))) |
42 | 30, 38, 41 | 3eqtr4rd 2788 |
1
β’ (π β (πΉβ(π΄ Β· π΅)) = ((πΉβπ΄) Β· (πΉβπ΅))) |