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

Theorem divides 12533
Description: Define the divides relation.  M  ||  N means  M divides into  N with no remainder. For example,  3  ||  6 (ex-dvds 20835). As proven in dvdsval3 12535, 
M  ||  N  <->  ( N  mod  M )  =  0. See divides 12533 and dvdsval2 12534 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
divides  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  ||  N  <->  E. n  e.  ZZ  (
n  x.  M )  =  N ) )
Distinct variable groups:    n, M    n, N

Proof of Theorem divides
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 4024 . . 3  |-  ( M 
||  N  <->  <. M ,  N >.  e.  ||  )
2 df-dvds 12532 . . . 4  |-  ||  =  { <. x ,  y
>.  |  ( (
x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x
)  =  y ) }
32eleq2i 2347 . . 3  |-  ( <. M ,  N >.  e. 
|| 
<-> 
<. M ,  N >.  e. 
{ <. x ,  y
>.  |  ( (
x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x
)  =  y ) } )
41, 3bitri 240 . 2  |-  ( M 
||  N  <->  <. M ,  N >.  e.  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) } )
5 oveq2 5866 . . . . 5  |-  ( x  =  M  ->  (
n  x.  x )  =  ( n  x.  M ) )
65eqeq1d 2291 . . . 4  |-  ( x  =  M  ->  (
( n  x.  x
)  =  y  <->  ( n  x.  M )  =  y ) )
76rexbidv 2564 . . 3  |-  ( x  =  M  ->  ( E. n  e.  ZZ  ( n  x.  x
)  =  y  <->  E. n  e.  ZZ  ( n  x.  M )  =  y ) )
8 eqeq2 2292 . . . 4  |-  ( y  =  N  ->  (
( n  x.  M
)  =  y  <->  ( n  x.  M )  =  N ) )
98rexbidv 2564 . . 3  |-  ( y  =  N  ->  ( E. n  e.  ZZ  ( n  x.  M
)  =  y  <->  E. n  e.  ZZ  ( n  x.  M )  =  N ) )
107, 9opelopab2 4285 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( <. M ,  N >.  e.  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }  <->  E. n  e.  ZZ  ( n  x.  M )  =  N ) )
114, 10syl5bb 248 1  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  ||  N  <->  E. n  e.  ZZ  (
n  x.  M )  =  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   E.wrex 2544   <.cop 3643   class class class wbr 4023   {copab 4076  (class class class)co 5858    x. cmul 8742   ZZcz 10024    || cdivides 12531
This theorem is referenced by:  dvdsval2  12534  dvds0lem  12539  dvds1lem  12540  dvds2lem  12541  0dvds  12549  dvdsle  12574  odd2np1  12587  oddm1even  12588  divalglem4  12595  divalglem9  12600  divalgb  12603  bezoutlem4  12720  gcddiv  12728  dvdssqim  12732  coprmdvds2  12782  opeo  12866  omeo  12867  prmpwdvds  12951  odmulg  14869  gexdvdsi  14894  lgsquadlem2  20594  dvdspw  24103  dvdsrabdioph  26891  jm2.26a  27093
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-iota 5219  df-fv 5263  df-ov 5861  df-dvds 12532
  Copyright terms: Public domain W3C validator