Step | Hyp | Ref
| Expression |
1 | | eldif 3925 |
. . . . . 6
β’ (π‘ β (β β π½) β (π‘ β β β§ Β¬ π‘ β π½)) |
2 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π§ = π‘ β (2 β₯ π§ β 2 β₯ π‘)) |
3 | 2 | notbid 318 |
. . . . . . . . . 10
β’ (π§ = π‘ β (Β¬ 2 β₯ π§ β Β¬ 2 β₯ π‘)) |
4 | | eulerpart.j |
. . . . . . . . . 10
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
5 | 3, 4 | elrab2 3653 |
. . . . . . . . 9
β’ (π‘ β π½ β (π‘ β β β§ Β¬ 2 β₯ π‘)) |
6 | 5 | simplbi2 502 |
. . . . . . . 8
β’ (π‘ β β β (Β¬ 2
β₯ π‘ β π‘ β π½)) |
7 | 6 | con1d 145 |
. . . . . . 7
β’ (π‘ β β β (Β¬
π‘ β π½ β 2 β₯ π‘)) |
8 | 7 | imp 408 |
. . . . . 6
β’ ((π‘ β β β§ Β¬
π‘ β π½) β 2 β₯ π‘) |
9 | 1, 8 | sylbi 216 |
. . . . 5
β’ (π‘ β (β β π½) β 2 β₯ π‘) |
10 | 9 | adantl 483 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β 2 β₯ π‘) |
11 | 10 | adantr 482 |
. . 3
β’ (((π΄ β (π β© π
) β§ π‘ β (β β π½)) β§ (π΄βπ‘) β β) β 2 β₯ π‘) |
12 | | simpll 766 |
. . . 4
β’ (((π΄ β (π β© π
) β§ π‘ β (β β π½)) β§ (π΄βπ‘) β β) β π΄ β (π β© π
)) |
13 | | eldifi 4091 |
. . . . . 6
β’ (π‘ β (β β π½) β π‘ β β) |
14 | | eulerpart.p |
. . . . . . . . . . 11
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
15 | | eulerpart.o |
. . . . . . . . . . 11
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
16 | | eulerpart.d |
. . . . . . . . . . 11
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
17 | | eulerpart.f |
. . . . . . . . . . 11
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
18 | | eulerpart.h |
. . . . . . . . . . 11
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
19 | | eulerpart.m |
. . . . . . . . . . 11
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
20 | | eulerpart.r |
. . . . . . . . . . 11
β’ π
= {π β£ (β‘π β β) β
Fin} |
21 | | eulerpart.t |
. . . . . . . . . . 11
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
22 | 14, 15, 16, 4, 17, 18, 19, 20, 21 | eulerpartlemt0 33009 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) |
23 | 22 | simp1bi 1146 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β π΄ β (β0
βm β)) |
24 | | elmapi 8794 |
. . . . . . . . 9
β’ (π΄ β (β0
βm β) β π΄:ββΆβ0) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β π΄:ββΆβ0) |
26 | | ffn 6673 |
. . . . . . . 8
β’ (π΄:ββΆβ0 β
π΄ Fn
β) |
27 | | elpreima 7013 |
. . . . . . . 8
β’ (π΄ Fn β β (π‘ β (β‘π΄ β β) β (π‘ β β β§ (π΄βπ‘) β β))) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . 7
β’ (π΄ β (π β© π
) β (π‘ β (β‘π΄ β β) β (π‘ β β β§ (π΄βπ‘) β β))) |
29 | 28 | baibd 541 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π‘ β β) β (π‘ β (β‘π΄ β β) β (π΄βπ‘) β β)) |
30 | 13, 29 | sylan2 594 |
. . . . 5
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β (π‘ β (β‘π΄ β β) β (π΄βπ‘) β β)) |
31 | 30 | biimpar 479 |
. . . 4
β’ (((π΄ β (π β© π
) β§ π‘ β (β β π½)) β§ (π΄βπ‘) β β) β π‘ β (β‘π΄ β β)) |
32 | 22 | simp3bi 1148 |
. . . . . 6
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β π½) |
33 | 32 | sselda 3949 |
. . . . 5
β’ ((π΄ β (π β© π
) β§ π‘ β (β‘π΄ β β)) β π‘ β π½) |
34 | 5 | simprbi 498 |
. . . . 5
β’ (π‘ β π½ β Β¬ 2 β₯ π‘) |
35 | 33, 34 | syl 17 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π‘ β (β‘π΄ β β)) β Β¬ 2 β₯
π‘) |
36 | 12, 31, 35 | syl2anc 585 |
. . 3
β’ (((π΄ β (π β© π
) β§ π‘ β (β β π½)) β§ (π΄βπ‘) β β) β Β¬ 2 β₯
π‘) |
37 | 11, 36 | pm2.65da 816 |
. 2
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β Β¬ (π΄βπ‘) β β) |
38 | 25 | adantr 482 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β π΄:ββΆβ0) |
39 | 13 | adantl 483 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β π‘ β β) |
40 | 38, 39 | ffvelcdmd 7041 |
. . 3
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β (π΄βπ‘) β
β0) |
41 | | elnn0 12422 |
. . 3
β’ ((π΄βπ‘) β β0 β ((π΄βπ‘) β β β¨ (π΄βπ‘) = 0)) |
42 | 40, 41 | sylib 217 |
. 2
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β ((π΄βπ‘) β β β¨ (π΄βπ‘) = 0)) |
43 | | orel1 888 |
. 2
β’ (Β¬
(π΄βπ‘) β β β (((π΄βπ‘) β β β¨ (π΄βπ‘) = 0) β (π΄βπ‘) = 0)) |
44 | 37, 42, 43 | sylc 65 |
1
β’ ((π΄ β (π β© π
) β§ π‘ β (β β π½)) β (π΄βπ‘) = 0) |