Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpart.p |
โข ๐ = { ๐ โ ( โ0 โm โ ) โฃ ( ( โก ๐ โ โ ) โ Fin โง ฮฃ ๐ โ โ ( ( ๐ โ ๐ ) ยท ๐ ) = ๐ ) } |
2 |
|
eulerpart.o |
โข ๐ = { ๐ โ ๐ โฃ โ ๐ โ ( โก ๐ โ โ ) ยฌ 2 โฅ ๐ } |
3 |
|
eulerpart.d |
โข ๐ท = { ๐ โ ๐ โฃ โ ๐ โ โ ( ๐ โ ๐ ) โค 1 } |
4 |
|
cnveq |
โข ( ๐ = ๐ด โ โก ๐ = โก ๐ด ) |
5 |
4
|
imaeq1d |
โข ( ๐ = ๐ด โ ( โก ๐ โ โ ) = ( โก ๐ด โ โ ) ) |
6 |
5
|
raleqdv |
โข ( ๐ = ๐ด โ ( โ ๐ โ ( โก ๐ โ โ ) ยฌ 2 โฅ ๐ โ โ ๐ โ ( โก ๐ด โ โ ) ยฌ 2 โฅ ๐ ) ) |
7 |
6 2
|
elrab2 |
โข ( ๐ด โ ๐ โ ( ๐ด โ ๐ โง โ ๐ โ ( โก ๐ด โ โ ) ยฌ 2 โฅ ๐ ) ) |