Metamath Proof Explorer


Theorem eulerpartlemgf

Description: Lemma for eulerpart : Images under G have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018)

Ref Expression
Hypotheses eulerpart.p 𝑃 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( ( 𝑓 “ ℕ ) ∈ 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 𝑇 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( 𝑓 “ ℕ ) ⊆ 𝐽 }
eulerpart.g 𝐺 = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
Assertion eulerpartlemgf ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ℕ ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 eulerpart.p 𝑃 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( ( 𝑓 “ ℕ ) ∈ 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 𝑇 = { 𝑓 ∈ ( ℕ0m ℕ ) ∣ ( 𝑓 “ ℕ ) ⊆ 𝐽 }
10 eulerpart.g 𝐺 = ( 𝑜 ∈ ( 𝑇𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜𝐽 ) ) ) ) ) )
11 1 2 3 4 5 6 7 8 9 10 eulerpartlemgv ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ) )
12 11 cnveqd ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) = ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ) )
13 12 imaeq1d ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ { 1 } ) = ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ) “ { 1 } ) )
14 nnex ℕ ∈ V
15 imassrn ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ⊆ ran 𝐹
16 4 5 oddpwdc 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ
17 f1of ( 𝐹 : ( 𝐽 × ℕ0 ) –1-1-onto→ ℕ → 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ )
18 frn ( 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ → ran 𝐹 ⊆ ℕ )
19 16 17 18 mp2b ran 𝐹 ⊆ ℕ
20 15 19 sstri ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ⊆ ℕ
21 indpi1 ( ( ℕ ∈ V ∧ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ⊆ ℕ ) → ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ) “ { 1 } ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) )
22 14 20 21 mp2an ( ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ) “ { 1 } ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) )
23 13 22 eqtrdi ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ { 1 } ) = ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) )
24 ffun ( 𝐹 : ( 𝐽 × ℕ0 ) ⟶ ℕ → Fun 𝐹 )
25 16 17 24 mp2b Fun 𝐹
26 inss2 ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ⊆ Fin
27 1 2 3 4 5 6 7 8 9 10 eulerpartlemmf ( 𝐴 ∈ ( 𝑇𝑅 ) → ( bits ∘ ( 𝐴𝐽 ) ) ∈ 𝐻 )
28 1 2 3 4 5 6 7 eulerpartlem1 𝑀 : 𝐻1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
29 f1of ( 𝑀 : 𝐻1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) → 𝑀 : 𝐻 ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
30 28 29 ax-mp 𝑀 : 𝐻 ⟶ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
31 30 ffvelrni ( ( bits ∘ ( 𝐴𝐽 ) ) ∈ 𝐻 → ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
32 27 31 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ∈ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
33 26 32 sselid ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ∈ Fin )
34 imafi ( ( Fun 𝐹 ∧ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ∈ Fin ) → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ∈ Fin )
35 25 33 34 sylancr ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝐴𝐽 ) ) ) ) ∈ Fin )
36 23 35 eqeltrd ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ { 1 } ) ∈ Fin )
37 1 2 3 4 5 6 7 8 9 10 eulerpartgbij 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
38 f1of ( 𝐺 : ( 𝑇𝑅 ) –1-1-onto→ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → 𝐺 : ( 𝑇𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
39 37 38 ax-mp 𝐺 : ( 𝑇𝑅 ) ⟶ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 )
40 39 ffvelrni ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) )
41 elin ( ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) ↔ ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) ∧ ( 𝐺𝐴 ) ∈ 𝑅 ) )
42 41 simplbi ( ( 𝐺𝐴 ) ∈ ( ( { 0 , 1 } ↑m ℕ ) ∩ 𝑅 ) → ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) )
43 elmapi ( ( 𝐺𝐴 ) ∈ ( { 0 , 1 } ↑m ℕ ) → ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } )
44 40 42 43 3syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } )
45 44 ffund ( 𝐴 ∈ ( 𝑇𝑅 ) → Fun ( 𝐺𝐴 ) )
46 ssv 0 ⊆ V
47 dfn2 ℕ = ( ℕ0 ∖ { 0 } )
48 ssdif ( ℕ0 ⊆ V → ( ℕ0 ∖ { 0 } ) ⊆ ( V ∖ { 0 } ) )
49 47 48 eqsstrid ( ℕ0 ⊆ V → ℕ ⊆ ( V ∖ { 0 } ) )
50 46 49 ax-mp ℕ ⊆ ( V ∖ { 0 } )
51 sspreima ( ( Fun ( 𝐺𝐴 ) ∧ ℕ ⊆ ( V ∖ { 0 } ) ) → ( ( 𝐺𝐴 ) “ ℕ ) ⊆ ( ( 𝐺𝐴 ) “ ( V ∖ { 0 } ) ) )
52 45 50 51 sylancl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ℕ ) ⊆ ( ( 𝐺𝐴 ) “ ( V ∖ { 0 } ) ) )
53 fvex ( 𝐺𝐴 ) ∈ V
54 0nn0 0 ∈ ℕ0
55 suppimacnv ( ( ( 𝐺𝐴 ) ∈ V ∧ 0 ∈ ℕ0 ) → ( ( 𝐺𝐴 ) supp 0 ) = ( ( 𝐺𝐴 ) “ ( V ∖ { 0 } ) ) )
56 53 54 55 mp2an ( ( 𝐺𝐴 ) supp 0 ) = ( ( 𝐺𝐴 ) “ ( V ∖ { 0 } ) )
57 0ne1 0 ≠ 1
58 difprsn1 ( 0 ≠ 1 → ( { 0 , 1 } ∖ { 0 } ) = { 1 } )
59 57 58 ax-mp ( { 0 , 1 } ∖ { 0 } ) = { 1 }
60 59 eqcomi { 1 } = ( { 0 , 1 } ∖ { 0 } )
61 60 ffs2 ( ( ℕ ∈ V ∧ 0 ∈ ℕ0 ∧ ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } ) → ( ( 𝐺𝐴 ) supp 0 ) = ( ( 𝐺𝐴 ) “ { 1 } ) )
62 14 54 61 mp3an12 ( ( 𝐺𝐴 ) : ℕ ⟶ { 0 , 1 } → ( ( 𝐺𝐴 ) supp 0 ) = ( ( 𝐺𝐴 ) “ { 1 } ) )
63 44 62 syl ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) supp 0 ) = ( ( 𝐺𝐴 ) “ { 1 } ) )
64 56 63 eqtr3id ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ( V ∖ { 0 } ) ) = ( ( 𝐺𝐴 ) “ { 1 } ) )
65 52 64 sseqtrd ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ℕ ) ⊆ ( ( 𝐺𝐴 ) “ { 1 } ) )
66 ssfi ( ( ( ( 𝐺𝐴 ) “ { 1 } ) ∈ Fin ∧ ( ( 𝐺𝐴 ) “ ℕ ) ⊆ ( ( 𝐺𝐴 ) “ { 1 } ) ) → ( ( 𝐺𝐴 ) “ ℕ ) ∈ Fin )
67 36 65 66 syl2anc ( 𝐴 ∈ ( 𝑇𝑅 ) → ( ( 𝐺𝐴 ) “ ℕ ) ∈ Fin )