Step | Hyp | Ref
| Expression |
1 | | eulerpartlems.r |
. . 3
β’ π
= {π β£ (β‘π β β) β
Fin} |
2 | | eulerpartlems.s |
. . 3
β’ π = (π β ((β0
βm β) β© π
) β¦ Ξ£π β β ((πβπ) Β· π)) |
3 | 1, 2 | eulerpartlemsv1 32996 |
. 2
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β β ((π΄βπ) Β· π)) |
4 | | cnvimass 6038 |
. . . 4
β’ (β‘π΄ β β) β dom π΄ |
5 | 1, 2 | eulerpartlemelr 32997 |
. . . . 5
β’ (π΄ β ((β0
βm β) β© π
) β (π΄:ββΆβ0 β§
(β‘π΄ β β) β
Fin)) |
6 | 5 | simpld 496 |
. . . 4
β’ (π΄ β ((β0
βm β) β© π
) β π΄:ββΆβ0) |
7 | 4, 6 | fssdm 6693 |
. . 3
β’ (π΄ β ((β0
βm β) β© π
) β (β‘π΄ β β) β
β) |
8 | 6 | adantr 482 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β‘π΄ β β)) β π΄:ββΆβ0) |
9 | 7 | sselda 3949 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β‘π΄ β β)) β π β β) |
10 | 8, 9 | ffvelcdmd 7041 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β‘π΄ β β)) β (π΄βπ) β
β0) |
11 | 9 | nnnn0d 12480 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β‘π΄ β β)) β π β β0) |
12 | 10, 11 | nn0mulcld 12485 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β‘π΄ β β)) β ((π΄βπ) Β· π) β
β0) |
13 | 12 | nn0cnd 12482 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β‘π΄ β β)) β ((π΄βπ) Β· π) β β) |
14 | | simpr 486 |
. . . . . . . 8
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β π β (β β (β‘π΄ β β))) |
15 | 14 | eldifad 3927 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β π β
β) |
16 | 14 | eldifbd 3928 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β Β¬ π β (β‘π΄ β β)) |
17 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β π΄:ββΆβ0) |
18 | | ffn 6673 |
. . . . . . . . . 10
β’ (π΄:ββΆβ0 β
π΄ Fn
β) |
19 | | elpreima 7013 |
. . . . . . . . . 10
β’ (π΄ Fn β β (π β (β‘π΄ β β) β (π β β β§ (π΄βπ) β β))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β (π β (β‘π΄ β β) β (π β β β§ (π΄βπ) β β))) |
21 | 16, 20 | mtbid 324 |
. . . . . . . 8
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β Β¬ (π β β β§ (π΄βπ) β β)) |
22 | | imnan 401 |
. . . . . . . 8
β’ ((π β β β Β¬
(π΄βπ) β β) β Β¬ (π β β β§ (π΄βπ) β β)) |
23 | 21, 22 | sylibr 233 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β (π β β β Β¬
(π΄βπ) β β)) |
24 | 15, 23 | mpd 15 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β Β¬ (π΄βπ) β β) |
25 | 17, 15 | ffvelcdmd 7041 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β (π΄βπ) β
β0) |
26 | | elnn0 12422 |
. . . . . . 7
β’ ((π΄βπ) β β0 β ((π΄βπ) β β β¨ (π΄βπ) = 0)) |
27 | 25, 26 | sylib 217 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β ((π΄βπ) β β β¨ (π΄βπ) = 0)) |
28 | | orel1 888 |
. . . . . 6
β’ (Β¬
(π΄βπ) β β β (((π΄βπ) β β β¨ (π΄βπ) = 0) β (π΄βπ) = 0)) |
29 | 24, 27, 28 | sylc 65 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β (π΄βπ) = 0) |
30 | 29 | oveq1d 7377 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β ((π΄βπ) Β· π) = (0 Β· π)) |
31 | 15 | nncnd 12176 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β π β
β) |
32 | 31 | mul02d 11360 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β (0 Β· π) = 0) |
33 | 30, 32 | eqtrd 2777 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (β‘π΄ β β))) β ((π΄βπ) Β· π) = 0) |
34 | | nnuz 12813 |
. . . . 5
β’ β =
(β€β₯β1) |
35 | 34 | eqimssi 4007 |
. . . 4
β’ β
β (β€β₯β1) |
36 | 35 | a1i 11 |
. . 3
β’ (π΄ β ((β0
βm β) β© π
) β β β
(β€β₯β1)) |
37 | 7, 13, 33, 36 | sumss 15616 |
. 2
β’ (π΄ β ((β0
βm β) β© π
) β Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = Ξ£π β β ((π΄βπ) Β· π)) |
38 | 3, 37 | eqtr4d 2780 |
1
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) |