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

Theorem 0p1e1 12209
Description: 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
0p1e1 (0 + 1) = 1

Proof of Theorem 0p1e1
StepHypRef Expression
1 ax-1cn 11043 . 2 1 ∈ ℂ
21addid2i 11277 1 (0 + 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7350  0cc0 10985  1c1 10986   + caddc 10988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  df-po 5543  df-so 5544  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7353  df-er 8582  df-en 8818  df-dom 8819  df-sdom 8820  df-pnf 11125  df-mnf 11126  df-ltxr 11128
This theorem is referenced by:  fv0p1e1  12210  zgt0ge1  12488  gtndiv  12511  nn0ind-raph  12534  1e0p1  12593  fz01en  13398  fz0tp  13471  fz0to3un2pr  13472  fz0sn0fz1  13487  fz0add1fz1  13571  elfzonlteqm1  13577  fzo0to2pr  13586  fzo0to3tp  13587  elfz0lmr  13616  fldiv4p1lem1div2  13669  mulp1mod1  13746  expp1  13903  facp1  14106  faclbnd  14118  bcval5  14146  bcpasc  14149  hash1  14232  hashge2el2dif  14307  relexpsucl  14850  relexpsucr  14851  relexpaddg  14872  binomlem  15649  isumnn0nn  15662  climcndslem1  15669  pwdif  15688  risefacval2  15828  fallfacval2  15829  risefac1  15851  fallfac1  15852  fallfacfwd  15854  bpolysum  15871  bpolydiflem  15872  bpoly2  15875  bpoly3  15876  bpoly4  15877  ege2le3  15907  ef4p  15930  eirrlem  16021  ruclem6  16052  p1modz1  16078  mod2eq1n2dvds  16164  nn0o1gt2  16198  pwp1fsum  16208  divalglem6  16215  bitsfzo  16250  pcfaclem  16705  4sqlem19  16770  vdwapun  16781  2exp16  16898  37prm  16928  631prm  16934  1259lem3  16940  1259lem4  16941  2503lem2  16945  4001lem1  16948  4001lem4  16951  smndex2dnrinv  18660  gsummptfzsplitl  19639  ablsimpgfindlem1  19815  srgbinomlem4  19884  pmatcollpw3fi1lem1  22057  cpmadugsumlemF  22147  dvn1  25212  c1lip2  25284  dvply1  25566  iaa  25607  dvtaylp  25651  cos02pilt1  25804  advlogexp  25932  leibpi  26214  log2ublem3  26220  fsumharmonic  26283  lgamgulmlem2  26301  lgamcvg2  26326  bposlem1  26554  lgsne0  26605  gausslemma2dlem4  26639  lgsquadlem2  26651  axlowdimlem16  27692  wlkl1loop  28372  uhgrwkspthlem2  28488  crctcshwlkn0lem6  28546  wwlksn0s  28592  clwwlkccatlem  28719  umgr2cwwk2dif  28794  1wlkdlem4  28870  konigsberglem1  28982  konigsberglem2  28983  konigsberglem3  28984  numclwwlk5  29118  numclwwlk7  29121  nndiffz1  31471  f1ocnt  31487  nn0min  31498  0dp2dp  31547  wrdt2ind  31589  cshw1s2  31596  xrsmulgzz  31651  cyc2fv1  31752  cycpmco2lem4  31760  cycpmco2lem5  31761  cycpmco2lem7  31763  cyc3fv1  31768  cycpmrn  31774  lmat22e12  32161  lmat22e21  32162  fib2  32763  sgnneg  32901  spthcycl  33484  usgrgt2cycl  33485  subfacp1lem6  33540  subfacval2  33542  bccolsum  34090  poimirlem5  35969  poimirlem18  35982  poimirlem21  35985  poimirlem22  35986  poimirlem27  35991  poimirlem28  35992  areacirclem4  36055  420gcd8e4  40349  3lexlogpow5ineq1  40397  3lexlogpow5ineq5  40403  aks4d1p1  40419  sticksstones9  40448  sticksstones10  40449  metakunt2  40464  fzsplit1nn0  40911  diophren  40970  jm2.17a  41118  jm2.17b  41119  k0004val0  42159  hashnzfz2  42334  bccn1  42357  dvradcnv2  42360  binomcxplemdvbinom  42366  binomcxplemnotnn0  42369  dvnmul  43906  stoweidlem26  43989  fourierdlem11  44081  fourierdlem24  44094  fourierdlem28  44098  fourierdlem30  44100  fourierdlem41  44111  fourierdlem60  44129  fourierdlem61  44130  fourierdlem73  44142  fourierdlem79  44148  fourierdlem81  44150  etransclem4  44201  etransclem24  44221  etransclem31  44228  etransclem32  44229  etransclem35  44232  natlocalincr  44833  1fzopredsuc  45274  m1mod0mod1  45279  iccpartigtl  45333  iccpartltu  45335  iccpartgt  45337  iccpartgel  45339  fmtnorec2  45453  fmtno5lem1  45463  fmtnofac2  45479  fmtnofac1  45480  fmtno5faclem1  45489  2exp340mod341  45643  8exp8mod9  45646  altgsumbcALT  46147  blen1  46388  blen1b  46392  nn0sumshdiglemA  46423  nn0sumshdiglemB  46424  nn0sumshdiglem1  46425  ackvalsuc0val  46491  ackval0012  46493
  Copyright terms: Public domain W3C validator