Axiom ax-1ne0 11109

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

This axiom is referenced by:  elimne0  11136  1re  11146  mul02lem2  11324  addrid  11327  ine0  11586  0lt1  11673  recne0  11823  div1  11845  recdiv  11861  divdiv1  11866  divdiv2  11867  recgt0ii  12062  neg1ne0  12146  nnne0  12193  0ne1  12230  fvf1tp  13723  expcl2lem  14010  expclzlem  14020  m1expcl2  14022  1exp  14028  hashrabsn1  14311  tpf1ofv1  14434  relexp1g  14963  geo2sum2  15811  geoihalfsum  15819  fprodntriv  15879  prod0  15880  prod1  15881  fprodn0  15916  fprodn0f  15928  efne0d  16034  efne0OLD  16036  tan0  16090  m1exp1  16317  divalg  16344  gcd1  16469  rpdvds  16601  m1dvdsndvds  16740  pcpre1  16784  pc1  16797  pcrec  16800  pcid  16815  ex-chn2  18575  m1expaddsub  19444  cndrng  21370  cndrngOLD  21371  cnmgpid  21401  gzrngunitlem  21404  gzrngunit  21405  zringnzr  21432  zringunit  21438  cnmsgnsubg  21549  cnmsgngrp  21551  psgninv  21554  mvrf1  21958  psdmvr  22129  pmatcollpw3fi1lem1  22747  dscmet  24533  xrhmeo  24917  clmopfne  25069  itg11  25665  ply1remlem  26143  dgrid  26243  plyrem  26286  facth  26287  fta1lem  26288  vieta1lem1  26291  vieta1lem2  26292  vieta1  26293  qaa  26304  iaa  26306  coseq00topi  26484  logneg2  26597  logtayl2  26644  1cxp  26654  cxpeq0  26660  logb1  26752  logbmpt  26771  ang180lem4  26795  ang180lem5  26796  isosctrlem2  26802  isosctrlem3  26803  angpined  26813  dcubic2  26827  dcubic  26829  dquartlem1  26834  atandmtan  26903  efrlim  26952  efrlimOLD  26953  mumullem2  27163  1sgm2ppw  27184  dchrn0  27234  lgsne0  27319  1lgs  27324  gausslemma2dlem0i  27348  lgseisenlem1  27359  lgseisenlem2  27360  lgsquadlem1  27364  lgsquad2lem2  27369  2lgs  27391  2sqlem7  27408  2sqlem8a  27409  2sqlem8  27410  chebbnd2  27461  chto1lb  27462  pnt2  27597  pnt  27598  qabvle  27609  qabvexp  27610  ostthlem2  27612  ostth3  27622  ostth  27623  axlowdimlem6  29038  axlowdimlem13  29045  axlowdimlem14  29046  axlowdim1  29050  usgrexmpldifpr  29349  pthdadjvtx  29819  upgr4cycl4dv4e  30278  konigsberglem1  30345  frgrreggt1  30486  norm1exi  31344  kbpj  32050  largei  32361  sgn0bi  32938  ind1a  32955  indsupp  32966  esplyfvaln  33757  ccfldextdgrr  33856  constrfin  33930  2sqr3minply  33964  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpinconstrlem1  33973  xrge0iif1  34122  cntnevol  34412  ballotlemii  34688  plymulx0  34731  signswch  34745  signstfvcl  34757  indispconn  35456  poimirlem23  37923  tan3rdpi  42751  remulinvcom  42832  sn-0lt1  42874  0dioph  43164  pell1234qrne0  43239  expgrowth  44720  binomcxplemradcnv  44737  xrralrecnnge  45777  iooiinioc  45945  stoweidlem13  46400  wallispi2lem1  46458  dirkertrigeq  46488  fourierdlem30  46524  fourierdlem62  46555  cjnpoly  47278  dfodd5  48049  usgrexmpl1lem  48410  usgrexmpl2lem  48415  usgrexmpl2nb1  48421  usgrexmpl2trifr  48426  gpgvtxedg0  48452  gpgvtxedg1  48453  gpgedgiov  48454  gpgedg2iv  48456  gpg5nbgrvtx03starlem1  48457  gpg5nbgrvtx03starlem3  48459  gpg5nbgrvtx13starlem1  48460  gpg5nbgrvtx13starlem2  48461  gpg5nbgrvtx13starlem3  48462  gpg3nbgrvtx0  48465  gpg3nbgrvtx0ALT  48466  gpg3nbgrvtx1  48467  gpgprismgr4cycllem2  48485  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  pgnbgreunbgrlem2lem3  48505  pgnbgreunbgrlem5lem1  48509  pgnbgreunbgrlem5lem2  48510  pgnbgreunbgrlem5lem3  48511  gpg5edgnedg  48519  itcoval1  49052  line2ylem  49140  sec0  50148