Theorem 0p1e1 12276

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

Syntax hints:   = wceq 1542  (class class class)co 7370  0cc0 11040  1c1 11041   + caddc 11043

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 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116

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 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-ltxr 11185

This theorem is referenced by:  fv0p1e1  12277  zgt0ge1  12560  gtndiv  12583  nn0ind-raph  12606  1e0p1  12663  fz01en  13482  fz0dif1  13536  fz0tp  13558  fz0to3un2pr  13559  fz0sn0fz1  13575  fz0add1fz1  13665  elfzonlteqm1  13671  fzo0to2pr  13680  fz01pr  13681  fzo0to3tp  13682  elfz0lmr  13713  fldiv4p1lem1div2  13769  mulp1mod1  13848  expp1  14005  facp1  14215  faclbnd  14227  bcval5  14255  bcpasc  14258  hash1  14341  hashge2el2dif  14417  relexpsucl  14968  relexpsucr  14969  relexpaddg  14990  binomlem  15766  isumnn0nn  15779  climcndslem1  15786  pwdif  15805  risefacval2  15947  fallfacval2  15948  risefac1  15970  fallfac1  15971  fallfacfwd  15973  bpolysum  15990  bpolydiflem  15991  bpoly2  15994  bpoly3  15995  bpoly4  15996  ege2le3  16027  ef4p  16052  eirrlem  16143  ruclem6  16174  p1modz1  16200  mod2eq1n2dvds  16288  nn0o1gt2  16322  pwp1fsum  16332  divalglem6  16339  bitsfzo  16376  pcfaclem  16840  4sqlem19  16905  vdwapun  16916  2exp16  17032  37prm  17062  631prm  17068  1259lem3  17074  1259lem4  17075  2503lem2  17079  4001lem1  17082  4001lem4  17085  chnub  18559  smndex2dnrinv  18857  gsummptfzsplitl  19879  ablsimpgfindlem1  20055  srgbinomlem4  20181  pzriprng1ALT  21468  psdmvr  22129  pmatcollpw3fi1lem1  22747  cpmadugsumlemF  22837  dvn1  25901  c1lip2  25976  dvply1  26264  iaa  26306  dvtaylp  26351  cos02pilt1  26508  advlogexp  26637  leibpi  26925  log2ublem3  26931  fsumharmonic  26995  lgamgulmlem2  27013  lgamcvg2  27038  bposlem1  27268  lgsne0  27319  gausslemma2dlem4  27353  lgsquadlem2  27365  axlowdimlem16  29048  wlkl1loop  29729  uhgrwkspthlem2  29845  crctcshwlkn0lem6  29906  wwlksn0s  29952  clwwlkccatlem  30082  umgr2cwwk2dif  30157  1wlkdlem4  30233  konigsberglem1  30345  konigsberglem2  30346  konigsberglem3  30347  numclwwlk5  30481  numclwwlk7  30484  nndiffz1  32883  f1ocnt  32897  nn0min  32918  sgnneg  32931  0dp2dp  33007  wrdt2ind  33052  cshw1s2  33059  xrsmulgzz  33108  cyc2fv1  33221  cycpmco2lem4  33229  cycpmco2lem5  33230  cycpmco2lem7  33232  cyc3fv1  33237  cycpmrn  33243  vietadeg1  33761  vietalem  33762  cos9thpiminplylem2  33967  lmat22e12  34003  lmat22e21  34004  fib2  34586  spthcycl  35351  usgrgt2cycl  35352  subfacp1lem6  35407  subfacval2  35409  bccolsum  35961  poimirlem5  37905  poimirlem18  37918  poimirlem21  37921  poimirlem22  37922  poimirlem27  37927  poimirlem28  37928  areacirclem4  37991  420gcd8e4  42405  3lexlogpow5ineq1  42453  3lexlogpow5ineq5  42459  aks4d1p1  42475  sticksstones9  42553  sticksstones10  42554  aks6d1c6lem3  42571  fzsplit1nn0  43140  diophren  43199  jm2.17a  43346  jm2.17b  43347  k0004val0  44539  hashnzfz2  44706  bccn1  44729  dvradcnv2  44732  binomcxplemdvbinom  44738  binomcxplemnotnn0  44741  dvnmul  46330  stoweidlem26  46413  fourierdlem11  46505  fourierdlem24  46518  fourierdlem28  46522  fourierdlem30  46524  fourierdlem41  46535  fourierdlem60  46553  fourierdlem61  46554  fourierdlem73  46566  fourierdlem79  46572  fourierdlem81  46574  etransclem4  46625  etransclem24  46645  etransclem31  46652  etransclem32  46653  etransclem35  46656  ormklocald  47261  natlocalincr  47263  chnerlem1  47269  1fzopredsuc  47713  m1mod0mod1  47743  iccpartigtl  47812  iccpartltu  47814  iccpartgt  47816  iccpartgel  47818  fmtnorec2  47932  fmtno5lem1  47942  fmtnofac2  47958  fmtnofac1  47959  fmtno5faclem1  47968  2exp340mod341  48122  8exp8mod9  48125  gpgprismgriedgdmss  48441  gpg5edgnedg  48519  altgsumbcALT  48742  blen1  48973  blen1b  48977  nn0sumshdiglemA  49008  nn0sumshdiglemB  49009  nn0sumshdiglem1  49010  ackvalsuc0val  49076  ackval0012  49078