MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1ne0 Unicode version

Axiom ax-1ne0 8806
Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 8782. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1ne0  |-  1  =/=  0

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8738 . 2  class  1
2 cc0 8737 . 2  class  0
31, 2wne 2446 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  8829  1re  8837  mul02lem2  8989  addid1  8992  ine0  9215  0lt1  9296  recne0  9437  div1  9453  recdiv  9466  divdiv1  9471  divdiv2  9472  recgt0ii  9662  expcl2lem  11115  m1expcl2  11125  expclzlem  11127  1exp  11131  s1nz  11445  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  geo2sum2  12330  geoihalfsum  12338  efne0  12377  tan0  12431  divalg  12602  gcd1  12711  rpdvds  12803  pcpre1  12895  pc1  12908  pcrec  12911  pcid  12925  prmreclem2  12964  mvrf1  16170  cndrng  16403  gzrngunitlem  16436  gzrngunit  16437  zrngunit  16438  dscmet  18095  xrhmeo  18444  i1f1lem  19044  itg11  19046  iblcnlem1  19142  itgcnlem  19144  ply1remlem  19548  dgrid  19645  dgrsub  19653  plyrem  19685  facth  19686  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  qaa  19703  iaa  19705  coseq00topi  19870  logneg2  19969  logtayl2  20009  1cxp  20019  cxpeq0  20025  root1eq1  20095  root1cj  20096  cxpeq  20097  angneg  20101  ang180lem1  20107  ang180lem4  20110  ang180lem5  20111  isosctrlem2  20119  isosctrlem3  20120  angpined  20127  1cubrlem  20137  dcubic2  20140  dcubic  20142  mcubic  20143  cubic2  20144  dquartlem1  20147  asinlem  20164  atandmtan  20216  atantayl2  20234  efrlim  20264  basellem2  20319  isnsqf  20373  mumullem2  20418  sqff1o  20420  1sgm2ppw  20439  dchrn0  20489  dchrfi  20494  dchrptlem1  20503  dchrptlem2  20504  dchrpt  20506  lgsne0  20572  lgsqr  20585  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquad2lem1  20597  lgsquad3  20600  m1lgs  20601  2sqlem7  20609  2sqlem8a  20610  2sqlem8  20611  chebbnd2  20626  chto1lb  20627  pnt2  20762  pnt  20763  qabvle  20774  qabvexp  20775  ostthlem2  20777  ostth3  20787  ostth  20788  ablomul  21022  mulid  21023  vcoprne  21135  hvsubcan  21653  hvsubcan2  21654  norm1exi  21829  kbpj  22536  largei  22847  superpos  22934  ballotlemii  23062  cntnevol  23175  xrge0iif1  23320  logb1  23405  ind1a  23604  indf1o  23607  indispcon  23765  konigsberg  23911  axlowdimlem6  24575  axlowdimlem13  24582  axlowdimlem14  24583  axlowdim1  24587  0dioph  26858  pell1234qrne0  26938  bezoutr1  27073  mncn0  27344  aaitgo  27367  psgnunilem4  27420  m1expaddsub  27421  psgnuni  27422  cnmsgnsubg  27434  cnmsgngrp  27436  proot1ex  27520  expgrowth  27552  stoweidlem7  27756  stoweidlem13  27762  wallispi2lem1  27820  f1oun2prg  28076  s2f1o  28091  usgraexmpldifpr  28132  usgraexmpl  28133  sec0  28230
  Copyright terms: Public domain W3C validator