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

Theorem 1m1e0 11302
Description: (1 − 1) = 0. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
1m1e0 (1 − 1) = 0

Proof of Theorem 1m1e0
StepHypRef Expression
1 ax-1cn 10207 . 2 1 ∈ ℂ
21subidi 10565 1 (1 − 1) = 0
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6815  0cc0 10149  1c1 10150  cmin 10479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-po 5188  df-so 5189  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-er 7914  df-en 8125  df-dom 8126  df-sdom 8127  df-pnf 10289  df-mnf 10290  df-ltxr 10292  df-sub 10481
This theorem is referenced by:  nnm1nn0  11547  xov1plusxeqvd  12532  fseq1p1m1  12628  elfzp1b  12631  elfzm1b  12632  fz1fzo0m1  12731  elfznelfzo  12788  fldiv4lem1div2  12853  fzennn  12982  faclbnd4lem4  13298  lsw1  13562  ccat2s1p2  13625  revs1  13735  arisum  14812  pwm1geoser  14820  geo2sum  14824  bpoly1  15002  nn0o  15322  exprmfct  15639  phiprmpw  15704  phiprm  15705  odzdvds  15723  prmpwdvds  15831  prmreclem4  15846  vdwapun  15901  sylow1lem1  18234  efgs1b  18370  efgsfo  18373  efgredlema  18374  efgredeu  18386  imasdsf1olem  22400  htpycom  22997  htpycc  23001  reparphti  23018  pcoval2  23037  pcocn  23038  pcohtpylem  23040  pcopt  23043  pcorevcl  23046  pcorevlem  23047  pi1xfrcnv  23078  dvexp  23936  dvlipcn  23977  dvply1  24259  vieta1  24287  pserdvlem2  24402  abelthlem2  24406  coseq1  24495  advlogexp  24622  logtayl  24627  cxpaddlelem  24713  isosctrlem2  24770  asin1  24842  leibpilem2  24889  log2ublem3  24896  scvxcvx  24933  1sgmprm  25145  dchrfi  25201  lgslem4  25246  lgsne0  25281  lgsquad2lem2  25331  2lgsoddprmlem3a  25356  rpvmasumlem  25397  selberg2lem  25460  logdivbnd  25466  pntrsumo1  25475  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  pntpbnd2  25497  ostth2lem2  25544  axpaschlem  26041  wwlksn0s  26992  clwwlkn1  27192  hst1h  29417  st0  29439  archirngz  30074  lmatfval  30211  lmat22e11  30215  fib2  30795  ballotlem4  30891  ballotlemi1  30895  ballotlemii  30896  ballotlemic  30899  ballotlem1c  30900  ballotlemfrceq  30921  signsvtn0  30978  signstfveq0a  30984  subfacp1lem6  31496  cvxpconn  31553  cvxsconn  31554  cvmliftlem10  31605  cvmliftlem13  31607  bcprod  31953  poimirlem3  33744  poimirlem4  33745  poimirlem13  33754  poimirlem19  33760  mapfzcons  37800  irrapxlem3  37909  2nn0ind  38031  jm2.18  38076  jm2.23  38084  dvnmul  40680  stoweidlem1  40740  stoweidlem11  40750  stoweidlem26  40765  stoweidlem34  40773  stoweidlem45  40784  wallispilem3  40806  wallispi  40809  stirlinglem5  40817  sqwvfourb  40968  pwdif  42030  proththdlem  42059  nnsgrpnmnd  42347  blen1b  42911  nn0sumshdiglem1  42944
  Copyright terms: Public domain W3C validator