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

Theorem 0p1e1 12208
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 11042 . 2 1 ∈ ℂ
21addid2i 11276 1 (0 + 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7349  0cc0 10984  1c1 10985   + caddc 10987
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-mulrcl 11047  ax-mulcom 11048  ax-addass 11049  ax-mulass 11050  ax-distr 11051  ax-i2m1 11052  ax-1ne0 11053  ax-1rid 11054  ax-rnegex 11055  ax-rrecex 11056  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059  ax-pre-ltadd 11060
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5528  df-po 5542  df-so 5543  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7352  df-er 8581  df-en 8817  df-dom 8818  df-sdom 8819  df-pnf 11124  df-mnf 11125  df-ltxr 11127
This theorem is referenced by:  fv0p1e1  12209  zgt0ge1  12487  gtndiv  12510  nn0ind-raph  12533  1e0p1  12592  fz01en  13397  fz0tp  13470  fz0to3un2pr  13471  fz0sn0fz1  13486  fz0add1fz1  13570  elfzonlteqm1  13576  fzo0to2pr  13585  fzo0to3tp  13586  elfz0lmr  13615  fldiv4p1lem1div2  13668  mulp1mod1  13745  expp1  13902  facp1  14105  faclbnd  14117  bcval5  14145  bcpasc  14148  hash1  14231  hashge2el2dif  14306  relexpsucl  14849  relexpsucr  14850  relexpaddg  14871  binomlem  15648  isumnn0nn  15661  climcndslem1  15668  pwdif  15687  risefacval2  15827  fallfacval2  15828  risefac1  15850  fallfac1  15851  fallfacfwd  15853  bpolysum  15870  bpolydiflem  15871  bpoly2  15874  bpoly3  15875  bpoly4  15876  ege2le3  15906  ef4p  15929  eirrlem  16020  ruclem6  16051  p1modz1  16077  mod2eq1n2dvds  16163  nn0o1gt2  16197  pwp1fsum  16207  divalglem6  16214  bitsfzo  16249  pcfaclem  16704  4sqlem19  16769  vdwapun  16780  2exp16  16897  37prm  16927  631prm  16933  1259lem3  16939  1259lem4  16940  2503lem2  16944  4001lem1  16947  4001lem4  16950  smndex2dnrinv  18659  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  27704  wlkl1loop  28384  uhgrwkspthlem2  28500  crctcshwlkn0lem6  28558  wwlksn0s  28604  clwwlkccatlem  28731  umgr2cwwk2dif  28806  1wlkdlem4  28882  konigsberglem1  28994  konigsberglem2  28995  konigsberglem3  28996  numclwwlk5  29130  numclwwlk7  29133  nndiffz1  31483  f1ocnt  31499  nn0min  31510  0dp2dp  31559  wrdt2ind  31601  cshw1s2  31608  xrsmulgzz  31663  cyc2fv1  31764  cycpmco2lem4  31772  cycpmco2lem5  31773  cycpmco2lem7  31775  cyc3fv1  31780  cycpmrn  31786  lmat22e12  32173  lmat22e21  32174  fib2  32775  sgnneg  32913  spthcycl  33496  usgrgt2cycl  33497  subfacp1lem6  33552  subfacval2  33554  bccolsum  34102  poimirlem5  35978  poimirlem18  35991  poimirlem21  35994  poimirlem22  35995  poimirlem27  36000  poimirlem28  36001  areacirclem4  36064  420gcd8e4  40358  3lexlogpow5ineq1  40406  3lexlogpow5ineq5  40412  aks4d1p1  40428  sticksstones9  40457  sticksstones10  40458  metakunt2  40473  fzsplit1nn0  40942  diophren  41001  jm2.17a  41149  jm2.17b  41150  k0004val0  42190  hashnzfz2  42365  bccn1  42388  dvradcnv2  42391  binomcxplemdvbinom  42397  binomcxplemnotnn0  42400  dvnmul  43937  stoweidlem26  44020  fourierdlem11  44112  fourierdlem24  44125  fourierdlem28  44129  fourierdlem30  44131  fourierdlem41  44142  fourierdlem60  44160  fourierdlem61  44161  fourierdlem73  44173  fourierdlem79  44179  fourierdlem81  44181  etransclem4  44232  etransclem24  44252  etransclem31  44259  etransclem32  44260  etransclem35  44263  natlocalincr  44864  1fzopredsuc  45305  m1mod0mod1  45310  iccpartigtl  45364  iccpartltu  45366  iccpartgt  45368  iccpartgel  45370  fmtnorec2  45484  fmtno5lem1  45494  fmtnofac2  45510  fmtnofac1  45511  fmtno5faclem1  45520  2exp340mod341  45674  8exp8mod9  45677  altgsumbcALT  46178  blen1  46419  blen1b  46423  nn0sumshdiglemA  46454  nn0sumshdiglemB  46455  nn0sumshdiglem1  46456  ackvalsuc0val  46522  ackval0012  46524
  Copyright terms: Public domain W3C validator