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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8996 . 2  class  1
2 cc0 8995 . 2  class  0
31, 2wne 2601 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  9087  1re  9095  mul02lem2  9248  addid1  9251  ine0  9474  0lt1  9555  recne0  9696  div1  9712  recdiv  9725  divdiv1  9730  divdiv2  9731  recgt0ii  9921  expcl2lem  11398  m1expcl2  11408  expclzlem  11410  1exp  11414  s1nz  11764  s2f1o  11868  f1oun2prg  11869  iseraltlem2  12481  iseraltlem3  12482  iseralt  12483  geo2sum2  12656  geoihalfsum  12664  efne0  12703  tan0  12757  divalg  12928  gcd1  13037  rpdvds  13129  pcpre1  13221  pc1  13234  pcrec  13237  pcid  13251  prmreclem2  13290  mvrf1  16494  cndrng  16735  gzrngunitlem  16768  gzrngunit  16769  zrngunit  16770  dscmet  18625  xrhmeo  18976  i1f1lem  19584  itg11  19586  iblcnlem1  19682  itgcnlem  19684  ply1remlem  20090  dgrid  20187  dgrsub  20195  plyrem  20227  facth  20228  fta1lem  20229  vieta1lem1  20232  vieta1lem2  20233  vieta1  20234  qaa  20245  iaa  20247  coseq00topi  20415  logneg2  20515  logtayl2  20558  1cxp  20568  cxpeq0  20574  root1eq1  20644  root1cj  20645  cxpeq  20646  angneg  20650  ang180lem1  20656  ang180lem4  20659  ang180lem5  20660  isosctrlem2  20668  isosctrlem3  20669  angpined  20676  1cubrlem  20686  dcubic2  20689  dcubic  20691  mcubic  20692  cubic2  20693  dquartlem1  20696  asinlem  20713  atandmtan  20765  atantayl2  20783  efrlim  20813  basellem2  20869  isnsqf  20923  mumullem2  20968  sqff1o  20970  1sgm2ppw  20989  dchrn0  21039  dchrfi  21044  dchrptlem1  21053  dchrptlem2  21054  dchrpt  21056  lgsne0  21122  lgsqr  21135  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem4  21141  lgseisen  21142  lgsquadlem1  21143  lgsquad2lem1  21147  lgsquad3  21150  m1lgs  21151  2sqlem7  21159  2sqlem8a  21160  2sqlem8  21161  chebbnd2  21176  chto1lb  21177  pnt2  21312  pnt  21313  qabvle  21324  qabvexp  21325  ostthlem2  21327  ostth3  21337  ostth  21338  usgraexmpldifpr  21424  usgraexmpl  21425  2trllemA  21555  2trllemH  21557  2trllemE  21558  2wlklemA  21559  2wlklemB  21560  2trllemD  21562  2trllemG  21563  wlkntrllem1  21564  wlkntrllem2  21565  wlkntrllem3  21566  constr1trl  21593  1pthon  21596  2wlklem1  21602  2pthon  21607  2pthon3v  21609  usgrcyclnl2  21633  constr3lem2  21638  constr3lem4  21639  constr3lem5  21640  constr3trllem1  21642  constr3trllem3  21644  constr3pthlem1  21647  4cycl4dv  21659  konigsberg  21714  ablomul  21948  mulid  21949  vcoprne  22063  hvsubcan  22581  hvsubcan2  22582  norm1exi  22757  kbpj  23464  largei  23775  superpos  23862  xrge0iif1  24329  logb1  24408  ind1a  24423  indf1o  24426  cntnevol  24587  ballotlemii  24766  m1expevenALT  24910  indispcon  24926  fprodntriv  25273  prod0  25274  prod1  25275  fprodn0  25308  axlowdimlem6  25891  axlowdimlem13  25898  axlowdimlem14  25899  axlowdim1  25903  0dioph  26850  pell1234qrne0  26929  bezoutr1  27064  mncn0  27334  aaitgo  27357  psgnunilem4  27410  m1expaddsub  27411  psgnuni  27412  cnmsgnsubg  27424  cnmsgngrp  27426  proot1ex  27510  expgrowth  27542  stoweidlem13  27751  wallispi2lem1  27809  f13idfv  28099  usgra2pthspth  28342  usgra2wlkspthlem1  28343  usgra2wlkspthlem2  28344  usgra2pthlem1  28347  sec0  28576
  Copyright terms: Public domain W3C validator