Theorem 0p1e1 12364

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 1534  (class class class)co 7420  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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  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 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-er 8724  df-en 8964  df-dom 8965  df-sdom 8966  df-pnf 11280  df-mnf 11281  df-ltxr 11283

This theorem is referenced by:  fv0p1e1  12365  zgt0ge1  12646  gtndiv  12669  nn0ind-raph  12692  1e0p1  12749  fz01en  13561  fz0tp  13634  fz0to3un2pr  13635  fz0sn0fz1  13650  fz0add1fz1  13734  elfzonlteqm1  13740  fzo0to2pr  13749  fzo0to3tp  13750  elfz0lmr  13779  fldiv4p1lem1div2  13832  mulp1mod1  13909  expp1  14065  facp1  14269  faclbnd  14281  bcval5  14309  bcpasc  14312  hash1  14395  hashge2el2dif  14473  relexpsucl  15010  relexpsucr  15011  relexpaddg  15032  binomlem  15807  isumnn0nn  15820  climcndslem1  15827  pwdif  15846  risefacval2  15986  fallfacval2  15987  risefac1  16009  fallfac1  16010  fallfacfwd  16012  bpolysum  16029  bpolydiflem  16030  bpoly2  16033  bpoly3  16034  bpoly4  16035  ege2le3  16066  ef4p  16089  eirrlem  16180  ruclem6  16211  p1modz1  16237  mod2eq1n2dvds  16323  nn0o1gt2  16357  pwp1fsum  16367  divalglem6  16374  bitsfzo  16409  pcfaclem  16866  4sqlem19  16931  vdwapun  16942  2exp16  17059  37prm  17089  631prm  17095  1259lem3  17101  1259lem4  17102  2503lem2  17106  4001lem1  17109  4001lem4  17112  smndex2dnrinv  18866  gsummptfzsplitl  19887  ablsimpgfindlem1  20063  srgbinomlem4  20168  pzriprng1ALT  21421  pmatcollpw3fi1lem1  22687  cpmadugsumlemF  22777  dvn1  25855  c1lip2  25930  dvply1  26217  iaa  26259  dvtaylp  26304  cos02pilt1  26459  advlogexp  26588  leibpi  26873  log2ublem3  26879  fsumharmonic  26943  lgamgulmlem2  26961  lgamcvg2  26986  bposlem1  27216  lgsne0  27267  gausslemma2dlem4  27301  lgsquadlem2  27313  axlowdimlem16  28767  wlkl1loop  29451  uhgrwkspthlem2  29567  crctcshwlkn0lem6  29625  wwlksn0s  29671  clwwlkccatlem  29798  umgr2cwwk2dif  29873  1wlkdlem4  29949  konigsberglem1  30061  konigsberglem2  30062  konigsberglem3  30063  numclwwlk5  30197  numclwwlk7  30200  nndiffz1  32554  f1ocnt  32570  nn0min  32583  0dp2dp  32632  wrdt2ind  32674  cshw1s2  32681  xrsmulgzz  32736  cyc2fv1  32842  cycpmco2lem4  32850  cycpmco2lem5  32851  cycpmco2lem7  32853  cyc3fv1  32858  cycpmrn  32864  lmat22e12  33420  lmat22e21  33421  fib2  34022  sgnneg  34160  spthcycl  34739  usgrgt2cycl  34740  subfacp1lem6  34795  subfacval2  34797  bccolsum  35333  poimirlem5  37098  poimirlem18  37111  poimirlem21  37114  poimirlem22  37115  poimirlem27  37120  poimirlem28  37121  areacirclem4  37184  420gcd8e4  41477  3lexlogpow5ineq1  41525  3lexlogpow5ineq5  41531  aks4d1p1  41547  sticksstones9  41626  sticksstones10  41627  aks6d1c6lem3  41644  metakunt2  41658  fzsplit1nn0  42174  diophren  42233  jm2.17a  42381  jm2.17b  42382  k0004val0  43584  hashnzfz2  43758  bccn1  43781  dvradcnv2  43784  binomcxplemdvbinom  43790  binomcxplemnotnn0  43793  dvnmul  45331  stoweidlem26  45414  fourierdlem11  45506  fourierdlem24  45519  fourierdlem28  45523  fourierdlem30  45525  fourierdlem41  45536  fourierdlem60  45554  fourierdlem61  45555  fourierdlem73  45567  fourierdlem79  45573  fourierdlem81  45575  etransclem4  45626  etransclem24  45646  etransclem31  45653  etransclem32  45654  etransclem35  45657  natlocalincr  46262  1fzopredsuc  46704  m1mod0mod1  46709  iccpartigtl  46763  iccpartltu  46765  iccpartgt  46767  iccpartgel  46769  fmtnorec2  46883  fmtno5lem1  46893  fmtnofac2  46909  fmtnofac1  46910  fmtno5faclem1  46919  2exp340mod341  47073  8exp8mod9  47076  altgsumbcALT  47417  blen1  47657  blen1b  47661  nn0sumshdiglemA  47692  nn0sumshdiglemB  47693  nn0sumshdiglem1  47694  ackvalsuc0val  47760  ackval0012  47762