MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1ne0 Structured version   Visualization version   GIF version

Axiom ax-1ne0 10293
Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 10269. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1ne0 1 ≠ 0

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 10225 . 2 class 1
2 cc0 10224 . 2 class 0
31, 2wne 2985 1 wff 1 ≠ 0
Colors of variables: wff setvar class
This axiom is referenced by:  elimne0  10318  1re  10328  mul02lem2  10501  addid1  10504  ine0  10753  0lt1  10838  recne0  10986  div1  11004  recdiv  11019  divdiv1  11024  divdiv2  11025  recgt0ii  11217  0ne1  11375  neg1ne0  11411  expcl2lem  13098  m1expcl2  13108  expclzlem  13110  1exp  13115  hashrabsn1  13384  relexp1g  13992  geo2sum2  14830  geoihalfsum  14838  fprodntriv  14896  prod0  14897  prod1  14898  fprodn0  14933  efne0  15050  tan0  15104  m1exp1  15316  divalg  15349  gcd1  15471  rpdvds  15595  m1dvdsndvds  15723  pcpre1  15767  pc1  15780  pcrec  15783  pcid  15797  m1expaddsub  18122  mvrf1  19637  cndrng  19986  cnmgpid  20019  gzrngunitlem  20022  gzrngunit  20023  zringnzr  20041  zringunit  20047  cnmsgnsubg  20133  cnmsgngrp  20135  psgninv  20138  pmatcollpw3fi1lem1  20808  dscmet  22594  xrhmeo  22962  clmopfne  23112  itg11  23678  ply1remlem  24142  dgrid  24240  plyrem  24280  facth  24281  fta1lem  24282  vieta1lem1  24285  vieta1lem2  24286  vieta1  24287  qaa  24298  iaa  24300  coseq00topi  24475  logneg2  24581  logtayl2  24628  1cxp  24638  cxpeq0  24644  logb1  24727  logbmpt  24746  ang180lem4  24762  ang180lem5  24763  isosctrlem2  24769  isosctrlem3  24770  angpined  24777  dcubic2  24791  dcubic  24793  dquartlem1  24798  atandmtan  24867  efrlim  24916  mumullem2  25126  1sgm2ppw  25145  dchrn0  25195  lgsne0  25280  1lgs  25285  gausslemma2dlem0i  25309  lgseisenlem1  25320  lgseisenlem2  25321  lgsquadlem1  25325  lgsquad2lem2  25330  2lgs  25352  2sqlem7  25369  2sqlem8a  25370  2sqlem8  25371  chebbnd2  25386  chto1lb  25387  pnt2  25522  pnt  25523  qabvle  25534  qabvexp  25535  ostthlem2  25537  ostth3  25547  ostth  25548  axlowdimlem6  26047  axlowdimlem13  26054  axlowdimlem14  26055  axlowdim1  26059  usgrexmpldifpr  26372  pthdadjvtx  26860  upgr4cycl4dv4e  27364  konigsberglem1  27431  frgrreggt1  27587  norm1exi  28441  kbpj  29149  largei  29460  xrge0iif1  30315  ind1a  30412  cntnevol  30622  ballotlemii  30896  sgn0bi  30940  plymulx0  30955  signswch  30969  signstfvcl  30981  indispconn  31544  poimirlem23  33747  0dioph  37845  pell1234qrne0  37920  expgrowth  39035  binomcxplemradcnv  39052  xrralrecnnge  40093  iooiinioc  40264  stoweidlem13  40710  wallispi2lem1  40768  dirkertrigeq  40798  fourierdlem30  40834  fourierdlem62  40865  dfodd5  42148  sec0  43073
  Copyright terms: Public domain W3C validator