Theorem 0p1e1 12264

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

Syntax hints:   = wceq 1542  (class class class)co 7358  0cc0 11028  1c1 11029   + caddc 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  fv0p1e1  12265  zgt0ge1  12548  gtndiv  12571  nn0ind-raph  12594  1e0p1  12651  fz01en  13470  fz0dif1  13524  fz0tp  13546  fz0to3un2pr  13547  fz0sn0fz1  13563  fz0add1fz1  13653  elfzonlteqm1  13659  fzo0to2pr  13668  fz01pr  13669  fzo0to3tp  13670  elfz0lmr  13701  fldiv4p1lem1div2  13757  mulp1mod1  13836  expp1  13993  facp1  14203  faclbnd  14215  bcval5  14243  bcpasc  14246  hash1  14329  hashge2el2dif  14405  relexpsucl  14956  relexpsucr  14957  relexpaddg  14978  binomlem  15754  isumnn0nn  15767  climcndslem1  15774  pwdif  15793  risefacval2  15935  fallfacval2  15936  risefac1  15958  fallfac1  15959  fallfacfwd  15961  bpolysum  15978  bpolydiflem  15979  bpoly2  15982  bpoly3  15983  bpoly4  15984  ege2le3  16015  ef4p  16040  eirrlem  16131  ruclem6  16162  p1modz1  16188  mod2eq1n2dvds  16276  nn0o1gt2  16310  pwp1fsum  16320  divalglem6  16327  bitsfzo  16364  pcfaclem  16828  4sqlem19  16893  vdwapun  16904  2exp16  17020  37prm  17050  631prm  17056  1259lem3  17062  1259lem4  17063  2503lem2  17067  4001lem1  17070  4001lem4  17073  chnub  18547  smndex2dnrinv  18842  gsummptfzsplitl  19864  ablsimpgfindlem1  20040  srgbinomlem4  20166  pzriprng1ALT  21453  psdmvr  22114  pmatcollpw3fi1lem1  22732  cpmadugsumlemF  22822  dvn1  25886  c1lip2  25961  dvply1  26249  iaa  26291  dvtaylp  26336  cos02pilt1  26493  advlogexp  26622  leibpi  26910  log2ublem3  26916  fsumharmonic  26980  lgamgulmlem2  26998  lgamcvg2  27023  bposlem1  27253  lgsne0  27304  gausslemma2dlem4  27338  lgsquadlem2  27350  axlowdimlem16  29011  wlkl1loop  29692  uhgrwkspthlem2  29808  crctcshwlkn0lem6  29869  wwlksn0s  29915  clwwlkccatlem  30045  umgr2cwwk2dif  30120  1wlkdlem4  30196  konigsberglem1  30308  konigsberglem2  30309  konigsberglem3  30310  numclwwlk5  30444  numclwwlk7  30447  nndiffz1  32845  f1ocnt  32859  nn0min  32880  sgnneg  32893  0dp2dp  32969  wrdt2ind  33014  cshw1s2  33021  xrsmulgzz  33070  cyc2fv1  33182  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem7  33193  cyc3fv1  33198  cycpmrn  33204  vietadeg1  33713  vietalem  33714  cos9thpiminplylem2  33919  lmat22e12  33955  lmat22e21  33956  fib2  34538  spthcycl  35302  usgrgt2cycl  35303  subfacp1lem6  35358  subfacval2  35360  bccolsum  35912  poimirlem5  37795  poimirlem18  37808  poimirlem21  37811  poimirlem22  37812  poimirlem27  37817  poimirlem28  37818  areacirclem4  37881  420gcd8e4  42295  3lexlogpow5ineq1  42343  3lexlogpow5ineq5  42349  aks4d1p1  42365  sticksstones9  42443  sticksstones10  42444  aks6d1c6lem3  42461  fzsplit1nn0  43033  diophren  43092  jm2.17a  43239  jm2.17b  43240  k0004val0  44432  hashnzfz2  44599  bccn1  44622  dvradcnv2  44625  binomcxplemdvbinom  44631  binomcxplemnotnn0  44634  dvnmul  46224  stoweidlem26  46307  fourierdlem11  46399  fourierdlem24  46412  fourierdlem28  46416  fourierdlem30  46418  fourierdlem41  46429  fourierdlem60  46447  fourierdlem61  46448  fourierdlem73  46460  fourierdlem79  46466  fourierdlem81  46468  etransclem4  46519  etransclem24  46539  etransclem31  46546  etransclem32  46547  etransclem35  46550  ormklocald  47155  natlocalincr  47157  chnerlem1  47163  1fzopredsuc  47607  m1mod0mod1  47637  iccpartigtl  47706  iccpartltu  47708  iccpartgt  47710  iccpartgel  47712  fmtnorec2  47826  fmtno5lem1  47836  fmtnofac2  47852  fmtnofac1  47853  fmtno5faclem1  47862  2exp340mod341  48016  8exp8mod9  48019  gpgprismgriedgdmss  48335  gpg5edgnedg  48413  altgsumbcALT  48636  blen1  48867  blen1b  48871  nn0sumshdiglemA  48902  nn0sumshdiglemB  48903  nn0sumshdiglem1  48904  ackvalsuc0val  48970  ackval0012  48972