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

Theorem eulerpartlemo 34347
Description: Lemma for eulerpart 34364: 𝑂 is the set of odd partitions of 𝑁. (Contributed by Thierry Arnoux, 10-Aug-2017.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0m ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
eulerpart.o 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
Assertion
Ref Expression
eulerpartlemo (𝐴𝑂 ↔ (𝐴𝑃 ∧ ∀𝑛 ∈ (𝐴 “ ℕ) ¬ 2 ∥ 𝑛))
Distinct variable groups:   𝑔,𝑛,𝐴   𝑃,𝑔
Allowed substitution hints:   𝐴(𝑓,𝑘)   𝐷(𝑓,𝑔,𝑘,𝑛)   𝑃(𝑓,𝑘,𝑛)   𝑁(𝑓,𝑔,𝑘,𝑛)   𝑂(𝑓,𝑔,𝑘,𝑛)

Proof of Theorem eulerpartlemo
StepHypRef Expression
1 cnveq 5887 . . . 4 (𝑔 = 𝐴𝑔 = 𝐴)
21imaeq1d 6079 . . 3 (𝑔 = 𝐴 → (𝑔 “ ℕ) = (𝐴 “ ℕ))
32raleqdv 3324 . 2 (𝑔 = 𝐴 → (∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ (𝐴 “ ℕ) ¬ 2 ∥ 𝑛))
4 eulerpart.o . 2 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
53, 4elrab2 3698 1 (𝐴𝑂 ↔ (𝐴𝑃 ∧ ∀𝑛 ∈ (𝐴 “ ℕ) ¬ 2 ∥ 𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  {crab 3433   class class class wbr 5148  ccnv 5688  cima 5692  cfv 6563  (class class class)co 7431  m cmap 8865  Fincfn 8984  1c1 11154   · cmul 11158  cle 11294  cn 12264  2c2 12319  0cn0 12524  Σcsu 15719  cdvds 16287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702
This theorem is referenced by:  eulerpartlemr  34356
  Copyright terms: Public domain W3C validator