Theorem 0p1e1 12371

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 11196	. 2 ⊢ 1 ∈ ℂ
2	1	addlidi 11432	1 ⊢ (0 + 1) = 1

Syntax hints:   = wceq 1539  (class class class)co 7414  0cc0 11138  1c1 11139   + caddc 11141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-po 5574  df-so 5575  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-ltxr 11283

This theorem is referenced by:  fv0p1e1  12372  zgt0ge1  12656  gtndiv  12679  nn0ind-raph  12702  1e0p1  12759  fz01en  13575  fz0dif1  13629  fz0tp  13651  fz0to3un2pr  13652  fz0sn0fz1  13668  fz0add1fz1  13757  elfzonlteqm1  13763  fzo0to2pr  13772  fz01pr  13773  fzo0to3tp  13774  elfz0lmr  13804  fldiv4p1lem1div2  13858  mulp1mod1  13935  expp1  14092  facp1  14300  faclbnd  14312  bcval5  14340  bcpasc  14343  hash1  14426  hashge2el2dif  14502  relexpsucl  15053  relexpsucr  15054  relexpaddg  15075  binomlem  15848  isumnn0nn  15861  climcndslem1  15868  pwdif  15887  risefacval2  16029  fallfacval2  16030  risefac1  16052  fallfac1  16053  fallfacfwd  16055  bpolysum  16072  bpolydiflem  16073  bpoly2  16076  bpoly3  16077  bpoly4  16078  ege2le3  16109  ef4p  16132  eirrlem  16223  ruclem6  16254  p1modz1  16280  mod2eq1n2dvds  16367  nn0o1gt2  16401  pwp1fsum  16411  divalglem6  16418  bitsfzo  16455  pcfaclem  16919  4sqlem19  16984  vdwapun  16995  2exp16  17111  37prm  17141  631prm  17147  1259lem3  17153  1259lem4  17154  2503lem2  17158  4001lem1  17161  4001lem4  17164  smndex2dnrinv  18902  gsummptfzsplitl  19924  ablsimpgfindlem1  20100  srgbinomlem4  20199  pzriprng1ALT  21474  psdmvr  22140  pmatcollpw3fi1lem1  22759  cpmadugsumlemF  22849  dvn1  25917  c1lip2  25992  dvply1  26280  iaa  26322  dvtaylp  26367  cos02pilt1  26523  advlogexp  26652  leibpi  26940  log2ublem3  26946  fsumharmonic  27010  lgamgulmlem2  27028  lgamcvg2  27053  bposlem1  27283  lgsne0  27334  gausslemma2dlem4  27368  lgsquadlem2  27380  axlowdimlem16  28921  wlkl1loop  29603  uhgrwkspthlem2  29721  crctcshwlkn0lem6  29782  wwlksn0s  29828  clwwlkccatlem  29955  umgr2cwwk2dif  30030  1wlkdlem4  30106  konigsberglem1  30218  konigsberglem2  30219  konigsberglem3  30220  numclwwlk5  30354  numclwwlk7  30357  nndiffz1  32735  f1ocnt  32751  nn0min  32769  0dp2dp  32838  wrdt2ind  32885  cshw1s2  32892  chnub  32948  xrsmulgzz  32957  cyc2fv1  33087  cycpmco2lem4  33095  cycpmco2lem5  33096  cycpmco2lem7  33098  cyc3fv1  33103  cycpmrn  33109  lmat22e12  33759  lmat22e21  33760  fib2  34345  sgnneg  34484  spthcycl  35075  usgrgt2cycl  35076  subfacp1lem6  35131  subfacval2  35133  bccolsum  35680  poimirlem5  37573  poimirlem18  37586  poimirlem21  37589  poimirlem22  37590  poimirlem27  37595  poimirlem28  37596  areacirclem4  37659  420gcd8e4  41948  3lexlogpow5ineq1  41996  3lexlogpow5ineq5  42002  aks4d1p1  42018  sticksstones9  42096  sticksstones10  42097  aks6d1c6lem3  42114  metakunt2  42148  fzsplit1nn0  42710  diophren  42769  jm2.17a  42917  jm2.17b  42918  k0004val0  44112  hashnzfz2  44285  bccn1  44308  dvradcnv2  44311  binomcxplemdvbinom  44317  binomcxplemnotnn0  44320  dvnmul  45903  stoweidlem26  45986  fourierdlem11  46078  fourierdlem24  46091  fourierdlem28  46095  fourierdlem30  46097  fourierdlem41  46108  fourierdlem60  46126  fourierdlem61  46127  fourierdlem73  46139  fourierdlem79  46145  fourierdlem81  46147  etransclem4  46198  etransclem24  46218  etransclem31  46225  etransclem32  46226  etransclem35  46229  ormklocald  46834  natlocalincr  46836  1fzopredsuc  47282  m1mod0mod1  47302  iccpartigtl  47356  iccpartltu  47358  iccpartgt  47360  iccpartgel  47362  fmtnorec2  47476  fmtno5lem1  47486  fmtnofac2  47502  fmtnofac1  47503  fmtno5faclem1  47512  2exp340mod341  47666  8exp8mod9  47669  altgsumbcALT  48215  blen1  48451  blen1b  48455  nn0sumshdiglemA  48486  nn0sumshdiglemB  48487  nn0sumshdiglem1  48488  ackvalsuc0val  48554  ackval0012  48556