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

Theorem 0p1e1 10728
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 9604 . 2  |-  1  e.  CC
21addid2i 9828 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437  (class class class)co 6305   0cc0 9546   1c1 9547    + caddc 9549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-ltxr 9687
This theorem is referenced by:  zgt0ge1  10997  nn0lt10bOLD  11006  gtndiv  11020  nn0ind-raph  11042  1e0p1  11086  fz01en  11834  fz0tp  11900  elfzonlteqm1  11995  fzo0to2pr  12004  fzo0to3tp  12005  expp1  12285  facp1  12470  faclbnd  12481  bcm1k  12506  bcval5  12509  bcpasc  12512  hash1  12587  hashge2el2dif  12641  wrdeqs1cat  12833  relexpsucr  13092  relexpsucl  13096  relexpaddg  13116  binomlem  13886  isumnn0nn  13899  climcndslem1  13906  mertenslem2  13940  risefacval2  14062  fallfacval2  14063  risefac1  14085  fallfac1  14086  fallfacfwd  14088  bpolysum  14105  bpolydiflem  14106  bpoly2  14109  bpoly3  14110  bpoly4  14111  ege2le3  14143  ef4p  14166  eirrlem  14255  ruclem6  14286  divalglem6  14377  bitsfzo  14408  pcfaclem  14842  4sqlem19  14912  vdwapun  14923  2exp16  15060  37prm  15091  631prm  15097  1259lem3  15103  1259lem4  15104  2503lem2  15108  4001lem1  15111  4001lem4  15114  gsummptfzsplitl  17565  srgbinomlem4  17775  pmatcollpw3fi1lem1  19808  cpmadugsumlemF  19898  dvn1  22878  c1lip2  22948  dvply1  23235  iaa  23279  dvtaylp  23323  advlogexp  23598  loglesqrt  23696  leibpi  23866  log2ublem3  23872  harmonicbnd3  23931  fsumharmonic  23935  lgamgulmlem2  23953  lgamcvg2  23978  facgam  23989  bposlem1  24210  lgslem4  24225  lgsne0  24259  lgsquadlem2  24281  axlowdimlem16  24985  wlkntrllem2  25288  2wlklem  25292  constr1trl  25316  fargshiftlem  25360  usgrcyclnl1  25366  3v3e3cycl1  25370  constr3trllem3  25378  constr3trllem5  25380  wwlkn0  25415  wwlkn0s  25431  clwwlkn2  25501  usg2cwwk2dif  25546  rusgranumwlkl1  25673  numclwwlk5  25838  numclwwlk7  25840  gxnn0suc  25990  nndiffz1  28372  f1ocnt  28382  nn0min  28391  xrsmulgzz  28447  lmat22e12  28653  lmat22e21  28654  fib2  29243  ballotlemodife  29338  sgnneg  29419  subfacp1lem6  29916  subfacval2  29918  bccolsum  30382  poimirlem5  31909  poimirlem18  31922  poimirlem21  31925  poimirlem22  31926  poimirlem27  31931  poimirlem28  31932  areacirclem4  31999  fzsplit1nn0  35565  diophren  35625  jm2.17a  35780  jm2.17b  35781  hashnzfz2  36640  bccn1  36663  dvradcnv2  36666  binomcxplemdvbinom  36672  binomcxplemnotnn0  36675  dvnmul  37758  stoweidlem26  37826  stoweidlem34  37835  fourierdlem11  37920  fourierdlem24  37933  fourierdlem28  37937  fourierdlem30  37939  fourierdlem41  37951  fourierdlem60  37970  fourierdlem61  37971  fourierdlem73  37983  fourierdlem79  37989  fourierdlem81  37991  etransclem4  38043  etransclem24  38063  etransclem31  38070  etransclem32  38071  etransclem35  38074  1fzopredsuc  38591  m1mod0mod1  38593  mod2eq1n2dvds  38595  iccpartigtl  38607  iccpartltu  38609  iccpartgt  38611  iccpartgel  38613  iccelpart  38617  bgoldbtbnd  38774  altgsumbcALT  39755  nn0o1gt2  39948  blen1  40016  blen1b  40020  nn0sumshdiglemA  40051  nn0sumshdiglemB  40052  nn0sumshdiglem1  40053
  Copyright terms: Public domain W3C validator