Theorem eulerpartlemf

Description: Lemma for eulerpart : Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-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 ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
Assertion	eulerpartlemf	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )

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		eldif	⊢ ( 𝑡 ∈ ( ℕ ∖ 𝐽 ) ↔ ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽 ) )
11		breq2	⊢ ( 𝑧 = 𝑡 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑡 ) )
12	11	notbid	⊢ ( 𝑧 = 𝑡 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑡 ) )
13	12 4	elrab2	⊢ ( 𝑡 ∈ 𝐽 ↔ ( 𝑡 ∈ ℕ ∧ ¬ 2 ∥ 𝑡 ) )
14	13	simplbi2	⊢ ( 𝑡 ∈ ℕ → ( ¬ 2 ∥ 𝑡 → 𝑡 ∈ 𝐽 ) )
15	14	con1d	⊢ ( 𝑡 ∈ ℕ → ( ¬ 𝑡 ∈ 𝐽 → 2 ∥ 𝑡 ) )
16	15	imp	⊢ ( ( 𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽 ) → 2 ∥ 𝑡 )
17	10 16	sylbi	⊢ ( 𝑡 ∈ ( ℕ ∖ 𝐽 ) → 2 ∥ 𝑡 )
18	17	adantl	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → 2 ∥ 𝑡 )
19	18	adantr	⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) → 2 ∥ 𝑡 )
20		simpll	⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) → 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) )
21		eldifi	⊢ ( 𝑡 ∈ ( ℕ ∖ 𝐽 ) → 𝑡 ∈ ℕ )
22	1 2 3 4 5 6 7 8 9	eulerpartlemt0	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 ) )
23	22	simp1bi	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 ∈ ( ℕ0 ↑m ℕ ) )
24		elmapi	⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) → 𝐴 : ℕ ⟶ ℕ0 )
25	23 24	syl	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
26		ffn	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
27		elpreima	⊢ ( 𝐴 Fn ℕ → ( 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) ) )
28	25 26 27	3syl	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑡 ∈ ℕ ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) ) )
29	28	baibd	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ℕ ) → ( 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) )
30	21 29	sylan2	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ( 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) )
31	30	biimpar	⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) → 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) )
32	22	simp3bi	⊢ ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ 𝐽 )
33	32	sselda	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑡 ∈ 𝐽 )
34	13	simprbi	⊢ ( 𝑡 ∈ 𝐽 → ¬ 2 ∥ 𝑡 )
35	33 34	syl	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ◡ 𝐴 “ ℕ ) ) → ¬ 2 ∥ 𝑡 )
36	20 31 35	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) ∧ ( 𝐴 ‘ 𝑡 ) ∈ ℕ ) → ¬ 2 ∥ 𝑡 )
37	19 36	pm2.65da	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ¬ ( 𝐴 ‘ 𝑡 ) ∈ ℕ )
38	25	adantr	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → 𝐴 : ℕ ⟶ ℕ0 )
39	21	adantl	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → 𝑡 ∈ ℕ )
40	38 39	ffvelcdmd	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 )
41		elnn0	⊢ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ0 ↔ ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑡 ) = 0 ) )
42	40 41	sylib	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑡 ) = 0 ) )
43		orel1	⊢ ( ¬ ( 𝐴 ‘ 𝑡 ) ∈ ℕ → ( ( ( 𝐴 ‘ 𝑡 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑡 ) = 0 ) → ( 𝐴 ‘ 𝑡 ) = 0 ) )
44	37 42 43	sylc	⊢ ( ( 𝐴 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℕ ∖ 𝐽 ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )