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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8947 . 2  class  1
2 cc0 8946 . 2  class  0
31, 2wne 2567 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  9038  1re  9046  mul02lem2  9199  addid1  9202  ine0  9425  0lt1  9506  recne0  9647  div1  9663  recdiv  9676  divdiv1  9681  divdiv2  9682  recgt0ii  9872  expcl2lem  11348  m1expcl2  11358  expclzlem  11360  1exp  11364  s1nz  11714  s2f1o  11818  f1oun2prg  11819  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  geo2sum2  12606  geoihalfsum  12614  efne0  12653  tan0  12707  divalg  12878  gcd1  12987  rpdvds  13079  pcpre1  13171  pc1  13184  pcrec  13187  pcid  13201  prmreclem2  13240  mvrf1  16444  cndrng  16685  gzrngunitlem  16718  gzrngunit  16719  zrngunit  16720  dscmet  18573  xrhmeo  18924  i1f1lem  19534  itg11  19536  iblcnlem1  19632  itgcnlem  19634  ply1remlem  20038  dgrid  20135  dgrsub  20143  plyrem  20175  facth  20176  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  qaa  20193  iaa  20195  coseq00topi  20363  logneg2  20463  logtayl2  20506  1cxp  20516  cxpeq0  20522  root1eq1  20592  root1cj  20593  cxpeq  20594  angneg  20598  ang180lem1  20604  ang180lem4  20607  ang180lem5  20608  isosctrlem2  20616  isosctrlem3  20617  angpined  20624  1cubrlem  20634  dcubic2  20637  dcubic  20639  mcubic  20640  cubic2  20641  dquartlem1  20644  asinlem  20661  atandmtan  20713  atantayl2  20731  efrlim  20761  basellem2  20817  isnsqf  20871  mumullem2  20916  sqff1o  20918  1sgm2ppw  20937  dchrn0  20987  dchrfi  20992  dchrptlem1  21001  dchrptlem2  21002  dchrpt  21004  lgsne0  21070  lgsqr  21083  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquad2lem1  21095  lgsquad3  21098  m1lgs  21099  2sqlem7  21107  2sqlem8a  21108  2sqlem8  21109  chebbnd2  21124  chto1lb  21125  pnt2  21260  pnt  21261  qabvle  21272  qabvexp  21273  ostthlem2  21275  ostth3  21285  ostth  21286  usgraexmpldifpr  21372  usgraexmpl  21373  2trllemA  21503  2trllemH  21505  2trllemE  21506  2wlklemA  21507  2wlklemB  21508  2trllemD  21510  2trllemG  21511  wlkntrllem1  21512  wlkntrllem2  21513  wlkntrllem3  21514  constr1trl  21541  1pthon  21544  2wlklem1  21550  2pthon  21555  2pthon3v  21557  usgrcyclnl2  21581  constr3lem2  21586  constr3lem4  21587  constr3lem5  21588  constr3trllem1  21590  constr3trllem3  21592  constr3pthlem1  21595  4cycl4dv  21607  konigsberg  21662  ablomul  21896  mulid  21897  vcoprne  22011  hvsubcan  22529  hvsubcan2  22530  norm1exi  22705  kbpj  23412  largei  23723  superpos  23810  xrge0iif1  24277  logb1  24356  ind1a  24371  indf1o  24374  cntnevol  24535  ballotlemii  24714  m1expevenALT  24858  indispcon  24874  fprodntriv  25221  prod0  25222  prod1  25223  fprodn0  25256  axlowdimlem6  25790  axlowdimlem13  25797  axlowdimlem14  25798  axlowdim1  25802  0dioph  26727  pell1234qrne0  26806  bezoutr1  26941  mncn0  27212  aaitgo  27235  psgnunilem4  27288  m1expaddsub  27289  psgnuni  27290  cnmsgnsubg  27302  cnmsgngrp  27304  proot1ex  27388  expgrowth  27420  stoweidlem13  27629  wallispi2lem1  27687  f13idfv  27963  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  sec0  28217
  Copyright terms: Public domain W3C validator