Theorem eulerpartlemf 32237

Description: Lemma for eulerpart 32249: Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017.)

Hypotheses

Ref	Expression
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

Ref	Expression
eulerpartlemf	⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0)

Distinct variable groups:   𝑧,𝑡   𝑓,𝑔,𝑘,𝑛,𝑡,𝐴   𝑓,𝐽   𝑓,𝑁   𝑃,𝑔

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑟)   𝐷(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑡,𝑓,𝑘,𝑛,𝑟)   𝑅(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑇(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐽(𝑥,𝑦,𝑧,𝑡,𝑔,𝑘,𝑛,𝑟)   𝑀(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑡,𝑔,𝑘,𝑛,𝑟)   𝑂(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑘,𝑛,𝑟)

Proof of Theorem eulerpartlemf

Step	Hyp	Ref	Expression
1		eldif 3893	. . . . . 6 ⊢ (𝑡 ∈ (ℕ ∖ 𝐽) ↔ (𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽))
2		breq2 5074	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑡))
3	2	notbid 317	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑡))
4		eulerpart.j	. . . . . . . . . 10 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
5	3, 4	elrab2 3620	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝐽 ↔ (𝑡 ∈ ℕ ∧ ¬ 2 ∥ 𝑡))
6	5	simplbi2 500	. . . . . . . 8 ⊢ (𝑡 ∈ ℕ → (¬ 2 ∥ 𝑡 → 𝑡 ∈ 𝐽))
7	6	con1d 145	. . . . . . 7 ⊢ (𝑡 ∈ ℕ → (¬ 𝑡 ∈ 𝐽 → 2 ∥ 𝑡))
8	7	imp 406	. . . . . 6 ⊢ ((𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽) → 2 ∥ 𝑡)
9	1, 8	sylbi 216	. . . . 5 ⊢ (𝑡 ∈ (ℕ ∖ 𝐽) → 2 ∥ 𝑡)
10	9	adantl 481	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → 2 ∥ 𝑡)
11	10	adantr 480	. . 3 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → 2 ∥ 𝑡)
12		simpll 763	. . . 4 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → 𝐴 ∈ (𝑇 ∩ 𝑅))
13		eldifi 4057	. . . . . 6 ⊢ (𝑡 ∈ (ℕ ∖ 𝐽) → 𝑡 ∈ ℕ)
14		eulerpart.p	. . . . . . . . . . 11 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
15		eulerpart.o	. . . . . . . . . . 11 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
16		eulerpart.d	. . . . . . . . . . 11 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
17		eulerpart.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
18		eulerpart.h	. . . . . . . . . . 11 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
19		eulerpart.m	. . . . . . . . . . 11 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
20		eulerpart.r	. . . . . . . . . . 11 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
21		eulerpart.t	. . . . . . . . . . 11 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
22	14, 15, 16, 4, 17, 18, 19, 20, 21	eulerpartlemt0 32236	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
23	22	simp1bi 1143	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0 ↑m ℕ))
24		elmapi 8595	. . . . . . . . 9 ⊢ (𝐴 ∈ (ℕ0 ↑m ℕ) → 𝐴:ℕ⟶ℕ0)
25	23, 24	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0)
26		ffn 6584	. . . . . . . 8 ⊢ (𝐴:ℕ⟶ℕ0 → 𝐴 Fn ℕ)
27		elpreima 6917	. . . . . . . 8 ⊢ (𝐴 Fn ℕ → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ)))
28	25, 26, 27	3syl 18	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ)))
29	28	baibd 539	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝐴‘𝑡) ∈ ℕ))
30	13, 29	sylan2 592	. . . . 5 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝐴‘𝑡) ∈ ℕ))
31	30	biimpar 477	. . . 4 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → 𝑡 ∈ (◡𝐴 “ ℕ))
32	22	simp3bi 1145	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽)
33	32	sselda 3917	. . . . 5 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (◡𝐴 “ ℕ)) → 𝑡 ∈ 𝐽)
34	5	simprbi 496	. . . . 5 ⊢ (𝑡 ∈ 𝐽 → ¬ 2 ∥ 𝑡)
35	33, 34	syl 17	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ 2 ∥ 𝑡)
36	12, 31, 35	syl2anc 583	. . 3 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) ∧ (𝐴‘𝑡) ∈ ℕ) → ¬ 2 ∥ 𝑡)
37	11, 36	pm2.65da 813	. 2 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → ¬ (𝐴‘𝑡) ∈ ℕ)
38	25	adantr 480	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → 𝐴:ℕ⟶ℕ0)
39	13	adantl 481	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → 𝑡 ∈ ℕ)
40	38, 39	ffvelrnd 6944	. . 3 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) ∈ ℕ0)
41		elnn0 12165	. . 3 ⊢ ((𝐴‘𝑡) ∈ ℕ0 ↔ ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0))
42	40, 41	sylib 217	. 2 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0))
43		orel1 885	. 2 ⊢ (¬ (𝐴‘𝑡) ∈ ℕ → (((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0) → (𝐴‘𝑡) = 0))
44	37, 42, 43	sylc 65	1 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108  {cab 2715  ∀wral 3063  {crab 3067   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530   class class class wbr 5070  {copab 5132   ↦ cmpt 5153  ^◡ccnv 5579   “ cima 5583   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257   supp csupp 7948   ↑_m cmap 8573  Fincfn 8691  0cc0 10802  1c1 10803   · cmul 10807   ≤ cle 10941  ℕcn 11903  2c2 11958  ℕ₀cn0 12163  ↑cexp 13710  Σcsu 15325   ∥ cdvds 15891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-map 8575  df-n0 12164

This theorem is referenced by:  eulerpartlemgh  32245