Theorem 0p1e1 12287

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

Syntax hints:   = wceq 1542  (class class class)co 7356  0cc0 11027  1c1 11028   + caddc 11030

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

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 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-ltxr 11173

This theorem is referenced by:  fv0p1e1  12288  zgt0ge1  12572  gtndiv  12595  nn0ind-raph  12618  1e0p1  12675  fz01en  13495  fz0dif1  13549  fz0tp  13571  fz0to3un2pr  13572  fz0sn0fz1  13588  fz0add1fz1  13679  elfzonlteqm1  13685  fzo0to2pr  13694  fz01pr  13695  fzo0to3tp  13696  elfz0lmr  13727  fldiv4p1lem1div2  13783  mulp1mod1  13862  expp1  14019  facp1  14229  faclbnd  14241  bcval5  14269  bcpasc  14272  hash1  14355  hashge2el2dif  14431  relexpsucl  14982  relexpsucr  14983  relexpaddg  15004  binomlem  15783  isumnn0nn  15796  climcndslem1  15803  pwdif  15822  risefacval2  15964  fallfacval2  15965  risefac1  15987  fallfac1  15988  fallfacfwd  15990  bpolysum  16007  bpolydiflem  16008  bpoly2  16011  bpoly3  16012  bpoly4  16013  ege2le3  16044  ef4p  16069  eirrlem  16160  ruclem6  16191  p1modz1  16217  mod2eq1n2dvds  16305  nn0o1gt2  16339  pwp1fsum  16349  divalglem6  16356  bitsfzo  16393  pcfaclem  16858  4sqlem19  16923  vdwapun  16934  2exp16  17050  37prm  17080  631prm  17086  1259lem3  17092  1259lem4  17093  2503lem2  17097  4001lem1  17100  4001lem4  17103  chnub  18577  smndex2dnrinv  18875  gsummptfzsplitl  19897  ablsimpgfindlem1  20073  srgbinomlem4  20199  pzriprng1ALT  21465  psdmvr  22124  pmatcollpw3fi1lem1  22739  cpmadugsumlemF  22829  dvn1  25881  c1lip2  25953  dvply1  26238  iaa  26279  dvtaylp  26323  cos02pilt1  26478  advlogexp  26607  leibpi  26894  log2ublem3  26900  fsumharmonic  26963  lgamgulmlem2  26981  lgamcvg2  27006  bposlem1  27235  lgsne0  27286  gausslemma2dlem4  27320  lgsquadlem2  27332  axlowdimlem16  29014  wlkl1loop  29694  uhgrwkspthlem2  29810  crctcshwlkn0lem6  29871  wwlksn0s  29917  clwwlkccatlem  30047  umgr2cwwk2dif  30122  1wlkdlem4  30198  konigsberglem1  30310  konigsberglem2  30311  konigsberglem3  30312  numclwwlk5  30446  numclwwlk7  30449  nndiffz1  32847  f1ocnt  32861  nn0min  32882  sgnneg  32894  0dp2dp  32956  wrdt2ind  33001  cshw1s2  33008  xrsmulgzz  33057  cyc2fv1  33170  cycpmco2lem4  33178  cycpmco2lem5  33179  cycpmco2lem7  33181  cyc3fv1  33186  cycpmrn  33192  vietadeg1  33710  vietalem  33711  cos9thpiminplylem2  33915  lmat22e12  33951  lmat22e21  33952  fib2  34534  spthcycl  35299  usgrgt2cycl  35300  subfacp1lem6  35355  subfacval2  35357  bccolsum  35909  poimirlem5  37934  poimirlem18  37947  poimirlem21  37950  poimirlem22  37951  poimirlem27  37956  poimirlem28  37957  areacirclem4  38020  420gcd8e4  42433  3lexlogpow5ineq1  42481  3lexlogpow5ineq5  42487  aks4d1p1  42503  sticksstones9  42581  sticksstones10  42582  aks6d1c6lem3  42599  fzsplit1nn0  43174  diophren  43229  jm2.17a  43376  jm2.17b  43377  k0004val0  44569  hashnzfz2  44736  bccn1  44759  dvradcnv2  44762  binomcxplemdvbinom  44768  binomcxplemnotnn0  44771  dvnmul  46359  stoweidlem26  46442  fourierdlem11  46534  fourierdlem24  46547  fourierdlem28  46551  fourierdlem30  46553  fourierdlem41  46564  fourierdlem60  46582  fourierdlem61  46583  fourierdlem73  46595  fourierdlem79  46601  fourierdlem81  46603  etransclem4  46654  etransclem24  46674  etransclem31  46681  etransclem32  46682  etransclem35  46685  ormklocald  47292  natlocalincr  47294  chnerlem1  47300  1fzopredsuc  47761  m1mod0mod1  47796  iccpartigtl  47871  iccpartltu  47873  iccpartgt  47875  iccpartgel  47877  fmtnorec2  47994  fmtno5lem1  48004  fmtnofac2  48020  fmtnofac1  48021  fmtno5faclem1  48030  2exp340mod341  48197  8exp8mod9  48200  gpgprismgriedgdmss  48516  gpg5edgnedg  48594  altgsumbcALT  48817  blen1  49048  blen1b  49052  nn0sumshdiglemA  49083  nn0sumshdiglemB  49084  nn0sumshdiglem1  49085  ackvalsuc0val  49151  ackval0012  49153