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

Theorem 0p1e1 11747
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 10583 . 2 1 ∈ ℂ
21addid2i 10816 1 (0 + 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145  0cc0 10525  1c1 10526   + caddc 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668
This theorem is referenced by:  fv0p1e1  11748  zgt0ge1  12024  gtndiv  12047  nn0ind-raph  12070  1e0p1  12128  fz01en  12923  fz0tp  12996  fz0to3un2pr  12997  fz0sn0fz1  13012  fz0add1fz1  13095  elfzonlteqm1  13101  fzo0to2pr  13110  fzo0to3tp  13111  elfz0lmr  13140  fldiv4p1lem1div2  13193  mulp1mod1  13268  expp1  13424  facp1  13626  faclbnd  13638  bcval5  13666  bcpasc  13669  hash1  13753  hashge2el2dif  13826  relexpsucr  14376  relexpsucl  14380  relexpaddg  14400  binomlem  15172  isumnn0nn  15185  climcndslem1  15192  pwdif  15211  risefacval2  15352  fallfacval2  15353  risefac1  15375  fallfac1  15376  fallfacfwd  15378  bpolysum  15395  bpolydiflem  15396  bpoly2  15399  bpoly3  15400  bpoly4  15401  ege2le3  15431  ef4p  15454  eirrlem  15545  ruclem6  15576  p1modz1  15602  mod2eq1n2dvds  15684  nn0o1gt2  15720  pwp1fsum  15730  divalglem6  15737  bitsfzo  15772  pcfaclem  16222  4sqlem19  16287  vdwapun  16298  2exp16  16412  37prm  16442  631prm  16448  1259lem3  16454  1259lem4  16455  2503lem2  16459  4001lem1  16462  4001lem4  16465  gsummptfzsplitl  18982  ablsimpgfindlem1  19158  srgbinomlem4  19222  pmatcollpw3fi1lem1  21322  cpmadugsumlemF  21412  dvn1  24450  c1lip2  24522  dvply1  24800  iaa  24841  dvtaylp  24885  cos02pilt1  25038  advlogexp  25165  leibpi  25447  log2ublem3  25453  fsumharmonic  25516  lgamgulmlem2  25534  lgamcvg2  25559  bposlem1  25787  lgsne0  25838  gausslemma2dlem4  25872  lgsquadlem2  25884  axlowdimlem16  26670  wlkl1loop  27346  uhgrwkspthlem2  27462  crctcshwlkn0lem6  27520  wwlksn0s  27566  clwwlkccatlem  27694  umgr2cwwk2dif  27770  1wlkdlem4  27846  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960  numclwwlk5  28094  numclwwlk7  28097  nndiffz1  30435  f1ocnt  30451  nn0min  30463  0dp2dp  30512  wrdt2ind  30554  cshw1s2  30561  xrsmulgzz  30592  cyc2fv1  30690  cycpmco2lem4  30698  cycpmco2lem5  30699  cycpmco2lem7  30701  cyc3fv1  30706  cycpmrn  30712  lmat22e12  30983  lmat22e21  30984  fib2  31559  sgnneg  31697  spthcycl  32273  usgrgt2cycl  32274  subfacp1lem6  32329  subfacval2  32331  bccolsum  32868  poimirlem5  34778  poimirlem18  34791  poimirlem21  34794  poimirlem22  34795  poimirlem27  34800  poimirlem28  34801  areacirclem4  34866  fzsplit1nn0  39229  diophren  39288  jm2.17a  39435  jm2.17b  39436  k0004val0  40382  hashnzfz2  40530  bccn1  40553  dvradcnv2  40556  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  dvnmul  42104  stoweidlem26  42188  fourierdlem11  42280  fourierdlem24  42293  fourierdlem28  42297  fourierdlem30  42299  fourierdlem41  42310  fourierdlem60  42328  fourierdlem61  42329  fourierdlem73  42341  fourierdlem79  42347  fourierdlem81  42349  etransclem4  42400  etransclem24  42420  etransclem31  42427  etransclem32  42428  etransclem35  42431  1fzopredsuc  43401  m1mod0mod1  43406  iccpartigtl  43460  iccpartltu  43462  iccpartgt  43464  iccpartgel  43466  fmtnorec2  43582  fmtno5lem1  43592  fmtnofac2  43608  fmtnofac1  43609  fmtno5faclem1  43618  2exp340mod341  43775  8exp8mod9  43778  smndex2dnrinv  44015  altgsumbcALT  44329  blen1  44572  blen1b  44576  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  nn0sumshdiglem1  44609
  Copyright terms: Public domain W3C validator