Theorem 1m1e0 12284

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 11125	. 2 ⊢ 1 ∈ ℂ
2	1	subidi 11496	1 ⊢ (1 − 1) = 0

Syntax hints:   = wceq 1559  (class class class)co 7391  0cc0 11067  1c1 11068   − cmin 11408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-ltxr 11215  df-sub 11410

This theorem is referenced by:  nnm1nn0  12516  xov1plusxeqvd  13496  fseq1p1m1  13597  elfzp1b  13600  elfzm1b  13601  elfznelfzo  13773  fldiv4lem1div2  13841  fzennn  13975  faclbnd4lem4  14303  lsw1  14574  ccat2s1p2  14638  revs1  14772  arisum  15881  pwdif  15889  geo2sum  15894  bpoly1  16072  nn0o  16408  exprmfct  16730  phiprmpw  16802  phiprm  16803  odzdvds  16822  prmpwdvds  16931  prmreclem4  16946  vdwapun  17001  chnub  18645  ex-chn1  18660  ex-chn2  18661  sylow1lem1  19629  efgs1b  19767  efgsfo  19770  efgredlema  19771  efgredeu  19783  pzriprng1ALT  21536  psdpw  22223  imasdsf1olem  24421  htpycom  25026  htpycc  25030  reparphti  25047  pcoval2  25066  pcocn  25067  pcohtpylem  25069  pcopt  25072  pcorevcl  25075  pcorevlem  25076  pi1xfrcnv  25107  dvexp  26003  dvlipcn  26044  dvply1  26336  vieta1  26364  pserdvlem2  26479  abelthlem2  26483  coseq1  26578  advlogexp  26708  logtayl  26713  cxpaddlelem  26804  isosctrlem2  26872  asin1  26947  leibpilem2  26994  log2ublem3  27001  scvxcvx  27038  1sgmprm  27251  dchrfi  27307  lgslem4  27352  lgsne0  27387  lgsquad2lem2  27437  2lgsoddprmlem3a  27462  rpvmasumlem  27539  selberg2lem  27602  logdivbnd  27608  pntrsumo1  27617  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntpbnd2  27639  ostth2lem2  27686  axpaschlem  29098  elntg2  29143  wwlksn0s  30018  clwwlkn1  30200  hst1h  32387  st0  32409  archirngz  33330  drngdimgt0  33876  cos9thpiminplylem3  34042  lmatfval  34072  lmat22e11  34076  fib2  34660  ballotlem4  34757  ballotlemi1  34761  ballotlemii  34762  ballotlemic  34765  ballotlem1c  34766  ballotlemfrceq  34787  signsvtn0  34825  signstfveq0a  34831  subfacp1lem6  35496  cvxpconn  35553  cvxsconn  35554  cvmliftlem10  35605  cvmliftlem13  35607  bcprod  36049  poimirlem3  38083  poimirlem4  38084  poimirlem13  38093  poimirlem19  38099  lcmfunnnd  42590  lcm1un  42591  lcmineqlem10  42616  lcmineqlem12  42618  lcmineqlem18  42624  mapfzcons  43258  irrapxlem3  43362  2nn0ind  43483  jm2.18  43526  jm2.23  43534  dvnmul  46478  stoweidlem1  46536  stoweidlem11  46546  stoweidlem26  46561  stoweidlem34  46569  stoweidlem45  46580  wallispilem3  46602  wallispi  46605  stirlinglem5  46613  sqwvfourb  46764  ceilhalf1  47893  proththdlem  48183  341fppr2  48317  nnsgrpnmnd  48761  blen1b  49171  nn0sumshdiglem1  49204