Theorem 0p1e1 12367

Description: 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
0p1e1	⊢ (0 + 1) = 1

Proof of Theorem 0p1e1

Step	Hyp	Ref	Expression
1		ax-1cn 11164	. 2 ⊢ 1 ∈ ℂ
2	1	addlidi 11404	1 ⊢ (0 + 1) = 1

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7412  0cc0 11106  1c1 11107   + caddc 11109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-po 5568  df-so 5569  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-ltxr 11254

This theorem is used by:  fv0p1e1  12368  zgt0ge1  12656  gtndiv  12679  nn0ind-raph  12702  1e0p1  12764  fz01en  13587  fz0dif1  13641  fz0tp  13663  fz0to3un2pr  13664  fz0sn0fz1  13680  fz0add1fz1  13771  elfzonlteqm1  13777  fzo0to2pr  13786  fz01pr  13787  fzo0to3tp  13788  elfz0lmr  13819  fldiv4p1lem1div2  13875  mulp1mod1  13954  expp1  14111  facp1  14321  faclbnd  14333  bcval5  14361  bcpasc  14364  hash1  14447  hashge2el2dif  14524  relexpsucl  15075  relexpsucr  15076  relexpaddg  15097  sgnneg  15144  binomlem  15890  isumnn0nn  15903  climcndslem1  15910  pwdif  15929  risefacval2  16071  fallfacval2  16072  risefac1  16093  fallfac1  16094  fallfacfwd  16096  bpolysum  16113  bpolydiflem  16114  bpoly2  16117  bpoly3  16118  bpoly4  16119  ege2le3  16150  ef4p  16175  eirrlem  16266  ruclem6  16297  p1modz1  16323  mod2eq1n2dvds  16411  nn0o1gt2  16445  pwp1fsum  16455  divalglem6  16462  bitsfzo  16499  pcfaclem  16964  4sqlem19  17029  vdwapun  17040  2exp16  17156  37prm  17187  631prm  17193  1259lem3  17199  1259lem4  17200  2503lem2  17204  4001lem1  17207  4001lem4  17210  chnub  18684  smndex2dnrinv  18983  gsummptfzsplitl  20009  ablsimpgfindlem1  20185  srgbinomlem4  20317  pzriprng1ALT  21657  psdmvr  22343  pmatcollpw3fi1lem1  22954  cpmadugsumlemF  23044  dvn1  26096  c1lip2  26168  dvply1  26456  iaa  26499  dvtaylp  26544  cos02pilt1  26702  advlogexp  26831  leibpi  27118  log2ublem3  27124  fsumharmonic  27187  lgamgulmlem2  27205  lgamcvg2  27230  bposlem1  27459  lgsne0  27510  gausslemma2dlem4  27544  lgsquadlem2  27556  axlowdimlem16  29318  wlkl1loop  29998  uhgrwkspthlem2  30114  crctcshwlkn0lem6  30175  wwlksn0s  30221  clwwlkccatlem  30351  umgr2cwwk2dif  30426  1wlkdlem4  30502  konigsberglem1  30614  konigsberglem2  30615  konigsberglem3  30616  numclwwlk5  30750  numclwwlk7  30753  nndiffz1  33142  f1ocnt  33156  nn0min  33176  0dp2dp  33239  wrdt2ind  33282  cshw1s2  33289  xrsmulgzz  33338  cyc2fv1  33450  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem7  33461  cyc3fv1  33466  cycpmrn  33472  vietadeg1  33977  vietalem  33978  cos9thpiminplylem2  34182  lmat22e12  34218  lmat22e21  34219  fib2  34801  spthcycl  35629  usgrgt2cycl  35630  subfacp1lem6  35685  subfacval2  35687  bccolsum  36239  poimirlem5  38304  poimirlem18  38317  poimirlem21  38320  poimirlem22  38321  poimirlem27  38326  poimirlem28  38327  areacirclem4  38390  420gcd8e4  42801  3lexlogpow5ineq1  42849  3lexlogpow5ineq5  42855  aks4d1p1  42871  sticksstones9  42949  sticksstones10  42950  aks6d1c6lem3  42967  fzsplit1nn0  43513  diophren  43568  jm2.17a  43715  jm2.17b  43716  k0004val0  44908  hashnzfz2  45059  bccn1  45082  dvradcnv2  45085  binomcxplemdvbinom  45091  binomcxplemnotnn0  45094  dvnmul  46685  stoweidlem26  46768  fourierdlem11  46860  fourierdlem24  46873  fourierdlem28  46877  fourierdlem30  46879  fourierdlem41  46890  fourierdlem60  46908  fourierdlem61  46909  fourierdlem73  46921  fourierdlem79  46927  fourierdlem81  46929  etransclem4  46980  etransclem24  47000  etransclem31  47007  etransclem32  47008  etransclem35  47011  ormklocald  47618  natlocalincr  47620  chnerlem1  47626  1fzopredsuc  48090  m1mod0mod1  48125  iccpartigtl  48200  iccpartltu  48202  iccpartgt  48204  iccpartgel  48206  fmtnorec2  48323  fmtno5lem1  48333  fmtnofac2  48349  fmtnofac1  48350  fmtno5faclem1  48359  2exp340mod341  48526  8exp8mod9  48529  gpgprismgriedgdmss  48845  gpg5edgnedg  48923  altgsumbcALT  49161  blen1  49392  blen1b  49396  nn0sumshdiglemA  49427  nn0sumshdiglemB  49428  nn0sumshdiglem1  49429  ackvalsuc0val  49495  ackval0012  49497