Step | Hyp | Ref
| Expression |
1 | | fzfid 13937 |
. . . 4
β’ (π β (1...π) β Fin) |
2 | | dvdsmulf1o.x |
. . . . 5
β’ π = {π₯ β β β£ π₯ β₯ π} |
3 | | dvdsmulf1o.1 |
. . . . . 6
β’ (π β π β β) |
4 | | dvdsssfz1 16260 |
. . . . . 6
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
6 | 2, 5 | eqsstrid 4030 |
. . . 4
β’ (π β π β (1...π)) |
7 | 1, 6 | ssfid 9266 |
. . 3
β’ (π β π β Fin) |
8 | | fzfid 13937 |
. . . . 5
β’ (π β (1...π) β Fin) |
9 | | dvdsmulf1o.y |
. . . . . 6
β’ π = {π₯ β β β£ π₯ β₯ π} |
10 | | dvdsmulf1o.2 |
. . . . . . 7
β’ (π β π β β) |
11 | | dvdsssfz1 16260 |
. . . . . . 7
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
12 | 10, 11 | syl 17 |
. . . . . 6
β’ (π β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
13 | 9, 12 | eqsstrid 4030 |
. . . . 5
β’ (π β π β (1...π)) |
14 | 8, 13 | ssfid 9266 |
. . . 4
β’ (π β π β Fin) |
15 | | fsumdvdsmul.5 |
. . . 4
β’ ((π β§ π β π) β π΅ β β) |
16 | 14, 15 | fsumcl 15678 |
. . 3
β’ (π β Ξ£π β π π΅ β β) |
17 | | fsumdvdsmul.4 |
. . 3
β’ ((π β§ π β π) β π΄ β β) |
18 | 7, 16, 17 | fsummulc1 15730 |
. 2
β’ (π β (Ξ£π β π π΄ Β· Ξ£π β π π΅) = Ξ£π β π (π΄ Β· Ξ£π β π π΅)) |
19 | 14 | adantr 481 |
. . . . 5
β’ ((π β§ π β π) β π β Fin) |
20 | 15 | adantlr 713 |
. . . . 5
β’ (((π β§ π β π) β§ π β π) β π΅ β β) |
21 | 19, 17, 20 | fsummulc2 15729 |
. . . 4
β’ ((π β§ π β π) β (π΄ Β· Ξ£π β π π΅) = Ξ£π β π (π΄ Β· π΅)) |
22 | | fsumdvdsmul.6 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π΄ Β· π΅) = π·) |
23 | 22 | anassrs 468 |
. . . . 5
β’ (((π β§ π β π) β§ π β π) β (π΄ Β· π΅) = π·) |
24 | 23 | sumeq2dv 15648 |
. . . 4
β’ ((π β§ π β π) β Ξ£π β π (π΄ Β· π΅) = Ξ£π β π π·) |
25 | 21, 24 | eqtrd 2772 |
. . 3
β’ ((π β§ π β π) β (π΄ Β· Ξ£π β π π΅) = Ξ£π β π π·) |
26 | 25 | sumeq2dv 15648 |
. 2
β’ (π β Ξ£π β π (π΄ Β· Ξ£π β π π΅) = Ξ£π β π Ξ£π β π π·) |
27 | | fveq2 6891 |
. . . . . . 7
β’ (π§ = β¨π, πβ© β ( Β· βπ§) = ( Β·
ββ¨π, πβ©)) |
28 | | df-ov 7411 |
. . . . . . 7
β’ (π Β· π) = ( Β· ββ¨π, πβ©) |
29 | 27, 28 | eqtr4di 2790 |
. . . . . 6
β’ (π§ = β¨π, πβ© β ( Β· βπ§) = (π Β· π)) |
30 | 29 | csbeq1d 3897 |
. . . . 5
β’ (π§ = β¨π, πβ© β β¦( Β·
βπ§) / πβ¦πΆ = β¦(π Β· π) / πβ¦πΆ) |
31 | | ovex 7441 |
. . . . . 6
β’ (π Β· π) β V |
32 | | fsumdvdsmul.7 |
. . . . . 6
β’ (π = (π Β· π) β πΆ = π·) |
33 | 31, 32 | csbie 3929 |
. . . . 5
β’
β¦(π
Β· π) / πβ¦πΆ = π· |
34 | 30, 33 | eqtrdi 2788 |
. . . 4
β’ (π§ = β¨π, πβ© β β¦( Β·
βπ§) / πβ¦πΆ = π·) |
35 | 17 | adantrr 715 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π΄ β β) |
36 | 15 | adantrl 714 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β π΅ β β) |
37 | 35, 36 | mulcld 11233 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β (π΄ Β· π΅) β β) |
38 | 22, 37 | eqeltrrd 2834 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β π· β β) |
39 | 34, 7, 14, 38 | fsumxp 15717 |
. . 3
β’ (π β Ξ£π β π Ξ£π β π π· = Ξ£π§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ) |
40 | | nfcv 2903 |
. . . . 5
β’
β²π€πΆ |
41 | | nfcsb1v 3918 |
. . . . 5
β’
β²πβ¦π€ / πβ¦πΆ |
42 | | csbeq1a 3907 |
. . . . 5
β’ (π = π€ β πΆ = β¦π€ / πβ¦πΆ) |
43 | 40, 41, 42 | cbvsumi 15642 |
. . . 4
β’
Ξ£π β
π πΆ = Ξ£π€ β π β¦π€ / πβ¦πΆ |
44 | | csbeq1 3896 |
. . . . 5
β’ (π€ = ( Β· βπ§) β β¦π€ / πβ¦πΆ = β¦( Β· βπ§) / πβ¦πΆ) |
45 | | xpfi 9316 |
. . . . . 6
β’ ((π β Fin β§ π β Fin) β (π Γ π) β Fin) |
46 | 7, 14, 45 | syl2anc 584 |
. . . . 5
β’ (π β (π Γ π) β Fin) |
47 | | dvdsmulf1o.3 |
. . . . . 6
β’ (π β (π gcd π) = 1) |
48 | | dvdsmulf1o.z |
. . . . . 6
β’ π = {π₯ β β β£ π₯ β₯ (π Β· π)} |
49 | 3, 10, 47, 2, 9, 48 | dvdsmulf1o 26695 |
. . . . 5
β’ (π β ( Β· βΎ (π Γ π)):(π Γ π)β1-1-ontoβπ) |
50 | | fvres 6910 |
. . . . . 6
β’ (π§ β (π Γ π) β (( Β· βΎ (π Γ π))βπ§) = ( Β· βπ§)) |
51 | 50 | adantl 482 |
. . . . 5
β’ ((π β§ π§ β (π Γ π)) β (( Β· βΎ (π Γ π))βπ§) = ( Β· βπ§)) |
52 | 38 | ralrimivva 3200 |
. . . . . . . 8
β’ (π β βπ β π βπ β π π· β β) |
53 | 34 | eleq1d 2818 |
. . . . . . . . 9
β’ (π§ = β¨π, πβ© β (β¦( Β·
βπ§) / πβ¦πΆ β β β π· β β)) |
54 | 53 | ralxp 5841 |
. . . . . . . 8
β’
(βπ§ β
(π Γ π)β¦( Β·
βπ§) / πβ¦πΆ β β β βπ β π βπ β π π· β β) |
55 | 52, 54 | sylibr 233 |
. . . . . . 7
β’ (π β βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β) |
56 | | ax-mulf 11189 |
. . . . . . . . . 10
β’ Β·
:(β Γ β)βΆβ |
57 | | ffn 6717 |
. . . . . . . . . 10
β’ (
Β· :(β Γ β)βΆβ β Β· Fn (β
Γ β)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . 9
β’ Β·
Fn (β Γ β) |
59 | 2 | ssrab3 4080 |
. . . . . . . . . . 11
β’ π β
β |
60 | | nnsscn 12216 |
. . . . . . . . . . 11
β’ β
β β |
61 | 59, 60 | sstri 3991 |
. . . . . . . . . 10
β’ π β
β |
62 | 9 | ssrab3 4080 |
. . . . . . . . . . 11
β’ π β
β |
63 | 62, 60 | sstri 3991 |
. . . . . . . . . 10
β’ π β
β |
64 | | xpss12 5691 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π Γ π) β (β Γ
β)) |
65 | 61, 63, 64 | mp2an 690 |
. . . . . . . . 9
β’ (π Γ π) β (β Γ
β) |
66 | 44 | eleq1d 2818 |
. . . . . . . . . 10
β’ (π€ = ( Β· βπ§) β (β¦π€ / πβ¦πΆ β β β β¦(
Β· βπ§) / πβ¦πΆ β β)) |
67 | 66 | ralima 7239 |
. . . . . . . . 9
β’ ((
Β· Fn (β Γ β) β§ (π Γ π) β (β Γ β)) β
(βπ€ β (
Β· β (π Γ
π))β¦π€ / πβ¦πΆ β β β βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β)) |
68 | 58, 65, 67 | mp2an 690 |
. . . . . . . 8
β’
(βπ€ β (
Β· β (π Γ
π))β¦π€ / πβ¦πΆ β β β βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β) |
69 | | df-ima 5689 |
. . . . . . . . . 10
β’ (
Β· β (π Γ
π)) = ran ( Β·
βΎ (π Γ π)) |
70 | | f1ofo 6840 |
. . . . . . . . . . 11
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)β1-1-ontoβπ β ( Β· βΎ
(π Γ π)):(π Γ π)βontoβπ) |
71 | | forn 6808 |
. . . . . . . . . . 11
β’ ((
Β· βΎ (π Γ
π)):(π Γ π)βontoβπ β ran ( Β· βΎ (π Γ π)) = π) |
72 | 49, 70, 71 | 3syl 18 |
. . . . . . . . . 10
β’ (π β ran ( Β· βΎ
(π Γ π)) = π) |
73 | 69, 72 | eqtrid 2784 |
. . . . . . . . 9
β’ (π β ( Β· β (π Γ π)) = π) |
74 | 73 | raleqdv 3325 |
. . . . . . . 8
β’ (π β (βπ€ β ( Β· β
(π Γ π))β¦π€ / πβ¦πΆ β β β βπ€ β π β¦π€ / πβ¦πΆ β β)) |
75 | 68, 74 | bitr3id 284 |
. . . . . . 7
β’ (π β (βπ§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ β β β βπ€ β π β¦π€ / πβ¦πΆ β β)) |
76 | 55, 75 | mpbid 231 |
. . . . . 6
β’ (π β βπ€ β π β¦π€ / πβ¦πΆ β β) |
77 | 76 | r19.21bi 3248 |
. . . . 5
β’ ((π β§ π€ β π) β β¦π€ / πβ¦πΆ β β) |
78 | 44, 46, 49, 51, 77 | fsumf1o 15668 |
. . . 4
β’ (π β Ξ£π€ β π β¦π€ / πβ¦πΆ = Ξ£π§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ) |
79 | 43, 78 | eqtrid 2784 |
. . 3
β’ (π β Ξ£π β π πΆ = Ξ£π§ β (π Γ π)β¦( Β· βπ§) / πβ¦πΆ) |
80 | 39, 79 | eqtr4d 2775 |
. 2
β’ (π β Ξ£π β π Ξ£π β π π· = Ξ£π β π πΆ) |
81 | 18, 26, 80 | 3eqtrd 2776 |
1
β’ (π β (Ξ£π β π π΄ Β· Ξ£π β π π΅) = Ξ£π β π πΆ) |