eulerpartlemgv - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > eulerpartlemgv		Structured version Visualization version GIF version

Theorem eulerpartlemgv 33671

Description: Lemma for eulerpart 33680: value of the function 𝐺. (Contributed by Thierry Arnoux, 13-Nov-2017.)

**Hypotheses**
Ref	Expression
eulerpart.p	⊢ 𝑃 = {𝑓 ∈ (ℕ₀ ↑_m ℕ) ∣ ((^◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
eulerpart.o	⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (^◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d	⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
eulerpart.j	⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f	⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ₀ ↦ ((2↑𝑦) · 𝑥))
eulerpart.h	⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ₀ ∩ Fin) ↑_m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m	⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
eulerpart.r	⊢ 𝑅 = {𝑓 ∣ (^◡𝑓 “ ℕ) ∈ Fin}
eulerpart.t	⊢ 𝑇 = {𝑓 ∈ (ℕ₀ ↑_m ℕ) ∣ (^◡𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g	⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))

**Assertion**
Ref	Expression
eulerpartlemgv	⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))))

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

**Proof of Theorem eulerpartlemgv**
Step	Hyp	Ref	Expression
1		reseq1 5975	. . . . . 6 ⊢ (𝑜 = 𝐴 → (𝑜 ↾ 𝐽) = (𝐴 ↾ 𝐽))
2	1	coeq2d 5862	. . . . 5 ⊢ (𝑜 = 𝐴 → (bits ∘ (𝑜 ↾ 𝐽)) = (bits ∘ (𝐴 ↾ 𝐽)))
3	2	fveq2d 6895	. . . 4 ⊢ (𝑜 = 𝐴 → (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))) = (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))
4	3	imaeq2d 6059	. . 3 ⊢ (𝑜 = 𝐴 → (𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))
5	4	fveq2d 6895	. 2 ⊢ (𝑜 = 𝐴 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))))
6		eulerpart.g	. 2 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
7		fvex 6904	. 2 ⊢ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))) ∈ V
8	5, 6, 7	fvmpt 6998	1 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2105 {cab 2708 ∀wral 3060 {crab 3431 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 ^◡ccnv 5675 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 ‘cfv 6543 (class class class)co 7412 ∈ cmpo 7414 supp csupp 8150 ↑_m cmap 8824 Fincfn 8943 1c1 11115 · cmul 11119 ≤ cle 11254 ℕcn 12217 2c2 12272 ℕ₀cn0 12477 ↑cexp 14032 Σcsu 15637 ∥ cdvds 16202 bitscbits 16365 𝟭cind 33307

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fv 6551

This theorem is referenced by: eulerpartlemgvv 33674 eulerpartlemgf 33677 eulerpartlemn 33679

W3C validator