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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 8825 . 2  class  1
2 cc0 8824 . 2  class  0
31, 2wne 2521 1  wff  1  =/=  0
Colors of variables: wff set class
This axiom is referenced by:  elimne0  8916  1re  8924  mul02lem2  9076  addid1  9079  ine0  9302  0lt1  9383  recne0  9524  div1  9540  recdiv  9553  divdiv1  9558  divdiv2  9559  recgt0ii  9749  expcl2lem  11205  m1expcl2  11215  expclzlem  11217  1exp  11221  s1nz  11535  iseraltlem2  12246  iseraltlem3  12247  iseralt  12248  geo2sum2  12421  geoihalfsum  12429  efne0  12468  tan0  12522  divalg  12693  gcd1  12802  rpdvds  12894  pcpre1  12986  pc1  12999  pcrec  13002  pcid  13016  prmreclem2  13055  mvrf1  16263  cndrng  16503  gzrngunitlem  16536  gzrngunit  16537  zrngunit  16538  dscmet  18191  xrhmeo  18542  i1f1lem  19142  itg11  19144  iblcnlem1  19240  itgcnlem  19242  ply1remlem  19646  dgrid  19743  dgrsub  19751  plyrem  19783  facth  19784  fta1lem  19785  vieta1lem1  19788  vieta1lem2  19789  vieta1  19790  qaa  19801  iaa  19803  coseq00topi  19971  logneg2  20071  logtayl2  20114  1cxp  20124  cxpeq0  20130  root1eq1  20200  root1cj  20201  cxpeq  20202  angneg  20206  ang180lem1  20212  ang180lem4  20215  ang180lem5  20216  isosctrlem2  20224  isosctrlem3  20225  angpined  20232  1cubrlem  20242  dcubic2  20245  dcubic  20247  mcubic  20248  cubic2  20249  dquartlem1  20252  asinlem  20269  atandmtan  20321  atantayl2  20339  efrlim  20369  basellem2  20425  isnsqf  20479  mumullem2  20524  sqff1o  20526  1sgm2ppw  20545  dchrn0  20595  dchrfi  20600  dchrptlem1  20609  dchrptlem2  20610  dchrpt  20612  lgsne0  20678  lgsqr  20691  lgseisenlem1  20694  lgseisenlem2  20695  lgseisenlem4  20697  lgseisen  20698  lgsquadlem1  20699  lgsquad2lem1  20703  lgsquad3  20706  m1lgs  20707  2sqlem7  20715  2sqlem8a  20716  2sqlem8  20717  chebbnd2  20732  chto1lb  20733  pnt2  20868  pnt  20869  qabvle  20880  qabvexp  20881  ostthlem2  20883  ostth3  20893  ostth  20894  ablomul  21128  mulid  21129  vcoprne  21243  hvsubcan  21761  hvsubcan2  21762  norm1exi  21937  kbpj  22644  largei  22955  superpos  23042  xrge0iif1  23480  logb1  23669  ind1a  23684  indf1o  23687  cntnevol  23846  ballotlemii  24010  indispcon  24169  konigsberg  24315  fprodntriv  24569  prod0  24570  prod1  24571  fprodn0  24604  risefacn0  24647  axlowdimlem6  25134  axlowdimlem13  25141  axlowdimlem14  25142  axlowdim1  25146  0dioph  26181  pell1234qrne0  26261  bezoutr1  26396  mncn0  26667  aaitgo  26690  psgnunilem4  26743  m1expaddsub  26744  psgnuni  26745  cnmsgnsubg  26757  cnmsgngrp  26759  proot1ex  26843  expgrowth  26875  stoweidlem7  27079  stoweidlem13  27085  wallispi2lem1  27143  f1oun2prg  27421  s2f1o  27494  usgraexmpldifpr  27565  usgraexmpl  27566  wlkntrllem1  27684  wlkntrllem2  27685  wlkntrllem3  27686  wlkntrllem4  27687  wlkntrllem5  27688  constr1trl  27707  1pthon  27710  2trllem1  27713  2trllem4  27716  constr2trl  27717  2pthonlem2  27719  2pthon  27721  2pthon3v  27723  usgrcyclnl2  27748  constr3lem2  27753  constr3lem4  27754  constr3lem5  27755  constr3trllem1  27757  constr3trllem3  27759  constr3pthlem1  27762  4cycl4dv  27774  sec0  27913
  Copyright terms: Public domain W3C validator