Theorem divides 11796

Description: Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 14485). As proven in dvdsval3 11798, M || N <-> ( N mod M ) = 0. See divides 11796 and dvdsval2 11797 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 4005	. . 3 |- ( M || N <-> <. M , N >. e. || )
2		df-dvds 11795	. . . 4 |- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
3	2	eleq2i 2244	. . 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 5883	. . . . 5 |- ( x = M -> ( n x. x ) = ( n x. M ) )
6	5	eqeq1d 2186	. . . 4 |- ( x = M -> ( ( n x. x ) = y <-> ( n x. M ) = y ) )
7	6	rexbidv 2478	. . 3 |- ( x = M -> ( E. n e. ZZ ( n x. x ) = y <-> E. n e. ZZ ( n x. M ) = y ) )
8		eqeq2 2187	. . . 4 |- ( y = N -> ( ( n x. M ) = y <-> ( n x. M ) = N ) )
9	8	rexbidv 2478	. . 3 |- ( y = N -> ( E. n e. ZZ ( n x. M ) = y <-> E. n e. ZZ ( n x. M ) = N ) )
10	7, 9	opelopab2 4271	. 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 2148   E.wrex 2456   <.cop 3596   class class class wbr 4004   {copab 4064  (class class class)co 5875   x. cmul 7816   ZZcz 9253   || cdvds 11794

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-iota 5179  df-fv 5225  df-ov 5878  df-dvds 11795

This theorem is referenced by:  dvdsval2  11797  dvds0lem  11808  dvds1lem  11809  dvds2lem  11810  0dvds  11818  dvdsle  11850  divconjdvds  11855  odd2np1  11878  even2n  11879  oddm1even  11880  opeo  11902  omeo  11903  m1exp1  11906  divalgb  11930  modremain  11934  zeqzmulgcd  11971  gcddiv  12020  dvdssqim  12025  coprmdvds2  12093  congr  12100  divgcdcoprm0  12101  cncongr2  12104  dvdsnprmd  12125  prmpwdvds  12353