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

Theorem 0p1e1 10582
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 9479 . 2  |-  1  e.  CC
21addid2i 9697 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399  (class class class)co 6214   0cc0 9421   1c1 9422    + caddc 9424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-ltxr 9562
This theorem is referenced by:  zgt0ge1  10852  nn0lt10bOLD  10861  gtndiv  10875  nn0ind-raph  10897  1e0p1  10941  fz01en  11652  fz0tp  11717  elfzonlteqm1  11808  fzo0to2pr  11817  fzo0to3tp  11818  expp1  12095  facp1  12279  faclbnd  12289  bcm1k  12314  bcval5  12317  bcpasc  12320  hash1  12392  hashge2el2dif  12444  wrdeqs1cat  12630  relexpsucr  12883  relexpsucl  12887  relexpaddg  12907  binomlem  13662  isumnn0nn  13675  climcndslem1  13682  mertenslem2  13715  ege2le3  13846  ef4p  13869  eirrlem  13958  ruclem6  13989  divalglem6  14077  bitsfzo  14106  pcfaclem  14438  4sqlem19  14502  vdwapun  14513  2exp16  14596  37prm  14627  631prm  14633  1259lem3  14636  1259lem4  14637  2503lem2  14641  4001lem1  14644  4001lem4  14647  gsummptfzsplitl  17088  srgbinomlem4  17326  pmatcollpw3fi1lem1  19391  cpmadugsumlemF  19481  dvn1  22433  c1lip2  22503  dvply1  22784  iaa  22825  dvtaylp  22869  advlogexp  23142  loglesqrt  23238  leibpi  23408  log2ublem3  23414  harmonicbnd3  23473  fsumharmonic  23477  bposlem1  23695  lgslem4  23710  lgsne0  23744  lgsquadlem2  23766  axlowdimlem16  24402  wlkntrllem2  24704  2wlklem  24708  constr1trl  24732  fargshiftlem  24776  usgrcyclnl1  24782  3v3e3cycl1  24786  constr3trllem3  24794  constr3trllem5  24796  wwlkn0  24831  wwlkn0s  24847  clwwlkn2  24917  usg2cwwk2dif  24962  rusgranumwlkl1  25089  numclwwlk5  25254  numclwwlk7  25256  gxnn0suc  25404  nndiffz1  27779  nn0min  27794  xrsmulgzz  27849  fib2  28560  ballotlemodife  28655  sgnneg  28698  lgamgulmlem2  28797  lgamcvg2  28822  facgam  28833  subfacp1lem6  28854  subfacval2  28856  risefacval2  29334  fallfacval2  29335  risefac1  29357  fallfac1  29358  fallfacfwd  29360  bpolysum  30004  bpolydiflem  30005  bpoly2  30008  bpoly3  30009  bpoly4  30010  areacirclem4  30312  fzsplit1nn0  30888  diophren  30948  jm2.17a  31099  jm2.17b  31100  hashnzfz2  31430  bccn1  31453  dvradcnv2  31456  binomcxplemdvbinom  31462  binomcxplemnotnn0  31465  dvnmul  31941  stoweidlem26  32009  stoweidlem34  32017  fourierdlem11  32101  fourierdlem24  32114  fourierdlem28  32118  fourierdlem30  32120  fourierdlem41  32131  fourierdlem60  32150  fourierdlem61  32151  fourierdlem73  32163  fourierdlem79  32169  fourierdlem81  32171  etransclem4  32222  etransclem24  32242  etransclem31  32249  etransclem32  32250  etransclem35  32253  m1mod0mod1  32495  mod2eq1n2dvds  32497  altgsumbcALT  33177  nn0o1gt2  33372  blen1  33440  blen1b  33444  nn0sumshdiglemA  33475  nn0sumshdiglemB  33476  nn0sumshdiglem1  33477
  Copyright terms: Public domain W3C validator