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 )