Axiom ax-1ne0 11196

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

This axiom is used by:  elimne0  11223  1re  11235  mul02lem2  11414  addrid  11417  ine0  11676  0lt1  11763  recne0  11912  div1  11931  recdiv  11948  divdiv1  11953  divdiv2  11954  recgt0ii  12148  neg1ne0  12232  ind1a  12256  nnne0  12297  0ne1  12339  fvf1tp  13852  expcl2lem  14139  expclzlem  14149  m1expcl2  14151  1exp  14157  hashrabsn1  14440  tpf1ofv1  14564  relexp1g  15101  sgn0bi  15178  geo2sum2  15965  geoihalfsum  15973  fprodntriv  16033  prod0  16034  prod1  16035  fprodn0  16070  fprodn0f  16082  efne0d  16187  efne0OLD  16189  tan0  16243  m1exp1  16470  divalg  16497  gcd1  16622  rpdvds  16754  m1dvdsndvds  16894  pcpre1  16938  pc1  16951  pcrec  16954  pcid  16969  ex-chn2  18730  m1expaddsub  19626  cndrng  21615  cnmgpid  21643  gzrngunitlem  21646  gzrngunit  21647  zringnzr  21674  zringunit  21680  cnmsgnsubg  21791  cnmsgngrp  21793  psgninv  21796  mvrf1  22201  psdmvr  22398  pmatcollpw3fi1lem1  23012  dscmet  24799  xrhmeo  25175  clmopfne  25325  itg11  25920  ply1remlem  26392  dgrid  26491  plyn0mulidp  26512  plyrem  26536  facth  26537  fta1lem  26538  vieta1lem1  26541  vieta1lem2  26542  vieta1  26543  qaa  26554  iaa  26558  coseq00topi  26737  logneg2  26850  logtayl2  26897  1cxp  26907  cxpeq0  26913  logb1  27004  logbmpt  27023  ang180lem4  27047  ang180lem5  27048  isosctrlem2  27054  isosctrlem3  27055  angpined  27065  dcubic2  27079  dcubic  27081  dquartlem1  27086  atandmtan  27155  efrlim  27204  mumullem2  27414  1sgm2ppw  27434  dchrn0  27484  lgsne0  27569  1lgs  27574  gausslemma2dlem0i  27598  lgseisenlem1  27609  lgseisenlem2  27610  lgsquadlem1  27614  lgsquad2lem2  27619  2lgs  27641  2sqlem7  27658  2sqlem8a  27659  2sqlem8  27660  chebbnd2  27711  chto1lb  27712  pnt2  27847  pnt  27848  qabvle  27859  qabvexp  27860  ostthlem2  27862  ostth3  27872  ostth  27873  axlowdimlem6  29390  axlowdimlem13  29397  axlowdimlem14  29398  axlowdim1  29402  usgrexmpldifpr  29704  pthdadjvtx  30178  upgr4cycl4dv4e  30651  konigsberglem1  30718  frgrreggt1  30859  norm1exi  31717  kbpj  32423  largei  32734  indsupp  33300  esplyfvaln  34071  ccfldextdgrr  34169  constrfin  34243  2sqr3minply  34277  cos9thpiminplylem1  34279  cos9thpiminplylem2  34280  cos9thpiminplylem3  34281  cos9thpinconstrlem1  34286  xrge0iif1  34435  cntnevol  34726  ballotlemii  35002  signswch  35056  signstfvcl  35068  indispconn  35800  poimirlem23  38379  25or6to4  43059  tan3rdpi  43214  remulinvcom  43295  sn-rediv1d  43314  rerecne0d  43318  sn-0lt1  43350  0dioph  43610  pell1234qrne0  43681  expgrowth  45146  binomcxplemradcnv  45163  xrralrecnnge  46206  iooiinioc  46373  stoweidlem13  46828  wallispi2lem1  46886  dirkertrigeq  46916  fourierdlem30  46952  fourierdlem62  46983  goldratval  47741  cjnpoly  47744  sqrtnpoly  47748  dfodd5  48563  usgrexmpl1lem  48924  usgrexmpl2lem  48929  usgrexmpl2nb1  48935  usgrexmpl2trifr  48940  gpgvtxedg0  48966  gpgvtxedg1  48967  gpgedgiov  48968  gpgedg2iv  48970  gpg5nbgrvtx03starlem1  48971  gpg5nbgrvtx03starlem3  48973  gpg5nbgrvtx13starlem1  48974  gpg5nbgrvtx13starlem2  48975  gpg5nbgrvtx13starlem3  48976  gpg3nbgrvtx0  48979  gpg3nbgrvtx0ALT  48980  gpg3nbgrvtx1  48981  gpgprismgr4cycllem2  48999  pgnbgreunbgrlem2lem1  49017  pgnbgreunbgrlem2lem2  49018  pgnbgreunbgrlem2lem3  49019  pgnbgreunbgrlem5lem1  49023  pgnbgreunbgrlem5lem2  49024  pgnbgreunbgrlem5lem3  49025  gpg5edgnedg  49033  itcoval1  49580  line2ylem  49668  sec0  50673