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

Detailed syntax breakdown of Axiom ax-1ne0
StepHypRef Expression
1 c1 10531 . 2 class 1
2 cc0 10530 . 2 class 0
31, 2wne 2990 1 wff 1 ≠ 0
Colors of variables: wff setvar class
This axiom is referenced by:  elimne0  10624  1re  10634  mul02lem2  10810  addid1  10813  ine0  11068  0lt1  11155  recne0  11304  div1  11322  recdiv  11339  divdiv1  11344  divdiv2  11345  recgt0ii  11539  nnne0  11663  0ne1  11700  neg1ne0  11745  expcl2lem  13441  m1expcl2  13451  expclzlem  13453  1exp  13458  hashrabsn1  13735  relexp1g  14381  geo2sum2  15226  geoihalfsum  15234  fprodntriv  15292  prod0  15293  prod1  15294  fprodn0  15329  fprodn0f  15341  efne0  15446  tan0  15500  m1exp1  15721  divalg  15748  gcd1  15870  rpdvds  15998  m1dvdsndvds  16129  pcpre1  16173  pc1  16186  pcrec  16189  pcid  16203  m1expaddsub  18622  cndrng  20124  cnmgpid  20157  gzrngunitlem  20160  gzrngunit  20161  zringnzr  20179  zringunit  20185  cnmsgnsubg  20270  cnmsgngrp  20272  psgninv  20275  mvrf1  20667  pmatcollpw3fi1lem1  21395  dscmet  23183  xrhmeo  23555  clmopfne  23705  itg11  24299  ply1remlem  24767  dgrid  24865  plyrem  24905  facth  24906  fta1lem  24907  vieta1lem1  24910  vieta1lem2  24911  vieta1  24912  qaa  24923  iaa  24925  coseq00topi  25099  logneg2  25210  logtayl2  25257  1cxp  25267  cxpeq0  25273  logb1  25359  logbmpt  25378  ang180lem4  25402  ang180lem5  25403  isosctrlem2  25409  isosctrlem3  25410  angpined  25420  dcubic2  25434  dcubic  25436  dquartlem1  25441  atandmtan  25510  efrlim  25559  mumullem2  25769  1sgm2ppw  25788  dchrn0  25838  lgsne0  25923  1lgs  25928  gausslemma2dlem0i  25952  lgseisenlem1  25963  lgseisenlem2  25964  lgsquadlem1  25968  lgsquad2lem2  25973  2lgs  25995  2sqlem7  26012  2sqlem8a  26013  2sqlem8  26014  chebbnd2  26065  chto1lb  26066  pnt2  26201  pnt  26202  qabvle  26213  qabvexp  26214  ostthlem2  26216  ostth3  26226  ostth  26227  axlowdimlem6  26745  axlowdimlem13  26752  axlowdimlem14  26753  axlowdim1  26757  usgrexmpldifpr  27052  pthdadjvtx  27523  upgr4cycl4dv4e  27974  konigsberglem1  28041  frgrreggt1  28182  norm1exi  29037  kbpj  29743  largei  30054  ccfldextdgrr  31149  xrge0iif1  31295  ind1a  31392  cntnevol  31601  ballotlemii  31875  sgn0bi  31919  plymulx0  31931  signswch  31945  signstfvcl  31957  indispconn  32595  poimirlem23  35079  remulinvcom  39562  sn-0lt1  39580  0dioph  39712  pell1234qrne0  39787  expgrowth  41032  binomcxplemradcnv  41049  xrralrecnnge  42019  iooiinioc  42186  stoweidlem13  42648  wallispi2lem1  42706  dirkertrigeq  42736  fourierdlem30  42772  fourierdlem62  42803  dfodd5  44171  itcoval1  45070  line2ylem  45158  sec0  45279
  Copyright terms: Public domain W3C validator