Step | Hyp | Ref
| Expression |
1 | | fzfid 13887 |
. . . 4
β’ (π β (1...π) β Fin) |
2 | | dvdsmulf1o.x |
. . . . 5
β’ π = {π₯ β β β£ π₯ β₯ π} |
3 | | dvdsmulf1o.1 |
. . . . . 6
β’ (π β π β β) |
4 | | dvdsssfz1 16208 |
. . . . . 6
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
6 | 2, 5 | eqsstrid 3996 |
. . . 4
β’ (π β π β (1...π)) |
7 | 1, 6 | ssfid 9217 |
. . 3
β’ (π β π β Fin) |
8 | | fzfid 13887 |
. . . . 5
β’ (π β (1...π) β Fin) |
9 | | dvdsmulf1o.y |
. . . . . 6
β’ π = {π₯ β β β£ π₯ β₯ π} |
10 | | dvdsmulf1o.2 |
. . . . . . 7
β’ (π β π β β) |
11 | | dvdsssfz1 16208 |
. . . . . . 7
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
12 | 10, 11 | syl 17 |
. . . . . 6
β’ (π β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
13 | 9, 12 | eqsstrid 3996 |
. . . . 5
β’ (π β π β (1...π)) |
14 | 8, 13 | ssfid 9217 |
. . . 4
β’ (π β π β Fin) |
15 | | fsumdvdsmul.5 |
. . . 4
β’ ((π β§ π β π) β π΅ β β) |
16 | 14, 15 | fsumcl 15626 |
. . 3
β’ (π β Ξ£π β π π΅ β β) |
17 | | fsumdvdsmul.4 |
. . 3
β’ ((π β§ π β π) β π΄ β β) |
18 | 7, 16, 17 | fsummulc1 15678 |
. 2
β’ (π β (Ξ£π β π π΄ Β· Ξ£π β π π΅) = Ξ£π β π (π΄ Β· Ξ£π β π π΅)) |
19 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β π β Fin) |
20 | 15 | adantlr 714 |
. . . . 5
β’ (((π β§ π β π) β§ π β π) β π΅ β β) |
21 | 19, 17, 20 | fsummulc2 15677 |
. . . 4
β’ ((π β§ π β π) β (π΄ Β· Ξ£π β π π΅) = Ξ£π β π (π΄ Β· π΅)) |
22 | | fsumdvdsmul.6 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π΄ Β· π΅) = π·) |
23 | 22 | anassrs 469 |
. . . . 5
β’ (((π β§ π β π) β§ π β π) β (π΄ Β· π΅) = π·) |
24 | 23 | sumeq2dv 15596 |
. . . 4
β’ ((π β§ π β π) β Ξ£π β π (π΄ Β· π΅) = Ξ£π β π π·) |
25 | 21, 24 | eqtrd 2773 |
. . 3
β’ ((π β§ π β π) β (π΄ Β· Ξ£π β π π΅) = Ξ£π β π π·) |
26 | 25 | sumeq2dv 15596 |
. 2
β’ (π β Ξ£π β π (π΄ Β· Ξ£π β π π΅) = Ξ£π β π Ξ£π β π π·) |
27 | | fveq2 6846 |
. . . . . . 7
β’ (π§ = β¨π, πβ© β ( Β· βπ§) = ( Β·
ββ¨π, πβ©)) |
28 | | df-ov 7364 |
. . . . . . 7
β’ (π Β· π) = ( Β· ββ¨π, πβ©) |
29 | 27, 28 | eqtr4di 2791 |
. . . . . 6
β’ (π§ = β¨π, πβ© β ( Β· βπ§) = (π Β· π)) |
30 | 29 | csbeq1d 3863 |
. . . . 5
β’ (π§ = β¨π, πβ© β β¦( Β·
βπ§) / πβ¦πΆ = β¦(π Β· π) / πβ¦πΆ) |
31 | | ovex 7394 |
. . . . . 6
β’ (π Β· π) β V |
32 | | fsumdvdsmul.7 |
. . . . . 6
β’ (π = (π Β· π) β πΆ = π·) |
33 | 31, 32 | csbie 3895 |
. . . . 5
β’
β¦(π
Β· π) / πβ¦πΆ = π· |
34 | 30, 33 | eqtrdi 2789 |
. . . 4
β’ (π§ = β¨π, πβ© β β¦( Β·
βπ§) / πβ¦πΆ = π·) |
35 | 17 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π΄ β β) |
36 | 15 | adantrl 715 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π΅ β β) |
37 | 35, 36 | mulcld 11183 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π΄ Β· π΅) β β) |
38 | 22, 37 | eqeltrrd 2835 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β π· β β) |
39 | 34, 7, 14, 38 | fsumxp 15665 |
. . 3
β’ (π β Ξ£π β π Ξ£π β π π· = Ξ£π§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ) |
40 | | nfcv 2904 |
. . . . 5
β’
β²π€πΆ |
41 | | nfcsb1v 3884 |
. . . . 5
β’
β²πβ¦π€ / πβ¦πΆ |
42 | | csbeq1a 3873 |
. . . . 5
β’ (π = π€ β πΆ = β¦π€ / πβ¦πΆ) |
43 | 40, 41, 42 | cbvsumi 15590 |
. . . 4
β’
Ξ£π β
π πΆ = Ξ£π€ β π β¦π€ / πβ¦πΆ |
44 | | csbeq1 3862 |
. . . . 5
β’ (π€ = ( Β· βπ§) β β¦π€ / πβ¦πΆ = β¦( Β· βπ§) / πβ¦πΆ) |
45 | | xpfi 9267 |
. . . . . 6
β’ ((π β Fin β§ π β Fin) β (π Γ π) β Fin) |
46 | 7, 14, 45 | syl2anc 585 |
. . . . 5
β’ (π β (π Γ π) β Fin) |
47 | | dvdsmulf1o.3 |
. . . . . 6
β’ (π β (π gcd π) = 1) |
48 | | dvdsmulf1o.z |
. . . . . 6
β’ π = {π₯ β β β£ π₯ β₯ (π Β· π)} |
49 | 3, 10, 47, 2, 9, 48 | dvdsmulf1o 26566 |
. . . . 5
β’ (π β ( Β· βΎ (π Γ π)):(π Γ π)β1-1-ontoβπ) |
50 | | fvres 6865 |
. . . . . 6
β’ (π§ β (π Γ π) β (( Β· βΎ (π Γ π))βπ§) = ( Β· βπ§)) |
51 | 50 | adantl 483 |
. . . . 5
β’ ((π β§ π§ β (π Γ π)) β (( Β· βΎ (π Γ π))βπ§) = ( Β· βπ§)) |
52 | 38 | ralrimivva 3194 |
. . . . . . . 8
β’ (π β βπ β π βπ β π π· β β) |
53 | 34 | eleq1d 2819 |
. . . . . . . . 9
β’ (π§ = β¨π, πβ© β (β¦( Β·
βπ§) / πβ¦πΆ β β β π· β β)) |
54 | 53 | ralxp 5801 |
. . . . . . . 8
β’
(βπ§ β
(π Γ π)β¦( Β·
βπ§) / πβ¦πΆ β β β βπ β π βπ β π π· β β) |
55 | 52, 54 | sylibr 233 |
. . . . . . 7
β’ (π β βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β) |
56 | | ax-mulf 11139 |
. . . . . . . . . 10
β’ Β·
:(β Γ β)βΆβ |
57 | | ffn 6672 |
. . . . . . . . . 10
β’ (
Β· :(β Γ β)βΆβ β Β· Fn (β
Γ β)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . 9
β’ Β·
Fn (β Γ β) |
59 | 2 | ssrab3 4044 |
. . . . . . . . . . 11
β’ π β
β |
60 | | nnsscn 12166 |
. . . . . . . . . . 11
β’ β
β β |
61 | 59, 60 | sstri 3957 |
. . . . . . . . . 10
β’ π β
β |
62 | 9 | ssrab3 4044 |
. . . . . . . . . . 11
β’ π β
β |
63 | 62, 60 | sstri 3957 |
. . . . . . . . . 10
β’ π β
β |
64 | | xpss12 5652 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π Γ π) β (β Γ
β)) |
65 | 61, 63, 64 | mp2an 691 |
. . . . . . . . 9
β’ (π Γ π) β (β Γ
β) |
66 | 44 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π€ = ( Β· βπ§) β (β¦π€ / πβ¦πΆ β β β β¦(
Β· βπ§) / πβ¦πΆ β β)) |
67 | 66 | ralima 7192 |
. . . . . . . . 9
β’ ((
Β· Fn (β Γ β) β§ (π Γ π) β (β Γ β)) β
(βπ€ β (
Β· β (π Γ
π))β¦π€ / πβ¦πΆ β β β βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β)) |
68 | 58, 65, 67 | mp2an 691 |
. . . . . . . 8
β’
(βπ€ β (
Β· β (π Γ
π))β¦π€ / πβ¦πΆ β β β βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β) |
69 | | df-ima 5650 |
. . . . . . . . . 10
β’ (
Β· β (π Γ
π)) = ran ( Β·
βΎ (π Γ π)) |
70 | | f1ofo 6795 |
. . . . . . . . . . 11
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)β1-1-ontoβπ β ( Β· βΎ
(π Γ π)):(π Γ π)βontoβπ) |
71 | | forn 6763 |
. . . . . . . . . . 11
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)βontoβπ β ran ( Β· βΎ (π Γ π)) = π) |
72 | 49, 70, 71 | 3syl 18 |
. . . . . . . . . 10
β’ (π β ran ( Β· βΎ
(π Γ π)) = π) |
73 | 69, 72 | eqtrid 2785 |
. . . . . . . . 9
β’ (π β ( Β· β (π Γ π)) = π) |
74 | 73 | raleqdv 3312 |
. . . . . . . 8
β’ (π β (βπ€ β ( Β· β
(π Γ π))β¦π€ / πβ¦πΆ β β β βπ€ β π β¦π€ / πβ¦πΆ β β)) |
75 | 68, 74 | bitr3id 285 |
. . . . . . 7
β’ (π β (βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β β βπ€ β π β¦π€ / πβ¦πΆ β β)) |
76 | 55, 75 | mpbid 231 |
. . . . . 6
β’ (π β βπ€ β π β¦π€ / πβ¦πΆ β β) |
77 | 76 | r19.21bi 3233 |
. . . . 5
β’ ((π β§ π€ β π) β β¦π€ / πβ¦πΆ β β) |
78 | 44, 46, 49, 51, 77 | fsumf1o 15616 |
. . . 4
β’ (π β Ξ£π€ β π β¦π€ / πβ¦πΆ = Ξ£π§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ) |
79 | 43, 78 | eqtrid 2785 |
. . 3
β’ (π β Ξ£π β π πΆ = Ξ£π§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ) |
80 | 39, 79 | eqtr4d 2776 |
. 2
β’ (π β Ξ£π β π Ξ£π β π π· = Ξ£π β π πΆ) |
81 | 18, 26, 80 | 3eqtrd 2777 |
1
β’ (π β (Ξ£π β π π΄ Β· Ξ£π β π π΅) = Ξ£π β π πΆ) |