Axiom ax-1ne0 10949

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 10925. (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 10881	. 2 class 1
2		cc0 10880	. 2 class 0
3	1, 2	wne 2944	1 wff 1 ≠ 0

This axiom is referenced by:  elimne0  10974  1re  10984  mul02lem2  11161  addid1  11164  ine0  11419  0lt1  11506  recne0  11655  div1  11673  recdiv  11690  divdiv1  11695  divdiv2  11696  recgt0ii  11890  nnne0  12016  0ne1  12053  neg1ne0  12098  expcl2lem  13803  m1expcl2  13813  expclzlem  13815  1exp  13821  hashrabsn1  14098  relexp1g  14746  geo2sum2  15595  geoihalfsum  15603  fprodntriv  15661  prod0  15662  prod1  15663  fprodn0  15698  fprodn0f  15710  efne0  15815  tan0  15869  m1exp1  16094  divalg  16121  gcd1  16244  rpdvds  16374  m1dvdsndvds  16508  pcpre1  16552  pc1  16565  pcrec  16568  pcid  16583  m1expaddsub  19115  cndrng  20636  cnmgpid  20669  gzrngunitlem  20672  gzrngunit  20673  zringnzr  20691  zringunit  20697  cnmsgnsubg  20791  cnmsgngrp  20793  psgninv  20796  mvrf1  21203  pmatcollpw3fi1lem1  21944  dscmet  23737  xrhmeo  24118  clmopfne  24268  itg11  24864  ply1remlem  25336  dgrid  25434  plyrem  25474  facth  25475  fta1lem  25476  vieta1lem1  25479  vieta1lem2  25480  vieta1  25481  qaa  25492  iaa  25494  coseq00topi  25668  logneg2  25779  logtayl2  25826  1cxp  25836  cxpeq0  25842  logb1  25928  logbmpt  25947  ang180lem4  25971  ang180lem5  25972  isosctrlem2  25978  isosctrlem3  25979  angpined  25989  dcubic2  26003  dcubic  26005  dquartlem1  26010  atandmtan  26079  efrlim  26128  mumullem2  26338  1sgm2ppw  26357  dchrn0  26407  lgsne0  26492  1lgs  26497  gausslemma2dlem0i  26521  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  lgsquad2lem2  26542  2lgs  26564  2sqlem7  26581  2sqlem8a  26582  2sqlem8  26583  chebbnd2  26634  chto1lb  26635  pnt2  26770  pnt  26771  qabvle  26782  qabvexp  26783  ostthlem2  26785  ostth3  26795  ostth  26796  axlowdimlem6  27324  axlowdimlem13  27331  axlowdimlem14  27332  axlowdim1  27336  usgrexmpldifpr  27634  pthdadjvtx  28107  upgr4cycl4dv4e  28558  konigsberglem1  28625  frgrreggt1  28766  norm1exi  29621  kbpj  30327  largei  30638  ccfldextdgrr  31751  xrge0iif1  31897  ind1a  31996  cntnevol  32205  ballotlemii  32479  sgn0bi  32523  plymulx0  32535  signswch  32549  signstfvcl  32561  indispconn  33205  poimirlem23  35809  remulinvcom  40421  sn-0lt1  40439  0dioph  40607  pell1234qrne0  40682  expgrowth  41960  binomcxplemradcnv  41977  xrralrecnnge  42937  iooiinioc  43101  stoweidlem13  43561  wallispi2lem1  43619  dirkertrigeq  43649  fourierdlem30  43685  fourierdlem62  43716  dfodd5  45123  itcoval1  46020  line2ylem  46108  sec0  46473