Axiom ax-1ne0 11137

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

This axiom is referenced by:  elimne0  11164  1re  11174  mul02lem2  11351  addrid  11354  ine0  11613  0lt1  11700  recne0  11850  div1  11872  recdiv  11888  divdiv1  11893  divdiv2  11894  recgt0ii  12089  neg1ne0  12173  nnne0  12220  0ne1  12257  fvf1tp  13751  expcl2lem  14038  expclzlem  14048  m1expcl2  14050  1exp  14056  hashrabsn1  14339  tpf1ofv1  14462  relexp1g  14992  geo2sum2  15840  geoihalfsum  15848  fprodntriv  15908  prod0  15909  prod1  15910  fprodn0  15945  fprodn0f  15957  efne0d  16063  efne0OLD  16065  tan0  16119  m1exp1  16346  divalg  16373  gcd1  16498  rpdvds  16630  m1dvdsndvds  16769  pcpre1  16813  pc1  16826  pcrec  16829  pcid  16844  m1expaddsub  19428  cndrng  21310  cndrngOLD  21311  cnmgpid  21346  gzrngunitlem  21349  gzrngunit  21350  zringnzr  21370  zringunit  21376  cnmsgnsubg  21486  cnmsgngrp  21488  psgninv  21491  mvrf1  21895  psdmvr  22056  pmatcollpw3fi1lem1  22673  dscmet  24460  xrhmeo  24844  clmopfne  24996  itg11  25592  ply1remlem  26070  dgrid  26170  plyrem  26213  facth  26214  fta1lem  26215  vieta1lem1  26218  vieta1lem2  26219  vieta1  26220  qaa  26231  iaa  26233  coseq00topi  26411  logneg2  26524  logtayl2  26571  1cxp  26581  cxpeq0  26587  logb1  26679  logbmpt  26698  ang180lem4  26722  ang180lem5  26723  isosctrlem2  26729  isosctrlem3  26730  angpined  26740  dcubic2  26754  dcubic  26756  dquartlem1  26761  atandmtan  26830  efrlim  26879  efrlimOLD  26880  mumullem2  27090  1sgm2ppw  27111  dchrn0  27161  lgsne0  27246  1lgs  27251  gausslemma2dlem0i  27275  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  lgsquad2lem2  27296  2lgs  27318  2sqlem7  27335  2sqlem8a  27336  2sqlem8  27337  chebbnd2  27388  chto1lb  27389  pnt2  27524  pnt  27525  qabvle  27536  qabvexp  27537  ostthlem2  27539  ostth3  27549  ostth  27550  axlowdimlem6  28874  axlowdimlem13  28881  axlowdimlem14  28882  axlowdim1  28886  usgrexmpldifpr  29185  pthdadjvtx  29658  upgr4cycl4dv4e  30114  konigsberglem1  30181  frgrreggt1  30322  norm1exi  31179  kbpj  31885  largei  32196  sgn0bi  32765  ind1a  32782  indsupp  32790  ccfldextdgrr  33667  constrfin  33736  2sqr3minply  33770  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpinconstrlem1  33779  xrge0iif1  33928  cntnevol  34218  ballotlemii  34495  plymulx0  34538  signswch  34552  signstfvcl  34564  indispconn  35221  poimirlem23  37637  tan3rdpi  42340  remulinvcom  42421  sn-0lt1  42463  0dioph  42766  pell1234qrne0  42841  expgrowth  44324  binomcxplemradcnv  44341  xrralrecnnge  45386  iooiinioc  45554  stoweidlem13  46011  wallispi2lem1  46069  dirkertrigeq  46099  fourierdlem30  46135  fourierdlem62  46166  cjnpoly  46890  dfodd5  47661  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb1  48023  usgrexmpl2trifr  48028  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpgedg2iv  48058  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  gpgprismgr4cycllem2  48086  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  itcoval1  48652  line2ylem  48740  sec0  49749