Axiom ax-1ne0 10763

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

This axiom is referenced by:  elimne0  10788  1re  10798  mul02lem2  10974  addid1  10977  ine0  11232  0lt1  11319  recne0  11468  div1  11486  recdiv  11503  divdiv1  11508  divdiv2  11509  recgt0ii  11703  nnne0  11829  0ne1  11866  neg1ne0  11911  expcl2lem  13612  m1expcl2  13622  expclzlem  13624  1exp  13629  hashrabsn1  13906  relexp1g  14554  geo2sum2  15401  geoihalfsum  15409  fprodntriv  15467  prod0  15468  prod1  15469  fprodn0  15504  fprodn0f  15516  efne0  15621  tan0  15675  m1exp1  15900  divalg  15927  gcd1  16050  rpdvds  16180  m1dvdsndvds  16314  pcpre1  16358  pc1  16371  pcrec  16374  pcid  16389  m1expaddsub  18844  cndrng  20346  cnmgpid  20379  gzrngunitlem  20382  gzrngunit  20383  zringnzr  20401  zringunit  20407  cnmsgnsubg  20493  cnmsgngrp  20495  psgninv  20498  mvrf1  20904  pmatcollpw3fi1lem1  21637  dscmet  23424  xrhmeo  23797  clmopfne  23947  itg11  24542  ply1remlem  25014  dgrid  25112  plyrem  25152  facth  25153  fta1lem  25154  vieta1lem1  25157  vieta1lem2  25158  vieta1  25159  qaa  25170  iaa  25172  coseq00topi  25346  logneg2  25457  logtayl2  25504  1cxp  25514  cxpeq0  25520  logb1  25606  logbmpt  25625  ang180lem4  25649  ang180lem5  25650  isosctrlem2  25656  isosctrlem3  25657  angpined  25667  dcubic2  25681  dcubic  25683  dquartlem1  25688  atandmtan  25757  efrlim  25806  mumullem2  26016  1sgm2ppw  26035  dchrn0  26085  lgsne0  26170  1lgs  26175  gausslemma2dlem0i  26199  lgseisenlem1  26210  lgseisenlem2  26211  lgsquadlem1  26215  lgsquad2lem2  26220  2lgs  26242  2sqlem7  26259  2sqlem8a  26260  2sqlem8  26261  chebbnd2  26312  chto1lb  26313  pnt2  26448  pnt  26449  qabvle  26460  qabvexp  26461  ostthlem2  26463  ostth3  26473  ostth  26474  axlowdimlem6  26992  axlowdimlem13  26999  axlowdimlem14  27000  axlowdim1  27004  usgrexmpldifpr  27300  pthdadjvtx  27771  upgr4cycl4dv4e  28222  konigsberglem1  28289  frgrreggt1  28430  norm1exi  29285  kbpj  29991  largei  30302  ccfldextdgrr  31410  xrge0iif1  31556  ind1a  31653  cntnevol  31862  ballotlemii  32136  sgn0bi  32180  plymulx0  32192  signswch  32206  signstfvcl  32218  indispconn  32863  poimirlem23  35486  remulinvcom  40063  sn-0lt1  40081  0dioph  40244  pell1234qrne0  40319  expgrowth  41567  binomcxplemradcnv  41584  xrralrecnnge  42544  iooiinioc  42710  stoweidlem13  43172  wallispi2lem1  43230  dirkertrigeq  43260  fourierdlem30  43296  fourierdlem62  43327  dfodd5  44728  itcoval1  45625  line2ylem  45713  sec0  46076