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

Theorem divides 14319
Description: Define the divides relation.  M  ||  N means  M divides into  N with no remainder. For example,  3  ||  6 (ex-dvds 25910). As proven in dvdsval3 14321, 
M  ||  N  <->  ( N  mod  M )  =  0. See divides 14319 and dvdsval2 14320 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 4406 . . 3  |-  ( M 
||  N  <->  <. M ,  N >.  e.  ||  )
2 df-dvds 14318 . . . 4  |-  ||  =  { <. x ,  y
>.  |  ( (
x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x
)  =  y ) }
32eleq2i 2523 . . 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 253 . 2  |-  ( M 
||  N  <->  <. M ,  N >.  e.  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) } )
5 oveq2 6303 . . . . 5  |-  ( x  =  M  ->  (
n  x.  x )  =  ( n  x.  M ) )
65eqeq1d 2455 . . . 4  |-  ( x  =  M  ->  (
( n  x.  x
)  =  y  <->  ( n  x.  M )  =  y ) )
76rexbidv 2903 . . 3  |-  ( x  =  M  ->  ( E. n  e.  ZZ  ( n  x.  x
)  =  y  <->  E. n  e.  ZZ  ( n  x.  M )  =  y ) )
8 eqeq2 2464 . . . 4  |-  ( y  =  N  ->  (
( n  x.  M
)  =  y  <->  ( n  x.  M )  =  N ) )
98rexbidv 2903 . . 3  |-  ( y  =  N  ->  ( E. n  e.  ZZ  ( n  x.  M
)  =  y  <->  E. n  e.  ZZ  ( n  x.  M )  =  N ) )
107, 9opelopab2 4725 . 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 261 1  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  ||  N  <->  E. n  e.  ZZ  (
n  x.  M )  =  N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1446    e. wcel 1889   E.wrex 2740   <.cop 3976   class class class wbr 4405   {copab 4463  (class class class)co 6295    x. cmul 9549   ZZcz 10944    || cdvds 14317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-iota 5549  df-fv 5593  df-ov 6298  df-dvds 14318
This theorem is referenced by:  dvdsval2  14320  dvds0lem  14325  dvds1lem  14326  dvds2lem  14327  0dvds  14335  dvdsle  14362  odd2np1  14377  oddm1even  14378  divalglem4  14387  divalglem9  14393  divalglem9OLD  14394  divalgb  14397  bezoutlem4OLD  14518  bezoutlem4  14521  gcddiv  14529  dvdssqim  14533  coprmdvds2  14672  opeo  14775  omeo  14776  prmpwdvds  14860  odmulg  17219  gexdvdsi  17246  lgsquadlem2  24295  dvdspw  30398  dvdsrabdioph  35665  jm2.26a  35867  coskpi2  37751  cosknegpi  37754  fourierswlem  38104  dfeven2  38789
  Copyright terms: Public domain W3C validator