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 2930	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  21370  cnmgpid  21398  gzrngunitlem  21401  gzrngunit  21402  zringnzr  21429  zringunit  21435  cnmsgnsubg  21546  cnmsgngrp  21548  psgninv  21551  mvrf1  21953  psdmvr  22124  pmatcollpw3fi1lem1  22739  dscmet  24525  xrhmeo  24901  clmopfne  25051  itg11  25646  ply1remlem  26118  dgrid  26217  plyrem  26259  facth  26260  fta1lem  26261  vieta1lem1  26264  vieta1lem2  26265  vieta1  26266  qaa  26277  iaa  26279  coseq00topi  26454  logneg2  26567  logtayl2  26614  1cxp  26624  cxpeq0  26630  logb1  26721  logbmpt  26740  ang180lem4  26764  ang180lem5  26765  isosctrlem2  26771  isosctrlem3  26772  angpined  26782  dcubic2  26796  dcubic  26798  dquartlem1  26803  atandmtan  26872  efrlim  26921  mumullem2  27131  1sgm2ppw  27151  dchrn0  27201  lgsne0  27286  1lgs  27291  gausslemma2dlem0i  27315  lgseisenlem1  27326  lgseisenlem2  27327  lgsquadlem1  27331  lgsquad2lem2  27336  2lgs  27358  2sqlem7  27375  2sqlem8a  27376  2sqlem8  27377  chebbnd2  27428  chto1lb  27429  pnt2  27564  pnt  27565  qabvle  27576  qabvexp  27577  ostthlem2  27579  ostth3  27589  ostth  27590  axlowdimlem6  29004  axlowdimlem13  29011  axlowdimlem14  29012  axlowdim1  29016  usgrexmpldifpr  29315  pthdadjvtx  29784  upgr4cycl4dv4e  30243  konigsberglem1  30310  frgrreggt1  30451  norm1exi  31309  kbpj  32015  largei  32326  sgn0bi  32901  indsupp  32915  esplyfvaln  33706  ccfldextdgrr  33804  constrfin  33878  2sqr3minply  33912  cos9thpiminplylem1  33914  cos9thpiminplylem2  33915  cos9thpiminplylem3  33916  cos9thpinconstrlem1  33921  xrge0iif1  34070  cntnevol  34360  ballotlemii  34636  plymulx0  34679  signswch  34693  signstfvcl  34705  indispconn  35404  poimirlem23  37952  tan3rdpi  42772  remulinvcom  42853  sn-rediv1d  42872  rerecne0d  42876  sn-0lt1  42908  0dioph  43198  pell1234qrne0  43269  expgrowth  44750  binomcxplemradcnv  44767  xrralrecnnge  45807  iooiinioc  45974  stoweidlem13  46429  wallispi2lem1  46487  dirkertrigeq  46517  fourierdlem30  46553  fourierdlem62  46584  cjnpoly  47325  dfodd5  48124  usgrexmpl1lem  48485  usgrexmpl2lem  48490  usgrexmpl2nb1  48496  usgrexmpl2trifr  48501  gpgvtxedg0  48527  gpgvtxedg1  48528  gpgedgiov  48529  gpgedg2iv  48531  gpg5nbgrvtx03starlem1  48532  gpg5nbgrvtx03starlem3  48534  gpg5nbgrvtx13starlem1  48535  gpg5nbgrvtx13starlem2  48536  gpg5nbgrvtx13starlem3  48537  gpg3nbgrvtx0  48540  gpg3nbgrvtx0ALT  48541  gpg3nbgrvtx1  48542  gpgprismgr4cycllem2  48560  pgnbgreunbgrlem2lem1  48578  pgnbgreunbgrlem2lem2  48579  pgnbgreunbgrlem2lem3  48580  pgnbgreunbgrlem5lem1  48584  pgnbgreunbgrlem5lem2  48585  pgnbgreunbgrlem5lem3  48586  gpg5edgnedg  48594  itcoval1  49127  line2ylem  49215  sec0  50223