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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8951 . 2  class  1
2 cc0 8950 . 2  class  0
31, 2wne 2571 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  9042  1re  9050  mul02lem2  9203  addid1  9206  ine0  9429  0lt1  9510  recne0  9651  div1  9667  recdiv  9680  divdiv1  9685  divdiv2  9686  recgt0ii  9876  expcl2lem  11352  m1expcl2  11362  expclzlem  11364  1exp  11368  s1nz  11718  s2f1o  11822  f1oun2prg  11823  iseraltlem2  12435  iseraltlem3  12436  iseralt  12437  geo2sum2  12610  geoihalfsum  12618  efne0  12657  tan0  12711  divalg  12882  gcd1  12991  rpdvds  13083  pcpre1  13175  pc1  13188  pcrec  13191  pcid  13205  prmreclem2  13244  mvrf1  16448  cndrng  16689  gzrngunitlem  16722  gzrngunit  16723  zrngunit  16724  dscmet  18577  xrhmeo  18928  i1f1lem  19538  itg11  19540  iblcnlem1  19636  itgcnlem  19638  ply1remlem  20042  dgrid  20139  dgrsub  20147  plyrem  20179  facth  20180  fta1lem  20181  vieta1lem1  20184  vieta1lem2  20185  vieta1  20186  qaa  20197  iaa  20199  coseq00topi  20367  logneg2  20467  logtayl2  20510  1cxp  20520  cxpeq0  20526  root1eq1  20596  root1cj  20597  cxpeq  20598  angneg  20602  ang180lem1  20608  ang180lem4  20611  ang180lem5  20612  isosctrlem2  20620  isosctrlem3  20621  angpined  20628  1cubrlem  20638  dcubic2  20641  dcubic  20643  mcubic  20644  cubic2  20645  dquartlem1  20648  asinlem  20665  atandmtan  20717  atantayl2  20735  efrlim  20765  basellem2  20821  isnsqf  20875  mumullem2  20920  sqff1o  20922  1sgm2ppw  20941  dchrn0  20991  dchrfi  20996  dchrptlem1  21005  dchrptlem2  21006  dchrpt  21008  lgsne0  21074  lgsqr  21087  lgseisenlem1  21090  lgseisenlem2  21091  lgseisenlem4  21093  lgseisen  21094  lgsquadlem1  21095  lgsquad2lem1  21099  lgsquad3  21102  m1lgs  21103  2sqlem7  21111  2sqlem8a  21112  2sqlem8  21113  chebbnd2  21128  chto1lb  21129  pnt2  21264  pnt  21265  qabvle  21276  qabvexp  21277  ostthlem2  21279  ostth3  21289  ostth  21290  usgraexmpldifpr  21376  usgraexmpl  21377  2trllemA  21507  2trllemH  21509  2trllemE  21510  2wlklemA  21511  2wlklemB  21512  2trllemD  21514  2trllemG  21515  wlkntrllem1  21516  wlkntrllem2  21517  wlkntrllem3  21518  constr1trl  21545  1pthon  21548  2wlklem1  21554  2pthon  21559  2pthon3v  21561  usgrcyclnl2  21585  constr3lem2  21590  constr3lem4  21591  constr3lem5  21592  constr3trllem1  21594  constr3trllem3  21596  constr3pthlem1  21599  4cycl4dv  21611  konigsberg  21666  ablomul  21900  mulid  21901  vcoprne  22015  hvsubcan  22533  hvsubcan2  22534  norm1exi  22709  kbpj  23416  largei  23727  superpos  23814  xrge0iif1  24281  logb1  24360  ind1a  24375  indf1o  24378  cntnevol  24539  ballotlemii  24718  m1expevenALT  24862  indispcon  24878  fprodntriv  25225  prod0  25226  prod1  25227  fprodn0  25260  axlowdimlem6  25794  axlowdimlem13  25801  axlowdimlem14  25802  axlowdim1  25806  0dioph  26731  pell1234qrne0  26810  bezoutr1  26945  mncn0  27216  aaitgo  27239  psgnunilem4  27292  m1expaddsub  27293  psgnuni  27294  cnmsgnsubg  27306  cnmsgngrp  27308  proot1ex  27392  expgrowth  27424  stoweidlem13  27633  wallispi2lem1  27691  f13idfv  27967  usgra2pthspth  28039  usgra2wlkspthlem1  28040  usgra2wlkspthlem2  28041  usgra2pthlem1  28044  sec0  28221
  Copyright terms: Public domain W3C validator