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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8983 . 2  class  1
2 cc0 8982 . 2  class  0
31, 2wne 2598 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  9074  1re  9082  mul02lem2  9235  addid1  9238  ine0  9461  0lt1  9542  recne0  9683  div1  9699  recdiv  9712  divdiv1  9717  divdiv2  9718  recgt0ii  9908  expcl2lem  11385  m1expcl2  11395  expclzlem  11397  1exp  11401  s1nz  11751  s2f1o  11855  f1oun2prg  11856  iseraltlem2  12468  iseraltlem3  12469  iseralt  12470  geo2sum2  12643  geoihalfsum  12651  efne0  12690  tan0  12744  divalg  12915  gcd1  13024  rpdvds  13116  pcpre1  13208  pc1  13221  pcrec  13224  pcid  13238  prmreclem2  13277  mvrf1  16481  cndrng  16722  gzrngunitlem  16755  gzrngunit  16756  zrngunit  16757  dscmet  18612  xrhmeo  18963  i1f1lem  19573  itg11  19575  iblcnlem1  19671  itgcnlem  19673  ply1remlem  20077  dgrid  20174  dgrsub  20182  plyrem  20214  facth  20215  fta1lem  20216  vieta1lem1  20219  vieta1lem2  20220  vieta1  20221  qaa  20232  iaa  20234  coseq00topi  20402  logneg2  20502  logtayl2  20545  1cxp  20555  cxpeq0  20561  root1eq1  20631  root1cj  20632  cxpeq  20633  angneg  20637  ang180lem1  20643  ang180lem4  20646  ang180lem5  20647  isosctrlem2  20655  isosctrlem3  20656  angpined  20663  1cubrlem  20673  dcubic2  20676  dcubic  20678  mcubic  20679  cubic2  20680  dquartlem1  20683  asinlem  20700  atandmtan  20752  atantayl2  20770  efrlim  20800  basellem2  20856  isnsqf  20910  mumullem2  20955  sqff1o  20957  1sgm2ppw  20976  dchrn0  21026  dchrfi  21031  dchrptlem1  21040  dchrptlem2  21041  dchrpt  21043  lgsne0  21109  lgsqr  21122  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem4  21128  lgseisen  21129  lgsquadlem1  21130  lgsquad2lem1  21134  lgsquad3  21137  m1lgs  21138  2sqlem7  21146  2sqlem8a  21147  2sqlem8  21148  chebbnd2  21163  chto1lb  21164  pnt2  21299  pnt  21300  qabvle  21311  qabvexp  21312  ostthlem2  21314  ostth3  21324  ostth  21325  usgraexmpldifpr  21411  usgraexmpl  21412  2trllemA  21542  2trllemH  21544  2trllemE  21545  2wlklemA  21546  2wlklemB  21547  2trllemD  21549  2trllemG  21550  wlkntrllem1  21551  wlkntrllem2  21552  wlkntrllem3  21553  constr1trl  21580  1pthon  21583  2wlklem1  21589  2pthon  21594  2pthon3v  21596  usgrcyclnl2  21620  constr3lem2  21625  constr3lem4  21626  constr3lem5  21627  constr3trllem1  21629  constr3trllem3  21631  constr3pthlem1  21634  4cycl4dv  21646  konigsberg  21701  ablomul  21935  mulid  21936  vcoprne  22050  hvsubcan  22568  hvsubcan2  22569  norm1exi  22744  kbpj  23451  largei  23762  superpos  23849  xrge0iif1  24316  logb1  24395  ind1a  24410  indf1o  24413  cntnevol  24574  ballotlemii  24753  m1expevenALT  24897  indispcon  24913  fprodntriv  25260  prod0  25261  prod1  25262  fprodn0  25295  axlowdimlem6  25878  axlowdimlem13  25885  axlowdimlem14  25886  axlowdim1  25890  0dioph  26818  pell1234qrne0  26897  bezoutr1  27032  mncn0  27302  aaitgo  27325  psgnunilem4  27378  m1expaddsub  27379  psgnuni  27380  cnmsgnsubg  27392  cnmsgngrp  27394  proot1ex  27478  expgrowth  27510  stoweidlem13  27719  wallispi2lem1  27777  f13idfv  28058  usgra2pthspth  28248  usgra2wlkspthlem1  28249  usgra2wlkspthlem2  28250  usgra2pthlem1  28253  sec0  28430
  Copyright terms: Public domain W3C validator