Metamath Proof Explorer

Theorem eulerpartlemr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 13-Nov-2017)

Ref Expression
Hypotheses eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
eulerpart.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
eulerpart.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
eulerpart.h โŠข ๐ป = { ๐‘Ÿ โˆˆ ( ( ๐’ซ โ„•0 โˆฉ Fin ) โ†‘m ๐ฝ ) โˆฃ ( ๐‘Ÿ supp โˆ… ) โˆˆ Fin }
eulerpart.m โŠข ๐‘€ = ( ๐‘Ÿ โˆˆ ๐ป โ†ฆ { โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ โˆฃ ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ) } )
eulerpart.r โŠข ๐‘… = { ๐‘“ โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
eulerpart.t โŠข ๐‘‡ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โŠ† ๐ฝ }
eulerpart.g โŠข ๐บ = ( ๐‘œ โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ( ๐Ÿญ โ€˜ โ„• ) โ€˜ ( ๐น โ€œ ( ๐‘€ โ€˜ ( bits โˆ˜ ( ๐‘œ โ†พ ๐ฝ ) ) ) ) ) )
Assertion eulerpartlemr ๐‘‚ = ( ( ๐‘‡ โˆฉ ๐‘… ) โˆฉ ๐‘ƒ )

Proof

Step Hyp Ref Expression
1 eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
2 eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
3 eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
4 eulerpart.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
5 eulerpart.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
6 eulerpart.h โŠข ๐ป = { ๐‘Ÿ โˆˆ ( ( ๐’ซ โ„•0 โˆฉ Fin ) โ†‘m ๐ฝ ) โˆฃ ( ๐‘Ÿ supp โˆ… ) โˆˆ Fin }
7 eulerpart.m โŠข ๐‘€ = ( ๐‘Ÿ โˆˆ ๐ป โ†ฆ { โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ โˆฃ ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ) } )
8 eulerpart.r โŠข ๐‘… = { ๐‘“ โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
9 eulerpart.t โŠข ๐‘‡ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โŠ† ๐ฝ }
10 eulerpart.g โŠข ๐บ = ( ๐‘œ โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ( ๐Ÿญ โ€˜ โ„• ) โ€˜ ( ๐น โ€œ ( ๐‘€ โ€˜ ( bits โˆ˜ ( ๐‘œ โ†พ ๐ฝ ) ) ) ) ) )
11 elin โŠข ( โ„Ž โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†” ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) )
12 11 anbi1i โŠข ( ( โ„Ž โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง โ„Ž โˆˆ ๐‘ƒ ) โ†” ( ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) โˆง โ„Ž โˆˆ ๐‘ƒ ) )
13 elin โŠข ( โ„Ž โˆˆ ( ( ๐‘‡ โˆฉ ๐‘… ) โˆฉ ๐‘ƒ ) โ†” ( โ„Ž โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง โ„Ž โˆˆ ๐‘ƒ ) )
14 1 2 3 eulerpartlemo โŠข ( โ„Ž โˆˆ ๐‘‚ โ†” ( โ„Ž โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) )
15 cnveq โŠข ( ๐‘“ = โ„Ž โ†’ โ—ก ๐‘“ = โ—ก โ„Ž )
16 15 imaeq1d โŠข ( ๐‘“ = โ„Ž โ†’ ( โ—ก ๐‘“ โ€œ โ„• ) = ( โ—ก โ„Ž โ€œ โ„• ) )
17 16 eleq1d โŠข ( ๐‘“ = โ„Ž โ†’ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โ†” ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) )
18 fveq1 โŠข ( ๐‘“ = โ„Ž โ†’ ( ๐‘“ โ€˜ ๐‘˜ ) = ( โ„Ž โ€˜ ๐‘˜ ) )
19 18 oveq1d โŠข ( ๐‘“ = โ„Ž โ†’ ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ( ( โ„Ž โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
20 19 sumeq2sdv โŠข ( ๐‘“ = โ„Ž โ†’ ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ฮฃ ๐‘˜ โˆˆ โ„• ( ( โ„Ž โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
21 20 eqeq1d โŠข ( ๐‘“ = โ„Ž โ†’ ( ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ โ†” ฮฃ ๐‘˜ โˆˆ โ„• ( ( โ„Ž โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) )
22 17 21 anbi12d โŠข ( ๐‘“ = โ„Ž โ†’ ( ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โ†” ( ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( โ„Ž โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) ) )
23 22 1 elrab2 โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†” ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( โ„Ž โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) ) )
24 23 simplbi โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) )
25 cnvimass โŠข ( โ—ก โ„Ž โ€œ โ„• ) โŠ† dom โ„Ž
26 nn0ex โŠข โ„•0 โˆˆ V
27 nnex โŠข โ„• โˆˆ V
28 26 27 elmap โŠข ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โ†” โ„Ž : โ„• โŸถ โ„•0 )
29 fdm โŠข ( โ„Ž : โ„• โŸถ โ„•0 โ†’ dom โ„Ž = โ„• )
30 28 29 sylbi โŠข ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โ†’ dom โ„Ž = โ„• )
31 25 30 sseqtrid โŠข ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โ†’ ( โ—ก โ„Ž โ€œ โ„• ) โŠ† โ„• )
32 24 31 syl โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( โ—ก โ„Ž โ€œ โ„• ) โŠ† โ„• )
33 32 sselda โŠข ( ( โ„Ž โˆˆ ๐‘ƒ โˆง ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ) โ†’ ๐‘› โˆˆ โ„• )
34 33 ralrimiva โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• )
35 34 biantrurd โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› โ†” ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) )
36 24 biantrurd โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) โ†” ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) ) )
37 23 simprbi โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( โ„Ž โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) )
38 37 simpld โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin )
39 38 biantrud โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) โ†” ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) ) )
40 35 36 39 3bitrd โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› โ†” ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) ) )
41 dfss3 โŠข ( ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ โ†” โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ ๐ฝ )
42 breq2 โŠข ( ๐‘ง = ๐‘› โ†’ ( 2 โˆฅ ๐‘ง โ†” 2 โˆฅ ๐‘› ) )
43 42 notbid โŠข ( ๐‘ง = ๐‘› โ†’ ( ยฌ 2 โˆฅ ๐‘ง โ†” ยฌ 2 โˆฅ ๐‘› ) )
44 43 4 elrab2 โŠข ( ๐‘› โˆˆ ๐ฝ โ†” ( ๐‘› โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘› ) )
45 44 ralbii โŠข ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ ๐ฝ โ†” โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ( ๐‘› โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘› ) )
46 r19.26 โŠข ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ( ๐‘› โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘› ) โ†” ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) )
47 41 45 46 3bitri โŠข ( ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ โ†” ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) )
48 47 anbi2i โŠข ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ ) โ†” ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) )
49 48 anbi1i โŠข ( ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) โ†” ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ๐‘› โˆˆ โ„• โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) )
50 40 49 bitr4di โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› โ†” ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) ) )
51 16 sseq1d โŠข ( ๐‘“ = โ„Ž โ†’ ( ( โ—ก ๐‘“ โ€œ โ„• ) โŠ† ๐ฝ โ†” ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ ) )
52 51 9 elrab2 โŠข ( โ„Ž โˆˆ ๐‘‡ โ†” ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ ) )
53 vex โŠข โ„Ž โˆˆ V
54 53 17 8 elab2 โŠข ( โ„Ž โˆˆ ๐‘… โ†” ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin )
55 52 54 anbi12i โŠข ( ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) โ†” ( ( โ„Ž โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โŠ† ๐ฝ ) โˆง ( โ—ก โ„Ž โ€œ โ„• ) โˆˆ Fin ) )
56 50 55 bitr4di โŠข ( โ„Ž โˆˆ ๐‘ƒ โ†’ ( โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› โ†” ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) ) )
57 56 pm5.32i โŠข ( ( โ„Ž โˆˆ ๐‘ƒ โˆง โˆ€ ๐‘› โˆˆ ( โ—ก โ„Ž โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› ) โ†” ( โ„Ž โˆˆ ๐‘ƒ โˆง ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) ) )
58 ancom โŠข ( ( โ„Ž โˆˆ ๐‘ƒ โˆง ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) ) โ†” ( ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) โˆง โ„Ž โˆˆ ๐‘ƒ ) )
59 14 57 58 3bitri โŠข ( โ„Ž โˆˆ ๐‘‚ โ†” ( ( โ„Ž โˆˆ ๐‘‡ โˆง โ„Ž โˆˆ ๐‘… ) โˆง โ„Ž โˆˆ ๐‘ƒ ) )
60 12 13 59 3bitr4ri โŠข ( โ„Ž โˆˆ ๐‘‚ โ†” โ„Ž โˆˆ ( ( ๐‘‡ โˆฉ ๐‘… ) โˆฉ ๐‘ƒ ) )
61 60 eqriv โŠข ๐‘‚ = ( ( ๐‘‡ โˆฉ ๐‘… ) โˆฉ ๐‘ƒ )