Step | Hyp | Ref
| Expression |
1 | | fveq1 6891 |
. . . . 5
β’ (π = π΄ β (πβπ) = (π΄βπ)) |
2 | 1 | breq1d 5159 |
. . . 4
β’ (π = π΄ β ((πβπ) β€ 1 β (π΄βπ) β€ 1)) |
3 | 2 | ralbidv 3178 |
. . 3
β’ (π = π΄ β (βπ β β (πβπ) β€ 1 β βπ β β (π΄βπ) β€ 1)) |
4 | | eulerpart.d |
. . 3
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
5 | 3, 4 | elrab2 3687 |
. 2
β’ (π΄ β π· β (π΄ β π β§ βπ β β (π΄βπ) β€ 1)) |
6 | | 2z 12594 |
. . . . . . . . 9
β’ 2 β
β€ |
7 | | fzoval 13633 |
. . . . . . . . 9
β’ (2 β
β€ β (0..^2) = (0...(2 β 1))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . 8
β’ (0..^2) =
(0...(2 β 1)) |
9 | | fzo0to2pr 13717 |
. . . . . . . 8
β’ (0..^2) =
{0, 1} |
10 | | 2m1e1 12338 |
. . . . . . . . 9
β’ (2
β 1) = 1 |
11 | 10 | oveq2i 7420 |
. . . . . . . 8
β’ (0...(2
β 1)) = (0...1) |
12 | 8, 9, 11 | 3eqtr3i 2769 |
. . . . . . 7
β’ {0, 1} =
(0...1) |
13 | 12 | eleq2i 2826 |
. . . . . 6
β’ ((π΄βπ) β {0, 1} β (π΄βπ) β (0...1)) |
14 | | eulerpart.p |
. . . . . . . . . 10
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
15 | 14 | eulerpartleme 33362 |
. . . . . . . . 9
β’ (π΄ β π β (π΄:ββΆβ0 β§
(β‘π΄ β β) β Fin β§
Ξ£π β β
((π΄βπ) Β· π) = π)) |
16 | 15 | simp1bi 1146 |
. . . . . . . 8
β’ (π΄ β π β π΄:ββΆβ0) |
17 | 16 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π΄ β π β§ π β β) β (π΄βπ) β
β0) |
18 | | 1nn0 12488 |
. . . . . . 7
β’ 1 β
β0 |
19 | | elfz2nn0 13592 |
. . . . . . . . 9
β’ ((π΄βπ) β (0...1) β ((π΄βπ) β β0 β§ 1 β
β0 β§ (π΄βπ) β€ 1)) |
20 | | df-3an 1090 |
. . . . . . . . 9
β’ (((π΄βπ) β β0 β§ 1 β
β0 β§ (π΄βπ) β€ 1) β (((π΄βπ) β β0 β§ 1 β
β0) β§ (π΄βπ) β€ 1)) |
21 | 19, 20 | bitri 275 |
. . . . . . . 8
β’ ((π΄βπ) β (0...1) β (((π΄βπ) β β0 β§ 1 β
β0) β§ (π΄βπ) β€ 1)) |
22 | 21 | baib 537 |
. . . . . . 7
β’ (((π΄βπ) β β0 β§ 1 β
β0) β ((π΄βπ) β (0...1) β (π΄βπ) β€ 1)) |
23 | 17, 18, 22 | sylancl 587 |
. . . . . 6
β’ ((π΄ β π β§ π β β) β ((π΄βπ) β (0...1) β (π΄βπ) β€ 1)) |
24 | 13, 23 | bitr2id 284 |
. . . . 5
β’ ((π΄ β π β§ π β β) β ((π΄βπ) β€ 1 β (π΄βπ) β {0, 1})) |
25 | 24 | ralbidva 3176 |
. . . 4
β’ (π΄ β π β (βπ β β (π΄βπ) β€ 1 β βπ β β (π΄βπ) β {0, 1})) |
26 | 16 | ffund 6722 |
. . . . 5
β’ (π΄ β π β Fun π΄) |
27 | | fdm 6727 |
. . . . . 6
β’ (π΄:ββΆβ0 β
dom π΄ =
β) |
28 | | eqimss2 4042 |
. . . . . 6
β’ (dom
π΄ = β β β
β dom π΄) |
29 | 16, 27, 28 | 3syl 18 |
. . . . 5
β’ (π΄ β π β β β dom π΄) |
30 | | funimass4 6957 |
. . . . 5
β’ ((Fun
π΄ β§ β β dom
π΄) β ((π΄ β β) β {0, 1}
β βπ β
β (π΄βπ) β {0,
1})) |
31 | 26, 29, 30 | syl2anc 585 |
. . . 4
β’ (π΄ β π β ((π΄ β β) β {0, 1} β
βπ β β
(π΄βπ) β {0, 1})) |
32 | 25, 31 | bitr4d 282 |
. . 3
β’ (π΄ β π β (βπ β β (π΄βπ) β€ 1 β (π΄ β β) β {0,
1})) |
33 | 32 | pm5.32i 576 |
. 2
β’ ((π΄ β π β§ βπ β β (π΄βπ) β€ 1) β (π΄ β π β§ (π΄ β β) β {0,
1})) |
34 | 5, 33 | bitri 275 |
1
β’ (π΄ β π· β (π΄ β π β§ (π΄ β β) β {0,
1})) |