Theorem 1m1e0 11760

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

Syntax hints:   = wceq 1539  (class class class)co 7157  0cc0 10589  1c1 10590   − cmin 10922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-ltxr 10732  df-sub 10924

This theorem is referenced by:  nnm1nn0  11989  xov1plusxeqvd  12944  fseq1p1m1  13044  elfzp1b  13047  elfzm1b  13048  elfznelfzo  13205  fldiv4lem1div2  13270  fzennn  13399  faclbnd4lem4  13720  lsw1  13980  ccat2s1p2  14047  ccat2s1p2OLD  14049  revs1  14188  arisum  15277  pwdif  15285  pwm1geoserOLD  15287  geo2sum  15291  bpoly1  15467  nn0o  15798  exprmfct  16115  phiprmpw  16183  phiprm  16184  odzdvds  16202  prmpwdvds  16310  prmreclem4  16325  vdwapun  16380  sylow1lem1  18805  efgs1b  18944  efgsfo  18947  efgredlema  18948  efgredeu  18960  imasdsf1olem  23090  htpycom  23692  htpycc  23696  reparphti  23713  pcoval2  23732  pcocn  23733  pcohtpylem  23735  pcopt  23738  pcorevcl  23741  pcorevlem  23742  pi1xfrcnv  23773  dvexp  24667  dvlipcn  24708  dvply1  24994  vieta1  25022  pserdvlem2  25137  abelthlem2  25141  coseq1  25231  advlogexp  25360  logtayl  25365  cxpaddlelem  25454  isosctrlem2  25519  asin1  25594  leibpilem2  25641  log2ublem3  25648  scvxcvx  25685  1sgmprm  25897  dchrfi  25953  lgslem4  25998  lgsne0  26033  lgsquad2lem2  26083  2lgsoddprmlem3a  26108  rpvmasumlem  26185  selberg2lem  26248  logdivbnd  26254  pntrsumo1  26263  pntrlog2bndlem4  26278  pntrlog2bndlem5  26279  pntpbnd2  26285  ostth2lem2  26332  axpaschlem  26848  elntg2  26893  wwlksn0s  27761  clwwlkn1  27940  hst1h  30124  st0  30146  archirngz  30983  drngdimgt0  31236  lmatfval  31299  lmat22e11  31303  fib2  31902  ballotlem4  31998  ballotlemi1  32002  ballotlemii  32003  ballotlemic  32006  ballotlem1c  32007  ballotlemfrceq  32028  signsvtn0  32082  signstfveq0a  32088  subfacp1lem6  32677  cvxpconn  32734  cvxsconn  32735  cvmliftlem10  32786  cvmliftlem13  32788  bcprod  33233  poimirlem3  35376  poimirlem4  35377  poimirlem13  35386  poimirlem19  35392  lcmfunnnd  39615  lcm1un  39616  lcmineqlem10  39641  lcmineqlem12  39643  lcmineqlem18  39649  metakunt30  39712  mapfzcons  40076  irrapxlem3  40184  2nn0ind  40305  jm2.18  40348  jm2.23  40356  dvnmul  42997  stoweidlem1  43055  stoweidlem11  43065  stoweidlem26  43080  stoweidlem34  43088  stoweidlem45  43099  wallispilem3  43121  wallispi  43124  stirlinglem5  43132  sqwvfourb  43283  proththdlem  44558  341fppr2  44679  nnsgrpnmnd  44865  blen1b  45427  nn0sumshdiglem1  45460