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

Theorem 0p1e1 10975
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 9846 . 2 1 ∈ ℂ
21addid2i 10071 1 (0 + 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6523  0cc0 9788  1c1 9789   + caddc 9791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-po 4945  df-so 4946  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-ov 6526  df-er 7602  df-en 7815  df-dom 7816  df-sdom 7817  df-pnf 9928  df-mnf 9929  df-ltxr 9931
This theorem is referenced by:  zgt0ge1  11260  gtndiv  11282  nn0ind-raph  11305  1e0p1  11380  fz01en  12191  fz0tp  12260  fz0to3un2pr  12261  fz0sn0fz1  12276  elfzonlteqm1  12361  fzo0to2pr  12371  fzo0to3tp  12372  fldiv4p1lem1div2  12449  mulp1mod1  12524  expp1  12680  facp1  12878  faclbnd  12890  bcm1k  12915  bcval5  12918  bcpasc  12921  hash1  13001  hashge2el2dif  13063  wrdeqs1cat  13268  relexpsucr  13559  relexpsucl  13563  relexpaddg  13583  binomlem  14342  isumnn0nn  14355  climcndslem1  14362  mertenslem2  14398  risefacval2  14522  fallfacval2  14523  risefac1  14545  fallfac1  14546  fallfacfwd  14548  bpolysum  14565  bpolydiflem  14566  bpoly2  14569  bpoly3  14570  bpoly4  14571  ege2le3  14601  ef4p  14624  eirrlem  14713  ruclem6  14745  mod2eq1n2dvds  14851  nn0o1gt2  14877  pwp1fsum  14894  divalglem6  14901  bitsfzo  14937  pcfaclem  15382  4sqlem19  15447  vdwapun  15458  2exp16  15577  37prm  15608  631prm  15614  1259lem3  15620  1259lem4  15621  2503lem2  15625  4001lem1  15628  4001lem4  15631  gsummptfzsplitl  18098  srgbinomlem4  18308  pmatcollpw3fi1lem1  20348  cpmadugsumlemF  20438  dvn1  23408  c1lip2  23478  dvply1  23756  iaa  23797  dvtaylp  23841  advlogexp  24114  loglesqrt  24212  leibpi  24382  log2ublem3  24388  harmonicbnd3  24447  fsumharmonic  24451  lgamgulmlem2  24469  lgamcvg2  24494  facgam  24505  bposlem1  24722  lgslem4  24738  lgsne0  24773  gausslemma2dlem4  24807  lgsquadlem2  24819  axlowdimlem16  25551  wlkntrllem2  25852  2wlklem  25856  constr1trl  25880  fargshiftlem  25924  usgrcyclnl1  25930  3v3e3cycl1  25934  constr3trllem3  25942  constr3trllem5  25944  wwlkn0  25979  wwlkn0s  25995  clwwlkn2  26065  usg2cwwk2dif  26110  rusgranumwlkl1  26236  numclwwlk5  26401  numclwwlk7  26403  nndiffz1  28738  f1ocnt  28748  nn0min  28756  xrsmulgzz  28811  lmat22e12  29015  lmat22e21  29016  fib2  29593  ballotlemodife  29688  sgnneg  29731  subfacp1lem6  30223  subfacval2  30225  bccolsum  30680  poimirlem5  32383  poimirlem18  32396  poimirlem21  32399  poimirlem22  32400  poimirlem27  32405  poimirlem28  32406  areacirclem4  32472  fzsplit1nn0  36134  diophren  36194  jm2.17a  36344  jm2.17b  36345  k0004val0  37271  hashnzfz2  37341  bccn1  37364  dvradcnv2  37367  binomcxplemdvbinom  37373  binomcxplemnotnn0  37376  dvnmul  38633  stoweidlem26  38719  stoweidlem34  38727  fourierdlem11  38811  fourierdlem24  38824  fourierdlem28  38828  fourierdlem30  38830  fourierdlem41  38841  fourierdlem60  38859  fourierdlem61  38860  fourierdlem73  38872  fourierdlem79  38878  fourierdlem81  38880  etransclem4  38931  etransclem24  38951  etransclem31  38958  etransclem32  38959  etransclem35  38962  1fzopredsuc  39748  m1mod0mod1  39750  iccpartigtl  39762  iccpartltu  39764  iccpartgt  39766  iccpartgel  39768  iccelpart  39772  fmtnorec2  39794  fmtno5lem1  39804  fmtnofac2  39820  fmtnofac1  39821  fmtno5faclem1  39830  pwdif  39840  bgoldbtbnd  40026  elfz0lmr  40190  1wlkl1loop  40840  wlkOnl1iedg  40871  2Wlklem  40873  pthdadjvtx  40934  uhgr1wlkspthlem2  40958  usgr2wlkneq  40960  usgr2trlncl  40964  lfgrn1cycl  41006  crctcsh1wlkn0lem6  41016  wwlksn0s  41055  0enwwlksnge1  41058  21wlkdlem5  41134  21wlkdlem10  41140  rusgrnumwwlkl1  41170  clwwlksn2  41215  umgr2cwwk2dif  41246  11wlkdlem4  41305  31wlkdlem5  41328  31wlkdlem10  41334  upgr3v3e3cycl  41345  upgr4cycl4dv4e  41350  konigsberglem1  41420  konigsberglem2  41421  konigsberglem3  41422  av-numclwwlk5  41540  av-numclwwlk7  41543  altgsumbcALT  41922  blen1  42174  blen1b  42178  nn0sumshdiglemA  42209  nn0sumshdiglemB  42210  nn0sumshdiglem1  42211
  Copyright terms: Public domain W3C validator