Theorem divides 12144

Description: Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 15740). As proven in dvdsval3 12146, M || N <-> ( N mod M ) = 0. See divides 12144 and dvdsval2 12145 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 4048	. . 3 |- ( M || N <-> <. M , N >. e. || )
2		df-dvds 12143	. . . 4 |- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
3	2	eleq2i 2273	. . 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 5959	. . . . 5 |- ( x = M -> ( n x. x ) = ( n x. M ) )
6	5	eqeq1d 2215	. . . 4 |- ( x = M -> ( ( n x. x ) = y <-> ( n x. M ) = y ) )
7	6	rexbidv 2508	. . 3 |- ( x = M -> ( E. n e. ZZ ( n x. x ) = y <-> E. n e. ZZ ( n x. M ) = y ) )
8		eqeq2 2216	. . . 4 |- ( y = N -> ( ( n x. M ) = y <-> ( n x. M ) = N ) )
9	8	rexbidv 2508	. . 3 |- ( y = N -> ( E. n e. ZZ ( n x. M ) = y <-> E. n e. ZZ ( n x. M ) = N ) )
10	7, 9	opelopab2 4321	. 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 1373   e. wcel 2177   E.wrex 2486   <.cop 3637   class class class wbr 4047   {copab 4108  (class class class)co 5951   x. cmul 7937   ZZcz 9379   || cdvds 12142

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-opab 4110  df-iota 5237  df-fv 5284  df-ov 5954  df-dvds 12143

This theorem is referenced by:  dvdsval2  12145  dvds0lem  12156  dvds1lem  12157  dvds2lem  12158  0dvds  12166  dvdsle  12199  divconjdvds  12204  odd2np1  12228  even2n  12229  oddm1even  12230  opeo  12252  omeo  12253  m1exp1  12256  divalgb  12280  modremain  12284  zeqzmulgcd  12335  gcddiv  12384  dvdssqim  12389  coprmdvds2  12459  congr  12466  divgcdcoprm0  12467  cncongr2  12470  dvdsnprmd  12491  prmpwdvds  12722  lgsquadlem2  15599