Axiom ax-1ne0 11099

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

This axiom is referenced by:  elimne0  11126  1re  11136  mul02lem2  11314  addrid  11317  ine0  11576  0lt1  11663  recne0  11813  div1  11835  recdiv  11851  divdiv1  11856  divdiv2  11857  recgt0ii  12052  neg1ne0  12136  nnne0  12183  0ne1  12220  fvf1tp  13713  expcl2lem  14000  expclzlem  14010  m1expcl2  14012  1exp  14018  hashrabsn1  14301  tpf1ofv1  14424  relexp1g  14953  geo2sum2  15801  geoihalfsum  15809  fprodntriv  15869  prod0  15870  prod1  15871  fprodn0  15906  fprodn0f  15918  efne0d  16024  efne0OLD  16026  tan0  16080  m1exp1  16307  divalg  16334  gcd1  16459  rpdvds  16591  m1dvdsndvds  16730  pcpre1  16774  pc1  16787  pcrec  16790  pcid  16805  ex-chn2  18565  m1expaddsub  19431  cndrng  21357  cndrngOLD  21358  cnmgpid  21388  gzrngunitlem  21391  gzrngunit  21392  zringnzr  21419  zringunit  21425  cnmsgnsubg  21536  cnmsgngrp  21538  psgninv  21541  mvrf1  21945  psdmvr  22116  pmatcollpw3fi1lem1  22734  dscmet  24520  xrhmeo  24904  clmopfne  25056  itg11  25652  ply1remlem  26130  dgrid  26230  plyrem  26273  facth  26274  fta1lem  26275  vieta1lem1  26278  vieta1lem2  26279  vieta1  26280  qaa  26291  iaa  26293  coseq00topi  26471  logneg2  26584  logtayl2  26631  1cxp  26641  cxpeq0  26647  logb1  26739  logbmpt  26758  ang180lem4  26782  ang180lem5  26783  isosctrlem2  26789  isosctrlem3  26790  angpined  26800  dcubic2  26814  dcubic  26816  dquartlem1  26821  atandmtan  26890  efrlim  26939  efrlimOLD  26940  mumullem2  27150  1sgm2ppw  27171  dchrn0  27221  lgsne0  27306  1lgs  27311  gausslemma2dlem0i  27335  lgseisenlem1  27346  lgseisenlem2  27347  lgsquadlem1  27351  lgsquad2lem2  27356  2lgs  27378  2sqlem7  27395  2sqlem8a  27396  2sqlem8  27397  chebbnd2  27448  chto1lb  27449  pnt2  27584  pnt  27585  qabvle  27596  qabvexp  27597  ostthlem2  27599  ostth3  27609  ostth  27610  axlowdimlem6  29024  axlowdimlem13  29031  axlowdimlem14  29032  axlowdim1  29036  usgrexmpldifpr  29335  pthdadjvtx  29805  upgr4cycl4dv4e  30264  konigsberglem1  30331  frgrreggt1  30472  norm1exi  31329  kbpj  32035  largei  32346  sgn0bi  32923  ind1a  32940  indsupp  32951  ccfldextdgrr  33831  constrfin  33905  2sqr3minply  33939  cos9thpiminplylem1  33941  cos9thpiminplylem2  33942  cos9thpiminplylem3  33943  cos9thpinconstrlem1  33948  xrge0iif1  34097  cntnevol  34387  ballotlemii  34663  plymulx0  34706  signswch  34720  signstfvcl  34732  indispconn  35430  poimirlem23  37846  tan3rdpi  42674  remulinvcom  42755  sn-0lt1  42797  0dioph  43087  pell1234qrne0  43162  expgrowth  44643  binomcxplemradcnv  44660  xrralrecnnge  45701  iooiinioc  45869  stoweidlem13  46324  wallispi2lem1  46382  dirkertrigeq  46412  fourierdlem30  46448  fourierdlem62  46479  cjnpoly  47202  dfodd5  47973  usgrexmpl1lem  48334  usgrexmpl2lem  48339  usgrexmpl2nb1  48345  usgrexmpl2trifr  48350  gpgvtxedg0  48376  gpgvtxedg1  48377  gpgedgiov  48378  gpgedg2iv  48380  gpg5nbgrvtx03starlem1  48381  gpg5nbgrvtx03starlem3  48383  gpg5nbgrvtx13starlem1  48384  gpg5nbgrvtx13starlem2  48385  gpg5nbgrvtx13starlem3  48386  gpg3nbgrvtx0  48389  gpg3nbgrvtx0ALT  48390  gpg3nbgrvtx1  48391  gpgprismgr4cycllem2  48409  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem2lem3  48429  pgnbgreunbgrlem5lem1  48433  pgnbgreunbgrlem5lem2  48434  pgnbgreunbgrlem5lem3  48435  gpg5edgnedg  48443  itcoval1  48976  line2ylem  49064  sec0  50072