Axiom ax-1ne0 9297

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

Assertion

Ref	Expression
ax-1ne0

Detailed syntax breakdown of Axiom ax-1ne0

Step	Hyp	Ref	Expression
1		c1 9229	. 2
2		cc0 9228	. 2
3	1, 2	wne 2585	1

This axiom is referenced by:  elimne0  9322  1re  9331  mul02lem2  9492  addid1  9495  ine0  9726  0lt1  9808  recne0  9953  div1  9969  recdiv  9983  divdiv1  9988  divdiv2  9989  recgt0ii  10184  0ne1  10335  neg1ne0  10373  expcl2lem  11818  m1expcl2  11828  expclzlem  11830  1exp  11834  s1nz  12238  geo2sum2  13274  geoihalfsum  13282  efne0  13321  tan0  13375  divalg  13547  gcd1  13656  rpdvds  13750  pcpre1  13849  pc1  13862  pcrec  13865  pcid  13879  m1expaddsub  15941  mvrf1  17309  cndrng  17555  gzrngunitlem  17587  gzrngunit  17588  zringunit  17622  zrngunit  17623  cnmsgnsubg  17715  cnmsgngrp  17717  psgninv  17720  dscmet  19865  xrhmeo  20218  itg11  20869  ply1remlem  21375  dgrid  21472  plyrem  21512  facth  21513  fta1lem  21514  vieta1lem1  21517  vieta1lem2  21518  vieta1  21519  qaa  21530  iaa  21532  coseq00topi  21705  logneg2  21805  logtayl2  21848  1cxp  21858  cxpeq0  21864  ang180lem4  21949  ang180lem5  21950  isosctrlem2  21958  isosctrlem3  21959  angpined  21966  dcubic2  21980  dcubic  21982  dquartlem1  21987  atandmtan  22056  efrlim  22104  mumullem2  22259  1sgm2ppw  22280  dchrn0  22330  lgsne0  22413  lgseisenlem1  22429  lgseisenlem2  22430  lgsquadlem1  22434  2sqlem7  22450  2sqlem8a  22451  2sqlem8  22452  chebbnd2  22467  chto1lb  22468  pnt2  22603  pnt  22604  qabvle  22615  qabvexp  22616  ostthlem2  22618  ostth3  22628  ostth  22629  axlowdimlem6  22872  axlowdimlem13  22879  axlowdimlem14  22880  axlowdim1  22884  usgraexmpldifpr  22997  2trllemA  23128  wlkntrllem3  23139  2pthon  23180  2pthon3v  23182  usgrcyclnl2  23206  4cycl4dv  23232  konigsberg  23287  ablomul  23521  mulid  23522  vcoprne  23636  norm1exi  24332  kbpj  25039  largei  25350  xrge0iif1  26077  logb1  26171  ind1a  26186  cntnevol  26351  ballotlemii  26589  sgn0bi  26633  plymulx0  26651  signswch  26665  signstfvcl  26677  indispcon  26826  fprodntriv  27157  prod0  27158  prod1  27159  fprodn0  27192  0dioph  28790  pell1234qrne0  28867  expgrowth  29282  stoweidlem13  29482  wallispi2lem1  29540  hashrabsn1  29907  m1dvdsndvds  29921  wwlkn0s  30013  frgrareggt1  30383  sec0  30679