Axiom ax-1ne0 11103

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

This axiom is referenced by:  elimne0  11130  1re  11140  mul02lem2  11319  addrid  11322  ine0  11581  0lt1  11668  recne0  11817  div1  11839  recdiv  11856  divdiv1  11861  divdiv2  11862  recgt0ii  12057  neg1ne0  12141  ind1a  12165  nnne0  12206  0ne1  12247  fvf1tp  13743  expcl2lem  14030  expclzlem  14040  m1expcl2  14042  1exp  14048  hashrabsn1  14331  tpf1ofv1  14454  relexp1g  14983  geo2sum2  15834  geoihalfsum  15842  fprodntriv  15902  prod0  15903  prod1  15904  fprodn0  15939  fprodn0f  15951  efne0d  16057  efne0OLD  16059  tan0  16113  m1exp1  16340  divalg  16367  gcd1  16492  rpdvds  16624  m1dvdsndvds  16764  pcpre1  16808  pc1  16821  pcrec  16824  pcid  16839  ex-chn2  18599  m1expaddsub  19467  cndrng  21379  cnmgpid  21407  gzrngunitlem  21410  gzrngunit  21411  zringnzr  21438  zringunit  21444  cnmsgnsubg  21555  cnmsgngrp  21557  psgninv  21560  mvrf1  21963  psdmvr  22160  pmatcollpw3fi1lem1  22772  dscmet  24558  xrhmeo  24934  clmopfne  25084  itg11  25679  ply1remlem  26151  dgrid  26250  plyrem  26292  facth  26293  fta1lem  26294  vieta1lem1  26297  vieta1lem2  26298  vieta1  26299  qaa  26310  iaa  26312  coseq00topi  26487  logneg2  26600  logtayl2  26647  1cxp  26657  cxpeq0  26663  logb1  26754  logbmpt  26773  ang180lem4  26797  ang180lem5  26798  isosctrlem2  26804  isosctrlem3  26805  angpined  26815  dcubic2  26829  dcubic  26831  dquartlem1  26836  atandmtan  26905  efrlim  26954  mumullem2  27164  1sgm2ppw  27184  dchrn0  27234  lgsne0  27319  1lgs  27324  gausslemma2dlem0i  27348  lgseisenlem1  27359  lgseisenlem2  27360  lgsquadlem1  27364  lgsquad2lem2  27369  2lgs  27391  2sqlem7  27408  2sqlem8a  27409  2sqlem8  27410  chebbnd2  27461  chto1lb  27462  pnt2  27597  pnt  27598  qabvle  27609  qabvexp  27610  ostthlem2  27612  ostth3  27622  ostth  27623  axlowdimlem6  29036  axlowdimlem13  29043  axlowdimlem14  29044  axlowdim1  29048  usgrexmpldifpr  29347  pthdadjvtx  29816  upgr4cycl4dv4e  30275  konigsberglem1  30342  frgrreggt1  30483  norm1exi  31341  kbpj  32047  largei  32358  sgn0bi  32934  indsupp  32948  esplyfvaln  33768  ccfldextdgrr  33866  constrfin  33940  2sqr3minply  33974  cos9thpiminplylem1  33976  cos9thpiminplylem2  33977  cos9thpiminplylem3  33978  cos9thpinconstrlem1  33983  xrge0iif1  34132  cntnevol  34422  ballotlemii  34698  plymulx0  34741  signswch  34755  signstfvcl  34767  indispconn  35475  poimirlem23  38023  tan3rdpi  42842  remulinvcom  42923  sn-rediv1d  42942  rerecne0d  42946  sn-0lt1  42978  0dioph  43240  pell1234qrne0  43311  expgrowth  44792  binomcxplemradcnv  44809  xrralrecnnge  45846  iooiinioc  46013  stoweidlem13  46468  wallispi2lem1  46526  dirkertrigeq  46556  fourierdlem30  46592  fourierdlem62  46623  cjnpoly  47364  dfodd5  48163  usgrexmpl1lem  48524  usgrexmpl2lem  48529  usgrexmpl2nb1  48535  usgrexmpl2trifr  48540  gpgvtxedg0  48566  gpgvtxedg1  48567  gpgedgiov  48568  gpgedg2iv  48570  gpg5nbgrvtx03starlem1  48571  gpg5nbgrvtx03starlem3  48573  gpg5nbgrvtx13starlem1  48574  gpg5nbgrvtx13starlem2  48575  gpg5nbgrvtx13starlem3  48576  gpg3nbgrvtx0  48579  gpg3nbgrvtx0ALT  48580  gpg3nbgrvtx1  48581  gpgprismgr4cycllem2  48599  pgnbgreunbgrlem2lem1  48617  pgnbgreunbgrlem2lem2  48618  pgnbgreunbgrlem2lem3  48619  pgnbgreunbgrlem5lem1  48623  pgnbgreunbgrlem5lem2  48624  pgnbgreunbgrlem5lem3  48625  gpg5edgnedg  48633  itcoval1  49166  line2ylem  49254  sec0  50262