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 2932	1 wff 1 ≠ 0

This axiom is referenced by:  elimne0  11223  1re  11233  mul02lem2  11410  addrid  11413  ine0  11670  0lt1  11757  recne0  11907  div1  11929  recdiv  11945  divdiv1  11950  divdiv2  11951  recgt0ii  12146  nnne0  12272  0ne1  12309  neg1ne0  12354  fvf1tp  13804  expcl2lem  14089  expclzlem  14099  m1expcl2  14101  1exp  14107  hashrabsn1  14390  tpf1ofv1  14513  relexp1g  15043  geo2sum2  15888  geoihalfsum  15896  fprodntriv  15956  prod0  15957  prod1  15958  fprodn0  15993  fprodn0f  16005  efne0d  16111  efne0OLD  16113  tan0  16167  m1exp1  16393  divalg  16420  gcd1  16545  rpdvds  16677  m1dvdsndvds  16816  pcpre1  16860  pc1  16873  pcrec  16876  pcid  16891  m1expaddsub  19477  cndrng  21359  cndrngOLD  21360  cnmgpid  21395  gzrngunitlem  21398  gzrngunit  21399  zringnzr  21419  zringunit  21425  cnmsgnsubg  21535  cnmsgngrp  21537  psgninv  21540  mvrf1  21944  psdmvr  22105  pmatcollpw3fi1lem1  22722  dscmet  24509  xrhmeo  24893  clmopfne  25045  itg11  25642  ply1remlem  26120  dgrid  26220  plyrem  26263  facth  26264  fta1lem  26265  vieta1lem1  26268  vieta1lem2  26269  vieta1  26270  qaa  26281  iaa  26283  coseq00topi  26461  logneg2  26574  logtayl2  26621  1cxp  26631  cxpeq0  26637  logb1  26729  logbmpt  26748  ang180lem4  26772  ang180lem5  26773  isosctrlem2  26779  isosctrlem3  26780  angpined  26790  dcubic2  26804  dcubic  26806  dquartlem1  26811  atandmtan  26880  efrlim  26929  efrlimOLD  26930  mumullem2  27140  1sgm2ppw  27161  dchrn0  27211  lgsne0  27296  1lgs  27301  gausslemma2dlem0i  27325  lgseisenlem1  27336  lgseisenlem2  27337  lgsquadlem1  27341  lgsquad2lem2  27346  2lgs  27368  2sqlem7  27385  2sqlem8a  27386  2sqlem8  27387  chebbnd2  27438  chto1lb  27439  pnt2  27574  pnt  27575  qabvle  27586  qabvexp  27587  ostthlem2  27589  ostth3  27599  ostth  27600  axlowdimlem6  28872  axlowdimlem13  28879  axlowdimlem14  28880  axlowdim1  28884  usgrexmpldifpr  29183  pthdadjvtx  29656  upgr4cycl4dv4e  30112  konigsberglem1  30179  frgrreggt1  30320  norm1exi  31177  kbpj  31883  largei  32194  sgn0bi  32765  ind1a  32782  indsupp  32790  ccfldextdgrr  33659  constrfin  33726  2sqr3minply  33760  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  cos9thpinconstrlem1  33769  xrge0iif1  33915  cntnevol  34205  ballotlemii  34482  plymulx0  34525  signswch  34539  signstfvcl  34551  indispconn  35202  poimirlem23  37613  tan3rdpi  42346  remulinvcom  42422  sn-0lt1  42453  0dioph  42748  pell1234qrne0  42823  expgrowth  44307  binomcxplemradcnv  44324  xrralrecnnge  45365  iooiinioc  45533  stoweidlem13  45990  wallispi2lem1  46048  dirkertrigeq  46078  fourierdlem30  46114  fourierdlem62  46145  dfodd5  47622  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb1  47984  usgrexmpl2trifr  47989  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg3nbgrvtx0  48026  gpg3nbgrvtx0ALT  48027  gpg3nbgrvtx1  48028  gpgprismgr4cycllem2  48043  itcoval1  48591  line2ylem  48679  sec0  49572