Axiom ax-1ne0 9582

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

Assertion

Ref	Expression
ax-1ne0

Detailed syntax breakdown of Axiom ax-1ne0

Step	Hyp	Ref	Expression
1		c1 9514	. 2
2		cc0 9513	. 2
3	1, 2	wne 2652	1

This axiom is referenced by:  elimne0  9607  1re  9616  mul02lem2  9778  addid1  9781  ine0  10017  0lt1  10100  recne0  10245  div1  10261  recdiv  10275  divdiv1  10280  divdiv2  10281  recgt0ii  10476  0ne1  10628  neg1ne0  10666  expcl2lem  12178  m1expcl2  12188  expclzlem  12190  1exp  12195  hashrabsn1  12442  s1nz  12618  geo2sum2  13683  geoihalfsum  13691  fprodntriv  13749  prod0  13750  prod1  13751  fprodn0  13783  efne0  13832  tan0  13886  divalg  14061  gcd1  14170  rpdvds  14265  m1dvdsndvds  14325  pcpre1  14366  pc1  14379  pcrec  14382  pcid  14396  m1expaddsub  16523  mvrf1  18081  cndrng  18447  gzrngunitlem  18482  gzrngunit  18483  zringnzr  18500  zringunit  18520  zrngunit  18521  cnmsgnsubg  18613  cnmsgngrp  18615  psgninv  18618  pmatcollpw3fi1lem1  19287  dscmet  21093  xrhmeo  21446  itg11  22098  ply1remlem  22563  dgrid  22661  plyrem  22701  facth  22702  fta1lem  22703  vieta1lem1  22706  vieta1lem2  22707  vieta1  22708  qaa  22719  iaa  22721  coseq00topi  22895  logneg2  23000  logtayl2  23043  1cxp  23053  cxpeq0  23059  ang180lem4  23144  ang180lem5  23145  isosctrlem2  23153  isosctrlem3  23154  angpined  23161  dcubic2  23175  dcubic  23177  dquartlem1  23182  atandmtan  23251  efrlim  23299  mumullem2  23454  1sgm2ppw  23475  dchrn0  23525  lgsne0  23608  lgseisenlem1  23624  lgseisenlem2  23625  lgsquadlem1  23629  2sqlem7  23645  2sqlem8a  23646  2sqlem8  23647  chebbnd2  23662  chto1lb  23663  pnt2  23798  pnt  23799  qabvle  23810  qabvexp  23811  ostthlem2  23813  ostth3  23823  ostth  23824  axlowdimlem6  24250  axlowdimlem13  24257  axlowdimlem14  24258  axlowdim1  24262  usgraexmpldifpr  24400  2trllemA  24552  wlkntrllem3  24563  2pthon  24604  2pthon3v  24606  usgrcyclnl2  24641  4cycl4dv  24667  wwlkn0s  24705  konigsberg  24987  frgrareggt1  25116  ablomul  25357  mulid  25358  vcoprne  25472  norm1exi  26168  kbpj  26875  largei  27186  xrge0iif1  27920  logb1  28019  ind1a  28034  cntnevol  28199  ballotlemii  28442  sgn0bi  28486  plymulx0  28504  signswch  28518  signstfvcl  28530  indispcon  28679  0dioph  30712  pell1234qrne0  30789  expgrowth  31240  binomcxplemradcnv  31257  stoweidlem13  31795  wallispi2lem1  31853  dirkertrigeq  31883  fourierdlem30  31919  fourierdlem62  31951  sec0  33154