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 9861
Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 9837. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1ne0 1 ≠ 0

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 9793 . 2 class 1
2 cc0 9792 . 2 class 0
31, 2wne 2779 1 wff 1 ≠ 0
Colors of variables: wff setvar class
This axiom is referenced by:  elimne0  9886  1re  9895  mul02lem2  10064  addid1  10067  ine0  10316  0lt1  10401  recne0  10549  div1  10567  recdiv  10582  divdiv1  10587  divdiv2  10588  recgt0ii  10780  0ne1  10937  neg1ne0  10975  expcl2lem  12691  m1expcl2  12701  expclzlem  12703  1exp  12708  hashrabsn1  12978  s1nzOLD  13188  relexp1g  13562  geo2sum2  14392  geoihalfsum  14401  fprodntriv  14459  prod0  14460  prod1  14461  fprodn0  14496  efne0  14614  tan0  14668  m1exp1  14879  divalg  14912  gcd1  15035  rpdvds  15160  m1dvdsndvds  15289  pcpre1  15333  pc1  15346  pcrec  15349  pcid  15363  m1expaddsub  17689  mvrf1  19194  cndrng  19542  cnmgpid  19575  gzrngunitlem  19578  gzrngunit  19579  zringnzr  19597  zringunit  19605  cnmsgnsubg  19689  cnmsgngrp  19691  psgninv  19694  pmatcollpw3fi1lem1  20357  dscmet  22134  xrhmeo  22500  clmopfne  22651  itg11  23208  ply1remlem  23670  dgrid  23768  plyrem  23808  facth  23809  fta1lem  23810  vieta1lem1  23813  vieta1lem2  23814  vieta1  23815  qaa  23826  iaa  23828  coseq00topi  24002  logneg2  24109  logtayl2  24152  1cxp  24162  cxpeq0  24168  logb1  24251  logbmpt  24270  ang180lem4  24286  ang180lem5  24287  isosctrlem2  24293  isosctrlem3  24294  angpined  24301  dcubic2  24315  dcubic  24317  dquartlem1  24322  atandmtan  24391  efrlim  24440  mumullem2  24650  1sgm2ppw  24669  dchrn0  24719  lgsne0  24804  1lgs  24809  gausslemma2dlem0i  24833  lgseisenlem1  24844  lgseisenlem2  24845  lgsquadlem1  24849  lgsquad2lem2  24854  2lgs  24876  2sqlem7  24893  2sqlem8a  24894  2sqlem8  24895  chebbnd2  24910  chto1lb  24911  pnt2  25046  pnt  25047  qabvle  25058  qabvexp  25059  ostthlem2  25061  ostth3  25071  ostth  25072  axlowdimlem6  25572  axlowdimlem13  25579  axlowdimlem14  25580  axlowdim1  25584  usgraexmpldifpr  25721  2trllemA  25873  wlkntrllem3  25884  2pthon  25925  2pthon3v  25927  usgrcyclnl2  25962  4cycl4dv  25988  wwlkn0s  26026  konigsberg  26307  frgrareggt1  26436  norm1exi  27284  kbpj  27992  largei  28303  xrge0iif1  29105  ind1a  29203  cntnevol  29411  ballotlemii  29685  sgn0bi  29729  plymulx0  29743  signswch  29757  signstfvcl  29769  indispcon  30263  poimirlem23  32385  0dioph  36143  pell1234qrne0  36218  expgrowth  37339  binomcxplemradcnv  37356  xrralrecnnge  38337  iooiinioc  38413  stoweidlem13  38689  wallispi2lem1  38747  dirkertrigeq  38777  fourierdlem30  38813  fourierdlem62  38844  dfodd5  39894  pthdadjvtx  40917  upgr4cycl4dv4e  41333  konigsberglem1  41403  av-frgrareggt1  41528  sec0  42242
  Copyright terms: Public domain W3C validator