Axiom ax-1ne0 11208

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11184. (Contributed by NM, 29-Jan-1995.)

Assertion

Ref	Expression
ax-1ne0	⊢ 1 ≠ 0

Detailed syntax breakdown of Axiom ax-1ne0

Step	Hyp	Ref	Expression
1		c1 11140	. 2 class 1
2		cc0 11139	. 2 class 0
3	1, 2	wne 2937	1 wff 1 ≠ 0

This axiom is referenced by:  elimne0  11235  1re  11245  mul02lem2  11422  addrid  11425  ine0  11680  0lt1  11767  recne0  11916  div1  11934  recdiv  11951  divdiv1  11956  divdiv2  11957  recgt0ii  12151  nnne0  12277  0ne1  12314  neg1ne0  12359  expcl2lem  14071  expclzlem  14081  m1expcl2  14083  1exp  14089  hashrabsn1  14366  relexp1g  15006  geo2sum2  15853  geoihalfsum  15861  fprodntriv  15919  prod0  15920  prod1  15921  fprodn0  15956  fprodn0f  15968  efne0  16074  tan0  16128  m1exp1  16353  divalg  16380  gcd1  16503  rpdvds  16631  m1dvdsndvds  16767  pcpre1  16811  pc1  16824  pcrec  16827  pcid  16842  m1expaddsub  19453  cndrng  21326  cndrngOLD  21327  cnmgpid  21362  gzrngunitlem  21365  gzrngunit  21366  zringnzr  21386  zringunit  21392  cnmsgnsubg  21509  cnmsgngrp  21511  psgninv  21514  mvrf1  21928  pmatcollpw3fi1lem1  22701  dscmet  24494  xrhmeo  24884  clmopfne  25036  itg11  25633  ply1remlem  26112  dgrid  26212  plyrem  26253  facth  26254  fta1lem  26255  vieta1lem1  26258  vieta1lem2  26259  vieta1  26260  qaa  26271  iaa  26273  coseq00topi  26450  logneg2  26562  logtayl2  26609  1cxp  26619  cxpeq0  26625  logb1  26714  logbmpt  26733  ang180lem4  26757  ang180lem5  26758  isosctrlem2  26764  isosctrlem3  26765  angpined  26775  dcubic2  26789  dcubic  26791  dquartlem1  26796  atandmtan  26865  efrlim  26914  efrlimOLD  26915  mumullem2  27125  1sgm2ppw  27146  dchrn0  27196  lgsne0  27281  1lgs  27286  gausslemma2dlem0i  27310  lgseisenlem1  27321  lgseisenlem2  27322  lgsquadlem1  27326  lgsquad2lem2  27331  2lgs  27353  2sqlem7  27370  2sqlem8a  27371  2sqlem8  27372  chebbnd2  27423  chto1lb  27424  pnt2  27559  pnt  27560  qabvle  27571  qabvexp  27572  ostthlem2  27574  ostth3  27584  ostth  27585  axlowdimlem6  28771  axlowdimlem13  28778  axlowdimlem14  28779  axlowdim1  28783  usgrexmpldifpr  29084  pthdadjvtx  29557  upgr4cycl4dv4e  30008  konigsberglem1  30075  frgrreggt1  30216  norm1exi  31073  kbpj  31779  largei  32090  ccfldextdgrr  33360  xrge0iif1  33539  ind1a  33638  cntnevol  33847  ballotlemii  34123  sgn0bi  34167  plymulx0  34179  signswch  34193  signstfvcl  34205  indispconn  34844  poimirlem23  37116  efne0d  41908  remulinvcom  41987  sn-0lt1  42017  0dioph  42198  pell1234qrne0  42273  expgrowth  43772  binomcxplemradcnv  43789  xrralrecnnge  44772  iooiinioc  44941  stoweidlem13  45401  wallispi2lem1  45459  dirkertrigeq  45489  fourierdlem30  45525  fourierdlem62  45556  dfodd5  47000  itcoval1  47736  line2ylem  47824  sec0  48191