Axiom ax-1ne0 11129

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

This axiom is referenced by:  elimne0  11154  1re  11164  mul02lem2  11341  addrid  11344  ine0  11599  0lt1  11686  recne0  11835  div1  11853  recdiv  11870  divdiv1  11875  divdiv2  11876  recgt0ii  12070  nnne0  12196  0ne1  12233  neg1ne0  12278  expcl2lem  13989  expclzlem  13999  m1expcl2  14001  1exp  14007  hashrabsn1  14284  relexp1g  14923  geo2sum2  15770  geoihalfsum  15778  fprodntriv  15836  prod0  15837  prod1  15838  fprodn0  15873  fprodn0f  15885  efne0  15990  tan0  16044  m1exp1  16269  divalg  16296  gcd1  16419  rpdvds  16547  m1dvdsndvds  16681  pcpre1  16725  pc1  16738  pcrec  16741  pcid  16756  m1expaddsub  19294  cndrng  20863  cnmgpid  20896  gzrngunitlem  20899  gzrngunit  20900  zringnzr  20918  zringunit  20924  cnmsgnsubg  21018  cnmsgngrp  21020  psgninv  21023  mvrf1  21431  pmatcollpw3fi1lem1  22172  dscmet  23965  xrhmeo  24346  clmopfne  24496  itg11  25092  ply1remlem  25564  dgrid  25662  plyrem  25702  facth  25703  fta1lem  25704  vieta1lem1  25707  vieta1lem2  25708  vieta1  25709  qaa  25720  iaa  25722  coseq00topi  25896  logneg2  26007  logtayl2  26054  1cxp  26064  cxpeq0  26070  logb1  26156  logbmpt  26175  ang180lem4  26199  ang180lem5  26200  isosctrlem2  26206  isosctrlem3  26207  angpined  26217  dcubic2  26231  dcubic  26233  dquartlem1  26238  atandmtan  26307  efrlim  26356  mumullem2  26566  1sgm2ppw  26585  dchrn0  26635  lgsne0  26720  1lgs  26725  gausslemma2dlem0i  26749  lgseisenlem1  26760  lgseisenlem2  26761  lgsquadlem1  26765  lgsquad2lem2  26770  2lgs  26792  2sqlem7  26809  2sqlem8a  26810  2sqlem8  26811  chebbnd2  26862  chto1lb  26863  pnt2  26998  pnt  26999  qabvle  27010  qabvexp  27011  ostthlem2  27013  ostth3  27023  ostth  27024  axlowdimlem6  27959  axlowdimlem13  27966  axlowdimlem14  27967  axlowdim1  27971  usgrexmpldifpr  28269  pthdadjvtx  28741  upgr4cycl4dv4e  29192  konigsberglem1  29259  frgrreggt1  29400  norm1exi  30255  kbpj  30961  largei  31272  ccfldextdgrr  32443  xrge0iif1  32608  ind1a  32707  cntnevol  32916  ballotlemii  33192  sgn0bi  33236  plymulx0  33248  signswch  33262  signstfvcl  33274  indispconn  33915  poimirlem23  36174  remulinvcom  40959  sn-0lt1  40989  0dioph  41159  pell1234qrne0  41234  expgrowth  42737  binomcxplemradcnv  42754  xrralrecnnge  43745  iooiinioc  43914  stoweidlem13  44374  wallispi2lem1  44432  dirkertrigeq  44462  fourierdlem30  44498  fourierdlem62  44529  dfodd5  45972  itcoval1  46869  line2ylem  46957  sec0  47325