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

Theorem 0p1e1 10026
Description: Zero plus one equals one. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
0p1e1  |-  ( 0  +  1 )  =  1

Proof of Theorem 0p1e1
StepHypRef Expression
1 ax-1cn 8982 . 2  |-  1  e.  CC
21addid2i 9187 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff set class
Syntax hints:    = wceq 1649  (class class class)co 6021   0cc0 8924   1c1 8925    + caddc 8927
This theorem is referenced by:  nn0lt10b  10269  recnz  10278  gtndiv  10280  nn0ind-raph  10303  1e0p1  10343  fz01en  11012  fzo0to2pr  11112  fzo0to3tp  11113  expp1  11316  facp1  11499  faclbnd  11509  bcm1k  11534  bcval5  11537  bcpasc  11540  hash1  11601  wrdeqs1cat  11717  binomlem  12536  isumnn0nn  12550  climcndslem1  12557  mertenslem2  12590  ege2le3  12620  ef4p  12642  eirrlem  12731  ruclem6  12762  divalglem6  12846  bitsfzo  12875  pcfaclem  13195  4sqlem19  13259  vdwapun  13270  37prm  13371  631prm  13377  1259lem3  13380  1259lem4  13381  2503lem2  13385  4001lem1  13388  4001lem4  13391  dvn1  19680  c1lip2  19750  dvply1  20069  iaa  20110  dvtaylp  20154  advlogexp  20414  loglesqr  20510  leibpi  20650  log2ublem3  20656  harmonicbnd3  20714  fsumharmonic  20718  bposlem1  20936  lgslem4  20951  lgsne0  20985  lgsquadlem2  21007  wlkntrllem3  21416  wlkntrllem4  21417  constr1trl  21437  constr2trl  21447  fargshiftlem  21470  usgrcyclnl1  21476  usgrcyclnl2  21477  3v3e3cycl1  21480  constr3trllem3  21488  constr3trllem5  21490  4cycl4v4e  21502  4cycl4dv4e  21504  gxnn0suc  21701  xrsmulgzz  24034  ballotlemodife  24535  lgamgulmlem2  24594  lgamcvg2  24619  facgam  24630  subfacp1lem6  24651  subfacval2  24653  relexpsucl  24912  risefacval2  25096  fallfacval2  25097  risefac1  25116  fallfac1  25117  fallfacfwd  25120  axlowdimlem16  25611  bpolysum  25814  bpolydiflem  25815  bpoly2  25818  bpoly3  25819  bpoly4  25820  areacirclem5  25987  fzsplit1nn0  26504  diophren  26566  jm2.17a  26717  jm2.17b  26718  jm2.23  26759  stoweidlem34  27452
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-resscn 8981  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-mulcom 8988  ax-addass 8989  ax-mulass 8990  ax-distr 8991  ax-i2m1 8992  ax-1ne0 8993  ax-1rid 8994  ax-rnegex 8995  ax-rrecex 8996  ax-cnre 8997  ax-pre-lttri 8998  ax-pre-lttrn 8999  ax-pre-ltadd 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-nel 2554  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-mpt 4210  df-id 4440  df-po 4445  df-so 4446  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-ov 6024  df-er 6842  df-en 7047  df-dom 7048  df-sdom 7049  df-pnf 9056  df-mnf 9057  df-ltxr 9059
  Copyright terms: Public domain W3C validator