Theorem dvdsmul2 12395

Description: An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)

Assertion

Ref	Expression
dvdsmul2	|- ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )

Proof of Theorem dvdsmul2

Step	Hyp	Ref	Expression
1		zmulcl 9535	. 2 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
2		eqid 2230	. . 3 |- ( M x. N ) = ( M x. N )
3		dvds0lem 12382	. . 3 |- ( ( ( M e. ZZ /\ N e. ZZ /\ ( M x. N ) e. ZZ ) /\ ( M x. N ) = ( M x. N ) ) -> N || ( M x. N ) )
4	2, 3	mpan2 425	. 2 |- ( ( M e. ZZ /\ N e. ZZ /\ ( M x. N ) e. ZZ ) -> N || ( M x. N ) )
5	1, 4	mpd3an3 1374	1 |- ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004   = wceq 1397   e. wcel 2201   class class class wbr 4087  (class class class)co 6020   x. cmul 8039   ZZcz 9481   || cdvds 12368

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-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4206  ax-pow 4263  ax-pr 4298  ax-setind 4634  ax-cnex 8125  ax-resscn 8126  ax-1cn 8127  ax-1re 8128  ax-icn 8129  ax-addcl 8130  ax-addrcl 8131  ax-mulcl 8132  ax-mulrcl 8133  ax-addcom 8134  ax-mulcom 8135  ax-addass 8136  ax-mulass 8137  ax-distr 8138  ax-i2m1 8139  ax-1rid 8141  ax-0id 8142  ax-rnegex 8143  ax-cnre 8145

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-ral 2514  df-rex 2515  df-reu 2516  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3653  df-sn 3674  df-pr 3675  df-op 3677  df-uni 3893  df-int 3928  df-br 4088  df-opab 4150  df-id 4389  df-xp 4730  df-rel 4731  df-cnv 4732  df-co 4733  df-dm 4734  df-iota 5285  df-fun 5327  df-fv 5333  df-riota 5973  df-ov 6023  df-oprab 6024  df-mpo 6025  df-sub 8354  df-neg 8355  df-inn 9146  df-n0 9405  df-z 9482  df-dvds 12369

This theorem is referenced by:  iddvdsexp  12396  dvdsmultr2  12414  dvdsfac  12441  dvdsexp  12442  bitsinv1lem  12542  dvdssqim  12615  lcmval  12655  lcmcllem  12659  qredeq  12688  cncongr1  12695  sqpweven  12767  2sqpwodd  12768  hashdvds  12813  phimullem  12817  difsqpwdvds  12931  oddprmdvds  12947  4sqlem8  12978  dec2dvds  13004  oddennn  13033  perfectlem2  15750  lgsdir2lem2  15784  gausslemma2dlem1f1o  15815  lgsquadlem2  15833  lgsquadlem3  15834  lgsquad2lem1  15836  lgsquad2lem2  15837  2sqlem3  15872  2sqlem8  15878