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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8991 . 2  class  1
2 cc0 8990 . 2  class  0
31, 2wne 2599 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  9082  1re  9090  mul02lem2  9243  addid1  9246  ine0  9469  0lt1  9550  recne0  9691  div1  9707  recdiv  9720  divdiv1  9725  divdiv2  9726  recgt0ii  9916  expcl2lem  11393  m1expcl2  11403  expclzlem  11405  1exp  11409  s1nz  11759  s2f1o  11863  f1oun2prg  11864  iseraltlem2  12476  iseraltlem3  12477  iseralt  12478  geo2sum2  12651  geoihalfsum  12659  efne0  12698  tan0  12752  divalg  12923  gcd1  13032  rpdvds  13124  pcpre1  13216  pc1  13229  pcrec  13232  pcid  13246  prmreclem2  13285  mvrf1  16489  cndrng  16730  gzrngunitlem  16763  gzrngunit  16764  zrngunit  16765  dscmet  18620  xrhmeo  18971  i1f1lem  19581  itg11  19583  iblcnlem1  19679  itgcnlem  19681  ply1remlem  20085  dgrid  20182  dgrsub  20190  plyrem  20222  facth  20223  fta1lem  20224  vieta1lem1  20227  vieta1lem2  20228  vieta1  20229  qaa  20240  iaa  20242  coseq00topi  20410  logneg2  20510  logtayl2  20553  1cxp  20563  cxpeq0  20569  root1eq1  20639  root1cj  20640  cxpeq  20641  angneg  20645  ang180lem1  20651  ang180lem4  20654  ang180lem5  20655  isosctrlem2  20663  isosctrlem3  20664  angpined  20671  1cubrlem  20681  dcubic2  20684  dcubic  20686  mcubic  20687  cubic2  20688  dquartlem1  20691  asinlem  20708  atandmtan  20760  atantayl2  20778  efrlim  20808  basellem2  20864  isnsqf  20918  mumullem2  20963  sqff1o  20965  1sgm2ppw  20984  dchrn0  21034  dchrfi  21039  dchrptlem1  21048  dchrptlem2  21049  dchrpt  21051  lgsne0  21117  lgsqr  21130  lgseisenlem1  21133  lgseisenlem2  21134  lgseisenlem4  21136  lgseisen  21137  lgsquadlem1  21138  lgsquad2lem1  21142  lgsquad3  21145  m1lgs  21146  2sqlem7  21154  2sqlem8a  21155  2sqlem8  21156  chebbnd2  21171  chto1lb  21172  pnt2  21307  pnt  21308  qabvle  21319  qabvexp  21320  ostthlem2  21322  ostth3  21332  ostth  21333  usgraexmpldifpr  21419  usgraexmpl  21420  2trllemA  21550  2trllemH  21552  2trllemE  21553  2wlklemA  21554  2wlklemB  21555  2trllemD  21557  2trllemG  21558  wlkntrllem1  21559  wlkntrllem2  21560  wlkntrllem3  21561  constr1trl  21588  1pthon  21591  2wlklem1  21597  2pthon  21602  2pthon3v  21604  usgrcyclnl2  21628  constr3lem2  21633  constr3lem4  21634  constr3lem5  21635  constr3trllem1  21637  constr3trllem3  21639  constr3pthlem1  21642  4cycl4dv  21654  konigsberg  21709  ablomul  21943  mulid  21944  vcoprne  22058  hvsubcan  22576  hvsubcan2  22577  norm1exi  22752  kbpj  23459  largei  23770  superpos  23857  xrge0iif1  24324  logb1  24403  ind1a  24418  indf1o  24421  cntnevol  24582  ballotlemii  24761  m1expevenALT  24905  indispcon  24921  fprodntriv  25268  prod0  25269  prod1  25270  fprodn0  25303  axlowdimlem6  25886  axlowdimlem13  25893  axlowdimlem14  25894  axlowdim1  25898  0dioph  26837  pell1234qrne0  26916  bezoutr1  27051  mncn0  27321  aaitgo  27344  psgnunilem4  27397  m1expaddsub  27398  psgnuni  27399  cnmsgnsubg  27411  cnmsgngrp  27413  proot1ex  27497  expgrowth  27529  stoweidlem13  27738  wallispi2lem1  27796  f13idfv  28082  usgra2pthspth  28305  usgra2wlkspthlem1  28306  usgra2wlkspthlem2  28307  usgra2pthlem1  28310  sec0  28503
  Copyright terms: Public domain W3C validator