MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  divides Structured version   Visualization version   GIF version

Theorem divides 16138
Description: Define the divides relation. ๐‘€ โˆฅ ๐‘ means ๐‘€ divides into ๐‘ with no remainder. For example, 3 โˆฅ 6 (ex-dvds 29400). As proven in dvdsval3 16140, ๐‘€ โˆฅ ๐‘ โ†” (๐‘ mod ๐‘€) = 0. See divides 16138 and dvdsval2 16139 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
divides ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
Distinct variable groups:   ๐‘›,๐‘€   ๐‘›,๐‘

Proof of Theorem divides
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 5106 . . 3 (๐‘€ โˆฅ ๐‘ โ†” โŸจ๐‘€, ๐‘โŸฉ โˆˆ โˆฅ )
2 df-dvds 16137 . . . 4 โˆฅ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)}
32eleq2i 2829 . . 3 (โŸจ๐‘€, ๐‘โŸฉ โˆˆ โˆฅ โ†” โŸจ๐‘€, ๐‘โŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)})
41, 3bitri 274 . 2 (๐‘€ โˆฅ ๐‘ โ†” โŸจ๐‘€, ๐‘โŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)})
5 oveq2 7365 . . . . 5 (๐‘ฅ = ๐‘€ โ†’ (๐‘› ยท ๐‘ฅ) = (๐‘› ยท ๐‘€))
65eqeq1d 2738 . . . 4 (๐‘ฅ = ๐‘€ โ†’ ((๐‘› ยท ๐‘ฅ) = ๐‘ฆ โ†” (๐‘› ยท ๐‘€) = ๐‘ฆ))
76rexbidv 3175 . . 3 (๐‘ฅ = ๐‘€ โ†’ (โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘ฆ))
8 eqeq2 2748 . . . 4 (๐‘ฆ = ๐‘ โ†’ ((๐‘› ยท ๐‘€) = ๐‘ฆ โ†” (๐‘› ยท ๐‘€) = ๐‘))
98rexbidv 3175 . . 3 (๐‘ฆ = ๐‘ โ†’ (โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘ฆ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
107, 9opelopab2 5498 . 2 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (โŸจ๐‘€, ๐‘โŸฉ โˆˆ {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โˆง โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘ฅ) = ๐‘ฆ)} โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
114, 10bitrid 282 1 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐‘€ โˆฅ ๐‘ โ†” โˆƒ๐‘› โˆˆ โ„ค (๐‘› ยท ๐‘€) = ๐‘))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106  โˆƒwrex 3073  โŸจcop 4592   class class class wbr 5105  {copab 5167  (class class class)co 7357   ยท cmul 11056  โ„คcz 12499   โˆฅ cdvds 16136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-iota 6448  df-fv 6504  df-ov 7360  df-dvds 16137
This theorem is referenced by:  dvdsval2  16139  dvds0lem  16149  dvds1lem  16150  dvds2lem  16151  0dvds  16159  dvdsle  16192  divconjdvds  16197  dvdsexp2im  16209  odd2np1  16223  even2n  16224  oddm1even  16225  opeo  16247  omeo  16248  m1exp1  16258  divalglem4  16278  divalglem9  16283  divalgb  16286  modremain  16290  zeqzmulgcd  16390  bezoutlem4  16423  gcddiv  16432  dvdssqim  16435  coprmdvds2  16530  congr  16540  divgcdcoprm0  16541  cncongr2  16544  dvdsnprmd  16566  prmpwdvds  16776  odmulg  19338  gexdvdsi  19365  lgsquadlem2  26729  dvdsexpim  40800  dvdsrabdioph  41119  jm2.26a  41310  coskpi2  44097  cosknegpi  44100  fourierswlem  44461  dfeven2  45831
  Copyright terms: Public domain W3C validator