Theorem divides 11831

Description: Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 14960). As proven in dvdsval3 11833, M || N <-> ( N mod M ) = 0. See divides 11831 and dvdsval2 11832 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.

Step	Hyp	Ref	Expression
1		df-br 4019	. . 3 |- ( M || N <-> <. M , N >. e. || )
2		df-dvds 11830	. . . 4 |- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
3	2	eleq2i 2256	. . 3 |- ( <. M , N >. e. || <-> <. M , N >. e. { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) } )
4	1, 3	bitri 184	. 2 |- ( M || N <-> <. M , N >. e. { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) } )
5		oveq2 5905	. . . . 5 |- ( x = M -> ( n x. x ) = ( n x. M ) )
6	5	eqeq1d 2198	. . . 4 |- ( x = M -> ( ( n x. x ) = y <-> ( n x. M ) = y ) )
7	6	rexbidv 2491	. . 3 |- ( x = M -> ( E. n e. ZZ ( n x. x ) = y <-> E. n e. ZZ ( n x. M ) = y ) )
8		eqeq2 2199	. . . 4 |- ( y = N -> ( ( n x. M ) = y <-> ( n x. M ) = N ) )
9	8	rexbidv 2491	. . 3 |- ( y = N -> ( E. n e. ZZ ( n x. M ) = y <-> E. n e. ZZ ( n x. M ) = N ) )
10	7, 9	opelopab2 4288	. 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 ) )
11	4, 10	bitrid 192	1 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2160   E.wrex 2469   <.cop 3610   class class class wbr 4018   {copab 4078  (class class class)co 5897   x. cmul 7847   ZZcz 9284   || cdvds 11829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-iota 5196  df-fv 5243  df-ov 5900  df-dvds 11830

This theorem is referenced by:  dvdsval2  11832  dvds0lem  11843  dvds1lem  11844  dvds2lem  11845  0dvds  11853  dvdsle  11885  divconjdvds  11890  odd2np1  11913  even2n  11914  oddm1even  11915  opeo  11937  omeo  11938  m1exp1  11941  divalgb  11965  modremain  11969  zeqzmulgcd  12006  gcddiv  12055  dvdssqim  12060  coprmdvds2  12128  congr  12135  divgcdcoprm0  12136  cncongr2  12139  dvdsnprmd  12160  prmpwdvds  12390