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 10595
Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 10571. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1ne0 1 ≠ 0

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 10527 . 2 class 1
2 cc0 10526 . 2 class 0
31, 2wne 3016 1 wff 1 ≠ 0
Colors of variables: wff setvar class
This axiom is referenced by:  elimne0  10620  1re  10630  mul02lem2  10806  addid1  10809  ine0  11064  0lt1  11151  recne0  11300  div1  11318  recdiv  11335  divdiv1  11340  divdiv2  11341  recgt0ii  11535  nnne0  11660  0ne1  11697  neg1ne0  11742  expcl2lem  13431  m1expcl2  13441  expclzlem  13443  1exp  13448  hashrabsn1  13725  relexp1g  14375  geo2sum2  15220  geoihalfsum  15228  fprodntriv  15286  prod0  15287  prod1  15288  fprodn0  15323  fprodn0f  15335  efne0  15440  tan0  15494  m1exp1  15717  divalg  15744  gcd1  15866  rpdvds  15994  m1dvdsndvds  16125  pcpre1  16169  pc1  16182  pcrec  16185  pcid  16199  m1expaddsub  18557  mvrf1  20135  cndrng  20504  cnmgpid  20537  gzrngunitlem  20540  gzrngunit  20541  zringnzr  20559  zringunit  20565  cnmsgnsubg  20651  cnmsgngrp  20653  psgninv  20656  pmatcollpw3fi1lem1  21324  dscmet  23111  xrhmeo  23479  clmopfne  23629  itg11  24221  ply1remlem  24685  dgrid  24783  plyrem  24823  facth  24824  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  vieta1  24830  qaa  24841  iaa  24843  coseq00topi  25017  logneg2  25125  logtayl2  25172  1cxp  25182  cxpeq0  25188  logb1  25274  logbmpt  25293  ang180lem4  25317  ang180lem5  25318  isosctrlem2  25324  isosctrlem3  25325  angpined  25335  dcubic2  25349  dcubic  25351  dquartlem1  25356  atandmtan  25425  efrlim  25475  mumullem2  25685  1sgm2ppw  25704  dchrn0  25754  lgsne0  25839  1lgs  25844  gausslemma2dlem0i  25868  lgseisenlem1  25879  lgseisenlem2  25880  lgsquadlem1  25884  lgsquad2lem2  25889  2lgs  25911  2sqlem7  25928  2sqlem8a  25929  2sqlem8  25930  chebbnd2  25981  chto1lb  25982  pnt2  26117  pnt  26118  qabvle  26129  qabvexp  26130  ostthlem2  26132  ostth3  26142  ostth  26143  axlowdimlem6  26661  axlowdimlem13  26668  axlowdimlem14  26669  axlowdim1  26673  usgrexmpldifpr  26968  pthdadjvtx  27439  upgr4cycl4dv4e  27892  konigsberglem1  27959  frgrreggt1  28100  norm1exi  28955  kbpj  29661  largei  29972  ccfldextdgrr  30957  xrge0iif1  31081  ind1a  31178  cntnevol  31387  ballotlemii  31661  sgn0bi  31705  plymulx0  31717  signswch  31731  signstfvcl  31743  indispconn  32379  poimirlem23  34797  sn-0lt1  39126  remulinvcom  39128  0dioph  39255  pell1234qrne0  39330  expgrowth  40547  binomcxplemradcnv  40564  xrralrecnnge  41542  iooiinioc  41712  stoweidlem13  42179  wallispi2lem1  42237  dirkertrigeq  42267  fourierdlem30  42303  fourierdlem62  42334  dfodd5  43672  line2ylem  44636  sec0  44757
  Copyright terms: Public domain W3C validator