Step | Hyp | Ref
| Expression |
1 | | eulerpart.p |
. . 3
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
2 | 1 | eulerpartleme 33003 |
. 2
β’ (π΄ β π β (π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β β
((π΄βπ) Β· π) = π)) |
3 | | cnvimass 6038 |
. . . . . . . . 9
β’ (β‘π΄ β β) β dom π΄ |
4 | | fdm 6682 |
. . . . . . . . 9
β’ (π΄:ββΆβ0 β
dom π΄ =
β) |
5 | 3, 4 | sseqtrid 4001 |
. . . . . . . 8
β’ (π΄:ββΆβ0 β
(β‘π΄ β β) β
β) |
6 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π΄:ββΆβ0 β§
π β (β‘π΄ β β)) β π΄:ββΆβ0) |
7 | 5 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π΄:ββΆβ0 β§
π β (β‘π΄ β β)) β π β β) |
8 | 6, 7 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π΄:ββΆβ0 β§
π β (β‘π΄ β β)) β (π΄βπ) β
β0) |
9 | 7 | nnnn0d 12480 |
. . . . . . . . . 10
β’ ((π΄:ββΆβ0 β§
π β (β‘π΄ β β)) β π β β0) |
10 | 8, 9 | nn0mulcld 12485 |
. . . . . . . . 9
β’ ((π΄:ββΆβ0 β§
π β (β‘π΄ β β)) β ((π΄βπ) Β· π) β
β0) |
11 | 10 | nn0cnd 12482 |
. . . . . . . 8
β’ ((π΄:ββΆβ0 β§
π β (β‘π΄ β β)) β ((π΄βπ) Β· π) β β) |
12 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β π β (β β (β‘π΄ β β))) |
13 | 12 | eldifad 3927 |
. . . . . . . . . . . 12
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β π β
β) |
14 | 12 | eldifbd 3928 |
. . . . . . . . . . . . . 14
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β Β¬ π β (β‘π΄ β β)) |
15 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β π΄:ββΆβ0) |
16 | | ffn 6673 |
. . . . . . . . . . . . . . 15
β’ (π΄:ββΆβ0 β
π΄ Fn
β) |
17 | | elpreima 7013 |
. . . . . . . . . . . . . . 15
β’ (π΄ Fn β β (π β (β‘π΄ β β) β (π β β β§ (π΄βπ) β β))) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β (π β (β‘π΄ β β) β (π β β β§ (π΄βπ) β β))) |
19 | 14, 18 | mtbid 324 |
. . . . . . . . . . . . 13
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β Β¬ (π β β β§ (π΄βπ) β β)) |
20 | | imnan 401 |
. . . . . . . . . . . . 13
β’ ((π β β β Β¬
(π΄βπ) β β) β Β¬ (π β β β§ (π΄βπ) β β)) |
21 | 19, 20 | sylibr 233 |
. . . . . . . . . . . 12
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β (π β β β Β¬
(π΄βπ) β β)) |
22 | 13, 21 | mpd 15 |
. . . . . . . . . . 11
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β Β¬ (π΄βπ) β β) |
23 | 15, 13 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β (π΄βπ) β
β0) |
24 | | elnn0 12422 |
. . . . . . . . . . . 12
β’ ((π΄βπ) β β0 β ((π΄βπ) β β β¨ (π΄βπ) = 0)) |
25 | 23, 24 | sylib 217 |
. . . . . . . . . . 11
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β ((π΄βπ) β β β¨ (π΄βπ) = 0)) |
26 | | orel1 888 |
. . . . . . . . . . 11
β’ (Β¬
(π΄βπ) β β β (((π΄βπ) β β β¨ (π΄βπ) = 0) β (π΄βπ) = 0)) |
27 | 22, 25, 26 | sylc 65 |
. . . . . . . . . 10
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β (π΄βπ) = 0) |
28 | 27 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β ((π΄βπ) Β· π) = (0 Β· π)) |
29 | 13 | nncnd 12176 |
. . . . . . . . . 10
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β π β
β) |
30 | 29 | mul02d 11360 |
. . . . . . . . 9
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β (0 Β· π) = 0) |
31 | 28, 30 | eqtrd 2777 |
. . . . . . . 8
β’ ((π΄:ββΆβ0 β§
π β (β β
(β‘π΄ β β))) β ((π΄βπ) Β· π) = 0) |
32 | | nnuz 12813 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
33 | 32 | eqimssi 4007 |
. . . . . . . . 9
β’ β
β (β€β₯β1) |
34 | 33 | a1i 11 |
. . . . . . . 8
β’ (π΄:ββΆβ0 β
β β (β€β₯β1)) |
35 | 5, 11, 31, 34 | sumss 15616 |
. . . . . . 7
β’ (π΄:ββΆβ0 β
Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = Ξ£π β β ((π΄βπ) Β· π)) |
36 | 35 | eqcomd 2743 |
. . . . . 6
β’ (π΄:ββΆβ0 β
Ξ£π β β
((π΄βπ) Β· π) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin) β
Ξ£π β β
((π΄βπ) Β· π) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) |
38 | 37 | eqeq1d 2739 |
. . . 4
β’ ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin) β
(Ξ£π β β
((π΄βπ) Β· π) = π β Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) |
39 | 38 | pm5.32i 576 |
. . 3
β’ (((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin) β§
Ξ£π β β
((π΄βπ) Β· π) = π) β ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin) β§
Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) |
40 | | df-3an 1090 |
. . 3
β’ ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β β
((π΄βπ) Β· π) = π) β ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin) β§
Ξ£π β β
((π΄βπ) Β· π) = π)) |
41 | | df-3an 1090 |
. . 3
β’ ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π) β ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin) β§
Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) |
42 | 39, 40, 41 | 3bitr4i 303 |
. 2
β’ ((π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β β
((π΄βπ) Β· π) = π) β (π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) |
43 | 2, 42 | bitri 275 |
1
β’ (π΄ β π β (π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π) = π)) |