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 33368
Description: Lemma for eulerpart 33381. (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 2819 . . . 4 (๐‘“ = ๐ด โ†’ ((โ—ก๐‘“ โ€œ โ„•) โˆˆ Fin โ†” (โ—ก๐ด โ€œ โ„•) โˆˆ Fin))
7 eulerpart.r . . . 4 ๐‘… = {๐‘“ โˆฃ (โ—ก๐‘“ โ€œ โ„•) โˆˆ Fin}
86, 7elab4g 3674 . . 3 (๐ด โˆˆ ๐‘… โ†” (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin))
95, 8anbi12i 628 . 2 ((๐ด โˆˆ ๐‘‡ โˆง ๐ด โˆˆ ๐‘…) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โˆง (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin)))
10 elin 3965 . 2 (๐ด โˆˆ (๐‘‡ โˆฉ ๐‘…) โ†” (๐ด โˆˆ ๐‘‡ โˆง ๐ด โˆˆ ๐‘…))
11 elex 3493 . . . . 5 (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โ†’ ๐ด โˆˆ V)
1211pm4.71i 561 . . . 4 (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ๐ด โˆˆ V))
1312anbi1i 625 . . 3 ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ๐ด โˆˆ V) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)))
14 3anass 1096 . . 3 ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)))
15 an42 656 . . 3 (((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โˆง (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin)) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง ๐ด โˆˆ V) โˆง ((โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ)))
1613, 14, 153bitr4i 303 . 2 ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โ†” ((๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ) โˆง (๐ด โˆˆ V โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin)))
179, 10, 163bitr4i 303 1 (๐ด โˆˆ (๐‘‡ โˆฉ ๐‘…) โ†” (๐ด โˆˆ (โ„•0 โ†‘m โ„•) โˆง (โ—ก๐ด โ€œ โ„•) โˆˆ Fin โˆง (โ—ก๐ด โ€œ โ„•) โŠ† ๐ฝ))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  {cab 2710  โˆ€wral 3062  {crab 3433  Vcvv 3475   โˆฉ 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 7409   โˆˆ cmpo 7411   supp csupp 8146   โ†‘m cmap 8820  Fincfn 8939  1c1 11111   ยท cmul 11115   โ‰ค cle 11249  โ„•cn 12212  2c2 12267  โ„•0cn0 12472  โ†‘cexp 14027  ฮฃcsu 15632   โˆฅ cdvds 16197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  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  33369  eulerpartlemt  33370  eulerpartlemmf  33374  eulerpartlemgvv  33375  eulerpartlemgu  33376  eulerpartlemgh  33377  eulerpartlemgs2  33379  eulerpartlemn  33380
  Copyright terms: Public domain W3C validator