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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 9816 . 2 class 1
2 cc0 9815 . 2 class 0
31, 2wne 2780 1 wff 1 ≠ 0
Colors of variables: wff setvar class
This axiom is referenced by:  elimne0  9909  1re  9918  mul02lem2  10092  addid1  10095  ine0  10344  0lt1  10429  recne0  10577  div1  10595  recdiv  10610  divdiv1  10615  divdiv2  10616  recgt0ii  10808  0ne1  10965  neg1ne0  11003  expcl2lem  12734  m1expcl2  12744  expclzlem  12746  1exp  12751  hashrabsn1  13024  s1nzOLD  13240  relexp1g  13614  geo2sum2  14444  geoihalfsum  14453  fprodntriv  14511  prod0  14512  prod1  14513  fprodn0  14548  efne0  14666  tan0  14720  m1exp1  14931  divalg  14964  gcd1  15087  rpdvds  15212  m1dvdsndvds  15341  pcpre1  15385  pc1  15398  pcrec  15401  pcid  15415  m1expaddsub  17741  mvrf1  19246  cndrng  19594  cnmgpid  19627  gzrngunitlem  19630  gzrngunit  19631  zringnzr  19649  zringunit  19655  cnmsgnsubg  19742  cnmsgngrp  19744  psgninv  19747  pmatcollpw3fi1lem1  20410  dscmet  22187  xrhmeo  22553  clmopfne  22704  itg11  23264  ply1remlem  23726  dgrid  23824  plyrem  23864  facth  23865  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  vieta1  23871  qaa  23882  iaa  23884  coseq00topi  24058  logneg2  24165  logtayl2  24208  1cxp  24218  cxpeq0  24224  logb1  24307  logbmpt  24326  ang180lem4  24342  ang180lem5  24343  isosctrlem2  24349  isosctrlem3  24350  angpined  24357  dcubic2  24371  dcubic  24373  dquartlem1  24378  atandmtan  24447  efrlim  24496  mumullem2  24706  1sgm2ppw  24725  dchrn0  24775  lgsne0  24860  1lgs  24865  gausslemma2dlem0i  24889  lgseisenlem1  24900  lgseisenlem2  24901  lgsquadlem1  24905  lgsquad2lem2  24910  2lgs  24932  2sqlem7  24949  2sqlem8a  24950  2sqlem8  24951  chebbnd2  24966  chto1lb  24967  pnt2  25102  pnt  25103  qabvle  25114  qabvexp  25115  ostthlem2  25117  ostth3  25127  ostth  25128  axlowdimlem6  25627  axlowdimlem13  25634  axlowdimlem14  25635  axlowdim1  25639  usgraexmpldifpr  25928  2trllemA  26080  wlkntrllem3  26091  2pthon  26132  2pthon3v  26134  usgrcyclnl2  26169  4cycl4dv  26195  wwlkn0s  26233  konigsberg  26514  frgrareggt1  26643  norm1exi  27491  kbpj  28199  largei  28510  xrge0iif1  29312  ind1a  29410  cntnevol  29618  ballotlemii  29892  sgn0bi  29936  plymulx0  29950  signswch  29964  signstfvcl  29976  indispcon  30470  poimirlem23  32602  0dioph  36360  pell1234qrne0  36435  expgrowth  37556  binomcxplemradcnv  37573  xrralrecnnge  38554  iooiinioc  38630  stoweidlem13  38906  wallispi2lem1  38964  dirkertrigeq  38994  fourierdlem30  39030  fourierdlem62  39061  dfodd5  40110  pthdadjvtx  40936  upgr4cycl4dv4e  41352  konigsberglem1  41422  av-frgrareggt1  41547  sec0  42300
  Copyright terms: Public domain W3C validator