Theorem 0p1e1 12266

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

Syntax hints:   = wceq 1542  (class class class)co 7360  0cc0 11030  1c1 11031   + caddc 11033

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 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  fv0p1e1  12267  zgt0ge1  12550  gtndiv  12573  nn0ind-raph  12596  1e0p1  12653  fz01en  13472  fz0dif1  13526  fz0tp  13548  fz0to3un2pr  13549  fz0sn0fz1  13565  fz0add1fz1  13655  elfzonlteqm1  13661  fzo0to2pr  13670  fz01pr  13671  fzo0to3tp  13672  elfz0lmr  13703  fldiv4p1lem1div2  13759  mulp1mod1  13838  expp1  13995  facp1  14205  faclbnd  14217  bcval5  14245  bcpasc  14248  hash1  14331  hashge2el2dif  14407  relexpsucl  14958  relexpsucr  14959  relexpaddg  14980  binomlem  15756  isumnn0nn  15769  climcndslem1  15776  pwdif  15795  risefacval2  15937  fallfacval2  15938  risefac1  15960  fallfac1  15961  fallfacfwd  15963  bpolysum  15980  bpolydiflem  15981  bpoly2  15984  bpoly3  15985  bpoly4  15986  ege2le3  16017  ef4p  16042  eirrlem  16133  ruclem6  16164  p1modz1  16190  mod2eq1n2dvds  16278  nn0o1gt2  16312  pwp1fsum  16322  divalglem6  16329  bitsfzo  16366  pcfaclem  16830  4sqlem19  16895  vdwapun  16906  2exp16  17022  37prm  17052  631prm  17058  1259lem3  17064  1259lem4  17065  2503lem2  17069  4001lem1  17072  4001lem4  17075  chnub  18549  smndex2dnrinv  18844  gsummptfzsplitl  19866  ablsimpgfindlem1  20042  srgbinomlem4  20168  pzriprng1ALT  21455  psdmvr  22116  pmatcollpw3fi1lem1  22734  cpmadugsumlemF  22824  dvn1  25888  c1lip2  25963  dvply1  26251  iaa  26293  dvtaylp  26338  cos02pilt1  26495  advlogexp  26624  leibpi  26912  log2ublem3  26918  fsumharmonic  26982  lgamgulmlem2  27000  lgamcvg2  27025  bposlem1  27255  lgsne0  27306  gausslemma2dlem4  27340  lgsquadlem2  27352  axlowdimlem16  29034  wlkl1loop  29715  uhgrwkspthlem2  29831  crctcshwlkn0lem6  29892  wwlksn0s  29938  clwwlkccatlem  30068  umgr2cwwk2dif  30143  1wlkdlem4  30219  konigsberglem1  30331  konigsberglem2  30332  konigsberglem3  30333  numclwwlk5  30467  numclwwlk7  30470  nndiffz1  32868  f1ocnt  32882  nn0min  32903  sgnneg  32916  0dp2dp  32992  wrdt2ind  33037  cshw1s2  33044  xrsmulgzz  33093  cyc2fv1  33205  cycpmco2lem4  33213  cycpmco2lem5  33214  cycpmco2lem7  33216  cyc3fv1  33221  cycpmrn  33227  vietadeg1  33736  vietalem  33737  cos9thpiminplylem2  33942  lmat22e12  33978  lmat22e21  33979  fib2  34561  spthcycl  35325  usgrgt2cycl  35326  subfacp1lem6  35381  subfacval2  35383  bccolsum  35935  poimirlem5  37828  poimirlem18  37841  poimirlem21  37844  poimirlem22  37845  poimirlem27  37850  poimirlem28  37851  areacirclem4  37914  420gcd8e4  42328  3lexlogpow5ineq1  42376  3lexlogpow5ineq5  42382  aks4d1p1  42398  sticksstones9  42476  sticksstones10  42477  aks6d1c6lem3  42494  fzsplit1nn0  43063  diophren  43122  jm2.17a  43269  jm2.17b  43270  k0004val0  44462  hashnzfz2  44629  bccn1  44652  dvradcnv2  44655  binomcxplemdvbinom  44661  binomcxplemnotnn0  44664  dvnmul  46254  stoweidlem26  46337  fourierdlem11  46429  fourierdlem24  46442  fourierdlem28  46446  fourierdlem30  46448  fourierdlem41  46459  fourierdlem60  46477  fourierdlem61  46478  fourierdlem73  46490  fourierdlem79  46496  fourierdlem81  46498  etransclem4  46549  etransclem24  46569  etransclem31  46576  etransclem32  46577  etransclem35  46580  ormklocald  47185  natlocalincr  47187  chnerlem1  47193  1fzopredsuc  47637  m1mod0mod1  47667  iccpartigtl  47736  iccpartltu  47738  iccpartgt  47740  iccpartgel  47742  fmtnorec2  47856  fmtno5lem1  47866  fmtnofac2  47882  fmtnofac1  47883  fmtno5faclem1  47892  2exp340mod341  48046  8exp8mod9  48049  gpgprismgriedgdmss  48365  gpg5edgnedg  48443  altgsumbcALT  48666  blen1  48897  blen1b  48901  nn0sumshdiglemA  48932  nn0sumshdiglemB  48933  nn0sumshdiglem1  48934  ackvalsuc0val  49000  ackval0012  49002