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

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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 9975 . 2 class 1
2 cc0 9974 . 2 class 0
31, 2wne 2823 1 wff 1 ≠ 0
Colors of variables: wff setvar class
This axiom is referenced by:  elimne0  10068  1re  10077  mul02lem2  10251  addid1  10254  ine0  10503  0lt1  10588  recne0  10736  div1  10754  recdiv  10769  divdiv1  10774  divdiv2  10775  recgt0ii  10967  0ne1  11126  neg1ne0  11164  expcl2lem  12912  m1expcl2  12922  expclzlem  12924  1exp  12929  hashrabsn1  13201  s1nzOLD  13424  relexp1g  13810  geo2sum2  14649  geoihalfsum  14658  fprodntriv  14716  prod0  14717  prod1  14718  fprodn0  14753  efne0  14871  tan0  14925  m1exp1  15140  divalg  15173  gcd1  15296  rpdvds  15421  m1dvdsndvds  15550  pcpre1  15594  pc1  15607  pcrec  15610  pcid  15624  m1expaddsub  17964  mvrf1  19473  cndrng  19823  cnmgpid  19856  gzrngunitlem  19859  gzrngunit  19860  zringnzr  19878  zringunit  19884  cnmsgnsubg  19971  cnmsgngrp  19973  psgninv  19976  pmatcollpw3fi1lem1  20639  dscmet  22424  xrhmeo  22792  clmopfne  22942  itg11  23503  ply1remlem  23967  dgrid  24065  plyrem  24105  facth  24106  fta1lem  24107  vieta1lem1  24110  vieta1lem2  24111  vieta1  24112  qaa  24123  iaa  24125  coseq00topi  24299  logneg2  24406  logtayl2  24453  1cxp  24463  cxpeq0  24469  logb1  24552  logbmpt  24571  ang180lem4  24587  ang180lem5  24588  isosctrlem2  24594  isosctrlem3  24595  angpined  24602  dcubic2  24616  dcubic  24618  dquartlem1  24623  atandmtan  24692  efrlim  24741  mumullem2  24951  1sgm2ppw  24970  dchrn0  25020  lgsne0  25105  1lgs  25110  gausslemma2dlem0i  25134  lgseisenlem1  25145  lgseisenlem2  25146  lgsquadlem1  25150  lgsquad2lem2  25155  2lgs  25177  2sqlem7  25194  2sqlem8a  25195  2sqlem8  25196  chebbnd2  25211  chto1lb  25212  pnt2  25347  pnt  25348  qabvle  25359  qabvexp  25360  ostthlem2  25362  ostth3  25372  ostth  25373  axlowdimlem6  25872  axlowdimlem13  25879  axlowdimlem14  25880  axlowdim1  25884  usgrexmpldifpr  26195  pthdadjvtx  26682  upgr4cycl4dv4e  27163  konigsberglem1  27230  frgrreggt1  27380  norm1exi  28235  kbpj  28943  largei  29254  xrge0iif1  30112  ind1a  30209  cntnevol  30419  ballotlemii  30693  sgn0bi  30737  plymulx0  30752  signswch  30766  signstfvcl  30778  indispconn  31342  poimirlem23  33562  0dioph  37659  pell1234qrne0  37734  expgrowth  38851  binomcxplemradcnv  38868  xrralrecnnge  39926  iooiinioc  40101  stoweidlem13  40548  wallispi2lem1  40606  dirkertrigeq  40636  fourierdlem30  40672  fourierdlem62  40703  dfodd5  41897  sec0  42829
  Copyright terms: Public domain W3C validator