Theorem 0p1e1 12242

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

Syntax hints:   = wceq 1541  (class class class)co 7346  0cc0 11006  1c1 11007   + caddc 11009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151

This theorem is referenced by:  fv0p1e1  12243  zgt0ge1  12527  gtndiv  12550  nn0ind-raph  12573  1e0p1  12630  fz01en  13452  fz0dif1  13506  fz0tp  13528  fz0to3un2pr  13529  fz0sn0fz1  13545  fz0add1fz1  13635  elfzonlteqm1  13641  fzo0to2pr  13650  fz01pr  13651  fzo0to3tp  13652  elfz0lmr  13683  fldiv4p1lem1div2  13739  mulp1mod1  13818  expp1  13975  facp1  14185  faclbnd  14197  bcval5  14225  bcpasc  14228  hash1  14311  hashge2el2dif  14387  relexpsucl  14938  relexpsucr  14939  relexpaddg  14960  binomlem  15736  isumnn0nn  15749  climcndslem1  15756  pwdif  15775  risefacval2  15917  fallfacval2  15918  risefac1  15940  fallfac1  15941  fallfacfwd  15943  bpolysum  15960  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  bpoly4  15966  ege2le3  15997  ef4p  16022  eirrlem  16113  ruclem6  16144  p1modz1  16170  mod2eq1n2dvds  16258  nn0o1gt2  16292  pwp1fsum  16302  divalglem6  16309  bitsfzo  16346  pcfaclem  16810  4sqlem19  16875  vdwapun  16886  2exp16  17002  37prm  17032  631prm  17038  1259lem3  17044  1259lem4  17045  2503lem2  17049  4001lem1  17052  4001lem4  17055  chnub  18528  smndex2dnrinv  18823  gsummptfzsplitl  19845  ablsimpgfindlem1  20021  srgbinomlem4  20147  pzriprng1ALT  21433  psdmvr  22084  pmatcollpw3fi1lem1  22701  cpmadugsumlemF  22791  dvn1  25855  c1lip2  25930  dvply1  26218  iaa  26260  dvtaylp  26305  cos02pilt1  26462  advlogexp  26591  leibpi  26879  log2ublem3  26885  fsumharmonic  26949  lgamgulmlem2  26967  lgamcvg2  26992  bposlem1  27222  lgsne0  27273  gausslemma2dlem4  27307  lgsquadlem2  27319  axlowdimlem16  28935  wlkl1loop  29616  uhgrwkspthlem2  29732  crctcshwlkn0lem6  29793  wwlksn0s  29839  clwwlkccatlem  29969  umgr2cwwk2dif  30044  1wlkdlem4  30120  konigsberglem1  30232  konigsberglem2  30233  konigsberglem3  30234  numclwwlk5  30368  numclwwlk7  30371  nndiffz1  32769  f1ocnt  32782  nn0min  32803  sgnneg  32816  0dp2dp  32889  wrdt2ind  32934  cshw1s2  32941  xrsmulgzz  32990  cyc2fv1  33090  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem7  33101  cyc3fv1  33106  cycpmrn  33112  cos9thpiminplylem2  33796  lmat22e12  33832  lmat22e21  33833  fib2  34415  spthcycl  35173  usgrgt2cycl  35174  subfacp1lem6  35229  subfacval2  35231  bccolsum  35783  poimirlem5  37664  poimirlem18  37677  poimirlem21  37680  poimirlem22  37681  poimirlem27  37686  poimirlem28  37687  areacirclem4  37750  420gcd8e4  42098  3lexlogpow5ineq1  42146  3lexlogpow5ineq5  42152  aks4d1p1  42168  sticksstones9  42246  sticksstones10  42247  aks6d1c6lem3  42264  fzsplit1nn0  42846  diophren  42905  jm2.17a  43052  jm2.17b  43053  k0004val0  44246  hashnzfz2  44413  bccn1  44436  dvradcnv2  44439  binomcxplemdvbinom  44445  binomcxplemnotnn0  44448  dvnmul  46040  stoweidlem26  46123  fourierdlem11  46215  fourierdlem24  46228  fourierdlem28  46232  fourierdlem30  46234  fourierdlem41  46245  fourierdlem60  46263  fourierdlem61  46264  fourierdlem73  46276  fourierdlem79  46282  fourierdlem81  46284  etransclem4  46335  etransclem24  46355  etransclem31  46362  etransclem32  46363  etransclem35  46366  ormklocald  46971  natlocalincr  46973  chnerlem1  46979  1fzopredsuc  47423  m1mod0mod1  47453  iccpartigtl  47522  iccpartltu  47524  iccpartgt  47526  iccpartgel  47528  fmtnorec2  47642  fmtno5lem1  47652  fmtnofac2  47668  fmtnofac1  47669  fmtno5faclem1  47678  2exp340mod341  47832  8exp8mod9  47835  gpgprismgriedgdmss  48151  gpg5edgnedg  48229  altgsumbcALT  48452  blen1  48684  blen1b  48688  nn0sumshdiglemA  48719  nn0sumshdiglemB  48720  nn0sumshdiglem1  48721  ackvalsuc0val  48787  ackval0012  48789