Axiom ax-1ne0 11019

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

This axiom is referenced by:  elimne0  11044  1re  11054  mul02lem2  11231  addid1  11234  ine0  11489  0lt1  11576  recne0  11725  div1  11743  recdiv  11760  divdiv1  11765  divdiv2  11766  recgt0ii  11960  nnne0  12086  0ne1  12123  neg1ne0  12168  expcl2lem  13873  m1expcl2  13883  expclzlem  13885  1exp  13891  hashrabsn1  14167  relexp1g  14813  geo2sum2  15662  geoihalfsum  15670  fprodntriv  15728  prod0  15729  prod1  15730  fprodn0  15765  fprodn0f  15777  efne0  15882  tan0  15936  m1exp1  16161  divalg  16188  gcd1  16311  rpdvds  16439  m1dvdsndvds  16573  pcpre1  16617  pc1  16630  pcrec  16633  pcid  16648  m1expaddsub  19179  cndrng  20707  cnmgpid  20740  gzrngunitlem  20743  gzrngunit  20744  zringnzr  20762  zringunit  20768  cnmsgnsubg  20862  cnmsgngrp  20864  psgninv  20867  mvrf1  21274  pmatcollpw3fi1lem1  22015  dscmet  23808  xrhmeo  24189  clmopfne  24339  itg11  24935  ply1remlem  25407  dgrid  25505  plyrem  25545  facth  25546  fta1lem  25547  vieta1lem1  25550  vieta1lem2  25551  vieta1  25552  qaa  25563  iaa  25565  coseq00topi  25739  logneg2  25850  logtayl2  25897  1cxp  25907  cxpeq0  25913  logb1  25999  logbmpt  26018  ang180lem4  26042  ang180lem5  26043  isosctrlem2  26049  isosctrlem3  26050  angpined  26060  dcubic2  26074  dcubic  26076  dquartlem1  26081  atandmtan  26150  efrlim  26199  mumullem2  26409  1sgm2ppw  26428  dchrn0  26478  lgsne0  26563  1lgs  26568  gausslemma2dlem0i  26592  lgseisenlem1  26603  lgseisenlem2  26604  lgsquadlem1  26608  lgsquad2lem2  26613  2lgs  26635  2sqlem7  26652  2sqlem8a  26653  2sqlem8  26654  chebbnd2  26705  chto1lb  26706  pnt2  26841  pnt  26842  qabvle  26853  qabvexp  26854  ostthlem2  26856  ostth3  26866  ostth  26867  axlowdimlem6  27448  axlowdimlem13  27455  axlowdimlem14  27456  axlowdim1  27460  usgrexmpldifpr  27758  pthdadjvtx  28230  upgr4cycl4dv4e  28681  konigsberglem1  28748  frgrreggt1  28889  norm1exi  29744  kbpj  30450  largei  30761  ccfldextdgrr  31878  xrge0iif1  32024  ind1a  32123  cntnevol  32332  ballotlemii  32606  sgn0bi  32650  plymulx0  32662  signswch  32676  signstfvcl  32688  indispconn  33331  poimirlem23  35877  remulinvcom  40635  sn-0lt1  40653  0dioph  40821  pell1234qrne0  40896  expgrowth  42192  binomcxplemradcnv  42209  xrralrecnnge  43184  iooiinioc  43349  stoweidlem13  43809  wallispi2lem1  43867  dirkertrigeq  43897  fourierdlem30  43933  fourierdlem62  43964  dfodd5  45382  itcoval1  46279  line2ylem  46367  sec0  46732