Theorem 1m1e0 12265

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

Syntax hints:   = wceq 1540  (class class class)co 7390  0cc0 11075  1c1 11076   − cmin 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414

This theorem is referenced by:  nnm1nn0  12490  xov1plusxeqvd  13466  fseq1p1m1  13566  elfzp1b  13569  elfzm1b  13570  elfznelfzo  13740  fldiv4lem1div2  13806  fzennn  13940  faclbnd4lem4  14268  lsw1  14539  ccat2s1p2  14602  revs1  14737  arisum  15833  pwdif  15841  geo2sum  15846  bpoly1  16024  nn0o  16360  exprmfct  16681  phiprmpw  16753  phiprm  16754  odzdvds  16773  prmpwdvds  16882  prmreclem4  16897  vdwapun  16952  sylow1lem1  19535  efgs1b  19673  efgsfo  19676  efgredlema  19677  efgredeu  19689  pzriprng1ALT  21413  psdpw  22064  imasdsf1olem  24268  htpycom  24882  htpycc  24886  reparphti  24903  reparphtiOLD  24904  pcoval2  24923  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcorevcl  24932  pcorevlem  24933  pi1xfrcnv  24964  dvexp  25864  dvlipcn  25906  dvply1  26198  vieta1  26227  pserdvlem2  26345  abelthlem2  26349  coseq1  26441  advlogexp  26571  logtayl  26576  cxpaddlelem  26668  isosctrlem2  26736  asin1  26811  leibpilem2  26858  log2ublem3  26865  scvxcvx  26903  1sgmprm  27117  dchrfi  27173  lgslem4  27218  lgsne0  27253  lgsquad2lem2  27303  2lgsoddprmlem3a  27328  rpvmasumlem  27405  selberg2lem  27468  logdivbnd  27474  pntrsumo1  27483  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntpbnd2  27505  ostth2lem2  27552  axpaschlem  28874  elntg2  28919  wwlksn0s  29798  clwwlkn1  29977  hst1h  32163  st0  32185  chnub  32945  archirngz  33150  drngdimgt0  33621  cos9thpiminplylem3  33781  lmatfval  33811  lmat22e11  33815  fib2  34400  ballotlem4  34497  ballotlemi1  34501  ballotlemii  34502  ballotlemic  34505  ballotlem1c  34506  ballotlemfrceq  34527  signsvtn0  34568  signstfveq0a  34574  subfacp1lem6  35179  cvxpconn  35236  cvxsconn  35237  cvmliftlem10  35288  cvmliftlem13  35290  bcprod  35732  poimirlem3  37624  poimirlem4  37625  poimirlem13  37634  poimirlem19  37640  lcmfunnnd  42007  lcm1un  42008  lcmineqlem10  42033  lcmineqlem12  42035  lcmineqlem18  42041  mapfzcons  42711  irrapxlem3  42819  2nn0ind  42941  jm2.18  42984  jm2.23  42992  dvnmul  45948  stoweidlem1  46006  stoweidlem11  46016  stoweidlem26  46031  stoweidlem34  46039  stoweidlem45  46050  wallispilem3  46072  wallispi  46075  stirlinglem5  46083  sqwvfourb  46234  upwordsing  46889  ceilhalf1  47339  proththdlem  47618  341fppr2  47739  nnsgrpnmnd  48170  blen1b  48581  nn0sumshdiglem1  48614