Axiom ax-1ne0 11096

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

This axiom is referenced by:  elimne0  11123  1re  11133  mul02lem2  11312  addrid  11315  ine0  11574  0lt1  11661  recne0  11811  div1  11833  recdiv  11850  divdiv1  11855  divdiv2  11856  recgt0ii  12051  neg1ne0  12135  ind1a  12159  nnne0  12200  0ne1  12241  fvf1tp  13737  expcl2lem  14024  expclzlem  14034  m1expcl2  14036  1exp  14042  hashrabsn1  14325  tpf1ofv1  14448  relexp1g  14977  geo2sum2  15828  geoihalfsum  15836  fprodntriv  15896  prod0  15897  prod1  15898  fprodn0  15933  fprodn0f  15945  efne0d  16051  efne0OLD  16053  tan0  16107  m1exp1  16334  divalg  16361  gcd1  16486  rpdvds  16618  m1dvdsndvds  16758  pcpre1  16802  pc1  16815  pcrec  16818  pcid  16833  ex-chn2  18593  m1expaddsub  19462  cndrng  21386  cndrngOLD  21387  cnmgpid  21417  gzrngunitlem  21420  gzrngunit  21421  zringnzr  21448  zringunit  21454  cnmsgnsubg  21565  cnmsgngrp  21567  psgninv  21570  mvrf1  21973  psdmvr  22144  pmatcollpw3fi1lem1  22760  dscmet  24546  xrhmeo  24922  clmopfne  25072  itg11  25667  ply1remlem  26142  dgrid  26241  plyrem  26284  facth  26285  fta1lem  26286  vieta1lem1  26289  vieta1lem2  26290  vieta1  26291  qaa  26302  iaa  26304  coseq00topi  26482  logneg2  26595  logtayl2  26642  1cxp  26652  cxpeq0  26658  logb1  26750  logbmpt  26769  ang180lem4  26793  ang180lem5  26794  isosctrlem2  26800  isosctrlem3  26801  angpined  26811  dcubic2  26825  dcubic  26827  dquartlem1  26832  atandmtan  26901  efrlim  26950  efrlimOLD  26951  mumullem2  27161  1sgm2ppw  27182  dchrn0  27232  lgsne0  27317  1lgs  27322  gausslemma2dlem0i  27346  lgseisenlem1  27357  lgseisenlem2  27358  lgsquadlem1  27362  lgsquad2lem2  27367  2lgs  27389  2sqlem7  27406  2sqlem8a  27407  2sqlem8  27408  chebbnd2  27459  chto1lb  27460  pnt2  27595  pnt  27596  qabvle  27607  qabvexp  27608  ostthlem2  27610  ostth3  27620  ostth  27621  axlowdimlem6  29035  axlowdimlem13  29042  axlowdimlem14  29043  axlowdim1  29047  usgrexmpldifpr  29346  pthdadjvtx  29816  upgr4cycl4dv4e  30275  konigsberglem1  30342  frgrreggt1  30483  norm1exi  31341  kbpj  32047  largei  32358  sgn0bi  32933  indsupp  32947  esplyfvaln  33738  ccfldextdgrr  33837  constrfin  33911  2sqr3minply  33945  cos9thpiminplylem1  33947  cos9thpiminplylem2  33948  cos9thpiminplylem3  33949  cos9thpinconstrlem1  33954  xrge0iif1  34103  cntnevol  34393  ballotlemii  34669  plymulx0  34712  signswch  34726  signstfvcl  34738  indispconn  35437  poimirlem23  37975  tan3rdpi  42795  remulinvcom  42876  sn-rediv1d  42895  rerecne0d  42899  sn-0lt1  42931  0dioph  43221  pell1234qrne0  43296  expgrowth  44777  binomcxplemradcnv  44794  xrralrecnnge  45834  iooiinioc  46001  stoweidlem13  46456  wallispi2lem1  46514  dirkertrigeq  46544  fourierdlem30  46580  fourierdlem62  46611  cjnpoly  47334  dfodd5  48133  usgrexmpl1lem  48494  usgrexmpl2lem  48499  usgrexmpl2nb1  48505  usgrexmpl2trifr  48510  gpgvtxedg0  48536  gpgvtxedg1  48537  gpgedgiov  48538  gpgedg2iv  48540  gpg5nbgrvtx03starlem1  48541  gpg5nbgrvtx03starlem3  48543  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem2  48545  gpg5nbgrvtx13starlem3  48546  gpg3nbgrvtx0  48549  gpg3nbgrvtx0ALT  48550  gpg3nbgrvtx1  48551  gpgprismgr4cycllem2  48569  pgnbgreunbgrlem2lem1  48587  pgnbgreunbgrlem2lem2  48588  pgnbgreunbgrlem2lem3  48589  pgnbgreunbgrlem5lem1  48593  pgnbgreunbgrlem5lem2  48594  pgnbgreunbgrlem5lem3  48595  gpg5edgnedg  48603  itcoval1  49136  line2ylem  49224  sec0  50232