Step | Hyp | Ref
| Expression |
1 | | eulerpartlems.r |
. . 3
β’ π
= {π β£ (β‘π β β) β
Fin} |
2 | | eulerpartlems.s |
. . 3
β’ π = (π β ((β0
βm β) β© π
) β¦ Ξ£π β β ((πβπ) Β· π)) |
3 | 1, 2 | eulerpartlemsv1 32996 |
. 2
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β β ((π΄βπ) Β· π)) |
4 | | fzssuz 13489 |
. . . . 5
β’
(1...(πβπ΄)) β
(β€β₯β1) |
5 | | nnuz 12813 |
. . . . 5
β’ β =
(β€β₯β1) |
6 | 4, 5 | sseqtrri 3986 |
. . . 4
β’
(1...(πβπ΄)) β
β |
7 | 6 | a1i 11 |
. . 3
β’ (π΄ β ((β0
βm β) β© π
) β (1...(πβπ΄)) β β) |
8 | 1, 2 | eulerpartlemelr 32997 |
. . . . . . . 8
β’ (π΄ β ((β0
βm β) β© π
) β (π΄:ββΆβ0 β§
(β‘π΄ β β) β
Fin)) |
9 | 8 | simpld 496 |
. . . . . . 7
β’ (π΄ β ((β0
βm β) β© π
) β π΄:ββΆβ0) |
10 | 9 | adantr 482 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β π΄:ββΆβ0) |
11 | 7 | sselda 3949 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β π β β) |
12 | 10, 11 | ffvelcdmd 7041 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β (π΄βπ) β
β0) |
13 | 12 | nn0cnd 12482 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β (π΄βπ) β β) |
14 | 11 | nncnd 12176 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β π β β) |
15 | 13, 14 | mulcld 11182 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (1...(πβπ΄))) β ((π΄βπ) Β· π) β β) |
16 | 1, 2 | eulerpartlems 33000 |
. . . . . . . . 9
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β€β₯β((πβπ΄) + 1))) β (π΄βπ‘) = 0) |
17 | 16 | ralrimiva 3144 |
. . . . . . . 8
β’ (π΄ β ((β0
βm β) β© π
) β βπ‘ β (β€β₯β((πβπ΄) + 1))(π΄βπ‘) = 0) |
18 | | fveqeq2 6856 |
. . . . . . . . 9
β’ (π = π‘ β ((π΄βπ) = 0 β (π΄βπ‘) = 0)) |
19 | 18 | cbvralvw 3228 |
. . . . . . . 8
β’
(βπ β
(β€β₯β((πβπ΄) + 1))(π΄βπ) = 0 β βπ‘ β (β€β₯β((πβπ΄) + 1))(π΄βπ‘) = 0) |
20 | 17, 19 | sylibr 233 |
. . . . . . 7
β’ (π΄ β ((β0
βm β) β© π
) β βπ β (β€β₯β((πβπ΄) + 1))(π΄βπ) = 0) |
21 | 1, 2 | eulerpartlemsf 32999 |
. . . . . . . . . 10
β’ π:((β0
βm β) β© π
)βΆβ0 |
22 | 21 | ffvelcdmi 7039 |
. . . . . . . . 9
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) β
β0) |
23 | | nndiffz1 31731 |
. . . . . . . . 9
β’ ((πβπ΄) β β0 β (β
β (1...(πβπ΄))) =
(β€β₯β((πβπ΄) + 1))) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (π΄ β ((β0
βm β) β© π
) β (β β (1...(πβπ΄))) = (β€β₯β((πβπ΄) + 1))) |
25 | 24 | raleqdv 3316 |
. . . . . . 7
β’ (π΄ β ((β0
βm β) β© π
) β (βπ β (β β (1...(πβπ΄)))(π΄βπ) = 0 β βπ β (β€β₯β((πβπ΄) + 1))(π΄βπ) = 0)) |
26 | 20, 25 | mpbird 257 |
. . . . . 6
β’ (π΄ β ((β0
βm β) β© π
) β βπ β (β β (1...(πβπ΄)))(π΄βπ) = 0) |
27 | 26 | r19.21bi 3237 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β (π΄βπ) = 0) |
28 | 27 | oveq1d 7377 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β ((π΄βπ) Β· π) = (0 Β· π)) |
29 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β π β (β β (1...(πβπ΄)))) |
30 | 29 | eldifad 3927 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β π β β) |
31 | 30 | nncnd 12176 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β π β β) |
32 | 31 | mul02d 11360 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β (0 Β· π) = 0) |
33 | 28, 32 | eqtrd 2777 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β (β β (1...(πβπ΄)))) β ((π΄βπ) Β· π) = 0) |
34 | 5 | eqimssi 4007 |
. . . 4
β’ β
β (β€β₯β1) |
35 | 34 | a1i 11 |
. . 3
β’ (π΄ β ((β0
βm β) β© π
) β β β
(β€β₯β1)) |
36 | 7, 15, 33, 35 | sumss 15616 |
. 2
β’ (π΄ β ((β0
βm β) β© π
) β Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π) = Ξ£π β β ((π΄βπ) Β· π)) |
37 | 3, 36 | eqtr4d 2780 |
1
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β (1...(πβπ΄))((π΄βπ) Β· π)) |