Step | Hyp | Ref
| Expression |
1 | | elin 3931 |
. . . 4
β’ (β β (π β© π
) β (β β π β§ β β π
)) |
2 | 1 | anbi1i 625 |
. . 3
β’ ((β β (π β© π
) β§ β β π) β ((β β π β§ β β π
) β§ β β π)) |
3 | | elin 3931 |
. . 3
β’ (β β ((π β© π
) β© π) β (β β (π β© π
) β§ β β π)) |
4 | | eulerpart.p |
. . . . 5
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
5 | | eulerpart.o |
. . . . 5
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
6 | | eulerpart.d |
. . . . 5
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
7 | 4, 5, 6 | eulerpartlemo 33005 |
. . . 4
β’ (β β π β (β β π β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) |
8 | | cnveq 5834 |
. . . . . . . . . . . . . . . . 17
β’ (π = β β β‘π = β‘β) |
9 | 8 | imaeq1d 6017 |
. . . . . . . . . . . . . . . 16
β’ (π = β β (β‘π β β) = (β‘β β β)) |
10 | 9 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = β β ((β‘π β β) β Fin β (β‘β β β) β
Fin)) |
11 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β β (πβπ) = (ββπ)) |
12 | 11 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = β β ((πβπ) Β· π) = ((ββπ) Β· π)) |
13 | 12 | sumeq2sdv 15596 |
. . . . . . . . . . . . . . . 16
β’ (π = β β Ξ£π β β ((πβπ) Β· π) = Ξ£π β β ((ββπ) Β· π)) |
14 | 13 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
β’ (π = β β (Ξ£π β β ((πβπ) Β· π) = π β Ξ£π β β ((ββπ) Β· π) = π)) |
15 | 10, 14 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = β β (((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β ((β‘β β β) β Fin β§
Ξ£π β β
((ββπ) Β· π) = π))) |
16 | 15, 4 | elrab2 3653 |
. . . . . . . . . . . . 13
β’ (β β π β (β β (β0
βm β) β§ ((β‘β β β) β Fin β§
Ξ£π β β
((ββπ) Β· π) = π))) |
17 | 16 | simplbi 499 |
. . . . . . . . . . . 12
β’ (β β π β β β (β0
βm β)) |
18 | | cnvimass 6038 |
. . . . . . . . . . . . 13
β’ (β‘β β β) β dom β |
19 | | nn0ex 12426 |
. . . . . . . . . . . . . . 15
β’
β0 β V |
20 | | nnex 12166 |
. . . . . . . . . . . . . . 15
β’ β
β V |
21 | 19, 20 | elmap 8816 |
. . . . . . . . . . . . . 14
β’ (β β (β0
βm β) β β:ββΆβ0) |
22 | | fdm 6682 |
. . . . . . . . . . . . . 14
β’ (β:ββΆβ0 β dom
β =
β) |
23 | 21, 22 | sylbi 216 |
. . . . . . . . . . . . 13
β’ (β β (β0
βm β) β dom β = β) |
24 | 18, 23 | sseqtrid 4001 |
. . . . . . . . . . . 12
β’ (β β (β0
βm β) β (β‘β β β) β
β) |
25 | 17, 24 | syl 17 |
. . . . . . . . . . 11
β’ (β β π β (β‘β β β) β
β) |
26 | 25 | sselda 3949 |
. . . . . . . . . 10
β’ ((β β π β§ π β (β‘β β β)) β π β β) |
27 | 26 | ralrimiva 3144 |
. . . . . . . . 9
β’ (β β π β βπ β (β‘β β β)π β β) |
28 | 27 | biantrurd 534 |
. . . . . . . 8
β’ (β β π β (βπ β (β‘β β β) Β¬ 2 β₯ π β (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π))) |
29 | 17 | biantrurd 534 |
. . . . . . . 8
β’ (β β π β ((βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π) β (β β (β0
βm β) β§ (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)))) |
30 | 16 | simprbi 498 |
. . . . . . . . . 10
β’ (β β π β ((β‘β β β) β Fin β§
Ξ£π β β
((ββπ) Β· π) = π)) |
31 | 30 | simpld 496 |
. . . . . . . . 9
β’ (β β π β (β‘β β β) β Fin) |
32 | 31 | biantrud 533 |
. . . . . . . 8
β’ (β β π β ((β β (β0
βm β) β§ (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) β ((β β (β0
βm β) β§ (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) β§ (β‘β β β) β
Fin))) |
33 | 28, 29, 32 | 3bitrd 305 |
. . . . . . 7
β’ (β β π β (βπ β (β‘β β β) Β¬ 2 β₯ π β ((β β (β0
βm β) β§ (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) β§ (β‘β β β) β
Fin))) |
34 | | dfss3 3937 |
. . . . . . . . . 10
β’ ((β‘β β β) β π½ β βπ β (β‘β β β)π β π½) |
35 | | breq2 5114 |
. . . . . . . . . . . . 13
β’ (π§ = π β (2 β₯ π§ β 2 β₯ π)) |
36 | 35 | notbid 318 |
. . . . . . . . . . . 12
β’ (π§ = π β (Β¬ 2 β₯ π§ β Β¬ 2 β₯ π)) |
37 | | eulerpart.j |
. . . . . . . . . . . 12
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
38 | 36, 37 | elrab2 3653 |
. . . . . . . . . . 11
β’ (π β π½ β (π β β β§ Β¬ 2 β₯ π)) |
39 | 38 | ralbii 3097 |
. . . . . . . . . 10
β’
(βπ β
(β‘β β β)π β π½ β βπ β (β‘β β β)(π β β β§ Β¬ 2 β₯ π)) |
40 | | r19.26 3115 |
. . . . . . . . . 10
β’
(βπ β
(β‘β β β)(π β β β§ Β¬ 2 β₯ π) β (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) |
41 | 34, 39, 40 | 3bitri 297 |
. . . . . . . . 9
β’ ((β‘β β β) β π½ β (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) |
42 | 41 | anbi2i 624 |
. . . . . . . 8
β’ ((β β (β0
βm β) β§ (β‘β β β) β π½) β (β β (β0
βm β) β§ (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π))) |
43 | 42 | anbi1i 625 |
. . . . . . 7
β’ (((β β (β0
βm β) β§ (β‘β β β) β π½) β§ (β‘β β β) β Fin) β ((β β (β0
βm β) β§ (βπ β (β‘β β β)π β β β§ βπ β (β‘β β β) Β¬ 2 β₯ π)) β§ (β‘β β β) β
Fin)) |
44 | 33, 43 | bitr4di 289 |
. . . . . 6
β’ (β β π β (βπ β (β‘β β β) Β¬ 2 β₯ π β ((β β (β0
βm β) β§ (β‘β β β) β π½) β§ (β‘β β β) β
Fin))) |
45 | 9 | sseq1d 3980 |
. . . . . . . 8
β’ (π = β β ((β‘π β β) β π½ β (β‘β β β) β π½)) |
46 | | eulerpart.t |
. . . . . . . 8
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
47 | 45, 46 | elrab2 3653 |
. . . . . . 7
β’ (β β π β (β β (β0
βm β) β§ (β‘β β β) β π½)) |
48 | | vex 3452 |
. . . . . . . 8
β’ β β V |
49 | | eulerpart.r |
. . . . . . . 8
β’ π
= {π β£ (β‘π β β) β
Fin} |
50 | 48, 10, 49 | elab2 3639 |
. . . . . . 7
β’ (β β π
β (β‘β β β) β Fin) |
51 | 47, 50 | anbi12i 628 |
. . . . . 6
β’ ((β β π β§ β β π
) β ((β β (β0
βm β) β§ (β‘β β β) β π½) β§ (β‘β β β) β
Fin)) |
52 | 44, 51 | bitr4di 289 |
. . . . 5
β’ (β β π β (βπ β (β‘β β β) Β¬ 2 β₯ π β (β β π β§ β β π
))) |
53 | 52 | pm5.32i 576 |
. . . 4
β’ ((β β π β§ βπ β (β‘β β β) Β¬ 2 β₯ π) β (β β π β§ (β β π β§ β β π
))) |
54 | | ancom 462 |
. . . 4
β’ ((β β π β§ (β β π β§ β β π
)) β ((β β π β§ β β π
) β§ β β π)) |
55 | 7, 53, 54 | 3bitri 297 |
. . 3
β’ (β β π β ((β β π β§ β β π
) β§ β β π)) |
56 | 2, 3, 55 | 3bitr4ri 304 |
. 2
β’ (β β π β β β ((π β© π
) β© π)) |
57 | 56 | eqriv 2734 |
1
β’ π = ((π β© π
) β© π) |