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

Syntax hints:   = wceq 1540  (class class class)co 7410  0cc0 11134  1c1 11135   + caddc 11137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-ltxr 11279

This theorem is referenced by:  fv0p1e1  12368  zgt0ge1  12652  gtndiv  12675  nn0ind-raph  12698  1e0p1  12755  fz01en  13574  fz0dif1  13628  fz0tp  13650  fz0to3un2pr  13651  fz0sn0fz1  13667  fz0add1fz1  13756  elfzonlteqm1  13762  fzo0to2pr  13771  fz01pr  13772  fzo0to3tp  13773  elfz0lmr  13803  fldiv4p1lem1div2  13857  mulp1mod1  13934  expp1  14091  facp1  14301  faclbnd  14313  bcval5  14341  bcpasc  14344  hash1  14427  hashge2el2dif  14503  relexpsucl  15055  relexpsucr  15056  relexpaddg  15077  binomlem  15850  isumnn0nn  15863  climcndslem1  15870  pwdif  15889  risefacval2  16031  fallfacval2  16032  risefac1  16054  fallfac1  16055  fallfacfwd  16057  bpolysum  16074  bpolydiflem  16075  bpoly2  16078  bpoly3  16079  bpoly4  16080  ege2le3  16111  ef4p  16136  eirrlem  16227  ruclem6  16258  p1modz1  16284  mod2eq1n2dvds  16371  nn0o1gt2  16405  pwp1fsum  16415  divalglem6  16422  bitsfzo  16459  pcfaclem  16923  4sqlem19  16988  vdwapun  16999  2exp16  17115  37prm  17145  631prm  17151  1259lem3  17157  1259lem4  17158  2503lem2  17162  4001lem1  17165  4001lem4  17168  smndex2dnrinv  18898  gsummptfzsplitl  19919  ablsimpgfindlem1  20095  srgbinomlem4  20194  pzriprng1ALT  21462  psdmvr  22112  pmatcollpw3fi1lem1  22729  cpmadugsumlemF  22819  dvn1  25885  c1lip2  25960  dvply1  26248  iaa  26290  dvtaylp  26335  cos02pilt1  26492  advlogexp  26621  leibpi  26909  log2ublem3  26915  fsumharmonic  26979  lgamgulmlem2  26997  lgamcvg2  27022  bposlem1  27252  lgsne0  27303  gausslemma2dlem4  27337  lgsquadlem2  27349  axlowdimlem16  28941  wlkl1loop  29623  uhgrwkspthlem2  29741  crctcshwlkn0lem6  29802  wwlksn0s  29848  clwwlkccatlem  29975  umgr2cwwk2dif  30050  1wlkdlem4  30126  konigsberglem1  30238  konigsberglem2  30239  konigsberglem3  30240  numclwwlk5  30374  numclwwlk7  30377  nndiffz1  32768  f1ocnt  32784  nn0min  32804  sgnneg  32817  0dp2dp  32888  wrdt2ind  32934  cshw1s2  32941  chnub  32997  xrsmulgzz  33006  cyc2fv1  33137  cycpmco2lem4  33145  cycpmco2lem5  33146  cycpmco2lem7  33148  cyc3fv1  33153  cycpmrn  33159  cos9thpiminplylem2  33822  lmat22e12  33855  lmat22e21  33856  fib2  34439  spthcycl  35156  usgrgt2cycl  35157  subfacp1lem6  35212  subfacval2  35214  bccolsum  35761  poimirlem5  37654  poimirlem18  37667  poimirlem21  37670  poimirlem22  37671  poimirlem27  37676  poimirlem28  37677  areacirclem4  37740  420gcd8e4  42024  3lexlogpow5ineq1  42072  3lexlogpow5ineq5  42078  aks4d1p1  42094  sticksstones9  42172  sticksstones10  42173  aks6d1c6lem3  42190  fzsplit1nn0  42752  diophren  42811  jm2.17a  42959  jm2.17b  42960  k0004val0  44153  hashnzfz2  44320  bccn1  44343  dvradcnv2  44346  binomcxplemdvbinom  44352  binomcxplemnotnn0  44355  dvnmul  45952  stoweidlem26  46035  fourierdlem11  46127  fourierdlem24  46140  fourierdlem28  46144  fourierdlem30  46146  fourierdlem41  46157  fourierdlem60  46175  fourierdlem61  46176  fourierdlem73  46188  fourierdlem79  46194  fourierdlem81  46196  etransclem4  46247  etransclem24  46267  etransclem31  46274  etransclem32  46275  etransclem35  46278  ormklocald  46883  natlocalincr  46885  1fzopredsuc  47333  m1mod0mod1  47363  iccpartigtl  47417  iccpartltu  47419  iccpartgt  47421  iccpartgel  47423  fmtnorec2  47537  fmtno5lem1  47547  fmtnofac2  47563  fmtnofac1  47564  fmtno5faclem1  47573  2exp340mod341  47727  8exp8mod9  47730  gpgprismgriedgdmss  48036  altgsumbcALT  48308  blen1  48544  blen1b  48548  nn0sumshdiglemA  48579  nn0sumshdiglemB  48580  nn0sumshdiglem1  48581  ackvalsuc0val  48647  ackval0012  48649