Theorem 1m1e0 12229

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

Syntax hints:   = wceq 1542  (class class class)co 7368  0cc0 11038  1c1 11039   − cmin 11376

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378

This theorem is referenced by:  nnm1nn0  12454  xov1plusxeqvd  13426  fseq1p1m1  13526  elfzp1b  13529  elfzm1b  13530  elfznelfzo  13701  fldiv4lem1div2  13769  fzennn  13903  faclbnd4lem4  14231  lsw1  14502  ccat2s1p2  14566  revs1  14700  arisum  15795  pwdif  15803  geo2sum  15808  bpoly1  15986  nn0o  16322  exprmfct  16643  phiprmpw  16715  phiprm  16716  odzdvds  16735  prmpwdvds  16844  prmreclem4  16859  vdwapun  16914  chnub  18557  ex-chn1  18572  ex-chn2  18573  sylow1lem1  19539  efgs1b  19677  efgsfo  19680  efgredlema  19681  efgredeu  19693  pzriprng1ALT  21463  psdpw  22125  imasdsf1olem  24329  htpycom  24943  htpycc  24947  reparphti  24964  reparphtiOLD  24965  pcoval2  24984  pcocn  24985  pcohtpylem  24987  pcopt  24990  pcorevcl  24993  pcorevlem  24994  pi1xfrcnv  25025  dvexp  25925  dvlipcn  25967  dvply1  26259  vieta1  26288  pserdvlem2  26406  abelthlem2  26410  coseq1  26502  advlogexp  26632  logtayl  26637  cxpaddlelem  26729  isosctrlem2  26797  asin1  26872  leibpilem2  26919  log2ublem3  26926  scvxcvx  26964  1sgmprm  27178  dchrfi  27234  lgslem4  27279  lgsne0  27314  lgsquad2lem2  27364  2lgsoddprmlem3a  27389  rpvmasumlem  27466  selberg2lem  27529  logdivbnd  27535  pntrsumo1  27544  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntpbnd2  27566  ostth2lem2  27613  axpaschlem  29025  elntg2  29070  wwlksn0s  29946  clwwlkn1  30128  hst1h  32314  st0  32336  archirngz  33282  drngdimgt0  33795  cos9thpiminplylem3  33961  lmatfval  33991  lmat22e11  33995  fib2  34579  ballotlem4  34676  ballotlemi1  34680  ballotlemii  34681  ballotlemic  34684  ballotlem1c  34685  ballotlemfrceq  34706  signsvtn0  34747  signstfveq0a  34753  subfacp1lem6  35398  cvxpconn  35455  cvxsconn  35456  cvmliftlem10  35507  cvmliftlem13  35509  bcprod  35951  poimirlem3  37871  poimirlem4  37872  poimirlem13  37881  poimirlem19  37887  lcmfunnnd  42379  lcm1un  42380  lcmineqlem10  42405  lcmineqlem12  42407  lcmineqlem18  42413  mapfzcons  43070  irrapxlem3  43178  2nn0ind  43299  jm2.18  43342  jm2.23  43350  dvnmul  46298  stoweidlem1  46356  stoweidlem11  46366  stoweidlem26  46381  stoweidlem34  46389  stoweidlem45  46400  wallispilem3  46422  wallispi  46425  stirlinglem5  46433  sqwvfourb  46584  ceilhalf1  47691  proththdlem  47970  341fppr2  48091  nnsgrpnmnd  48535  blen1b  48945  nn0sumshdiglem1  48978