Metamath Proof Explorer

Theorem eulerpartlemelr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 8-Aug-2018)

Ref Expression
Hypotheses eulerpartlems.r โŠข ๐‘… = { ๐‘“ โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
eulerpartlems.s โŠข ๐‘† = ( ๐‘“ โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†ฆ ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
Assertion eulerpartlemelr ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ( ๐ด : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐ด โ€œ โ„• ) โˆˆ Fin ) )

Proof

Step Hyp Ref Expression
1 eulerpartlems.r โŠข ๐‘… = { ๐‘“ โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
2 eulerpartlems.s โŠข ๐‘† = ( ๐‘“ โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†ฆ ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
3 inss1 โŠข ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โŠ† ( โ„•0 โ†‘m โ„• )
4 3 sseli โŠข ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ๐ด โˆˆ ( โ„•0 โ†‘m โ„• ) )
5 elmapi โŠข ( ๐ด โˆˆ ( โ„•0 โ†‘m โ„• ) โ†’ ๐ด : โ„• โŸถ โ„•0 )
6 4 5 syl โŠข ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ๐ด : โ„• โŸถ โ„•0 )
7 inss2 โŠข ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โŠ† ๐‘…
8 7 sseli โŠข ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ๐ด โˆˆ ๐‘… )
9 cnveq โŠข ( ๐‘“ = ๐ด โ†’ โ—ก ๐‘“ = โ—ก ๐ด )
10 9 imaeq1d โŠข ( ๐‘“ = ๐ด โ†’ ( โ—ก ๐‘“ โ€œ โ„• ) = ( โ—ก ๐ด โ€œ โ„• ) )
11 10 eleq1d โŠข ( ๐‘“ = ๐ด โ†’ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โ†” ( โ—ก ๐ด โ€œ โ„• ) โˆˆ Fin ) )
12 11 1 elab2g โŠข ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ( ๐ด โˆˆ ๐‘… โ†” ( โ—ก ๐ด โ€œ โ„• ) โˆˆ Fin ) )
13 8 12 mpbid โŠข ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ( โ—ก ๐ด โ€œ โ„• ) โˆˆ Fin )
14 6 13 jca โŠข ( ๐ด โˆˆ ( ( โ„•0 โ†‘m โ„• ) โˆฉ ๐‘… ) โ†’ ( ๐ด : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐ด โ€œ โ„• ) โˆˆ Fin ) )