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

Theorem eulerpartlemt0 33663
Description: Lemma for eulerpart 33676. (Contributed by Thierry Arnoux, 19-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
eulerpartlemt0 (๐ด โˆˆ (๐‘‡ โˆฉ ๐‘…) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ))
Distinct variable groups:   ๐ด,๐‘“   ๐‘“,๐ฝ
Allowed substitution hints:   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐‘ƒ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐‘…(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐‘‡(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐น(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐ป(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐ฝ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐‘€(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)   ๐‘‚(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”,๐‘˜,๐‘›,๐‘Ÿ)

Proof of Theorem eulerpartlemt0
StepHypRef Expression
1 cnveq 5874 . . . . . 6 (๐‘“ = ๐ด โ†’ โ—ก๐‘“ = โ—ก๐ด)
21imaeq1d 6059 . . . . 5 (๐‘“ = ๐ด โ†’ (โ—ก๐‘“ โ€œ โ„•) = (โ—ก๐ด โ€œ โ„•))
32sseq1d 4014 . . . 4 (๐‘“ = ๐ด โ†’ ((โ—ก๐‘“ โ€œ โ„•) โŠ† ๐ฝ โ†” (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ))
4 eulerpart.t . . . 4 ๐‘‡ = {๐‘“ โˆˆ (โ„•0 โ†‘m โ„•) โˆฃ (โ—ก๐‘“ โ€œ โ„•) โŠ† ๐ฝ}
53, 4elrab2 3687 . . 3 (๐ด โˆˆ ๐‘‡ โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ))
62eleq1d 2817 . . . 4 (๐‘“ = ๐ด โ†’ ((โ—ก๐‘“ โ€œ โ„•) โˆˆ Fin โ†” (โ—ก๐ด โ€œ โ„•) โˆˆ Fin))
7 eulerpart.r . . . 4 ๐‘… = {๐‘“ โˆฃ (โ—ก๐‘“ โ€œ โ„•) โˆˆ Fin}
86, 7elab4g 3674 . . 3 (๐ด โˆˆ ๐‘… โ†” (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin))
95, 8anbi12i 626 . 2 ((๐ด โˆˆ ๐‘‡ โˆง ๐ด โˆˆ ๐‘…) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โˆง (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin)))
10 elin 3965 . 2 (๐ด โˆˆ (๐‘‡ โˆฉ ๐‘…) โ†” (๐ด โˆˆ ๐‘‡ โˆง ๐ด โˆˆ ๐‘…))
11 elex 3492 . . . . 5 (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โ†’ ๐ด โˆˆ V)
1211pm4.71i 559 . . . 4 (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ๐ด โˆˆ V))
1312anbi1i 623 . . 3 ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ๐ด โˆˆ V) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)))
14 3anass 1094 . . 3 ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)))
15 an42 654 . . 3 (((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โˆง (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin)) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ๐ด โˆˆ V) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)))
1613, 14, 153bitr4i 302 . 2 ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โˆง (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin)))
179, 10, 163bitr4i 302 1 (๐ด โˆˆ (๐‘‡ โˆฉ ๐‘…) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†” wb 205   โˆง wa 395   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105  {cab 2708  โˆ€wral 3060  {crab 3431  Vcvv 3473   โˆฉ cin 3948   โŠ† wss 3949  โˆ…c0 4323  ๐’ซ cpw 4603   class class class wbr 5149  {copab 5211   โ†ฆ cmpt 5232  โ—กccnv 5676   โ€œ cima 5680  โ€˜cfv 6544  (class class class)co 7412   โˆˆ cmpo 7414   supp csupp 8149   โ†‘m cmap 8823  Fincfn 8942  1c1 11114   ยท cmul 11118   โ‰ค cle 11254  โ„•cn 12217  2c2 12272  โ„•0cn0 12477  โ†‘cexp 14032  ฮฃcsu 15637   โˆฅ cdvds 16202
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-ext 2702
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-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690
This theorem is referenced by:  eulerpartlemf  33664  eulerpartlemt  33665  eulerpartlemmf  33669  eulerpartlemgvv  33670  eulerpartlemgu  33671  eulerpartlemgh  33672  eulerpartlemgs2  33674  eulerpartlemn  33675
  Copyright terms: Public domain W3C validator