Theorem 0p1e1 12295

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

Syntax hints:   = wceq 1542  (class class class)co 7364  0cc0 11035  1c1 11036   + caddc 11038

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 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-po 5536  df-so 5537  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7367  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-ltxr 11181

This theorem is referenced by:  fv0p1e1  12296  zgt0ge1  12580  gtndiv  12603  nn0ind-raph  12626  1e0p1  12683  fz01en  13503  fz0dif1  13557  fz0tp  13579  fz0to3un2pr  13580  fz0sn0fz1  13596  fz0add1fz1  13687  elfzonlteqm1  13693  fzo0to2pr  13702  fz01pr  13703  fzo0to3tp  13704  elfz0lmr  13735  fldiv4p1lem1div2  13791  mulp1mod1  13870  expp1  14027  facp1  14237  faclbnd  14249  bcval5  14277  bcpasc  14280  hash1  14363  hashge2el2dif  14439  relexpsucl  14990  relexpsucr  14991  relexpaddg  15012  binomlem  15791  isumnn0nn  15804  climcndslem1  15811  pwdif  15830  risefacval2  15972  fallfacval2  15973  risefac1  15995  fallfac1  15996  fallfacfwd  15998  bpolysum  16015  bpolydiflem  16016  bpoly2  16019  bpoly3  16020  bpoly4  16021  ege2le3  16052  ef4p  16077  eirrlem  16168  ruclem6  16199  p1modz1  16225  mod2eq1n2dvds  16313  nn0o1gt2  16347  pwp1fsum  16357  divalglem6  16364  bitsfzo  16401  pcfaclem  16866  4sqlem19  16931  vdwapun  16942  2exp16  17058  37prm  17088  631prm  17094  1259lem3  17100  1259lem4  17101  2503lem2  17105  4001lem1  17108  4001lem4  17111  chnub  18585  smndex2dnrinv  18883  gsummptfzsplitl  19905  ablsimpgfindlem1  20081  srgbinomlem4  20207  pzriprng1ALT  21492  psdmvr  22151  pmatcollpw3fi1lem1  22767  cpmadugsumlemF  22857  dvn1  25909  c1lip2  25981  dvply1  26266  iaa  26308  dvtaylp  26353  cos02pilt1  26509  advlogexp  26638  leibpi  26925  log2ublem3  26931  fsumharmonic  26995  lgamgulmlem2  27013  lgamcvg2  27038  bposlem1  27267  lgsne0  27318  gausslemma2dlem4  27352  lgsquadlem2  27364  axlowdimlem16  29046  wlkl1loop  29727  uhgrwkspthlem2  29843  crctcshwlkn0lem6  29904  wwlksn0s  29950  clwwlkccatlem  30080  umgr2cwwk2dif  30155  1wlkdlem4  30231  konigsberglem1  30343  konigsberglem2  30344  konigsberglem3  30345  numclwwlk5  30479  numclwwlk7  30482  nndiffz1  32880  f1ocnt  32894  nn0min  32915  sgnneg  32927  0dp2dp  32989  wrdt2ind  33034  cshw1s2  33041  xrsmulgzz  33090  cyc2fv1  33203  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem7  33214  cyc3fv1  33219  cycpmrn  33225  vietadeg1  33743  vietalem  33744  cos9thpiminplylem2  33949  lmat22e12  33985  lmat22e21  33986  fib2  34568  spthcycl  35333  usgrgt2cycl  35334  subfacp1lem6  35389  subfacval2  35391  bccolsum  35943  poimirlem5  37968  poimirlem18  37981  poimirlem21  37984  poimirlem22  37985  poimirlem27  37990  poimirlem28  37991  areacirclem4  38054  420gcd8e4  42467  3lexlogpow5ineq1  42515  3lexlogpow5ineq5  42521  aks4d1p1  42537  sticksstones9  42615  sticksstones10  42616  aks6d1c6lem3  42633  fzsplit1nn0  43208  diophren  43267  jm2.17a  43414  jm2.17b  43415  k0004val0  44607  hashnzfz2  44774  bccn1  44797  dvradcnv2  44800  binomcxplemdvbinom  44806  binomcxplemnotnn0  44809  dvnmul  46397  stoweidlem26  46480  fourierdlem11  46572  fourierdlem24  46585  fourierdlem28  46589  fourierdlem30  46591  fourierdlem41  46602  fourierdlem60  46620  fourierdlem61  46621  fourierdlem73  46633  fourierdlem79  46639  fourierdlem81  46641  etransclem4  46692  etransclem24  46712  etransclem31  46719  etransclem32  46720  etransclem35  46723  ormklocald  47328  natlocalincr  47330  chnerlem1  47336  1fzopredsuc  47793  m1mod0mod1  47828  iccpartigtl  47903  iccpartltu  47905  iccpartgt  47907  iccpartgel  47909  fmtnorec2  48026  fmtno5lem1  48036  fmtnofac2  48052  fmtnofac1  48053  fmtno5faclem1  48062  2exp340mod341  48229  8exp8mod9  48232  gpgprismgriedgdmss  48548  gpg5edgnedg  48626  altgsumbcALT  48849  blen1  49080  blen1b  49084  nn0sumshdiglemA  49115  nn0sumshdiglemB  49116  nn0sumshdiglem1  49117  ackvalsuc0val  49183  ackval0012  49185