Theorem 0p1e1 12385

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

Syntax hints:   = wceq 1536  (class class class)co 7430  0cc0 11152  1c1 11153   + caddc 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297

This theorem is referenced by:  fv0p1e1  12386  zgt0ge1  12669  gtndiv  12692  nn0ind-raph  12715  1e0p1  12772  fz01en  13588  fz0dif1  13642  fz0tp  13664  fz0to3un2pr  13665  fz0sn0fz1  13681  fz0add1fz1  13770  elfzonlteqm1  13776  fzo0to2pr  13785  fz01pr  13786  fzo0to3tp  13787  elfz0lmr  13817  fldiv4p1lem1div2  13871  mulp1mod1  13948  expp1  14105  facp1  14313  faclbnd  14325  bcval5  14353  bcpasc  14356  hash1  14439  hashge2el2dif  14515  relexpsucl  15066  relexpsucr  15067  relexpaddg  15088  binomlem  15861  isumnn0nn  15874  climcndslem1  15881  pwdif  15900  risefacval2  16042  fallfacval2  16043  risefac1  16065  fallfac1  16066  fallfacfwd  16068  bpolysum  16085  bpolydiflem  16086  bpoly2  16089  bpoly3  16090  bpoly4  16091  ege2le3  16122  ef4p  16145  eirrlem  16236  ruclem6  16267  p1modz1  16293  mod2eq1n2dvds  16380  nn0o1gt2  16414  pwp1fsum  16424  divalglem6  16431  bitsfzo  16468  pcfaclem  16931  4sqlem19  16996  vdwapun  17007  2exp16  17124  37prm  17154  631prm  17160  1259lem3  17166  1259lem4  17167  2503lem2  17171  4001lem1  17174  4001lem4  17177  smndex2dnrinv  18940  gsummptfzsplitl  19965  ablsimpgfindlem1  20141  srgbinomlem4  20246  pzriprng1ALT  21524  pmatcollpw3fi1lem1  22807  cpmadugsumlemF  22897  dvn1  25976  c1lip2  26051  dvply1  26339  iaa  26381  dvtaylp  26426  cos02pilt1  26582  advlogexp  26711  leibpi  26999  log2ublem3  27005  fsumharmonic  27069  lgamgulmlem2  27087  lgamcvg2  27112  bposlem1  27342  lgsne0  27393  gausslemma2dlem4  27427  lgsquadlem2  27439  axlowdimlem16  28986  wlkl1loop  29670  uhgrwkspthlem2  29786  crctcshwlkn0lem6  29844  wwlksn0s  29890  clwwlkccatlem  30017  umgr2cwwk2dif  30092  1wlkdlem4  30168  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  numclwwlk5  30416  numclwwlk7  30419  nndiffz1  32794  f1ocnt  32809  nn0min  32826  0dp2dp  32875  wrdt2ind  32922  cshw1s2  32929  chnub  32985  xrsmulgzz  32993  cyc2fv1  33123  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem7  33134  cyc3fv1  33139  cycpmrn  33145  lmat22e12  33779  lmat22e21  33780  fib2  34383  sgnneg  34521  spthcycl  35113  usgrgt2cycl  35114  subfacp1lem6  35169  subfacval2  35171  bccolsum  35718  poimirlem5  37611  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem27  37633  poimirlem28  37634  areacirclem4  37697  420gcd8e4  41987  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1  42057  sticksstones9  42135  sticksstones10  42136  aks6d1c6lem3  42153  metakunt2  42187  fzsplit1nn0  42741  diophren  42800  jm2.17a  42948  jm2.17b  42949  k0004val0  44143  hashnzfz2  44316  bccn1  44339  dvradcnv2  44342  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  dvnmul  45898  stoweidlem26  45981  fourierdlem11  46073  fourierdlem24  46086  fourierdlem28  46090  fourierdlem30  46092  fourierdlem41  46103  fourierdlem60  46121  fourierdlem61  46122  fourierdlem73  46134  fourierdlem79  46140  fourierdlem81  46142  etransclem4  46193  etransclem24  46213  etransclem31  46220  etransclem32  46221  etransclem35  46224  natlocalincr  46829  1fzopredsuc  47273  m1mod0mod1  47293  iccpartigtl  47347  iccpartltu  47349  iccpartgt  47351  iccpartgel  47353  fmtnorec2  47467  fmtno5lem1  47477  fmtnofac2  47493  fmtnofac1  47494  fmtno5faclem1  47503  2exp340mod341  47657  8exp8mod9  47660  altgsumbcALT  48197  blen1  48433  blen1b  48437  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  ackvalsuc0val  48536  ackval0012  48538