Axiom ax-1ne0 11240

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

This axiom is used by:  elimne0  11267  1re  11279  mul02lem2  11458  addrid  11461  ine0  11720  0lt1  11807  recne0  11956  div1  11975  recdiv  11992  divdiv1  11997  divdiv2  11998  recgt0ii  12192  neg1ne0  12276  ind1a  12300  nnne0  12341  0ne1  12383  fvf1tp  13897  expcl2lem  14184  expclzlem  14194  m1expcl2  14196  1exp  14202  hashrabsn1  14485  tpf1ofv1  14609  relexp1g  15146  sgn0bi  15223  geo2sum2  16010  geoihalfsum  16018  fprodntriv  16076  prod0  16077  prod1  16078  fprodn0  16113  fprodn0f  16125  efne0d  16230  efne0OLD  16232  tan0  16286  m1exp1  16513  divalg  16540  gcd1  16665  rpdvds  16797  m1dvdsndvds  16937  pcpre1  16981  pc1  16994  pcrec  16997  pcid  17012  ex-chn2  18773  m1expaddsub  19673  cndrng  21668  cnmgpid  21696  gzrngunitlem  21699  gzrngunit  21700  zringnzr  21727  zringunit  21733  cnmsgnsubg  21844  cnmsgngrp  21846  psgninv  21849  mvrf1  22254  psdmvr  22451  pmatcollpw3fi1lem1  23065  dscmet  24852  xrhmeo  25228  clmopfne  25378  itg11  25973  ply1remlem  26444  dgrid  26544  plyn0mulidp  26565  plyrem  26589  facth  26590  fta1lem  26591  vieta1lem1  26596  vieta1lem2  26597  vieta1  26598  qaa  26610  iaa  26614  iaaOLD  26615  coseq00topi  26794  logneg2  26906  logtayl2  26953  1cxp  26963  cxpeq0  26969  logb1  27060  logbmpt  27079  ang180lem4  27103  ang180lem5  27104  isosctrlem2  27110  isosctrlem3  27111  angpined  27121  dcubic2  27135  dcubic  27137  dquartlem1  27142  atandmtan  27211  efrlim  27260  mumullem2  27470  1sgm2ppw  27490  dchrn0  27540  lgsne0  27625  1lgs  27630  gausslemma2dlem0i  27654  lgseisenlem1  27665  lgseisenlem2  27666  lgsquadlem1  27670  lgsquad2lem2  27675  2lgs  27697  2sqlem7  27714  2sqlem8a  27715  2sqlem8  27716  chebbnd2  27767  chto1lb  27768  pnt2  27903  pnt  27904  qabvle  27915  qabvexp  27916  ostthlem2  27918  ostth3  27928  ostth  27929  axlowdimlem6  29458  axlowdimlem13  29465  axlowdimlem14  29466  axlowdim1  29470  usgrexmpldifpr  29772  pthdadjvtx  30246  upgr4cycl4dv4e  30719  konigsberglem1  30786  frgrreggt1  30927  norm1exi  31785  kbpj  32491  largei  32802  indsupp  33367  esplyfvaln  34139  ccfldextdgrr  34237  constrfin  34311  2sqr3minply  34345  cos9thpiminplylem1  34347  cos9thpiminplylem2  34348  cos9thpiminplylem3  34349  cos9thpinconstrlem1  34354  xrge0iif1  34503  cntnevol  34794  ballotlemii  35070  signswch  35124  signstfvcl  35136  indispconn  35920  poimirlem23  38481  25or6to4  43176  tan3rdpi  43331  remulinvcom  43412  sn-rediv1d  43431  rerecne0d  43435  sn-0lt1  43467  0dioph  43727  pell1234qrne0  43798  expgrowth  45263  binomcxplemradcnv  45280  xrralrecnnge  46323  iooiinioc  46490  stoweidlem13  46945  wallispi2lem1  47003  dirkertrigeq  47033  fourierdlem30  47069  fourierdlem62  47100  goldratval  47858  cjnpoly  47861  sqrtnpoly  47865  dfodd5  48680  usgrexmpl1lem  49041  usgrexmpl2lem  49046  usgrexmpl2nb1  49052  usgrexmpl2trifr  49057  gpgvtxedg0  49083  gpgvtxedg1  49084  gpgedgiov  49085  gpgedg2iv  49087  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem2  49092  gpg5nbgrvtx13starlem3  49093  gpg3nbgrvtx0  49096  gpg3nbgrvtx0ALT  49097  gpg3nbgrvtx1  49098  gpgprismgr4cycllem2  49116  pgnbgreunbgrlem2lem1  49134  pgnbgreunbgrlem2lem2  49135  pgnbgreunbgrlem2lem3  49136  pgnbgreunbgrlem5lem1  49140  pgnbgreunbgrlem5lem2  49141  pgnbgreunbgrlem5lem3  49142  gpg5edgnedg  49150  itcoval1  49697  line2ylem  49785  sec0  50775