Theorem 0p1e1 12000

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 10835	. 2 ⊢ 1 ∈ ℂ
2	1	addid2i 11068	1 ⊢ (0 + 1) = 1

Syntax hints:   = wceq 1543  (class class class)co 7252  0cc0 10777  1c1 10778   + caddc 10780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-addrcl 10838  ax-mulcl 10839  ax-mulrcl 10840  ax-mulcom 10841  ax-addass 10842  ax-mulass 10843  ax-distr 10844  ax-i2m1 10845  ax-1ne0 10846  ax-1rid 10847  ax-rnegex 10848  ax-rrecex 10849  ax-cnre 10850  ax-pre-lttri 10851  ax-pre-lttrn 10852  ax-pre-ltadd 10853

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5153  df-id 5479  df-po 5493  df-so 5494  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-er 8433  df-en 8669  df-dom 8670  df-sdom 8671  df-pnf 10917  df-mnf 10918  df-ltxr 10920

This theorem is referenced by:  fv0p1e1  12001  zgt0ge1  12279  gtndiv  12302  nn0ind-raph  12325  1e0p1  12383  fz01en  13188  fz0tp  13261  fz0to3un2pr  13262  fz0sn0fz1  13277  fz0add1fz1  13360  elfzonlteqm1  13366  fzo0to2pr  13375  fzo0to3tp  13376  elfz0lmr  13405  fldiv4p1lem1div2  13458  mulp1mod1  13535  expp1  13692  facp1  13895  faclbnd  13907  bcval5  13935  bcpasc  13938  hash1  14022  hashge2el2dif  14097  relexpsucl  14645  relexpsucr  14646  relexpaddg  14667  binomlem  15444  isumnn0nn  15457  climcndslem1  15464  pwdif  15483  risefacval2  15623  fallfacval2  15624  risefac1  15646  fallfac1  15647  fallfacfwd  15649  bpolysum  15666  bpolydiflem  15667  bpoly2  15670  bpoly3  15671  bpoly4  15672  ege2le3  15702  ef4p  15725  eirrlem  15816  ruclem6  15847  p1modz1  15873  mod2eq1n2dvds  15959  nn0o1gt2  15993  pwp1fsum  16003  divalglem6  16010  bitsfzo  16045  pcfaclem  16502  4sqlem19  16567  vdwapun  16578  2exp16  16695  37prm  16725  631prm  16731  1259lem3  16737  1259lem4  16738  2503lem2  16742  4001lem1  16745  4001lem4  16748  smndex2dnrinv  18444  gsummptfzsplitl  19424  ablsimpgfindlem1  19600  srgbinomlem4  19669  pmatcollpw3fi1lem1  21818  cpmadugsumlemF  21908  dvn1  24970  c1lip2  25042  dvply1  25324  iaa  25365  dvtaylp  25409  cos02pilt1  25562  advlogexp  25690  leibpi  25972  log2ublem3  25978  fsumharmonic  26041  lgamgulmlem2  26059  lgamcvg2  26084  bposlem1  26312  lgsne0  26363  gausslemma2dlem4  26397  lgsquadlem2  26409  axlowdimlem16  27203  wlkl1loop  27882  uhgrwkspthlem2  27998  crctcshwlkn0lem6  28056  wwlksn0s  28102  clwwlkccatlem  28229  umgr2cwwk2dif  28304  1wlkdlem4  28380  konigsberglem1  28492  konigsberglem2  28493  konigsberglem3  28494  numclwwlk5  28628  numclwwlk7  28631  nndiffz1  30984  f1ocnt  31000  nn0min  31011  0dp2dp  31060  wrdt2ind  31102  cshw1s2  31109  xrsmulgzz  31164  cyc2fv1  31265  cycpmco2lem4  31273  cycpmco2lem5  31274  cycpmco2lem7  31276  cyc3fv1  31281  cycpmrn  31287  lmat22e12  31646  lmat22e21  31647  fib2  32244  sgnneg  32382  spthcycl  32966  usgrgt2cycl  32967  subfacp1lem6  33022  subfacval2  33024  bccolsum  33586  poimirlem5  35688  poimirlem18  35701  poimirlem21  35704  poimirlem22  35705  poimirlem27  35710  poimirlem28  35711  areacirclem4  35774  420gcd8e4  39921  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1  39990  sticksstones9  40010  sticksstones10  40011  metakunt2  40026  fzsplit1nn0  40464  diophren  40523  jm2.17a  40670  jm2.17b  40671  k0004val0  41626  hashnzfz2  41801  bccn1  41824  dvradcnv2  41827  binomcxplemdvbinom  41833  binomcxplemnotnn0  41836  dvnmul  43347  stoweidlem26  43430  fourierdlem11  43522  fourierdlem24  43535  fourierdlem28  43539  fourierdlem30  43541  fourierdlem41  43552  fourierdlem60  43570  fourierdlem61  43571  fourierdlem73  43583  fourierdlem79  43589  fourierdlem81  43591  etransclem4  43642  etransclem24  43662  etransclem31  43669  etransclem32  43670  etransclem35  43673  1fzopredsuc  44677  m1mod0mod1  44682  iccpartigtl  44736  iccpartltu  44738  iccpartgt  44740  iccpartgel  44742  fmtnorec2  44856  fmtno5lem1  44866  fmtnofac2  44882  fmtnofac1  44883  fmtno5faclem1  44892  2exp340mod341  45046  8exp8mod9  45049  altgsumbcALT  45550  blen1  45791  blen1b  45795  nn0sumshdiglemA  45826  nn0sumshdiglemB  45827  nn0sumshdiglem1  45828  ackvalsuc0val  45894  ackval0012  45896