Theorem 1m1e0 11697

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

Syntax hints:   = wceq 1538  (class class class)co 7135  0cc0 10526  1c1 10527   − cmin 10859

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861

This theorem is referenced by:  nnm1nn0  11926  xov1plusxeqvd  12876  fseq1p1m1  12976  elfzp1b  12979  elfzm1b  12980  elfznelfzo  13137  fldiv4lem1div2  13202  fzennn  13331  faclbnd4lem4  13652  lsw1  13910  ccat2s1p2  13977  ccat2s1p2OLD  13979  revs1  14118  arisum  15207  pwdif  15215  pwm1geoserOLD  15217  geo2sum  15221  bpoly1  15397  nn0o  15724  exprmfct  16038  phiprmpw  16103  phiprm  16104  odzdvds  16122  prmpwdvds  16230  prmreclem4  16245  vdwapun  16300  sylow1lem1  18715  efgs1b  18854  efgsfo  18857  efgredlema  18858  efgredeu  18870  imasdsf1olem  22980  htpycom  23581  htpycc  23585  reparphti  23602  pcoval2  23621  pcocn  23622  pcohtpylem  23624  pcopt  23627  pcorevcl  23630  pcorevlem  23631  pi1xfrcnv  23662  dvexp  24556  dvlipcn  24597  dvply1  24880  vieta1  24908  pserdvlem2  25023  abelthlem2  25027  coseq1  25117  advlogexp  25246  logtayl  25251  cxpaddlelem  25340  isosctrlem2  25405  asin1  25480  leibpilem2  25527  log2ublem3  25534  scvxcvx  25571  1sgmprm  25783  dchrfi  25839  lgslem4  25884  lgsne0  25919  lgsquad2lem2  25969  2lgsoddprmlem3a  25994  rpvmasumlem  26071  selberg2lem  26134  logdivbnd  26140  pntrsumo1  26149  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntpbnd2  26171  ostth2lem2  26218  axpaschlem  26734  elntg2  26779  wwlksn0s  27647  clwwlkn1  27826  hst1h  30010  st0  30032  archirngz  30868  drngdimgt0  31104  lmatfval  31167  lmat22e11  31171  fib2  31770  ballotlem4  31866  ballotlemi1  31870  ballotlemii  31871  ballotlemic  31874  ballotlem1c  31875  ballotlemfrceq  31896  signsvtn0  31950  signstfveq0a  31956  subfacp1lem6  32545  cvxpconn  32602  cvxsconn  32603  cvmliftlem10  32654  cvmliftlem13  32656  bcprod  33083  poimirlem3  35060  poimirlem4  35061  poimirlem13  35070  poimirlem19  35076  lcmfunnnd  39300  lcm1un  39301  lcmineqlem10  39326  lcmineqlem12  39328  lcmineqlem18  39334  metakunt30  39379  mapfzcons  39657  irrapxlem3  39765  2nn0ind  39886  jm2.18  39929  jm2.23  39937  dvnmul  42585  stoweidlem1  42643  stoweidlem11  42653  stoweidlem26  42668  stoweidlem34  42676  stoweidlem45  42687  wallispilem3  42709  wallispi  42712  stirlinglem5  42720  sqwvfourb  42871  proththdlem  44131  341fppr2  44252  nnsgrpnmnd  44438  blen1b  45002  nn0sumshdiglem1  45035