Axiom ax-1ne0 11144

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

This axiom is referenced by:  elimne0  11171  1re  11181  mul02lem2  11358  addrid  11361  ine0  11620  0lt1  11707  recne0  11857  div1  11879  recdiv  11895  divdiv1  11900  divdiv2  11901  recgt0ii  12096  neg1ne0  12180  nnne0  12227  0ne1  12264  fvf1tp  13758  expcl2lem  14045  expclzlem  14055  m1expcl2  14057  1exp  14063  hashrabsn1  14346  tpf1ofv1  14469  relexp1g  14999  geo2sum2  15847  geoihalfsum  15855  fprodntriv  15915  prod0  15916  prod1  15917  fprodn0  15952  fprodn0f  15964  efne0d  16070  efne0OLD  16072  tan0  16126  m1exp1  16353  divalg  16380  gcd1  16505  rpdvds  16637  m1dvdsndvds  16776  pcpre1  16820  pc1  16833  pcrec  16836  pcid  16851  m1expaddsub  19435  cndrng  21317  cndrngOLD  21318  cnmgpid  21353  gzrngunitlem  21356  gzrngunit  21357  zringnzr  21377  zringunit  21383  cnmsgnsubg  21493  cnmsgngrp  21495  psgninv  21498  mvrf1  21902  psdmvr  22063  pmatcollpw3fi1lem1  22680  dscmet  24467  xrhmeo  24851  clmopfne  25003  itg11  25599  ply1remlem  26077  dgrid  26177  plyrem  26220  facth  26221  fta1lem  26222  vieta1lem1  26225  vieta1lem2  26226  vieta1  26227  qaa  26238  iaa  26240  coseq00topi  26418  logneg2  26531  logtayl2  26578  1cxp  26588  cxpeq0  26594  logb1  26686  logbmpt  26705  ang180lem4  26729  ang180lem5  26730  isosctrlem2  26736  isosctrlem3  26737  angpined  26747  dcubic2  26761  dcubic  26763  dquartlem1  26768  atandmtan  26837  efrlim  26886  efrlimOLD  26887  mumullem2  27097  1sgm2ppw  27118  dchrn0  27168  lgsne0  27253  1lgs  27258  gausslemma2dlem0i  27282  lgseisenlem1  27293  lgseisenlem2  27294  lgsquadlem1  27298  lgsquad2lem2  27303  2lgs  27325  2sqlem7  27342  2sqlem8a  27343  2sqlem8  27344  chebbnd2  27395  chto1lb  27396  pnt2  27531  pnt  27532  qabvle  27543  qabvexp  27544  ostthlem2  27546  ostth3  27556  ostth  27557  axlowdimlem6  28881  axlowdimlem13  28888  axlowdimlem14  28889  axlowdim1  28893  usgrexmpldifpr  29192  pthdadjvtx  29665  upgr4cycl4dv4e  30121  konigsberglem1  30188  frgrreggt1  30329  norm1exi  31186  kbpj  31892  largei  32203  sgn0bi  32772  ind1a  32789  indsupp  32797  ccfldextdgrr  33674  constrfin  33743  2sqr3minply  33777  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpinconstrlem1  33786  xrge0iif1  33935  cntnevol  34225  ballotlemii  34502  plymulx0  34545  signswch  34559  signstfvcl  34571  indispconn  35228  poimirlem23  37644  tan3rdpi  42347  remulinvcom  42428  sn-0lt1  42470  0dioph  42773  pell1234qrne0  42848  expgrowth  44331  binomcxplemradcnv  44348  xrralrecnnge  45393  iooiinioc  45561  stoweidlem13  46018  wallispi2lem1  46076  dirkertrigeq  46106  fourierdlem30  46142  fourierdlem62  46173  dfodd5  47665  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb1  48027  usgrexmpl2trifr  48032  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpgedg2iv  48062  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  gpgprismgr4cycllem2  48090  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  itcoval1  48656  line2ylem  48744  sec0  49753