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

Theorem eulerpartlemgv 29565
Description: Lemma for eulerpart 29574: value of the function 𝐺. (Contributed by Thierry Arnoux, 13-Nov-2017.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
eulerpart.o 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
eulerpart.j 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
eulerpart.r 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
eulerpart.t 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
Assertion
Ref Expression
eulerpartlemgv (𝐴 ∈ (𝑇𝑅) → (𝐺𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽))))))
Distinct variable groups:   𝐴,𝑜   𝑜,𝐹   𝑜,𝐽   𝑜,𝑀   𝑅,𝑜   𝑇,𝑜
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑅(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑇(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐺(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝐽(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑀(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑂(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)

Proof of Theorem eulerpartlemgv
StepHypRef Expression
1 reseq1 5295 . . . . . 6 (𝑜 = 𝐴 → (𝑜𝐽) = (𝐴𝐽))
21coeq2d 5191 . . . . 5 (𝑜 = 𝐴 → (bits ∘ (𝑜𝐽)) = (bits ∘ (𝐴𝐽)))
32fveq2d 6089 . . . 4 (𝑜 = 𝐴 → (𝑀‘(bits ∘ (𝑜𝐽))) = (𝑀‘(bits ∘ (𝐴𝐽))))
43imaeq2d 5369 . . 3 (𝑜 = 𝐴 → (𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽)))) = (𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽)))))
54fveq2d 6089 . 2 (𝑜 = 𝐴 → ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽))))))
6 eulerpart.g . 2 𝐺 = (𝑜 ∈ (𝑇𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜𝐽))))))
7 fvex 6095 . 2 ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽))))) ∈ V
85, 6, 7fvmpt 6173 1 (𝐴 ∈ (𝑇𝑅) → (𝐺𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴𝐽))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1976  {cab 2592  wral 2892  {crab 2896  cin 3535  wss 3536  c0 3870  𝒫 cpw 4104   class class class wbr 4574  {copab 4633  cmpt 4634  ccnv 5024  cres 5027  cima 5028  ccom 5029  cfv 5787  (class class class)co 6524  cmpt2 6526   supp csupp 7156  𝑚 cmap 7718  Fincfn 7815  1c1 9790   · cmul 9794  cle 9928  cn 10864  2c2 10914  0cn0 11136  cexp 12674  Σcsu 14207  cdvds 14764  bitscbits 14922  𝟭cind 29203
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fv 5795
This theorem is referenced by:  eulerpartlemgvv  29568  eulerpartlemgf  29571  eulerpartlemn  29573
  Copyright terms: Public domain W3C validator