Axiom ax-1ne0 10871

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

This axiom is referenced by:  elimne0  10896  1re  10906  mul02lem2  11082  addid1  11085  ine0  11340  0lt1  11427  recne0  11576  div1  11594  recdiv  11611  divdiv1  11616  divdiv2  11617  recgt0ii  11811  nnne0  11937  0ne1  11974  neg1ne0  12019  expcl2lem  13722  m1expcl2  13732  expclzlem  13734  1exp  13740  hashrabsn1  14017  relexp1g  14665  geo2sum2  15514  geoihalfsum  15522  fprodntriv  15580  prod0  15581  prod1  15582  fprodn0  15617  fprodn0f  15629  efne0  15734  tan0  15788  m1exp1  16013  divalg  16040  gcd1  16163  rpdvds  16293  m1dvdsndvds  16427  pcpre1  16471  pc1  16484  pcrec  16487  pcid  16502  m1expaddsub  19021  cndrng  20539  cnmgpid  20572  gzrngunitlem  20575  gzrngunit  20576  zringnzr  20594  zringunit  20600  cnmsgnsubg  20694  cnmsgngrp  20696  psgninv  20699  mvrf1  21104  pmatcollpw3fi1lem1  21843  dscmet  23634  xrhmeo  24015  clmopfne  24165  itg11  24760  ply1remlem  25232  dgrid  25330  plyrem  25370  facth  25371  fta1lem  25372  vieta1lem1  25375  vieta1lem2  25376  vieta1  25377  qaa  25388  iaa  25390  coseq00topi  25564  logneg2  25675  logtayl2  25722  1cxp  25732  cxpeq0  25738  logb1  25824  logbmpt  25843  ang180lem4  25867  ang180lem5  25868  isosctrlem2  25874  isosctrlem3  25875  angpined  25885  dcubic2  25899  dcubic  25901  dquartlem1  25906  atandmtan  25975  efrlim  26024  mumullem2  26234  1sgm2ppw  26253  dchrn0  26303  lgsne0  26388  1lgs  26393  gausslemma2dlem0i  26417  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  lgsquad2lem2  26438  2lgs  26460  2sqlem7  26477  2sqlem8a  26478  2sqlem8  26479  chebbnd2  26530  chto1lb  26531  pnt2  26666  pnt  26667  qabvle  26678  qabvexp  26679  ostthlem2  26681  ostth3  26691  ostth  26692  axlowdimlem6  27218  axlowdimlem13  27225  axlowdimlem14  27226  axlowdim1  27230  usgrexmpldifpr  27528  pthdadjvtx  27999  upgr4cycl4dv4e  28450  konigsberglem1  28517  frgrreggt1  28658  norm1exi  29513  kbpj  30219  largei  30530  ccfldextdgrr  31644  xrge0iif1  31790  ind1a  31887  cntnevol  32096  ballotlemii  32370  sgn0bi  32414  plymulx0  32426  signswch  32440  signstfvcl  32452  indispconn  33096  poimirlem23  35727  remulinvcom  40335  sn-0lt1  40353  0dioph  40516  pell1234qrne0  40591  expgrowth  41842  binomcxplemradcnv  41859  xrralrecnnge  42820  iooiinioc  42984  stoweidlem13  43444  wallispi2lem1  43502  dirkertrigeq  43532  fourierdlem30  43568  fourierdlem62  43599  dfodd5  45000  itcoval1  45897  line2ylem  45985  sec0  46348