Theorem 0p1e1 12463

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7420  0cc0 11200  1c1 11201   + caddc 11203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348

This theorem is used by:  fv0p1e1  12464  zgt0ge1  12752  gtndiv  12776  nn0ind-raph  12799  1e0p1  12861  fz01en  13686  fz0dif1  13740  fz0tp  13762  fz0to3un2pr  13763  fz0sn0fz1  13779  fz0add1fz1  13870  elfzonlteqm1  13876  fzo0to2pr  13885  fz01pr  13886  fzo0to3tp  13887  elfz0lmr  13918  fldiv4p1lem1div2  13975  mulp1mod1  14054  expp1  14211  facp1  14422  faclbnd  14434  bcval5  14462  bcpasc  14465  hash1  14548  hashge2el2dif  14625  relexpsucl  15184  relexpsucr  15185  relexpaddg  15206  sgnneg  15253  binomlem  15998  isumnn0nn  16011  climcndslem1  16018  pwdif  16037  risefacval2  16177  fallfacval2  16178  risefac1  16199  fallfac1  16200  fallfacfwd  16202  bpolysum  16219  bpolydiflem  16220  bpoly2  16223  bpoly3  16224  bpoly4  16225  ege2le3  16256  ef4p  16281  eirrlem  16372  ruclem6  16403  p1modz1  16429  mod2eq1n2dvds  16517  nn0o1gt2  16551  pwp1fsum  16561  divalglem6  16568  bitsfzo  16605  pcfaclem  17076  4sqlem19  17141  vdwapun  17152  2exp16  17268  37prm  17299  631prm  17305  1259lem3  17311  1259lem4  17312  2503lem2  17316  4001lem1  17319  4001lem4  17322  chnub  18796  smndex2dnrinv  19114  gsummptfzsplitl  20147  ablsimpgfindlem1  20323  srgbinomlem4  20455  pzriprng1ALT  21802  psdmvr  22490  pmatcollpw3fi1lem1  23104  cpmadugsumlemF  23194  dvn1  26246  c1lip2  26318  dvply1  26605  iaaOLD  26652  dvtaylp  26697  cos02pilt1  26854  advlogexp  26983  leibpi  27270  log2ublem3  27276  fsumharmonic  27339  lgamgulmlem2  27357  lgamcvg2  27382  bposlem1  27611  lgsne0  27662  gausslemma2dlem4  27696  lgsquadlem2  27708  axlowdimlem16  29535  wlkl1loop  30218  uhgrwkspthlem2  30340  spthcycl  30392  crctcshwlkn0lem6  30404  wwlksn0s  30450  clwwlkccatlem  30580  umgr2cwwk2dif  30655  1wlkdlem4  30731  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  numclwwlk5  30989  numclwwlk7  30992  nndiffz1  33420  f1ocnt  33434  nn0min  33454  0dp2dp  33517  wrdt2ind  33558  cshw1s2  33563  xrsmulgzz  33612  cyc2fv1  33724  cycpmco2lem4  33732  cycpmco2lem5  33733  cycpmco2lem7  33735  cyc3fv1  33740  cycpmrn  33746  vietadeg1  34252  vietalem  34253  cos9thpiminplylem2  34457  lmat22e12  34493  lmat22e21  34494  fib2  35076  usgrgt2cycl  35951  subfacp1lem6  35992  subfacval2  35994  bccolsum  36546  poimirlem5  38586  poimirlem18  38599  poimirlem21  38602  poimirlem22  38603  poimirlem27  38608  poimirlem28  38609  areacirclem4  38672  420gcd8e4  43099  3lexlogpow5ineq1  43147  3lexlogpow5ineq5  43153  aks4d1p1  43169  sticksstones9  43247  sticksstones10  43248  aks6d1c6lem3  43265  fzsplit1nn0  43807  diophren  43862  jm2.17a  44009  jm2.17b  44010  k0004val0  45196  hashnzfz2  45347  bccn1  45370  dvradcnv2  45373  binomcxplemdvbinom  45379  binomcxplemnotnn0  45382  dvnmul  46995  stoweidlem26  47078  fourierdlem11  47170  fourierdlem24  47183  fourierdlem28  47187  fourierdlem30  47189  fourierdlem41  47200  fourierdlem60  47218  fourierdlem61  47219  fourierdlem73  47231  fourierdlem79  47237  fourierdlem81  47239  etransclem4  47290  etransclem24  47310  etransclem31  47317  etransclem32  47318  etransclem35  47321  ormklocald  47928  chnerlem1  47934  1fzopredsuc  48437  m1mod0mod1  48472  iccpartigtl  48547  iccpartltu  48549  iccpartgt  48551  iccpartgel  48553  fmtnorec2  48670  fmtno5lem1  48680  fmtnofac2  48696  fmtnofac1  48697  fmtno5faclem1  48706  2exp340mod341  48873  8exp8mod9  48876  gpgprismgriedgdmss  49192  gpg5edgnedg  49270  altgsumbcALT  49507  blen1  49738  blen1b  49742  nn0sumshdiglemA  49773  nn0sumshdiglemB  49774  nn0sumshdiglem1  49775  ackvalsuc0val  49841  ackval0012  49843