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 ⊢ 𝑃 = { 𝑓 ∈ ( ℕ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 eulerpartlemgf ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ ( 𝐺 ‘ 𝐴 ) “ ℕ ) ∈ Fin )

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 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 ffvelcdmi ⊢ ( ( 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 ffvelcdmi ⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝐺 ‘ 𝐴 ) ∈ ( ( { 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 )