Metamath Proof Explorer


Theorem eulerpartlemo

Description: Lemma for eulerpart : O is the set of odd partitions of N . (Contributed by Thierry Arnoux, 10-Aug-2017)

Ref Expression
Hypotheses eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
Assertion eulerpartlemo ( ๐ด โˆˆ ๐‘‚ โ†” ( ๐ด โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘› โˆˆ ( โ—ก ๐ด โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) )

Proof

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 โˆฅ ๐‘› ) )