Axiom ax-1ne0 11253

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

This axiom is referenced by:  elimne0  11280  1re  11290  mul02lem2  11467  addrid  11470  ine0  11725  0lt1  11812  recne0  11962  div1  11984  recdiv  12000  divdiv1  12005  divdiv2  12006  recgt0ii  12201  nnne0  12327  0ne1  12364  neg1ne0  12409  fvf1tp  13840  expcl2lem  14124  expclzlem  14134  m1expcl2  14136  1exp  14142  hashrabsn1  14423  tpf1ofv1  14546  relexp1g  15075  geo2sum2  15922  geoihalfsum  15930  fprodntriv  15990  prod0  15991  prod1  15992  fprodn0  16027  fprodn0f  16039  efne0  16145  tan0  16199  m1exp1  16424  divalg  16451  gcd1  16574  rpdvds  16707  m1dvdsndvds  16845  pcpre1  16889  pc1  16902  pcrec  16905  pcid  16920  m1expaddsub  19540  cndrng  21434  cndrngOLD  21435  cnmgpid  21470  gzrngunitlem  21473  gzrngunit  21474  zringnzr  21494  zringunit  21500  cnmsgnsubg  21618  cnmsgngrp  21620  psgninv  21623  mvrf1  22029  pmatcollpw3fi1lem1  22813  dscmet  24606  xrhmeo  24996  clmopfne  25148  itg11  25745  ply1remlem  26224  dgrid  26324  plyrem  26365  facth  26366  fta1lem  26367  vieta1lem1  26370  vieta1lem2  26371  vieta1  26372  qaa  26383  iaa  26385  coseq00topi  26562  logneg2  26675  logtayl2  26722  1cxp  26732  cxpeq0  26738  logb1  26830  logbmpt  26849  ang180lem4  26873  ang180lem5  26874  isosctrlem2  26880  isosctrlem3  26881  angpined  26891  dcubic2  26905  dcubic  26907  dquartlem1  26912  atandmtan  26981  efrlim  27030  efrlimOLD  27031  mumullem2  27241  1sgm2ppw  27262  dchrn0  27312  lgsne0  27397  1lgs  27402  gausslemma2dlem0i  27426  lgseisenlem1  27437  lgseisenlem2  27438  lgsquadlem1  27442  lgsquad2lem2  27447  2lgs  27469  2sqlem7  27486  2sqlem8a  27487  2sqlem8  27488  chebbnd2  27539  chto1lb  27540  pnt2  27675  pnt  27676  qabvle  27687  qabvexp  27688  ostthlem2  27690  ostth3  27700  ostth  27701  axlowdimlem6  28980  axlowdimlem13  28987  axlowdimlem14  28988  axlowdim1  28992  usgrexmpldifpr  29293  pthdadjvtx  29766  upgr4cycl4dv4e  30217  konigsberglem1  30284  frgrreggt1  30425  norm1exi  31282  kbpj  31988  largei  32299  ccfldextdgrr  33682  constrfin  33736  2sqr3minply  33738  xrge0iif1  33884  ind1a  33983  cntnevol  34192  ballotlemii  34468  sgn0bi  34512  plymulx0  34524  signswch  34538  signstfvcl  34550  indispconn  35202  poimirlem23  37603  efne0d  42325  tan3rdpi  42338  remulinvcom  42408  sn-0lt1  42439  0dioph  42734  pell1234qrne0  42809  expgrowth  44304  binomcxplemradcnv  44321  xrralrecnnge  45305  iooiinioc  45474  stoweidlem13  45934  wallispi2lem1  45992  dirkertrigeq  46022  fourierdlem30  46058  fourierdlem62  46089  dfodd5  47534  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb1  47847  usgrexmpl2trifr  47852  itcoval1  48397  line2ylem  48485  sec0  48852