Axiom ax-1ne0 10005

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

This axiom is referenced by:  elimne0  10030  1re  10039  mul02lem2  10213  addid1  10216  ine0  10465  0lt1  10550  recne0  10698  div1  10716  recdiv  10731  divdiv1  10736  divdiv2  10737  recgt0ii  10929  0ne1  11088  neg1ne0  11126  expcl2lem  12872  m1expcl2  12882  expclzlem  12884  1exp  12889  hashrabsn1  13163  s1nzOLD  13387  relexp1g  13766  geo2sum2  14605  geoihalfsum  14614  fprodntriv  14672  prod0  14673  prod1  14674  fprodn0  14709  efne0  14827  tan0  14881  m1exp1  15093  divalg  15126  gcd1  15249  rpdvds  15374  m1dvdsndvds  15503  pcpre1  15547  pc1  15560  pcrec  15563  pcid  15577  m1expaddsub  17918  mvrf1  19425  cndrng  19775  cnmgpid  19808  gzrngunitlem  19811  gzrngunit  19812  zringnzr  19830  zringunit  19836  cnmsgnsubg  19923  cnmsgngrp  19925  psgninv  19928  pmatcollpw3fi1lem1  20591  dscmet  22377  xrhmeo  22745  clmopfne  22896  itg11  23458  ply1remlem  23922  dgrid  24020  plyrem  24060  facth  24061  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  vieta1  24067  qaa  24078  iaa  24080  coseq00topi  24254  logneg2  24361  logtayl2  24408  1cxp  24418  cxpeq0  24424  logb1  24507  logbmpt  24526  ang180lem4  24542  ang180lem5  24543  isosctrlem2  24549  isosctrlem3  24550  angpined  24557  dcubic2  24571  dcubic  24573  dquartlem1  24578  atandmtan  24647  efrlim  24696  mumullem2  24906  1sgm2ppw  24925  dchrn0  24975  lgsne0  25060  1lgs  25065  gausslemma2dlem0i  25089  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  lgsquad2lem2  25110  2lgs  25132  2sqlem7  25149  2sqlem8a  25150  2sqlem8  25151  chebbnd2  25166  chto1lb  25167  pnt2  25302  pnt  25303  qabvle  25314  qabvexp  25315  ostthlem2  25317  ostth3  25327  ostth  25328  axlowdimlem6  25827  axlowdimlem13  25834  axlowdimlem14  25835  axlowdim1  25839  usgrexmpldifpr  26150  pthdadjvtx  26626  upgr4cycl4dv4e  27045  konigsberglem1  27114  frgrreggt1  27251  norm1exi  28107  kbpj  28815  largei  29126  xrge0iif1  29984  ind1a  30081  cntnevol  30291  ballotlemii  30565  sgn0bi  30609  plymulx0  30624  signswch  30638  signstfvcl  30650  indispconn  31216  poimirlem23  33432  0dioph  37342  pell1234qrne0  37417  expgrowth  38534  binomcxplemradcnv  38551  xrralrecnnge  39613  iooiinioc  39783  stoweidlem13  40230  wallispi2lem1  40288  dirkertrigeq  40318  fourierdlem30  40354  fourierdlem62  40385  dfodd5  41572  sec0  42501