Axiom ax-1ne0 11269

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

This axiom is used by:  elimne0  11296  1re  11308  mul02lem2  11487  addrid  11490  ine0  11751  0lt1  11838  recne0  11987  div1  12006  recdiv  12023  divdiv1  12028  divdiv2  12029  recgt0ii  12223  neg1ne0  12307  ind1a  12331  nnne0  12372  0ne1  12414  fvf1tp  13929  expcl2lem  14216  expclzlem  14226  m1expcl2  14228  1exp  14234  hashrabsn1  14518  tpf1ofv1  14642  relexp1g  15179  sgn0bi  15256  geo2sum2  16043  geoihalfsum  16051  fprodntriv  16109  prod0  16110  prod1  16111  fprodn0  16146  fprodn0f  16158  efne0d  16263  efne0OLD  16265  tan0  16319  m1exp1  16546  divalg  16573  gcd1  16701  rpdvds  16835  m1dvdsndvds  16976  pcpre1  17020  pc1  17033  pcrec  17036  pcid  17051  ex-chn2  18812  m1expaddsub  19712  cndrng  21707  cnmgpid  21735  gzrngunitlem  21738  gzrngunit  21739  zringnzr  21766  zringunit  21772  cnmsgnsubg  21883  cnmsgngrp  21885  psgninv  21888  mvrf1  22293  psdmvr  22490  pmatcollpw3fi1lem1  23104  dscmet  24891  xrhmeo  25267  clmopfne  25417  itg11  26012  ply1remlem  26483  dgrid  26583  plyn0mulidp  26602  plyrem  26626  facth  26627  fta1lem  26628  vieta1lem1  26633  vieta1lem2  26634  vieta1  26635  qaa  26647  iaa  26651  iaaOLD  26652  coseq00topi  26831  logneg2  26943  logtayl2  26990  1cxp  27000  cxpeq0  27006  logb1  27097  logbmpt  27116  ang180lem4  27140  ang180lem5  27141  isosctrlem2  27147  isosctrlem3  27148  angpined  27158  dcubic2  27172  dcubic  27174  dquartlem1  27179  atandmtan  27248  efrlim  27297  mumullem2  27507  1sgm2ppw  27527  dchrn0  27577  lgsne0  27662  1lgs  27667  gausslemma2dlem0i  27691  lgseisenlem1  27702  lgseisenlem2  27703  lgsquadlem1  27707  lgsquad2lem2  27712  2lgs  27734  2sqlem7  27751  2sqlem8a  27752  2sqlem8  27753  chebbnd2  27804  chto1lb  27805  pnt2  27940  pnt  27941  qabvle  27952  qabvexp  27953  ostthlem2  27955  ostth3  27965  ostth  27966  axlowdimlem6  29525  axlowdimlem13  29532  axlowdimlem14  29533  axlowdim1  29537  usgrexmpldifpr  29839  pthdadjvtx  30313  upgr4cycl4dv4e  30786  konigsberglem1  30853  frgrreggt1  30994  norm1exi  31852  kbpj  32558  largei  32869  indsupp  33476  esplyfvaln  34248  ccfldextdgrr  34346  constrfin  34420  2sqr3minply  34454  cos9thpiminplylem1  34456  cos9thpiminplylem2  34457  cos9thpiminplylem3  34458  cos9thpinconstrlem1  34463  xrge0iif1  34612  cntnevol  34903  ballotlemii  35178  signswch  35232  signstfvcl  35244  indispconn  36041  poimirlem23  38604  25or6to4  43299  tan3rdpi  43446  remulinvcom  43527  sn-rediv1d  43546  rerecne0d  43550  sn-0lt1  43582  0dioph  43831  pell1234qrne0  43902  expgrowth  45361  binomcxplemradcnv  45378  xrralrecnnge  46443  iooiinioc  46610  stoweidlem13  47065  wallispi2lem1  47123  dirkertrigeq  47153  fourierdlem30  47189  fourierdlem62  47220  goldratval  47978  cjnpoly  47981  sqrtnpoly  47985  dfodd5  48800  usgrexmpl1lem  49161  usgrexmpl2lem  49166  usgrexmpl2nb1  49172  usgrexmpl2trifr  49177  gpgvtxedg0  49203  gpgvtxedg1  49204  gpgedgiov  49205  gpgedg2iv  49207  gpg5nbgrvtx03starlem1  49208  gpg5nbgrvtx03starlem3  49210  gpg5nbgrvtx13starlem1  49211  gpg5nbgrvtx13starlem2  49212  gpg5nbgrvtx13starlem3  49213  gpg3nbgrvtx0  49216  gpg3nbgrvtx0ALT  49217  gpg3nbgrvtx1  49218  gpgprismgr4cycllem2  49236  pgnbgreunbgrlem2lem1  49254  pgnbgreunbgrlem2lem2  49255  pgnbgreunbgrlem2lem3  49256  pgnbgreunbgrlem5lem1  49260  pgnbgreunbgrlem5lem2  49261  pgnbgreunbgrlem5lem3  49262  gpg5edgnedg  49270  itcoval1  49817  line2ylem  49905  sec0  50895