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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8754 . 2  class  1
2 cc0 8753 . 2  class  0
31, 2wne 2459 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  8845  1re  8853  mul02lem2  9005  addid1  9008  ine0  9231  0lt1  9312  recne0  9453  div1  9469  recdiv  9482  divdiv1  9487  divdiv2  9488  recgt0ii  9678  expcl2lem  11131  m1expcl2  11141  expclzlem  11143  1exp  11147  s1nz  11461  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  geo2sum2  12346  geoihalfsum  12354  efne0  12393  tan0  12447  divalg  12618  gcd1  12727  rpdvds  12819  pcpre1  12911  pc1  12924  pcrec  12927  pcid  12941  prmreclem2  12980  mvrf1  16186  cndrng  16419  gzrngunitlem  16452  gzrngunit  16453  zrngunit  16454  dscmet  18111  xrhmeo  18460  i1f1lem  19060  itg11  19062  iblcnlem1  19158  itgcnlem  19160  ply1remlem  19564  dgrid  19661  dgrsub  19669  plyrem  19701  facth  19702  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  vieta1  19708  qaa  19719  iaa  19721  coseq00topi  19886  logneg2  19985  logtayl2  20025  1cxp  20035  cxpeq0  20041  root1eq1  20111  root1cj  20112  cxpeq  20113  angneg  20117  ang180lem1  20123  ang180lem4  20126  ang180lem5  20127  isosctrlem2  20135  isosctrlem3  20136  angpined  20143  1cubrlem  20153  dcubic2  20156  dcubic  20158  mcubic  20159  cubic2  20160  dquartlem1  20163  asinlem  20180  atandmtan  20232  atantayl2  20250  efrlim  20280  basellem2  20335  isnsqf  20389  mumullem2  20434  sqff1o  20436  1sgm2ppw  20455  dchrn0  20505  dchrfi  20510  dchrptlem1  20519  dchrptlem2  20520  dchrpt  20522  lgsne0  20588  lgsqr  20601  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquad2lem1  20613  lgsquad3  20616  m1lgs  20617  2sqlem7  20625  2sqlem8a  20626  2sqlem8  20627  chebbnd2  20642  chto1lb  20643  pnt2  20778  pnt  20779  qabvle  20790  qabvexp  20791  ostthlem2  20793  ostth3  20803  ostth  20804  ablomul  21038  mulid  21039  vcoprne  21151  hvsubcan  21669  hvsubcan2  21670  norm1exi  21845  kbpj  22552  largei  22863  superpos  22950  ballotlemii  23078  cntnevol  23191  xrge0iif1  23335  logb1  23420  ind1a  23619  indf1o  23622  indispcon  23780  konigsberg  23926  prod0  24168  prod1  24169  axlowdimlem6  24646  axlowdimlem13  24653  axlowdimlem14  24654  axlowdim1  24658  0dioph  26960  pell1234qrne0  27040  bezoutr1  27175  mncn0  27446  aaitgo  27469  psgnunilem4  27522  m1expaddsub  27523  psgnuni  27524  cnmsgnsubg  27536  cnmsgngrp  27538  proot1ex  27622  expgrowth  27654  stoweidlem7  27858  stoweidlem13  27864  wallispi2lem1  27922  f1oun2prg  28186  s2f1o  28222  usgraexmpldifpr  28265  usgraexmpl  28266  wlkntrllem1  28344  wlkntrllem2  28345  wlkntrllem3  28346  wlkntrllem4  28347  wlkntrllem5  28348  usgrcyclnl2  28386  constr3lem2  28391  constr3lem4  28392  constr3lem5  28393  constr3trllem1  28395  constr3trllem3  28397  constr3pthlem1  28400  4cycl4dv  28412  sec0  28483
  Copyright terms: Public domain W3C validator