Theorem 1m1e0 12283

Description: One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1m1e0	⊢ (1 − 1) = 0

Proof of Theorem 1m1e0

Step	Hyp	Ref	Expression
1		ax-1cn 11167	. 2 ⊢ 1 ∈ ℂ
2	1	subidi 11530	1 ⊢ (1 − 1) = 0

Syntax hints:   = wceq 1541  (class class class)co 7408  0cc0 11109  1c1 11110   − cmin 11443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-ltxr 11252  df-sub 11445

This theorem is referenced by:  nnm1nn0  12512  xov1plusxeqvd  13474  fseq1p1m1  13574  elfzp1b  13577  elfzm1b  13578  elfznelfzo  13736  fldiv4lem1div2  13801  fzennn  13932  faclbnd4lem4  14255  lsw1  14516  ccat2s1p2  14579  revs1  14714  arisum  15805  pwdif  15813  geo2sum  15818  bpoly1  15994  nn0o  16325  exprmfct  16640  phiprmpw  16708  phiprm  16709  odzdvds  16727  prmpwdvds  16836  prmreclem4  16851  vdwapun  16906  sylow1lem1  19465  efgs1b  19603  efgsfo  19606  efgredlema  19607  efgredeu  19619  imasdsf1olem  23878  htpycom  24491  htpycc  24495  reparphti  24512  pcoval2  24531  pcocn  24532  pcohtpylem  24534  pcopt  24537  pcorevcl  24540  pcorevlem  24541  pi1xfrcnv  24572  dvexp  25469  dvlipcn  25510  dvply1  25796  vieta1  25824  pserdvlem2  25939  abelthlem2  25943  coseq1  26033  advlogexp  26162  logtayl  26167  cxpaddlelem  26256  isosctrlem2  26321  asin1  26396  leibpilem2  26443  log2ublem3  26450  scvxcvx  26487  1sgmprm  26699  dchrfi  26755  lgslem4  26800  lgsne0  26835  lgsquad2lem2  26885  2lgsoddprmlem3a  26910  rpvmasumlem  26987  selberg2lem  27050  logdivbnd  27056  pntrsumo1  27065  pntrlog2bndlem4  27080  pntrlog2bndlem5  27081  pntpbnd2  27087  ostth2lem2  27134  axpaschlem  28195  elntg2  28240  wwlksn0s  29112  clwwlkn1  29291  hst1h  31475  st0  31497  archirngz  32330  drngdimgt0  32698  lmatfval  32789  lmat22e11  32793  fib2  33396  ballotlem4  33492  ballotlemi1  33496  ballotlemii  33497  ballotlemic  33500  ballotlem1c  33501  ballotlemfrceq  33522  signsvtn0  33576  signstfveq0a  33582  subfacp1lem6  34171  cvxpconn  34228  cvxsconn  34229  cvmliftlem10  34280  cvmliftlem13  34282  bcprod  34703  gg-reparphti  35167  poimirlem3  36486  poimirlem4  36487  poimirlem13  36496  poimirlem19  36502  lcmfunnnd  40872  lcm1un  40873  lcmineqlem10  40898  lcmineqlem12  40900  lcmineqlem18  40906  metakunt30  41009  mapfzcons  41444  irrapxlem3  41552  2nn0ind  41674  jm2.18  41717  jm2.23  41725  dvnmul  44649  stoweidlem1  44707  stoweidlem11  44717  stoweidlem26  44732  stoweidlem34  44740  stoweidlem45  44751  wallispilem3  44773  wallispi  44776  stirlinglem5  44784  sqwvfourb  44935  upwordsing  45588  proththdlem  46271  341fppr2  46392  nnsgrpnmnd  46578  pzriprng1ALT  46810  blen1b  47264  nn0sumshdiglem1  47297