Axiom ax-1ne0 11293

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

This axiom is used by:  elimne0  11320  1re  11332  mul02lem2  11511  addrid  11514  ine0  11775  0lt1  11862  recne0  12011  div1  12030  recdiv  12047  divdiv1  12052  divdiv2  12053  recgt0ii  12247  neg1ne0  12331  ind1a  12355  nnne0  12396  0ne1  12438  fvf1tp  13953  expcl2lem  14240  expclzlem  14250  m1expcl2  14252  1exp  14258  hashrabsn1  14542  tpf1ofv1  14666  relexp1g  15205  sgn0bi  15282  geo2sum2  16069  geoihalfsum  16077  fprodntriv  16135  prod0  16136  prod1  16137  fprodn0  16172  fprodn0f  16184  efne0d  16289  efne0OLD  16291  tan0  16345  m1exp1  16572  divalg  16599  gcd1  16727  rpdvds  16861  m1dvdsndvds  17002  pcpre1  17046  pc1  17059  pcrec  17062  pcid  17077  ex-chn2  18838  m1expaddsub  19739  cndrng  21734  cnmgpid  21762  gzrngunitlem  21765  gzrngunit  21766  zringnzr  21793  zringunit  21799  cnmsgnsubg  21910  cnmsgngrp  21912  psgninv  21915  mvrf1  22320  psdmvr  22517  pmatcollpw3fi1lem1  23131  dscmet  24918  xrhmeo  25294  clmopfne  25444  itg11  26039  ply1remlem  26510  dgrid  26610  plyn0mulidp  26629  plyrem  26653  facth  26654  fta1lem  26655  vieta1lem1  26660  vieta1lem2  26661  vieta1  26662  qaa  26674  iaa  26678  iaaOLD  26679  coseq00topi  26858  logneg2  26970  logtayl2  27017  1cxp  27027  cxpeq0  27033  logb1  27124  logbmpt  27143  ang180lem4  27167  ang180lem5  27168  isosctrlem2  27174  isosctrlem3  27175  angpined  27185  dcubic2  27199  dcubic  27201  dquartlem1  27206  atandmtan  27275  efrlim  27324  mumullem2  27534  1sgm2ppw  27554  dchrn0  27604  lgsne0  27689  1lgs  27694  gausslemma2dlem0i  27718  lgseisenlem1  27729  lgseisenlem2  27730  lgsquadlem1  27734  lgsquad2lem2  27739  2lgs  27761  2sqlem7  27778  2sqlem8a  27779  2sqlem8  27780  chebbnd2  27831  chto1lb  27832  pnt2  27967  pnt  27968  qabvle  27979  qabvexp  27980  ostthlem2  27982  ostth3  27992  ostth  27993  axlowdimlem6  29552  axlowdimlem13  29559  axlowdimlem14  29560  axlowdim1  29564  usgrexmpldifpr  29866  pthdadjvtx  30340  upgr4cycl4dv4e  30813  konigsberglem1  30880  frgrreggt1  31021  norm1exi  31879  kbpj  32585  largei  32896  indsupp  33501  esplyfvaln  34273  ccfldextdgrr  34371  constrfin  34445  2sqr3minply  34479  cos9thpiminplylem1  34481  cos9thpiminplylem2  34482  cos9thpiminplylem3  34483  cos9thpinconstrlem1  34488  xrge0iif1  34637  cntnevol  34928  ballotlemii  35203  signswch  35257  signstfvcl  35269  indispconn  36165  poimirlem23  38752  25or6to4  43447  tan3rdpi  43594  remulinvcom  43675  sn-rediv1d  43694  rerecne0d  43698  sn-0lt1  43730  0dioph  43980  pell1234qrne0  44051  expgrowth  45509  binomcxplemradcnv  45526  xrralrecnnge  46604  iooiinioc  46771  stoweidlem13  47226  wallispi2lem1  47284  dirkertrigeq  47314  fourierdlem30  47350  fourierdlem62  47381  goldratval  48139  cjnpoly  48142  sqrtnpoly  48146  dfodd5  48961  usgrexmpl1lem  49322  usgrexmpl2lem  49327  usgrexmpl2nb1  49333  usgrexmpl2trifr  49338  gpgvtxedg0  49364  gpgvtxedg1  49365  gpgedgiov  49366  gpgedg2iv  49368  gpg5nbgrvtx03starlem1  49369  gpg5nbgrvtx03starlem3  49371  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem2  49373  gpg5nbgrvtx13starlem3  49374  gpg3nbgrvtx0  49377  gpg3nbgrvtx0ALT  49378  gpg3nbgrvtx1  49379  gpgprismgr4cycllem2  49397  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem2lem3  49417  pgnbgreunbgrlem5lem1  49421  pgnbgreunbgrlem5lem2  49422  pgnbgreunbgrlem5lem3  49423  gpg5edgnedg  49431  itcoval1  49978  line2ylem  50066  sec0  51131