Theorem 0p1e1 12418

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7409  0cc0 11157  1c1 11158   + caddc 11160

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-addrcl 11218  ax-mulcl 11219  ax-mulrcl 11220  ax-mulcom 11221  ax-addass 11222  ax-mulass 11223  ax-distr 11224  ax-i2m1 11225  ax-1ne0 11226  ax-1rid 11227  ax-rnegex 11228  ax-rrecex 11229  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232  ax-pre-ltadd 11233

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-ltxr 11305

This theorem is used by:  fv0p1e1  12419  zgt0ge1  12707  gtndiv  12731  nn0ind-raph  12754  1e0p1  12816  fz01en  13640  fz0dif1  13694  fz0tp  13716  fz0to3un2pr  13717  fz0sn0fz1  13733  fz0add1fz1  13824  elfzonlteqm1  13830  fzo0to2pr  13839  fz01pr  13840  fzo0to3tp  13841  elfz0lmr  13872  fldiv4p1lem1div2  13929  mulp1mod1  14008  expp1  14165  facp1  14375  faclbnd  14387  bcval5  14415  bcpasc  14418  hash1  14501  hashge2el2dif  14578  relexpsucl  15137  relexpsucr  15138  relexpaddg  15159  sgnneg  15206  binomlem  15951  isumnn0nn  15964  climcndslem1  15971  pwdif  15990  risefacval2  16130  fallfacval2  16131  risefac1  16152  fallfac1  16153  fallfacfwd  16155  bpolysum  16172  bpolydiflem  16173  bpoly2  16176  bpoly3  16177  bpoly4  16178  ege2le3  16209  ef4p  16234  eirrlem  16325  ruclem6  16356  p1modz1  16382  mod2eq1n2dvds  16470  nn0o1gt2  16504  pwp1fsum  16514  divalglem6  16521  bitsfzo  16558  pcfaclem  17023  4sqlem19  17088  vdwapun  17099  2exp16  17215  37prm  17246  631prm  17252  1259lem3  17258  1259lem4  17259  2503lem2  17263  4001lem1  17266  4001lem4  17269  chnub  18743  smndex2dnrinv  19061  gsummptfzsplitl  20094  ablsimpgfindlem1  20270  srgbinomlem4  20402  pzriprng1ALT  21749  psdmvr  22437  pmatcollpw3fi1lem1  23051  cpmadugsumlemF  23141  dvn1  26193  c1lip2  26265  dvply1  26554  iaaOLD  26601  dvtaylp  26646  cos02pilt1  26803  advlogexp  26932  leibpi  27219  log2ublem3  27225  fsumharmonic  27288  lgamgulmlem2  27306  lgamcvg2  27331  bposlem1  27560  lgsne0  27611  gausslemma2dlem4  27645  lgsquadlem2  27657  axlowdimlem16  29454  wlkl1loop  30137  uhgrwkspthlem2  30259  spthcycl  30311  crctcshwlkn0lem6  30323  wwlksn0s  30369  clwwlkccatlem  30499  umgr2cwwk2dif  30574  1wlkdlem4  30650  konigsberglem1  30772  konigsberglem2  30773  konigsberglem3  30774  numclwwlk5  30908  numclwwlk7  30911  nndiffz1  33297  f1ocnt  33311  nn0min  33331  0dp2dp  33394  wrdt2ind  33435  cshw1s2  33440  xrsmulgzz  33489  cyc2fv1  33601  cycpmco2lem4  33609  cycpmco2lem5  33610  cycpmco2lem7  33612  cyc3fv1  33617  cycpmrn  33623  vietadeg1  34129  vietalem  34130  cos9thpiminplylem2  34334  lmat22e12  34370  lmat22e21  34371  fib2  34954  usgrgt2cycl  35824  subfacp1lem6  35865  subfacval2  35867  bccolsum  36419  poimirlem5  38457  poimirlem18  38470  poimirlem21  38473  poimirlem22  38474  poimirlem27  38479  poimirlem28  38480  areacirclem4  38543  420gcd8e4  42970  3lexlogpow5ineq1  43018  3lexlogpow5ineq5  43024  aks4d1p1  43040  sticksstones9  43118  sticksstones10  43119  aks6d1c6lem3  43136  fzsplit1nn0  43697  diophren  43752  jm2.17a  43899  jm2.17b  43900  k0004val0  45092  hashnzfz2  45243  bccn1  45266  dvradcnv2  45269  binomcxplemdvbinom  45275  binomcxplemnotnn0  45278  dvnmul  46869  stoweidlem26  46952  fourierdlem11  47044  fourierdlem24  47057  fourierdlem28  47061  fourierdlem30  47063  fourierdlem41  47074  fourierdlem60  47092  fourierdlem61  47093  fourierdlem73  47105  fourierdlem79  47111  fourierdlem81  47113  etransclem4  47164  etransclem24  47184  etransclem31  47191  etransclem32  47192  etransclem35  47195  ormklocald  47802  chnerlem1  47808  1fzopredsuc  48311  m1mod0mod1  48346  iccpartigtl  48421  iccpartltu  48423  iccpartgt  48425  iccpartgel  48427  fmtnorec2  48544  fmtno5lem1  48554  fmtnofac2  48570  fmtnofac1  48571  fmtno5faclem1  48580  2exp340mod341  48747  8exp8mod9  48750  gpgprismgriedgdmss  49066  gpg5edgnedg  49144  altgsumbcALT  49381  blen1  49612  blen1b  49616  nn0sumshdiglemA  49647  nn0sumshdiglemB  49648  nn0sumshdiglem1  49649  ackvalsuc0val  49715  ackval0012  49717