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

Theorem 0p1e1 10710
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 9584 . 2  |-  1  e.  CC
21addid2i 9808 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1448  (class class class)co 6276   0cc0 9526   1c1 9527    + caddc 9529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-po 4733  df-so 4734  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-ov 6279  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9664  df-mnf 9665  df-ltxr 9667
This theorem is referenced by:  zgt0ge1  10980  nn0lt10bOLD  10989  gtndiv  11003  nn0ind-raph  11025  1e0p1  11069  fz01en  11818  fz0tp  11884  fz0to3un2pr  11885  elfzonlteqm1  11982  fzo0to2pr  11991  fzo0to3tp  11992  expp1  12273  facp1  12458  faclbnd  12469  bcm1k  12494  bcval5  12497  bcpasc  12500  hash1  12575  hashge2el2dif  12632  wrdeqs1cat  12830  relexpsucr  13103  relexpsucl  13107  relexpaddg  13127  binomlem  13898  isumnn0nn  13911  climcndslem1  13918  mertenslem2  13952  risefacval2  14074  fallfacval2  14075  risefac1  14097  fallfac1  14098  fallfacfwd  14100  bpolysum  14117  bpolydiflem  14118  bpoly2  14121  bpoly3  14122  bpoly4  14123  ege2le3  14155  ef4p  14178  eirrlem  14267  ruclem6  14298  divalglem6  14389  bitsfzo  14420  pcfaclem  14854  4sqlem19  14924  vdwapun  14935  2exp16  15072  37prm  15103  631prm  15109  1259lem3  15115  1259lem4  15116  2503lem2  15120  4001lem1  15123  4001lem4  15126  gsummptfzsplitl  17577  srgbinomlem4  17787  pmatcollpw3fi1lem1  19821  cpmadugsumlemF  19911  dvn1  22892  c1lip2  22962  dvply1  23249  iaa  23293  dvtaylp  23337  advlogexp  23612  loglesqrt  23710  leibpi  23880  log2ublem3  23886  harmonicbnd3  23945  fsumharmonic  23949  lgamgulmlem2  23967  lgamcvg2  23992  facgam  24003  bposlem1  24224  lgslem4  24239  lgsne0  24273  lgsquadlem2  24295  axlowdimlem16  24999  wlkntrllem2  25302  2wlklem  25306  constr1trl  25330  fargshiftlem  25374  usgrcyclnl1  25380  3v3e3cycl1  25384  constr3trllem3  25392  constr3trllem5  25394  wwlkn0  25429  wwlkn0s  25445  clwwlkn2  25515  usg2cwwk2dif  25560  rusgranumwlkl1  25687  numclwwlk5  25852  numclwwlk7  25854  gxnn0suc  26004  nndiffz1  28374  f1ocnt  28384  nn0min  28392  xrsmulgzz  28448  lmat22e12  28652  lmat22e21  28653  fib2  29241  ballotlemodife  29336  sgnneg  29417  subfacp1lem6  29914  subfacval2  29916  bccolsum  30381  poimirlem5  31947  poimirlem18  31960  poimirlem21  31963  poimirlem22  31964  poimirlem27  31969  poimirlem28  31970  areacirclem4  32037  fzsplit1nn0  35598  diophren  35658  jm2.17a  35812  jm2.17b  35813  hashnzfz2  36671  bccn1  36694  dvradcnv2  36697  binomcxplemdvbinom  36703  binomcxplemnotnn0  36706  dvnmul  37860  stoweidlem26  37943  stoweidlem34  37952  fourierdlem11  38037  fourierdlem24  38050  fourierdlem28  38054  fourierdlem30  38056  fourierdlem41  38068  fourierdlem60  38087  fourierdlem61  38088  fourierdlem73  38100  fourierdlem79  38106  fourierdlem81  38108  etransclem4  38160  etransclem24  38180  etransclem31  38187  etransclem32  38188  etransclem35  38191  1fzopredsuc  38812  m1mod0mod1  38814  mod2eq1n2dvds  38816  iccpartigtl  38828  iccpartltu  38830  iccpartgt  38832  iccpartgel  38834  iccelpart  38838  bgoldbtbnd  38995  elfz0lmr  39164  2Wlklem  39766  pthdadjvtx  39815  uhgr1wlkspthlem2  39838  usgr2wlkneq  39840  lfgrn1cycl  39876  11wlkdlem4  39907  21wlkdlem5  39930  21wlkdlem10  39936  31wlkdlem5  39956  31wlkdlem10  39962  upgr3v3e3cycl  39973  upgr4cycl4dv4e  39978  altgsumbcALT  40459  nn0o1gt2  40652  blen1  40720  blen1b  40724  nn0sumshdiglemA  40755  nn0sumshdiglemB  40756  nn0sumshdiglem1  40757
  Copyright terms: Public domain W3C validator