Axiom ax-1ne0 11072

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

This axiom is referenced by:  elimne0  11099  1re  11109  mul02lem2  11287  addrid  11290  ine0  11549  0lt1  11636  recne0  11786  div1  11808  recdiv  11824  divdiv1  11829  divdiv2  11830  recgt0ii  12025  neg1ne0  12109  nnne0  12156  0ne1  12193  fvf1tp  13690  expcl2lem  13977  expclzlem  13987  m1expcl2  13989  1exp  13995  hashrabsn1  14278  tpf1ofv1  14401  relexp1g  14930  geo2sum2  15778  geoihalfsum  15786  fprodntriv  15846  prod0  15847  prod1  15848  fprodn0  15883  fprodn0f  15895  efne0d  16001  efne0OLD  16003  tan0  16057  m1exp1  16284  divalg  16311  gcd1  16436  rpdvds  16568  m1dvdsndvds  16707  pcpre1  16751  pc1  16764  pcrec  16767  pcid  16782  ex-chn2  18541  m1expaddsub  19408  cndrng  21333  cndrngOLD  21334  cnmgpid  21364  gzrngunitlem  21367  gzrngunit  21368  zringnzr  21395  zringunit  21401  cnmsgnsubg  21512  cnmsgngrp  21514  psgninv  21517  mvrf1  21921  psdmvr  22082  pmatcollpw3fi1lem1  22699  dscmet  24485  xrhmeo  24869  clmopfne  25021  itg11  25617  ply1remlem  26095  dgrid  26195  plyrem  26238  facth  26239  fta1lem  26240  vieta1lem1  26243  vieta1lem2  26244  vieta1  26245  qaa  26256  iaa  26258  coseq00topi  26436  logneg2  26549  logtayl2  26596  1cxp  26606  cxpeq0  26612  logb1  26704  logbmpt  26723  ang180lem4  26747  ang180lem5  26748  isosctrlem2  26754  isosctrlem3  26755  angpined  26765  dcubic2  26779  dcubic  26781  dquartlem1  26786  atandmtan  26855  efrlim  26904  efrlimOLD  26905  mumullem2  27115  1sgm2ppw  27136  dchrn0  27186  lgsne0  27271  1lgs  27276  gausslemma2dlem0i  27300  lgseisenlem1  27311  lgseisenlem2  27312  lgsquadlem1  27316  lgsquad2lem2  27321  2lgs  27343  2sqlem7  27360  2sqlem8a  27361  2sqlem8  27362  chebbnd2  27413  chto1lb  27414  pnt2  27549  pnt  27550  qabvle  27561  qabvexp  27562  ostthlem2  27564  ostth3  27574  ostth  27575  axlowdimlem6  28923  axlowdimlem13  28930  axlowdimlem14  28931  axlowdim1  28935  usgrexmpldifpr  29234  pthdadjvtx  29704  upgr4cycl4dv4e  30160  konigsberglem1  30227  frgrreggt1  30368  norm1exi  31225  kbpj  31931  largei  32242  sgn0bi  32818  ind1a  32835  indsupp  32843  ccfldextdgrr  33680  constrfin  33754  2sqr3minply  33788  cos9thpiminplylem1  33790  cos9thpiminplylem2  33791  cos9thpiminplylem3  33792  cos9thpinconstrlem1  33797  xrge0iif1  33946  cntnevol  34236  ballotlemii  34512  plymulx0  34555  signswch  34569  signstfvcl  34581  indispconn  35266  poimirlem23  37682  tan3rdpi  42384  remulinvcom  42465  sn-0lt1  42507  0dioph  42810  pell1234qrne0  42885  expgrowth  44367  binomcxplemradcnv  44384  xrralrecnnge  45427  iooiinioc  45595  stoweidlem13  46050  wallispi2lem1  46108  dirkertrigeq  46138  fourierdlem30  46174  fourierdlem62  46205  cjnpoly  46919  dfodd5  47690  usgrexmpl1lem  48051  usgrexmpl2lem  48056  usgrexmpl2nb1  48062  usgrexmpl2trifr  48067  gpgvtxedg0  48093  gpgvtxedg1  48094  gpgedgiov  48095  gpgedg2iv  48097  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpg3nbgrvtx0  48106  gpg3nbgrvtx0ALT  48107  gpg3nbgrvtx1  48108  gpgprismgr4cycllem2  48126  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  gpg5edgnedg  48160  itcoval1  48694  line2ylem  48782  sec0  49791