Axiom ax-1ne0 11179

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

This axiom is referenced by:  elimne0  11204  1re  11214  mul02lem2  11391  addrid  11394  ine0  11649  0lt1  11736  recne0  11885  div1  11903  recdiv  11920  divdiv1  11925  divdiv2  11926  recgt0ii  12120  nnne0  12246  0ne1  12283  neg1ne0  12328  expcl2lem  14039  expclzlem  14049  m1expcl2  14051  1exp  14057  hashrabsn1  14334  relexp1g  14973  geo2sum2  15820  geoihalfsum  15828  fprodntriv  15886  prod0  15887  prod1  15888  fprodn0  15923  fprodn0f  15935  efne0  16040  tan0  16094  m1exp1  16319  divalg  16346  gcd1  16469  rpdvds  16597  m1dvdsndvds  16731  pcpre1  16775  pc1  16788  pcrec  16791  pcid  16806  m1expaddsub  19366  cndrng  20974  cnmgpid  21007  gzrngunitlem  21010  gzrngunit  21011  zringnzr  21030  zringunit  21036  cnmsgnsubg  21130  cnmsgngrp  21132  psgninv  21135  mvrf1  21545  pmatcollpw3fi1lem1  22288  dscmet  24081  xrhmeo  24462  clmopfne  24612  itg11  25208  ply1remlem  25680  dgrid  25778  plyrem  25818  facth  25819  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  vieta1  25825  qaa  25836  iaa  25838  coseq00topi  26012  logneg2  26123  logtayl2  26170  1cxp  26180  cxpeq0  26186  logb1  26274  logbmpt  26293  ang180lem4  26317  ang180lem5  26318  isosctrlem2  26324  isosctrlem3  26325  angpined  26335  dcubic2  26349  dcubic  26351  dquartlem1  26356  atandmtan  26425  efrlim  26474  mumullem2  26684  1sgm2ppw  26703  dchrn0  26753  lgsne0  26838  1lgs  26843  gausslemma2dlem0i  26867  lgseisenlem1  26878  lgseisenlem2  26879  lgsquadlem1  26883  lgsquad2lem2  26888  2lgs  26910  2sqlem7  26927  2sqlem8a  26928  2sqlem8  26929  chebbnd2  26980  chto1lb  26981  pnt2  27116  pnt  27117  qabvle  27128  qabvexp  27129  ostthlem2  27131  ostth3  27141  ostth  27142  axlowdimlem6  28205  axlowdimlem13  28212  axlowdimlem14  28213  axlowdim1  28217  usgrexmpldifpr  28515  pthdadjvtx  28987  upgr4cycl4dv4e  29438  konigsberglem1  29505  frgrreggt1  29646  norm1exi  30503  kbpj  31209  largei  31520  ccfldextdgrr  32746  xrge0iif1  32918  ind1a  33017  cntnevol  33226  ballotlemii  33502  sgn0bi  33546  plymulx0  33558  signswch  33572  signstfvcl  33584  indispconn  34225  poimirlem23  36511  remulinvcom  41305  sn-0lt1  41335  0dioph  41516  pell1234qrne0  41591  expgrowth  43094  binomcxplemradcnv  43111  xrralrecnnge  44100  iooiinioc  44269  stoweidlem13  44729  wallispi2lem1  44787  dirkertrigeq  44817  fourierdlem30  44853  fourierdlem62  44884  dfodd5  46328  itcoval1  47349  line2ylem  47437  sec0  47805