Axiom ax-1ne0 11082

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

This axiom is referenced by:  elimne0  11109  1re  11119  mul02lem2  11297  addrid  11300  ine0  11559  0lt1  11646  recne0  11796  div1  11818  recdiv  11834  divdiv1  11839  divdiv2  11840  recgt0ii  12035  neg1ne0  12119  nnne0  12166  0ne1  12203  fvf1tp  13695  expcl2lem  13982  expclzlem  13992  m1expcl2  13994  1exp  14000  hashrabsn1  14283  tpf1ofv1  14406  relexp1g  14935  geo2sum2  15783  geoihalfsum  15791  fprodntriv  15851  prod0  15852  prod1  15853  fprodn0  15888  fprodn0f  15900  efne0d  16006  efne0OLD  16008  tan0  16062  m1exp1  16289  divalg  16316  gcd1  16441  rpdvds  16573  m1dvdsndvds  16712  pcpre1  16756  pc1  16769  pcrec  16772  pcid  16787  ex-chn2  18546  m1expaddsub  19412  cndrng  21337  cndrngOLD  21338  cnmgpid  21368  gzrngunitlem  21371  gzrngunit  21372  zringnzr  21399  zringunit  21405  cnmsgnsubg  21516  cnmsgngrp  21518  psgninv  21521  mvrf1  21924  psdmvr  22085  pmatcollpw3fi1lem1  22702  dscmet  24488  xrhmeo  24872  clmopfne  25024  itg11  25620  ply1remlem  26098  dgrid  26198  plyrem  26241  facth  26242  fta1lem  26243  vieta1lem1  26246  vieta1lem2  26247  vieta1  26248  qaa  26259  iaa  26261  coseq00topi  26439  logneg2  26552  logtayl2  26599  1cxp  26609  cxpeq0  26615  logb1  26707  logbmpt  26726  ang180lem4  26750  ang180lem5  26751  isosctrlem2  26757  isosctrlem3  26758  angpined  26768  dcubic2  26782  dcubic  26784  dquartlem1  26789  atandmtan  26858  efrlim  26907  efrlimOLD  26908  mumullem2  27118  1sgm2ppw  27139  dchrn0  27189  lgsne0  27274  1lgs  27279  gausslemma2dlem0i  27303  lgseisenlem1  27314  lgseisenlem2  27315  lgsquadlem1  27319  lgsquad2lem2  27324  2lgs  27346  2sqlem7  27363  2sqlem8a  27364  2sqlem8  27365  chebbnd2  27416  chto1lb  27417  pnt2  27552  pnt  27553  qabvle  27564  qabvexp  27565  ostthlem2  27567  ostth3  27577  ostth  27578  axlowdimlem6  28927  axlowdimlem13  28934  axlowdimlem14  28935  axlowdim1  28939  usgrexmpldifpr  29238  pthdadjvtx  29708  upgr4cycl4dv4e  30167  konigsberglem1  30234  frgrreggt1  30375  norm1exi  31232  kbpj  31938  largei  32249  sgn0bi  32828  ind1a  32845  indsupp  32855  ccfldextdgrr  33706  constrfin  33780  2sqr3minply  33814  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  cos9thpiminplylem3  33818  cos9thpinconstrlem1  33823  xrge0iif1  33972  cntnevol  34262  ballotlemii  34538  plymulx0  34581  signswch  34595  signstfvcl  34607  indispconn  35299  poimirlem23  37703  tan3rdpi  42470  remulinvcom  42551  sn-0lt1  42593  0dioph  42895  pell1234qrne0  42970  expgrowth  44452  binomcxplemradcnv  44469  xrralrecnnge  45512  iooiinioc  45680  stoweidlem13  46135  wallispi2lem1  46193  dirkertrigeq  46223  fourierdlem30  46259  fourierdlem62  46290  cjnpoly  47013  dfodd5  47784  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2nb1  48156  usgrexmpl2trifr  48161  gpgvtxedg0  48187  gpgvtxedg1  48188  gpgedgiov  48189  gpgedg2iv  48191  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpg3nbgrvtx0  48200  gpg3nbgrvtx0ALT  48201  gpg3nbgrvtx1  48202  gpgprismgr4cycllem2  48220  pgnbgreunbgrlem2lem1  48238  pgnbgreunbgrlem2lem2  48239  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem5lem1  48244  pgnbgreunbgrlem5lem2  48245  pgnbgreunbgrlem5lem3  48246  gpg5edgnedg  48254  itcoval1  48788  line2ylem  48876  sec0  49885