Axiom ax-1ne0 11175

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

This axiom is used by:  elimne0  11202  1re  11214  mul02lem2  11393  addrid  11396  ine0  11655  0lt1  11742  recne0  11891  div1  11910  recdiv  11927  divdiv1  11932  divdiv2  11933  recgt0ii  12127  neg1ne0  12211  ind1a  12235  nnne0  12276  0ne1  12318  fvf1tp  13829  expcl2lem  14116  expclzlem  14126  m1expcl2  14128  1exp  14134  hashrabsn1  14417  tpf1ofv1  14541  relexp1g  15070  sgn0bi  15147  geo2sum2  15935  geoihalfsum  15943  fprodntriv  16003  prod0  16004  prod1  16005  fprodn0  16040  fprodn0f  16052  efne0d  16157  efne0OLD  16159  tan0  16213  m1exp1  16440  divalg  16467  gcd1  16592  rpdvds  16724  m1dvdsndvds  16864  pcpre1  16908  pc1  16921  pcrec  16924  pcid  16939  ex-chn2  18700  m1expaddsub  19574  cndrng  21562  cnmgpid  21590  gzrngunitlem  21593  gzrngunit  21594  zringnzr  21621  zringunit  21627  cnmsgnsubg  21738  cnmsgngrp  21740  psgninv  21743  mvrf1  22146  psdmvr  22343  pmatcollpw3fi1lem1  22954  dscmet  24740  xrhmeo  25116  clmopfne  25266  itg11  25861  ply1remlem  26333  dgrid  26432  plyn0mulidp  26453  plyrem  26477  facth  26478  fta1lem  26479  vieta1lem1  26482  vieta1lem2  26483  vieta1  26484  qaa  26495  iaa  26499  coseq00topi  26678  logneg2  26791  logtayl2  26838  1cxp  26848  cxpeq0  26854  logb1  26945  logbmpt  26964  ang180lem4  26988  ang180lem5  26989  isosctrlem2  26995  isosctrlem3  26996  angpined  27006  dcubic2  27020  dcubic  27022  dquartlem1  27027  atandmtan  27096  efrlim  27145  mumullem2  27355  1sgm2ppw  27375  dchrn0  27425  lgsne0  27510  1lgs  27515  gausslemma2dlem0i  27539  lgseisenlem1  27550  lgseisenlem2  27551  lgsquadlem1  27555  lgsquad2lem2  27560  2lgs  27582  2sqlem7  27599  2sqlem8a  27600  2sqlem8  27601  chebbnd2  27652  chto1lb  27653  pnt2  27788  pnt  27789  qabvle  27800  qabvexp  27801  ostthlem2  27803  ostth3  27813  ostth  27814  axlowdimlem6  29308  axlowdimlem13  29315  axlowdimlem14  29316  axlowdim1  29320  usgrexmpldifpr  29619  pthdadjvtx  30088  upgr4cycl4dv4e  30547  konigsberglem1  30614  frgrreggt1  30755  norm1exi  31613  kbpj  32319  largei  32630  indsupp  33198  esplyfvaln  33973  ccfldextdgrr  34071  constrfin  34145  2sqr3minply  34179  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  cos9thpiminplylem3  34183  cos9thpinconstrlem1  34188  xrge0iif1  34337  cntnevol  34627  ballotlemii  34903  signswch  34957  signstfvcl  34969  indispconn  35734  poimirlem23  38322  25or6to4  43001  tan3rdpi  43141  remulinvcom  43222  sn-rediv1d  43241  rerecne0d  43245  sn-0lt1  43277  0dioph  43537  pell1234qrne0  43608  expgrowth  45073  binomcxplemradcnv  45090  xrralrecnnge  46133  iooiinioc  46300  stoweidlem13  46755  wallispi2lem1  46813  dirkertrigeq  46843  fourierdlem30  46879  fourierdlem62  46910  cjnpoly  47654  dfodd5  48453  usgrexmpl1lem  48814  usgrexmpl2lem  48819  usgrexmpl2nb1  48825  usgrexmpl2trifr  48830  gpgvtxedg0  48856  gpgvtxedg1  48857  gpgedgiov  48858  gpgedg2iv  48860  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  gpg3nbgrvtx0  48869  gpg3nbgrvtx0ALT  48870  gpg3nbgrvtx1  48871  gpgprismgr4cycllem2  48889  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  pgnbgreunbgrlem5lem1  48913  pgnbgreunbgrlem5lem2  48914  pgnbgreunbgrlem5lem3  48915  gpg5edgnedg  48923  itcoval1  49471  line2ylem  49559  sec0  50566