Axiom ax-1ne0 11181

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

This axiom is referenced by:  elimne0  11208  1re  11218  mul02lem2  11395  addrid  11398  ine0  11653  0lt1  11740  recne0  11889  div1  11907  recdiv  11924  divdiv1  11929  divdiv2  11930  recgt0ii  12124  nnne0  12250  0ne1  12287  neg1ne0  12332  expcl2lem  14043  expclzlem  14053  m1expcl2  14055  1exp  14061  hashrabsn1  14338  relexp1g  14977  geo2sum2  15824  geoihalfsum  15832  fprodntriv  15890  prod0  15891  prod1  15892  fprodn0  15927  fprodn0f  15939  efne0  16044  tan0  16098  m1exp1  16323  divalg  16350  gcd1  16473  rpdvds  16601  m1dvdsndvds  16735  pcpre1  16779  pc1  16792  pcrec  16795  pcid  16810  m1expaddsub  19407  cndrng  21174  cnmgpid  21207  gzrngunitlem  21210  gzrngunit  21211  zringnzr  21231  zringunit  21237  cnmsgnsubg  21349  cnmsgngrp  21351  psgninv  21354  mvrf1  21764  pmatcollpw3fi1lem1  22508  dscmet  24301  xrhmeo  24691  clmopfne  24843  itg11  25440  ply1remlem  25915  dgrid  26014  plyrem  26054  facth  26055  fta1lem  26056  vieta1lem1  26059  vieta1lem2  26060  vieta1  26061  qaa  26072  iaa  26074  coseq00topi  26248  logneg2  26359  logtayl2  26406  1cxp  26416  cxpeq0  26422  logb1  26510  logbmpt  26529  ang180lem4  26553  ang180lem5  26554  isosctrlem2  26560  isosctrlem3  26561  angpined  26571  dcubic2  26585  dcubic  26587  dquartlem1  26592  atandmtan  26661  efrlim  26710  mumullem2  26920  1sgm2ppw  26939  dchrn0  26989  lgsne0  27074  1lgs  27079  gausslemma2dlem0i  27103  lgseisenlem1  27114  lgseisenlem2  27115  lgsquadlem1  27119  lgsquad2lem2  27124  2lgs  27146  2sqlem7  27163  2sqlem8a  27164  2sqlem8  27165  chebbnd2  27216  chto1lb  27217  pnt2  27352  pnt  27353  qabvle  27364  qabvexp  27365  ostthlem2  27367  ostth3  27377  ostth  27378  axlowdimlem6  28472  axlowdimlem13  28479  axlowdimlem14  28480  axlowdim1  28484  usgrexmpldifpr  28782  pthdadjvtx  29254  upgr4cycl4dv4e  29705  konigsberglem1  29772  frgrreggt1  29913  norm1exi  30770  kbpj  31476  largei  31787  ccfldextdgrr  33035  xrge0iif1  33216  ind1a  33315  cntnevol  33524  ballotlemii  33800  sgn0bi  33844  plymulx0  33856  signswch  33870  signstfvcl  33882  indispconn  34523  poimirlem23  36814  remulinvcom  41607  sn-0lt1  41637  0dioph  41818  pell1234qrne0  41893  expgrowth  43396  binomcxplemradcnv  43413  xrralrecnnge  44398  iooiinioc  44567  stoweidlem13  45027  wallispi2lem1  45085  dirkertrigeq  45115  fourierdlem30  45151  fourierdlem62  45182  dfodd5  46626  itcoval1  47436  line2ylem  47524  sec0  47892