Theorem eulerpartlemgu 34791

Description: Lemma for eulerpart 34796: Rewriting the 𝑈 set for an odd partition Note that interestingly, this proof reuses marypha2lem2 9406. (Contributed by Thierry Arnoux, 10-Aug-2018.)

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 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g	⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
eulerpartlemgh.1	⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))

Assertion

Ref	Expression
eulerpartlemgu	⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))})

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

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

Proof of Theorem eulerpartlemgu

Step	Hyp	Ref	Expression
1		eulerpartlemgh.1	. 2 ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))
2		eulerpart.p	. . . . . . . . . . 11 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
3		eulerpart.o	. . . . . . . . . . 11 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
4		eulerpart.d	. . . . . . . . . . 11 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
5		eulerpart.j	. . . . . . . . . . 11 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
6		eulerpart.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
7		eulerpart.h	. . . . . . . . . . 11 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
8		eulerpart.m	. . . . . . . . . . 11 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
9		eulerpart.r	. . . . . . . . . . 11 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
10		eulerpart.t	. . . . . . . . . . 11 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
11	2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemt0 34783	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
12	11	simp1bi 1163	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0 ↑m ℕ))
13		elmapi 8855	. . . . . . . . 9 ⊢ (𝐴 ∈ (ℕ0 ↑m ℕ) → 𝐴:ℕ⟶ℕ0)
14	12, 13	syl 18	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0)
15	14	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0)
16	15	ffund 6717	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → Fun 𝐴)
17		inss1 4192	. . . . . . . . 9 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)
18		cnvimass 6089	. . . . . . . . . 10 ⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴
19	18, 14	fssdm 6732	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ ℕ)
20	17, 19	sstrid 3951	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ)
21	20	sselda 3940	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ)
22	14	fdmd 6723	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom 𝐴 = ℕ)
23	22	eleq2d 2852	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ))
24	23	adantr 486	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝑡 ∈ dom 𝐴 ↔ 𝑡 ∈ ℕ))
25	21, 24	mpbird 260	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ dom 𝐴)
26		fvco 6986	. . . . . 6 ⊢ ((Fun 𝐴 ∧ 𝑡 ∈ dom 𝐴) → ((bits ∘ 𝐴)‘𝑡) = (bits‘(𝐴‘𝑡)))
27	16, 25, 26	syl2anc 596	. . . . 5 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ((bits ∘ 𝐴)‘𝑡) = (bits‘(𝐴‘𝑡)))
28	27	xpeq2d 5696	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ({𝑡} × (bits‘(𝐴‘𝑡))))
29	28	iuneq2dv 4986	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))
30		eqid 2766	. . . 4 ⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡))
31	30	marypha2lem2 9406	. . 3 ⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × ((bits ∘ 𝐴)‘𝑡)) = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))}
32	29, 31	eqtr3di 2816	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))})
33	1, 32	eqtrid 2813	1 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑈 = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ ((bits ∘ 𝐴)‘𝑡))})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {cab 2744  ∀wral 3082  {crab 3419   ∩ cin 3907   ⊆ wss 3908  ∅c0 4289  𝒫 cpw 4567  {csn 4594  ∪ ciun 4961   class class class wbr 5114  {copab 5178   ↦ cmpt 5197   × cxp 5664  ^◡ccnv 5665  dom cdm 5666   ↾ cres 5668   “ cima 5669   ∘ ccom 5670  Fun wfun 6537  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423   ∈ cmpo 7425   supp csupp 8165   ↑_m cmap 8833  Fincfn 8952  1c1 11119   · cmul 11123   ≤ cle 11262  𝟭cind 12236  ℕcn 12251  2c2 12313  ℕ₀cn0 12522  ↑cexp 14117  Σcsu 15763   ∥ cdvds 16335  bitscbits 16502

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-map 8835

This theorem is used by: (None)