MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0dvds Unicode version

Theorem 0dvds 13339
Description: Only 0 is divisible by 0 . (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
0dvds

Proof of Theorem 0dvds
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 0z 10464 . . . 4
2 divides 13323 . . . 4
31, 2mpan 653 . . 3
4 zcn 10458 . . . . . . 7
54mul01d 9388 . . . . . 6
6 eqtr2 2499 . . . . . 6
75, 6sylan2 462 . . . . 5
87ancoms 441 . . . 4
98rexlimiva 2871 . . 3
103, 9syl6bi 221 . 2
11 dvds0 13334 . . . 4
121, 11ax-mp 5 . . 3
13 breq2 4306 . . 3
1412, 13mpbiri 226 . 2
1510, 14impbid1 196 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1662  e.wcel 1724  E.wrex 2752   class class class wbr 4302  (class class class)co 6067  0cc0 9104   cmul 9109   cz 10453   cdivides 13321
This theorem is referenced by:  fsumdvds  13362  dvdseq  13366  dvdssq  13530  rpdvds  13596  pcdvdstr  13728  pc2dvds  13731  mndodcongi  15684  oddvdsnn0  15685  oddvds  15688  odmulgeq  15696  odf1  15701  odf1o1  15709  gexdvds  15721  gexnnod  15725  torsubg  15972  znf1o  17335  jm2.19  27993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338  ax-resscn 9161  ax-1cn 9162  ax-icn 9163  ax-addcl 9164  ax-addrcl 9165  ax-mulcl 9166  ax-mulrcl 9167  ax-mulcom 9168  ax-addass 9169  ax-mulass 9170  ax-distr 9171  ax-i2m1 9172  ax-1ne0 9173  ax-1rid 9174  ax-rnegex 9175  ax-rrecex 9176  ax-cnre 9177  ax-pre-lttri 9178  ax-pre-lttrn 9179  ax-pre-ltadd 9180
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-nel 2647  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-mpt 4362  df-id 4639  df-po 4644  df-so 4645  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6070  df-er 7017  df-en 7222  df-dom 7223  df-sdom 7224  df-pnf 9242  df-mnf 9243  df-ltxr 9245  df-neg 9418  df-z 10454  df-dvds 13322
  Copyright terms: Public domain W3C validator