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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8734 . 2  class  1
2 cc0 8733 . 2  class  0
31, 2wne 2448 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  8825  1re  8833  mul02lem2  8985  addid1  8988  ine0  9211  0lt1  9292  recne0  9433  div1  9449  recdiv  9462  divdiv1  9467  divdiv2  9468  recgt0ii  9658  expcl2lem  11110  m1expcl2  11120  expclzlem  11122  1exp  11126  s1nz  11440  iseraltlem2  12150  iseraltlem3  12151  iseralt  12152  geo2sum2  12325  geoihalfsum  12333  efne0  12372  tan0  12426  divalg  12597  gcd1  12706  rpdvds  12798  pcpre1  12890  pc1  12903  pcrec  12906  pcid  12920  prmreclem2  12959  mvrf1  16165  cndrng  16398  gzrngunitlem  16431  gzrngunit  16432  zrngunit  16433  dscmet  18090  xrhmeo  18439  i1f1lem  19039  itg11  19041  iblcnlem1  19137  itgcnlem  19139  ply1remlem  19543  dgrid  19640  dgrsub  19648  plyrem  19680  facth  19681  fta1lem  19682  vieta1lem1  19685  vieta1lem2  19686  vieta1  19687  qaa  19698  iaa  19700  coseq00topi  19865  logneg2  19964  logtayl2  20004  1cxp  20014  cxpeq0  20020  root1eq1  20090  root1cj  20091  cxpeq  20092  angneg  20096  ang180lem1  20102  ang180lem4  20105  ang180lem5  20106  isosctrlem2  20114  isosctrlem3  20115  angpined  20122  1cubrlem  20132  dcubic2  20135  dcubic  20137  mcubic  20138  cubic2  20139  dquartlem1  20142  asinlem  20159  atandmtan  20211  atantayl2  20229  efrlim  20259  basellem2  20314  isnsqf  20368  mumullem2  20413  sqff1o  20415  1sgm2ppw  20434  dchrn0  20484  dchrfi  20489  dchrptlem1  20498  dchrptlem2  20499  dchrpt  20501  lgsne0  20567  lgsqr  20580  lgseisenlem1  20583  lgseisenlem2  20584  lgseisenlem4  20586  lgseisen  20587  lgsquadlem1  20588  lgsquad2lem1  20592  lgsquad3  20595  m1lgs  20596  2sqlem7  20604  2sqlem8a  20605  2sqlem8  20606  chebbnd2  20621  chto1lb  20622  pnt2  20757  pnt  20758  qabvle  20769  qabvexp  20770  ostthlem2  20772  ostth3  20782  ostth  20783  ablomul  21015  mulid  21016  vcoprne  21128  hvsubcan  21646  hvsubcan2  21647  norm1exi  21822  kbpj  22529  largei  22840  superpos  22927  ballotlemii  23056  indispcon  23170  konigsberg  23316  axlowdimlem6  23983  axlowdimlem13  23990  axlowdimlem14  23991  axlowdim1  23995  0dioph  26258  pell1234qrne0  26338  bezoutr1  26473  mncn0  26744  aaitgo  26767  psgnunilem4  26820  m1expaddsub  26821  psgnuni  26822  cnmsgnsubg  26834  cnmsgngrp  26836  proot1ex  26920  expgrowth  26952  stoweidlem7  27156  stoweidlem13  27162  wallispi2lem1  27220  sec0  27491
  Copyright terms: Public domain W3C validator