Theorem divides 11764

Description: Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 14051). As proven in dvdsval3 11766, M || N <-> ( N mod M ) = 0. See divides 11764 and dvdsval2 11765 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 3999	. . 3 |- ( M || N <-> <. M , N >. e. || )
2		df-dvds 11763	. . . 4 |- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
3	2	eleq2i 2242	. . 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 5873	. . . . 5 |- ( x = M -> ( n x. x ) = ( n x. M ) )
6	5	eqeq1d 2184	. . . 4 |- ( x = M -> ( ( n x. x ) = y <-> ( n x. M ) = y ) )
7	6	rexbidv 2476	. . 3 |- ( x = M -> ( E. n e. ZZ ( n x. x ) = y <-> E. n e. ZZ ( n x. M ) = y ) )
8		eqeq2 2185	. . . 4 |- ( y = N -> ( ( n x. M ) = y <-> ( n x. M ) = N ) )
9	8	rexbidv 2476	. . 3 |- ( y = N -> ( E. n e. ZZ ( n x. M ) = y <-> E. n e. ZZ ( n x. M ) = N ) )
10	7, 9	opelopab2 4264	. 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 1353   e. wcel 2146   E.wrex 2454   <.cop 3592   class class class wbr 3998   {copab 4058  (class class class)co 5865   x. cmul 7791   ZZcz 9226   || cdvds 11762

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-opab 4060  df-iota 5170  df-fv 5216  df-ov 5868  df-dvds 11763

This theorem is referenced by:  dvdsval2  11765  dvds0lem  11776  dvds1lem  11777  dvds2lem  11778  0dvds  11786  dvdsle  11817  divconjdvds  11822  odd2np1  11845  even2n  11846  oddm1even  11847  opeo  11869  omeo  11870  m1exp1  11873  divalgb  11897  modremain  11901  zeqzmulgcd  11938  gcddiv  11987  dvdssqim  11992  coprmdvds2  12060  congr  12067  divgcdcoprm0  12068  cncongr2  12071  dvdsnprmd  12092  prmpwdvds  12320