Axiom ax-1ne0 10400

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 10376. (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 10332	. 2 class 1
2		cc0 10331	. 2 class 0
3	1, 2	wne 2964	1 wff 1 ≠ 0

This axiom is referenced by:  elimne0  10425  1re  10435  mul02lem2  10613  addid1  10616  ine0  10872  0lt1  10959  recne0  11108  div1  11126  recdiv  11143  divdiv1  11148  divdiv2  11149  recgt0ii  11343  nnne0  11471  0ne1  11508  neg1ne0  11560  expcl2lem  13253  m1expcl2  13263  expclzlem  13265  1exp  13270  hashrabsn1  13545  relexp1g  14240  geo2sum2  15084  geoihalfsum  15092  fprodntriv  15150  prod0  15151  prod1  15152  fprodn0  15187  fprodn0f  15199  efne0  15304  tan0  15358  m1exp1  15581  divalg  15608  gcd1  15730  rpdvds  15854  m1dvdsndvds  15985  pcpre1  16029  pc1  16042  pcrec  16045  pcid  16059  m1expaddsub  18382  mvrf1  19913  cndrng  20270  cnmgpid  20303  gzrngunitlem  20306  gzrngunit  20307  zringnzr  20325  zringunit  20331  cnmsgnsubg  20417  cnmsgngrp  20419  psgninv  20422  pmatcollpw3fi1lem1  21092  dscmet  22879  xrhmeo  23247  clmopfne  23397  itg11  23989  ply1remlem  24453  dgrid  24551  plyrem  24591  facth  24592  fta1lem  24593  vieta1lem1  24596  vieta1lem2  24597  vieta1  24598  qaa  24609  iaa  24611  coseq00topi  24785  logneg2  24893  logtayl2  24940  1cxp  24950  cxpeq0  24956  logb1  25042  logbmpt  25061  ang180lem4  25085  ang180lem5  25086  isosctrlem2  25092  isosctrlem3  25093  angpined  25103  dcubic2  25117  dcubic  25119  dquartlem1  25124  atandmtan  25193  efrlim  25243  mumullem2  25453  1sgm2ppw  25472  dchrn0  25522  lgsne0  25607  1lgs  25612  gausslemma2dlem0i  25636  lgseisenlem1  25647  lgseisenlem2  25648  lgsquadlem1  25652  lgsquad2lem2  25657  2lgs  25679  2sqlem7  25696  2sqlem8a  25697  2sqlem8  25698  chebbnd2  25749  chto1lb  25750  pnt2  25885  pnt  25886  qabvle  25897  qabvexp  25898  ostthlem2  25900  ostth3  25910  ostth  25911  axlowdimlem6  26430  axlowdimlem13  26437  axlowdimlem14  26438  axlowdim1  26442  usgrexmpldifpr  26737  pthdadjvtx  27213  upgr4cycl4dv4e  27708  konigsberglem1  27778  frgrreggt1  27944  norm1exi  28800  kbpj  29508  largei  29819  ccfldextdgrr  30677  xrge0iif1  30816  ind1a  30913  cntnevol  31123  ballotlemii  31398  sgn0bi  31442  plymulx0  31454  signswch  31468  signstfvcl  31481  indispconn  32056  poimirlem23  34334  0dioph  38749  pell1234qrne0  38824  expgrowth  40060  binomcxplemradcnv  40077  xrralrecnnge  41071  iooiinioc  41242  stoweidlem13  41708  wallispi2lem1  41766  dirkertrigeq  41796  fourierdlem30  41832  fourierdlem62  41863  dfodd5  43167  line2ylem  44080  sec0  44200