Axiom ax-1ne0 11144

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

This axiom is referenced by:  elimne0  11171  1re  11183  mul02lem2  11362  addrid  11365  ine0  11624  0lt1  11711  recne0  11860  div1  11882  recdiv  11899  divdiv1  11904  divdiv2  11905  recgt0ii  12100  neg1ne0  12184  ind1a  12208  nnne0  12249  0ne1  12291  fvf1tp  13801  expcl2lem  14088  expclzlem  14098  m1expcl2  14100  1exp  14106  hashrabsn1  14389  tpf1ofv1  14512  relexp1g  15041  sgn0bi  15118  geo2sum2  15906  geoihalfsum  15914  fprodntriv  15974  prod0  15975  prod1  15976  fprodn0  16011  fprodn0f  16023  efne0d  16129  efne0OLD  16131  tan0  16185  m1exp1  16412  divalg  16439  gcd1  16564  rpdvds  16696  m1dvdsndvds  16836  pcpre1  16880  pc1  16893  pcrec  16896  pcid  16911  ex-chn2  18672  m1expaddsub  19540  cndrng  21455  cnmgpid  21483  gzrngunitlem  21486  gzrngunit  21487  zringnzr  21514  zringunit  21520  cnmsgnsubg  21631  cnmsgngrp  21633  psgninv  21636  mvrf1  22039  psdmvr  22236  pmatcollpw3fi1lem1  22848  dscmet  24634  xrhmeo  25010  clmopfne  25160  itg11  25755  ply1remlem  26227  dgrid  26326  plyn0mulidp  26347  plyrem  26371  facth  26372  fta1lem  26373  vieta1lem1  26376  vieta1lem2  26377  vieta1  26378  qaa  26389  iaa  26391  coseq00topi  26569  logneg2  26682  logtayl2  26729  1cxp  26739  cxpeq0  26745  logb1  26836  logbmpt  26855  ang180lem4  26879  ang180lem5  26880  isosctrlem2  26886  isosctrlem3  26887  angpined  26897  dcubic2  26911  dcubic  26913  dquartlem1  26918  atandmtan  26987  efrlim  27036  mumullem2  27246  1sgm2ppw  27266  dchrn0  27316  lgsne0  27401  1lgs  27406  gausslemma2dlem0i  27430  lgseisenlem1  27441  lgseisenlem2  27442  lgsquadlem1  27446  lgsquad2lem2  27451  2lgs  27473  2sqlem7  27490  2sqlem8a  27491  2sqlem8  27492  chebbnd2  27543  chto1lb  27544  pnt2  27679  pnt  27680  qabvle  27691  qabvexp  27692  ostthlem2  27694  ostth3  27704  ostth  27705  axlowdimlem6  29150  axlowdimlem13  29157  axlowdimlem14  29158  axlowdim1  29162  usgrexmpldifpr  29461  pthdadjvtx  29930  upgr4cycl4dv4e  30389  konigsberglem1  30456  frgrreggt1  30597  norm1exi  31455  kbpj  32161  largei  32472  indsupp  33047  esplyfvaln  33873  ccfldextdgrr  33971  constrfin  34045  2sqr3minply  34079  cos9thpiminplylem1  34081  cos9thpiminplylem2  34082  cos9thpiminplylem3  34083  cos9thpinconstrlem1  34088  xrge0iif1  34237  cntnevol  34527  ballotlemii  34803  signswch  34857  signstfvcl  34869  indispconn  35589  poimirlem23  38147  tan3rdpi  42966  remulinvcom  43047  sn-rediv1d  43066  rerecne0d  43070  sn-0lt1  43102  0dioph  43364  pell1234qrne0  43435  expgrowth  44916  binomcxplemradcnv  44933  xrralrecnnge  45970  iooiinioc  46137  stoweidlem13  46592  wallispi2lem1  46650  dirkertrigeq  46680  fourierdlem30  46716  fourierdlem62  46747  cjnpoly  47488  dfodd5  48287  usgrexmpl1lem  48648  usgrexmpl2lem  48653  usgrexmpl2nb1  48659  usgrexmpl2trifr  48664  gpgvtxedg0  48690  gpgvtxedg1  48691  gpgedgiov  48692  gpgedg2iv  48694  gpg5nbgrvtx03starlem1  48695  gpg5nbgrvtx03starlem3  48697  gpg5nbgrvtx13starlem1  48698  gpg5nbgrvtx13starlem2  48699  gpg5nbgrvtx13starlem3  48700  gpg3nbgrvtx0  48703  gpg3nbgrvtx0ALT  48704  gpg3nbgrvtx1  48705  gpgprismgr4cycllem2  48723  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  pgnbgreunbgrlem2lem3  48743  pgnbgreunbgrlem5lem1  48747  pgnbgreunbgrlem5lem2  48748  pgnbgreunbgrlem5lem3  48749  gpg5edgnedg  48757  itcoval1  49290  line2ylem  49378  sec0  50386