Theorem 0p1e1 11504

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

Syntax hints:   = wceq 1601  (class class class)co 6922  0cc0 10272  1c1 10273   + caddc 10275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-ltxr 10416

This theorem is referenced by:  fv0p1e1  11505  zgt0ge1  11783  gtndiv  11806  nn0ind-raph  11829  1e0p1  11888  fz01en  12686  fz0tp  12759  fz0to3un2pr  12760  fz0sn0fz1  12775  fz0add1fz1  12857  elfzonlteqm1  12863  fzo0to2pr  12872  fzo0to3tp  12873  elfz0lmr  12902  fldiv4p1lem1div2  12955  mulp1mod1  13030  expp1  13185  facp1  13383  faclbnd  13395  bcval5  13423  bcpasc  13426  hash1  13506  hashge2el2dif  13576  wrdeqs1catOLD  13840  relexpsucr  14176  relexpsucl  14180  relexpaddg  14200  binomlem  14965  isumnn0nn  14978  climcndslem1  14985  risefacval2  15143  fallfacval2  15144  risefac1  15166  fallfac1  15167  fallfacfwd  15169  bpolysum  15186  bpolydiflem  15187  bpoly2  15190  bpoly3  15191  bpoly4  15192  ege2le3  15222  ef4p  15245  eirrlem  15336  ruclem6  15368  p1modz1  15394  mod2eq1n2dvds  15475  nn0o1gt2  15511  pwp1fsum  15521  divalglem6  15528  bitsfzo  15563  pcfaclem  16006  4sqlem19  16071  vdwapun  16082  2exp16  16196  37prm  16226  631prm  16232  1259lem3  16238  1259lem4  16239  2503lem2  16243  4001lem1  16246  4001lem4  16249  gsummptfzsplitl  18719  srgbinomlem4  18930  pmatcollpw3fi1lem1  20998  cpmadugsumlemF  21088  dvn1  24126  c1lip2  24198  dvply1  24476  iaa  24517  dvtaylp  24561  advlogexp  24838  leibpi  25121  log2ublem3  25127  fsumharmonic  25190  lgamgulmlem2  25208  lgamcvg2  25233  bposlem1  25461  lgsne0  25512  gausslemma2dlem4  25546  lgsquadlem2  25558  axlowdimlem16  26306  wlkl1loop  26985  uhgrwkspthlem2  27106  crctcshwlkn0lem6  27164  wwlksn0s  27210  clwwlkccatlem  27369  umgr2cwwk2dif  27462  1wlkdlem4  27543  konigsberglem1  27658  konigsberglem2  27659  konigsberglem3  27660  numclwwlk5  27820  numclwwlk7  27823  nndiffz1  30112  f1ocnt  30123  nn0min  30131  0dp2dp  30179  xrsmulgzz  30240  lmat22e12  30483  lmat22e21  30484  fib2  31063  sgnneg  31201  subfacp1lem6  31766  subfacval2  31768  bccolsum  32219  poimirlem5  34042  poimirlem18  34055  poimirlem21  34058  poimirlem22  34059  poimirlem27  34064  poimirlem28  34065  areacirclem4  34130  fzsplit1nn0  38281  diophren  38341  jm2.17a  38490  jm2.17b  38491  k0004val0  39412  hashnzfz2  39480  bccn1  39503  dvradcnv2  39506  binomcxplemdvbinom  39512  binomcxplemnotnn0  39515  dvnmul  41090  stoweidlem26  41174  fourierdlem11  41266  fourierdlem24  41279  fourierdlem28  41283  fourierdlem30  41285  fourierdlem41  41296  fourierdlem60  41314  fourierdlem61  41315  fourierdlem73  41327  fourierdlem79  41333  fourierdlem81  41335  etransclem4  41386  etransclem24  41406  etransclem31  41413  etransclem32  41414  etransclem35  41417  1fzopredsuc  42370  m1mod0mod1  42375  iccpartigtl  42395  iccpartltu  42397  iccpartgt  42399  iccpartgel  42401  fmtnorec2  42480  fmtno5lem1  42490  fmtnofac2  42506  fmtnofac1  42507  fmtno5faclem1  42516  pwdif  42526  altgsumbcALT  43150  blen1  43397  blen1b  43401  nn0sumshdiglemA  43432  nn0sumshdiglemB  43433  nn0sumshdiglem1  43434