Axiom ax-1ne0 11104

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

This axiom is referenced by:  elimne0  11131  1re  11141  mul02lem2  11320  addrid  11323  ine0  11582  0lt1  11669  recne0  11819  div1  11841  recdiv  11858  divdiv1  11863  divdiv2  11864  recgt0ii  12059  neg1ne0  12143  ind1a  12167  nnne0  12208  0ne1  12249  fvf1tp  13745  expcl2lem  14032  expclzlem  14042  m1expcl2  14044  1exp  14050  hashrabsn1  14333  tpf1ofv1  14456  relexp1g  14985  geo2sum2  15836  geoihalfsum  15844  fprodntriv  15904  prod0  15905  prod1  15906  fprodn0  15941  fprodn0f  15953  efne0d  16059  efne0OLD  16061  tan0  16115  m1exp1  16342  divalg  16369  gcd1  16494  rpdvds  16626  m1dvdsndvds  16766  pcpre1  16810  pc1  16823  pcrec  16826  pcid  16841  ex-chn2  18601  m1expaddsub  19470  cndrng  21378  cnmgpid  21406  gzrngunitlem  21409  gzrngunit  21410  zringnzr  21437  zringunit  21443  cnmsgnsubg  21554  cnmsgngrp  21556  psgninv  21559  mvrf1  21961  psdmvr  22132  pmatcollpw3fi1lem1  22748  dscmet  24534  xrhmeo  24910  clmopfne  25060  itg11  25655  ply1remlem  26127  dgrid  26226  plyrem  26268  facth  26269  fta1lem  26270  vieta1lem1  26273  vieta1lem2  26274  vieta1  26275  qaa  26286  iaa  26288  coseq00topi  26463  logneg2  26576  logtayl2  26623  1cxp  26633  cxpeq0  26639  logb1  26730  logbmpt  26749  ang180lem4  26773  ang180lem5  26774  isosctrlem2  26780  isosctrlem3  26781  angpined  26791  dcubic2  26805  dcubic  26807  dquartlem1  26812  atandmtan  26881  efrlim  26930  mumullem2  27140  1sgm2ppw  27160  dchrn0  27210  lgsne0  27295  1lgs  27300  gausslemma2dlem0i  27324  lgseisenlem1  27335  lgseisenlem2  27336  lgsquadlem1  27340  lgsquad2lem2  27345  2lgs  27367  2sqlem7  27384  2sqlem8a  27385  2sqlem8  27386  chebbnd2  27437  chto1lb  27438  pnt2  27573  pnt  27574  qabvle  27585  qabvexp  27586  ostthlem2  27588  ostth3  27598  ostth  27599  axlowdimlem6  29013  axlowdimlem13  29020  axlowdimlem14  29021  axlowdim1  29025  usgrexmpldifpr  29324  pthdadjvtx  29793  upgr4cycl4dv4e  30252  konigsberglem1  30319  frgrreggt1  30460  norm1exi  31318  kbpj  32024  largei  32335  sgn0bi  32910  indsupp  32924  esplyfvaln  33715  ccfldextdgrr  33813  constrfin  33887  2sqr3minply  33921  cos9thpiminplylem1  33923  cos9thpiminplylem2  33924  cos9thpiminplylem3  33925  cos9thpinconstrlem1  33930  xrge0iif1  34079  cntnevol  34369  ballotlemii  34645  plymulx0  34688  signswch  34702  signstfvcl  34714  indispconn  35413  poimirlem23  37961  tan3rdpi  42781  remulinvcom  42862  sn-rediv1d  42881  rerecne0d  42885  sn-0lt1  42917  0dioph  43207  pell1234qrne0  43278  expgrowth  44759  binomcxplemradcnv  44776  xrralrecnnge  45816  iooiinioc  45983  stoweidlem13  46438  wallispi2lem1  46496  dirkertrigeq  46526  fourierdlem30  46562  fourierdlem62  46593  cjnpoly  47328  dfodd5  48127  usgrexmpl1lem  48488  usgrexmpl2lem  48493  usgrexmpl2nb1  48499  usgrexmpl2trifr  48504  gpgvtxedg0  48530  gpgvtxedg1  48531  gpgedgiov  48532  gpgedg2iv  48534  gpg5nbgrvtx03starlem1  48535  gpg5nbgrvtx03starlem3  48537  gpg5nbgrvtx13starlem1  48538  gpg5nbgrvtx13starlem2  48539  gpg5nbgrvtx13starlem3  48540  gpg3nbgrvtx0  48543  gpg3nbgrvtx0ALT  48544  gpg3nbgrvtx1  48545  gpgprismgr4cycllem2  48563  pgnbgreunbgrlem2lem1  48581  pgnbgreunbgrlem2lem2  48582  pgnbgreunbgrlem2lem3  48583  pgnbgreunbgrlem5lem1  48587  pgnbgreunbgrlem5lem2  48588  pgnbgreunbgrlem5lem3  48589  gpg5edgnedg  48597  itcoval1  49130  line2ylem  49218  sec0  50226