Axiom ax-1ne0 11221

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

This axiom is referenced by:  elimne0  11248  1re  11258  mul02lem2  11435  addrid  11438  ine0  11695  0lt1  11782  recne0  11932  div1  11954  recdiv  11970  divdiv1  11975  divdiv2  11976  recgt0ii  12171  nnne0  12297  0ne1  12334  neg1ne0  12379  fvf1tp  13825  expcl2lem  14110  expclzlem  14120  m1expcl2  14122  1exp  14128  hashrabsn1  14409  tpf1ofv1  14532  relexp1g  15061  geo2sum2  15906  geoihalfsum  15914  fprodntriv  15974  prod0  15975  prod1  15976  fprodn0  16011  fprodn0f  16023  efne0  16129  tan0  16183  m1exp1  16409  divalg  16436  gcd1  16561  rpdvds  16693  m1dvdsndvds  16831  pcpre1  16875  pc1  16888  pcrec  16891  pcid  16906  m1expaddsub  19530  cndrng  21428  cndrngOLD  21429  cnmgpid  21464  gzrngunitlem  21467  gzrngunit  21468  zringnzr  21488  zringunit  21494  cnmsgnsubg  21612  cnmsgngrp  21614  psgninv  21617  mvrf1  22023  pmatcollpw3fi1lem1  22807  dscmet  24600  xrhmeo  24990  clmopfne  25142  itg11  25739  ply1remlem  26218  dgrid  26318  plyrem  26361  facth  26362  fta1lem  26363  vieta1lem1  26366  vieta1lem2  26367  vieta1  26368  qaa  26379  iaa  26381  coseq00topi  26558  logneg2  26671  logtayl2  26718  1cxp  26728  cxpeq0  26734  logb1  26826  logbmpt  26845  ang180lem4  26869  ang180lem5  26870  isosctrlem2  26876  isosctrlem3  26877  angpined  26887  dcubic2  26901  dcubic  26903  dquartlem1  26908  atandmtan  26977  efrlim  27026  efrlimOLD  27027  mumullem2  27237  1sgm2ppw  27258  dchrn0  27308  lgsne0  27393  1lgs  27398  gausslemma2dlem0i  27422  lgseisenlem1  27433  lgseisenlem2  27434  lgsquadlem1  27438  lgsquad2lem2  27443  2lgs  27465  2sqlem7  27482  2sqlem8a  27483  2sqlem8  27484  chebbnd2  27535  chto1lb  27536  pnt2  27671  pnt  27672  qabvle  27683  qabvexp  27684  ostthlem2  27686  ostth3  27696  ostth  27697  axlowdimlem6  28976  axlowdimlem13  28983  axlowdimlem14  28984  axlowdim1  28988  usgrexmpldifpr  29289  pthdadjvtx  29762  upgr4cycl4dv4e  30213  konigsberglem1  30280  frgrreggt1  30421  norm1exi  31278  kbpj  31984  largei  32295  ccfldextdgrr  33696  constrfin  33750  2sqr3minply  33752  xrge0iif1  33898  ind1a  33999  cntnevol  34208  ballotlemii  34484  sgn0bi  34528  plymulx0  34540  signswch  34554  signstfvcl  34566  indispconn  35218  poimirlem23  37629  efne0d  42351  tan3rdpi  42364  remulinvcom  42438  sn-0lt1  42469  0dioph  42765  pell1234qrne0  42840  expgrowth  44330  binomcxplemradcnv  44347  xrralrecnnge  45339  iooiinioc  45508  stoweidlem13  45968  wallispi2lem1  46026  dirkertrigeq  46056  fourierdlem30  46092  fourierdlem62  46123  dfodd5  47584  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb1  47926  usgrexmpl2trifr  47931  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  itcoval1  48512  line2ylem  48600  sec0  48990