Axiom ax-1ne0 10606

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 10582. (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 10538	. 2 class 1
2		cc0 10537	. 2 class 0
3	1, 2	wne 3016	1 wff 1 ≠ 0

This axiom is referenced by:  elimne0  10631  1re  10641  mul02lem2  10817  addid1  10820  ine0  11075  0lt1  11162  recne0  11311  div1  11329  recdiv  11346  divdiv1  11351  divdiv2  11352  recgt0ii  11546  nnne0  11672  0ne1  11709  neg1ne0  11754  expcl2lem  13442  m1expcl2  13452  expclzlem  13454  1exp  13459  hashrabsn1  13736  relexp1g  14385  geo2sum2  15230  geoihalfsum  15238  fprodntriv  15296  prod0  15297  prod1  15298  fprodn0  15333  fprodn0f  15345  efne0  15450  tan0  15504  m1exp1  15727  divalg  15754  gcd1  15876  rpdvds  16004  m1dvdsndvds  16135  pcpre1  16179  pc1  16192  pcrec  16195  pcid  16209  m1expaddsub  18626  mvrf1  20205  cndrng  20574  cnmgpid  20607  gzrngunitlem  20610  gzrngunit  20611  zringnzr  20629  zringunit  20635  cnmsgnsubg  20721  cnmsgngrp  20723  psgninv  20726  pmatcollpw3fi1lem1  21394  dscmet  23182  xrhmeo  23550  clmopfne  23700  itg11  24292  ply1remlem  24756  dgrid  24854  plyrem  24894  facth  24895  fta1lem  24896  vieta1lem1  24899  vieta1lem2  24900  vieta1  24901  qaa  24912  iaa  24914  coseq00topi  25088  logneg2  25198  logtayl2  25245  1cxp  25255  cxpeq0  25261  logb1  25347  logbmpt  25366  ang180lem4  25390  ang180lem5  25391  isosctrlem2  25397  isosctrlem3  25398  angpined  25408  dcubic2  25422  dcubic  25424  dquartlem1  25429  atandmtan  25498  efrlim  25547  mumullem2  25757  1sgm2ppw  25776  dchrn0  25826  lgsne0  25911  1lgs  25916  gausslemma2dlem0i  25940  lgseisenlem1  25951  lgseisenlem2  25952  lgsquadlem1  25956  lgsquad2lem2  25961  2lgs  25983  2sqlem7  26000  2sqlem8a  26001  2sqlem8  26002  chebbnd2  26053  chto1lb  26054  pnt2  26189  pnt  26190  qabvle  26201  qabvexp  26202  ostthlem2  26204  ostth3  26214  ostth  26215  axlowdimlem6  26733  axlowdimlem13  26740  axlowdimlem14  26741  axlowdim1  26745  usgrexmpldifpr  27040  pthdadjvtx  27511  upgr4cycl4dv4e  27964  konigsberglem1  28031  frgrreggt1  28172  norm1exi  29027  kbpj  29733  largei  30044  ccfldextdgrr  31057  xrge0iif1  31181  ind1a  31278  cntnevol  31487  ballotlemii  31761  sgn0bi  31805  plymulx0  31817  signswch  31831  signstfvcl  31843  indispconn  32481  poimirlem23  34930  sn-0lt1  39266  remulinvcom  39268  0dioph  39395  pell1234qrne0  39470  expgrowth  40687  binomcxplemradcnv  40704  xrralrecnnge  41682  iooiinioc  41852  stoweidlem13  42318  wallispi2lem1  42376  dirkertrigeq  42406  fourierdlem30  42442  fourierdlem62  42473  dfodd5  43845  line2ylem  44758  sec0  44879