Axiom ax-1ne0 11097

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

This axiom is referenced by:  elimne0  11124  1re  11134  mul02lem2  11311  addrid  11314  ine0  11573  0lt1  11660  recne0  11810  div1  11832  recdiv  11848  divdiv1  11853  divdiv2  11854  recgt0ii  12049  neg1ne0  12133  nnne0  12180  0ne1  12217  fvf1tp  13711  expcl2lem  13998  expclzlem  14008  m1expcl2  14010  1exp  14016  hashrabsn1  14299  tpf1ofv1  14422  relexp1g  14951  geo2sum2  15799  geoihalfsum  15807  fprodntriv  15867  prod0  15868  prod1  15869  fprodn0  15904  fprodn0f  15916  efne0d  16022  efne0OLD  16024  tan0  16078  m1exp1  16305  divalg  16332  gcd1  16457  rpdvds  16589  m1dvdsndvds  16728  pcpre1  16772  pc1  16785  pcrec  16788  pcid  16803  m1expaddsub  19395  cndrng  21323  cndrngOLD  21324  cnmgpid  21354  gzrngunitlem  21357  gzrngunit  21358  zringnzr  21385  zringunit  21391  cnmsgnsubg  21502  cnmsgngrp  21504  psgninv  21507  mvrf1  21911  psdmvr  22072  pmatcollpw3fi1lem1  22689  dscmet  24476  xrhmeo  24860  clmopfne  25012  itg11  25608  ply1remlem  26086  dgrid  26186  plyrem  26229  facth  26230  fta1lem  26231  vieta1lem1  26234  vieta1lem2  26235  vieta1  26236  qaa  26247  iaa  26249  coseq00topi  26427  logneg2  26540  logtayl2  26587  1cxp  26597  cxpeq0  26603  logb1  26695  logbmpt  26714  ang180lem4  26738  ang180lem5  26739  isosctrlem2  26745  isosctrlem3  26746  angpined  26756  dcubic2  26770  dcubic  26772  dquartlem1  26777  atandmtan  26846  efrlim  26895  efrlimOLD  26896  mumullem2  27106  1sgm2ppw  27127  dchrn0  27177  lgsne0  27262  1lgs  27267  gausslemma2dlem0i  27291  lgseisenlem1  27302  lgseisenlem2  27303  lgsquadlem1  27307  lgsquad2lem2  27312  2lgs  27334  2sqlem7  27351  2sqlem8a  27352  2sqlem8  27353  chebbnd2  27404  chto1lb  27405  pnt2  27540  pnt  27541  qabvle  27552  qabvexp  27553  ostthlem2  27555  ostth3  27565  ostth  27566  axlowdimlem6  28910  axlowdimlem13  28917  axlowdimlem14  28918  axlowdim1  28922  usgrexmpldifpr  29221  pthdadjvtx  29691  upgr4cycl4dv4e  30147  konigsberglem1  30214  frgrreggt1  30355  norm1exi  31212  kbpj  31918  largei  32229  sgn0bi  32798  ind1a  32815  indsupp  32823  ccfldextdgrr  33643  constrfin  33712  2sqr3minply  33746  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  cos9thpiminplylem3  33750  cos9thpinconstrlem1  33755  xrge0iif1  33904  cntnevol  34194  ballotlemii  34471  plymulx0  34514  signswch  34528  signstfvcl  34540  indispconn  35206  poimirlem23  37622  tan3rdpi  42325  remulinvcom  42406  sn-0lt1  42448  0dioph  42751  pell1234qrne0  42826  expgrowth  44308  binomcxplemradcnv  44325  xrralrecnnge  45370  iooiinioc  45538  stoweidlem13  45995  wallispi2lem1  46053  dirkertrigeq  46083  fourierdlem30  46119  fourierdlem62  46150  cjnpoly  46874  dfodd5  47645  usgrexmpl1lem  48006  usgrexmpl2lem  48011  usgrexmpl2nb1  48017  usgrexmpl2trifr  48022  gpgvtxedg0  48048  gpgvtxedg1  48049  gpgedgiov  48050  gpgedg2iv  48052  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpg3nbgrvtx0  48061  gpg3nbgrvtx0ALT  48062  gpg3nbgrvtx1  48063  gpgprismgr4cycllem2  48081  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem5lem1  48105  pgnbgreunbgrlem5lem2  48106  pgnbgreunbgrlem5lem3  48107  gpg5edgnedg  48115  itcoval1  48649  line2ylem  48737  sec0  49746