Metamath Proof Explorer

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 )