Theorem 1m1e0 11708

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

Syntax hints:   = wceq 1533  (class class class)co 7155  0cc0 10536  1c1 10537   − cmin 10869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-ltxr 10679  df-sub 10871

This theorem is referenced by:  nnm1nn0  11937  xov1plusxeqvd  12883  fseq1p1m1  12980  elfzp1b  12983  elfzm1b  12984  elfznelfzo  13141  fldiv4lem1div2  13206  fzennn  13335  faclbnd4lem4  13655  lsw1  13918  ccat2s1p2  13985  ccat2s1p2OLD  13987  revs1  14126  arisum  15214  pwdif  15222  pwm1geoserOLD  15224  geo2sum  15228  bpoly1  15404  nn0o  15733  exprmfct  16047  phiprmpw  16112  phiprm  16113  odzdvds  16131  prmpwdvds  16239  prmreclem4  16254  vdwapun  16309  sylow1lem1  18722  efgs1b  18861  efgsfo  18864  efgredlema  18865  efgredeu  18877  imasdsf1olem  22982  htpycom  23579  htpycc  23583  reparphti  23600  pcoval2  23619  pcocn  23620  pcohtpylem  23622  pcopt  23625  pcorevcl  23628  pcorevlem  23629  pi1xfrcnv  23660  dvexp  24549  dvlipcn  24590  dvply1  24872  vieta1  24900  pserdvlem2  25015  abelthlem2  25019  coseq1  25109  advlogexp  25237  logtayl  25242  cxpaddlelem  25331  isosctrlem2  25396  asin1  25471  leibpilem2  25518  log2ublem3  25525  scvxcvx  25562  1sgmprm  25774  dchrfi  25830  lgslem4  25875  lgsne0  25910  lgsquad2lem2  25960  2lgsoddprmlem3a  25985  rpvmasumlem  26062  selberg2lem  26125  logdivbnd  26131  pntrsumo1  26140  pntrlog2bndlem4  26155  pntrlog2bndlem5  26156  pntpbnd2  26162  ostth2lem2  26209  axpaschlem  26725  elntg2  26770  wwlksn0s  27638  clwwlkn1  27818  hst1h  30003  st0  30025  archirngz  30818  drngdimgt0  31016  lmatfval  31079  lmat22e11  31083  fib2  31660  ballotlem4  31756  ballotlemi1  31760  ballotlemii  31761  ballotlemic  31764  ballotlem1c  31765  ballotlemfrceq  31786  signsvtn0  31840  signstfveq0a  31846  subfacp1lem6  32432  cvxpconn  32489  cvxsconn  32490  cvmliftlem10  32541  cvmliftlem13  32543  bcprod  32970  poimirlem3  34894  poimirlem4  34895  poimirlem13  34904  poimirlem19  34910  mapfzcons  39311  irrapxlem3  39419  2nn0ind  39540  jm2.18  39583  jm2.23  39591  dvnmul  42226  stoweidlem1  42285  stoweidlem11  42295  stoweidlem26  42310  stoweidlem34  42318  stoweidlem45  42329  wallispilem3  42351  wallispi  42354  stirlinglem5  42362  sqwvfourb  42513  proththdlem  43777  341fppr2  43898  nnsgrpnmnd  44084  blen1b  44647  nn0sumshdiglem1  44680