Axiom ax-1ne0 11224

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

This axiom is referenced by:  elimne0  11251  1re  11261  mul02lem2  11438  addrid  11441  ine0  11698  0lt1  11785  recne0  11935  div1  11957  recdiv  11973  divdiv1  11978  divdiv2  11979  recgt0ii  12174  nnne0  12300  0ne1  12337  neg1ne0  12382  fvf1tp  13829  expcl2lem  14114  expclzlem  14124  m1expcl2  14126  1exp  14132  hashrabsn1  14413  tpf1ofv1  14536  relexp1g  15065  geo2sum2  15910  geoihalfsum  15918  fprodntriv  15978  prod0  15979  prod1  15980  fprodn0  16015  fprodn0f  16027  efne0  16133  tan0  16187  m1exp1  16413  divalg  16440  gcd1  16565  rpdvds  16697  m1dvdsndvds  16836  pcpre1  16880  pc1  16893  pcrec  16896  pcid  16911  m1expaddsub  19516  cndrng  21411  cndrngOLD  21412  cnmgpid  21447  gzrngunitlem  21450  gzrngunit  21451  zringnzr  21471  zringunit  21477  cnmsgnsubg  21595  cnmsgngrp  21597  psgninv  21600  mvrf1  22006  psdmvr  22173  pmatcollpw3fi1lem1  22792  dscmet  24585  xrhmeo  24977  clmopfne  25129  itg11  25726  ply1remlem  26204  dgrid  26304  plyrem  26347  facth  26348  fta1lem  26349  vieta1lem1  26352  vieta1lem2  26353  vieta1  26354  qaa  26365  iaa  26367  coseq00topi  26544  logneg2  26657  logtayl2  26704  1cxp  26714  cxpeq0  26720  logb1  26812  logbmpt  26831  ang180lem4  26855  ang180lem5  26856  isosctrlem2  26862  isosctrlem3  26863  angpined  26873  dcubic2  26887  dcubic  26889  dquartlem1  26894  atandmtan  26963  efrlim  27012  efrlimOLD  27013  mumullem2  27223  1sgm2ppw  27244  dchrn0  27294  lgsne0  27379  1lgs  27384  gausslemma2dlem0i  27408  lgseisenlem1  27419  lgseisenlem2  27420  lgsquadlem1  27424  lgsquad2lem2  27429  2lgs  27451  2sqlem7  27468  2sqlem8a  27469  2sqlem8  27470  chebbnd2  27521  chto1lb  27522  pnt2  27657  pnt  27658  qabvle  27669  qabvexp  27670  ostthlem2  27672  ostth3  27682  ostth  27683  axlowdimlem6  28962  axlowdimlem13  28969  axlowdimlem14  28970  axlowdim1  28974  usgrexmpldifpr  29275  pthdadjvtx  29748  upgr4cycl4dv4e  30204  konigsberglem1  30271  frgrreggt1  30412  norm1exi  31269  kbpj  31975  largei  32286  ind1a  32844  indsupp  32852  ccfldextdgrr  33722  constrfin  33787  2sqr3minply  33791  xrge0iif1  33937  cntnevol  34229  ballotlemii  34506  sgn0bi  34550  plymulx0  34562  signswch  34576  signstfvcl  34588  indispconn  35239  poimirlem23  37650  efne0d  42373  tan3rdpi  42386  remulinvcom  42462  sn-0lt1  42493  0dioph  42789  pell1234qrne0  42864  expgrowth  44354  binomcxplemradcnv  44371  xrralrecnnge  45401  iooiinioc  45569  stoweidlem13  46028  wallispi2lem1  46086  dirkertrigeq  46116  fourierdlem30  46152  fourierdlem62  46183  dfodd5  47647  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb1  47991  usgrexmpl2trifr  47996  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  itcoval1  48584  line2ylem  48672  sec0  49279