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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8917 . 2  class  1
2 cc0 8916 . 2  class  0
31, 2wne 2543 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  9008  1re  9016  mul02lem2  9168  addid1  9171  ine0  9394  0lt1  9475  recne0  9616  div1  9632  recdiv  9645  divdiv1  9650  divdiv2  9651  recgt0ii  9841  expcl2lem  11313  m1expcl2  11323  expclzlem  11325  1exp  11329  s1nz  11679  s2f1o  11783  f1oun2prg  11784  iseraltlem2  12396  iseraltlem3  12397  iseralt  12398  geo2sum2  12571  geoihalfsum  12579  efne0  12618  tan0  12672  divalg  12843  gcd1  12952  rpdvds  13044  pcpre1  13136  pc1  13149  pcrec  13152  pcid  13166  prmreclem2  13205  mvrf1  16409  cndrng  16646  gzrngunitlem  16679  gzrngunit  16680  zrngunit  16681  dscmet  18484  xrhmeo  18835  i1f1lem  19441  itg11  19443  iblcnlem1  19539  itgcnlem  19541  ply1remlem  19945  dgrid  20042  dgrsub  20050  plyrem  20082  facth  20083  fta1lem  20084  vieta1lem1  20087  vieta1lem2  20088  vieta1  20089  qaa  20100  iaa  20102  coseq00topi  20270  logneg2  20370  logtayl2  20413  1cxp  20423  cxpeq0  20429  root1eq1  20499  root1cj  20500  cxpeq  20501  angneg  20505  ang180lem1  20511  ang180lem4  20514  ang180lem5  20515  isosctrlem2  20523  isosctrlem3  20524  angpined  20531  1cubrlem  20541  dcubic2  20544  dcubic  20546  mcubic  20547  cubic2  20548  dquartlem1  20551  asinlem  20568  atandmtan  20620  atantayl2  20638  efrlim  20668  basellem2  20724  isnsqf  20778  mumullem2  20823  sqff1o  20825  1sgm2ppw  20844  dchrn0  20894  dchrfi  20899  dchrptlem1  20908  dchrptlem2  20909  dchrpt  20911  lgsne0  20977  lgsqr  20990  lgseisenlem1  20993  lgseisenlem2  20994  lgseisenlem4  20996  lgseisen  20997  lgsquadlem1  20998  lgsquad2lem1  21002  lgsquad3  21005  m1lgs  21006  2sqlem7  21014  2sqlem8a  21015  2sqlem8  21016  chebbnd2  21031  chto1lb  21032  pnt2  21167  pnt  21168  qabvle  21179  qabvexp  21180  ostthlem2  21182  ostth3  21192  ostth  21193  usgraexmpldifpr  21278  usgraexmpl  21279  wlkntrllem1  21406  wlkntrllem2  21407  wlkntrllem3  21408  wlkntrllem4  21409  wlkntrllem5  21410  constr1trl  21429  1pthon  21432  2trllem1  21435  2trllem4  21438  constr2trl  21439  2pthonlem2  21441  2pthon  21443  2pthon3v  21445  usgrcyclnl2  21469  constr3lem2  21474  constr3lem4  21475  constr3lem5  21476  constr3trllem1  21478  constr3trllem3  21480  constr3pthlem1  21483  4cycl4dv  21495  konigsberg  21550  ablomul  21784  mulid  21785  vcoprne  21899  hvsubcan  22417  hvsubcan2  22418  norm1exi  22593  kbpj  23300  largei  23611  superpos  23698  xrge0iif1  24121  logb1  24192  ind1a  24207  indf1o  24210  cntnevol  24369  ballotlemii  24533  m1expevenALT  24677  indispcon  24693  fprodntriv  25040  prod0  25041  prod1  25042  fprodn0  25075  axlowdimlem6  25593  axlowdimlem13  25600  axlowdimlem14  25601  axlowdim1  25605  0dioph  26521  pell1234qrne0  26600  bezoutr1  26735  mncn0  27006  aaitgo  27029  psgnunilem4  27082  m1expaddsub  27083  psgnuni  27084  cnmsgnsubg  27096  cnmsgngrp  27098  proot1ex  27182  expgrowth  27214  stoweidlem13  27423  wallispi2lem1  27481  sec0  27842
  Copyright terms: Public domain W3C validator