Axiom ax-1ne0 9436

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

Assertion

Ref	Expression
ax-1ne0

Detailed syntax breakdown of Axiom ax-1ne0

Step	Hyp	Ref	Expression
1		c1 9368	. 2
2		cc0 9367	. 2
3	1, 2	wne 2641	1

This axiom is referenced by:  elimne0  9461  1re  9470  mul02lem2  9631  addid1  9634  ine0  9865  0lt1  9947  recne0  10092  div1  10108  recdiv  10122  divdiv1  10127  divdiv2  10128  recgt0ii  10323  0ne1  10474  neg1ne0  10512  expcl2lem  11962  m1expcl2  11972  expclzlem  11974  1exp  11978  s1nz  12383  geo2sum2  13420  geoihalfsum  13428  efne0  13467  tan0  13521  divalg  13693  gcd1  13802  rpdvds  13896  pcpre1  13995  pc1  14008  pcrec  14011  pcid  14025  m1expaddsub  16090  mvrf1  17589  cndrng  17938  gzrngunitlem  17970  gzrngunit  17971  zringunit  18007  zrngunit  18008  cnmsgnsubg  18100  cnmsgngrp  18102  psgninv  18105  dscmet  20265  xrhmeo  20618  itg11  21269  ply1remlem  21734  dgrid  21831  plyrem  21871  facth  21872  fta1lem  21873  vieta1lem1  21876  vieta1lem2  21877  vieta1  21878  qaa  21889  iaa  21891  coseq00topi  22064  logneg2  22164  logtayl2  22207  1cxp  22217  cxpeq0  22223  ang180lem4  22308  ang180lem5  22309  isosctrlem2  22317  isosctrlem3  22318  angpined  22325  dcubic2  22339  dcubic  22341  dquartlem1  22346  atandmtan  22415  efrlim  22463  mumullem2  22618  1sgm2ppw  22639  dchrn0  22689  lgsne0  22772  lgseisenlem1  22788  lgseisenlem2  22789  lgsquadlem1  22793  2sqlem7  22809  2sqlem8a  22810  2sqlem8  22811  chebbnd2  22826  chto1lb  22827  pnt2  22962  pnt  22963  qabvle  22974  qabvexp  22975  ostthlem2  22977  ostth3  22987  ostth  22988  axlowdimlem6  23312  axlowdimlem13  23319  axlowdimlem14  23320  axlowdim1  23324  usgraexmpldifpr  23437  2trllemA  23568  wlkntrllem3  23579  2pthon  23620  2pthon3v  23622  usgrcyclnl2  23646  4cycl4dv  23672  konigsberg  23727  ablomul  23961  mulid  23962  vcoprne  24076  norm1exi  24772  kbpj  25479  largei  25790  xrge0iif1  26486  logb1  26580  ind1a  26595  cntnevol  26760  eulerpartlemgf  26880  ballotlemii  27004  sgn0bi  27048  plymulx0  27066  signswch  27080  signstfvcl  27092  indispcon  27241  fprodntriv  27573  prod0  27574  prod1  27575  fprodn0  27608  0dioph  29239  pell1234qrne0  29316  expgrowth  29731  stoweidlem13  29930  wallispi2lem1  29988  hashrabsn1  30355  m1dvdsndvds  30369  wwlkn0s  30461  frgrareggt1  30831  pmatcollpw4fi1lem1  31297  sec0  31376