MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1m1e0 Structured version   Visualization version   GIF version

Theorem 1m1e0 11703
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
StepHypRef Expression
1 ax-1cn 10589 . 2 1 ∈ ℂ
21subidi 10951 1 (1 − 1) = 0
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7150  0cc0 10531  1c1 10532  cmin 10864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  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 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-ltxr 10674  df-sub 10866
This theorem is referenced by:  nnm1nn0  11932  xov1plusxeqvd  12879  fseq1p1m1  12976  elfzp1b  12979  elfzm1b  12980  elfznelfzo  13137  fldiv4lem1div2  13202  fzennn  13331  faclbnd4lem4  13651  lsw1  13914  ccat2s1p2  13981  ccat2s1p2OLD  13983  revs1  14122  arisum  15210  pwdif  15218  pwm1geoserOLD  15220  geo2sum  15224  bpoly1  15400  nn0o  15729  exprmfct  16043  phiprmpw  16108  phiprm  16109  odzdvds  16127  prmpwdvds  16235  prmreclem4  16250  vdwapun  16305  sylow1lem1  18659  efgs1b  18798  efgsfo  18801  efgredlema  18802  efgredeu  18814  imasdsf1olem  22917  htpycom  23514  htpycc  23518  reparphti  23535  pcoval2  23554  pcocn  23555  pcohtpylem  23557  pcopt  23560  pcorevcl  23563  pcorevlem  23564  pi1xfrcnv  23595  dvexp  24484  dvlipcn  24525  dvply1  24807  vieta1  24835  pserdvlem2  24950  abelthlem2  24954  coseq1  25044  advlogexp  25170  logtayl  25175  cxpaddlelem  25264  isosctrlem2  25329  asin1  25404  leibpilem2  25452  log2ublem3  25459  scvxcvx  25496  1sgmprm  25708  dchrfi  25764  lgslem4  25809  lgsne0  25844  lgsquad2lem2  25894  2lgsoddprmlem3a  25919  rpvmasumlem  25996  selberg2lem  26059  logdivbnd  26065  pntrsumo1  26074  pntrlog2bndlem4  26089  pntrlog2bndlem5  26090  pntpbnd2  26096  ostth2lem2  26143  axpaschlem  26659  elntg2  26704  wwlksn0s  27572  clwwlkn1  27752  hst1h  29937  st0  29959  archirngz  30751  drngdimgt0  30921  lmatfval  30984  lmat22e11  30988  fib2  31565  ballotlem4  31661  ballotlemi1  31665  ballotlemii  31666  ballotlemic  31669  ballotlem1c  31670  ballotlemfrceq  31691  signsvtn0  31745  signstfveq0a  31751  subfacp1lem6  32335  cvxpconn  32392  cvxsconn  32393  cvmliftlem10  32444  cvmliftlem13  32446  bcprod  32873  poimirlem3  34781  poimirlem4  34782  poimirlem13  34791  poimirlem19  34797  mapfzcons  39197  irrapxlem3  39305  2nn0ind  39426  jm2.18  39469  jm2.23  39477  dvnmul  42112  stoweidlem1  42171  stoweidlem11  42181  stoweidlem26  42196  stoweidlem34  42204  stoweidlem45  42215  wallispilem3  42237  wallispi  42240  stirlinglem5  42248  sqwvfourb  42399  proththdlem  43629  341fppr2  43750  nnsgrpnmnd  43936  blen1b  44550  nn0sumshdiglem1  44583
  Copyright terms: Public domain W3C validator