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

Theorem 0p1e1 10654
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 9553 . 2  |-  1  e.  CC
21addid2i 9771 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383  (class class class)co 6281   0cc0 9495   1c1 9496    + caddc 9498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-po 4790  df-so 4791  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-ltxr 9636
This theorem is referenced by:  zgt0ge1  10924  nn0lt10bOLD  10933  gtndiv  10947  nn0ind-raph  10971  1e0p1  11014  fz01en  11724  fz0tp  11788  elfzonlteqm1  11873  fzo0to2pr  11881  fzo0to3tp  11882  expp1  12155  facp1  12340  faclbnd  12350  bcm1k  12375  bcval5  12378  bcpasc  12381  hash1  12451  hashge2el2dif  12503  wrdeqs1cat  12682  binomlem  13623  isumnn0nn  13636  climcndslem1  13643  mertenslem2  13676  ege2le3  13807  ef4p  13830  eirrlem  13919  ruclem6  13950  divalglem6  14038  bitsfzo  14067  pcfaclem  14399  4sqlem19  14463  vdwapun  14474  2exp16  14557  37prm  14588  631prm  14594  1259lem3  14597  1259lem4  14598  2503lem2  14602  4001lem1  14605  4001lem4  14608  gsummptfzsplitl  16932  srgbinomlem4  17173  pmatcollpw3fi1lem1  19265  cpmadugsumlemF  19355  dvn1  22307  c1lip2  22377  dvply1  22658  iaa  22699  dvtaylp  22743  advlogexp  23014  loglesqrt  23110  leibpi  23251  log2ublem3  23257  harmonicbnd3  23315  fsumharmonic  23319  bposlem1  23537  lgslem4  23552  lgsne0  23586  lgsquadlem2  23608  axlowdimlem16  24238  wlkntrllem2  24540  2wlklem  24544  constr1trl  24568  fargshiftlem  24612  usgrcyclnl1  24618  3v3e3cycl1  24622  constr3trllem3  24630  constr3trllem5  24632  wwlkn0  24667  wwlkn0s  24683  clwwlkn2  24753  usg2cwwk2dif  24798  rusgranumwlkl1  24925  numclwwlk5  25090  numclwwlk7  25092  gxnn0suc  25244  nndiffz1  27574  nn0min  27589  xrsmulgzz  27644  fib2  28319  ballotlemodife  28414  sgnneg  28457  lgamgulmlem2  28550  lgamcvg2  28575  facgam  28586  subfacp1lem6  28607  subfacval2  28609  relexpsucl  29033  risefacval2  29108  fallfacval2  29109  risefac1  29131  fallfac1  29132  fallfacfwd  29134  bpolysum  29791  bpolydiflem  29792  bpoly2  29795  bpoly3  29796  bpoly4  29797  areacirclem4  30086  fzsplit1nn0  30663  diophren  30723  jm2.17a  30874  jm2.17b  30875  hashnzfz2  31202  dvnmul  31694  stoweidlem26  31762  stoweidlem34  31770  fourierdlem11  31854  fourierdlem24  31867  fourierdlem28  31871  fourierdlem30  31873  fourierdlem41  31884  fourierdlem60  31903  fourierdlem61  31904  fourierdlem73  31916  fourierdlem79  31922  fourierdlem81  31924  etransclem4  31975  etransclem24  31995  etransclem31  32002  etransclem32  32003  etransclem35  32006  altgsumbcALT  32810
  Copyright terms: Public domain W3C validator