Theorem 0p1e1 12293

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

Syntax hints:   = wceq 1548  (class class class)co 7360  0cc0 11033  1c1 11034   + caddc 11036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-ltxr 11179

This theorem is referenced by:  fv0p1e1  12294  zgt0ge1  12578  gtndiv  12601  nn0ind-raph  12624  1e0p1  12681  fz01en  13501  fz0dif1  13555  fz0tp  13577  fz0to3un2pr  13578  fz0sn0fz1  13594  fz0add1fz1  13685  elfzonlteqm1  13691  fzo0to2pr  13700  fz01pr  13701  fzo0to3tp  13702  elfz0lmr  13733  fldiv4p1lem1div2  13789  mulp1mod1  13868  expp1  14025  facp1  14235  faclbnd  14247  bcval5  14275  bcpasc  14278  hash1  14361  hashge2el2dif  14437  relexpsucl  14988  relexpsucr  14989  relexpaddg  15010  binomlem  15789  isumnn0nn  15802  climcndslem1  15809  pwdif  15828  risefacval2  15970  fallfacval2  15971  risefac1  15993  fallfac1  15994  fallfacfwd  15996  bpolysum  16013  bpolydiflem  16014  bpoly2  16017  bpoly3  16018  bpoly4  16019  ege2le3  16050  ef4p  16075  eirrlem  16166  ruclem6  16197  p1modz1  16223  mod2eq1n2dvds  16311  nn0o1gt2  16345  pwp1fsum  16355  divalglem6  16362  bitsfzo  16399  pcfaclem  16864  4sqlem19  16929  vdwapun  16940  2exp16  17056  37prm  17086  631prm  17092  1259lem3  17098  1259lem4  17099  2503lem2  17103  4001lem1  17106  4001lem4  17109  chnub  18583  smndex2dnrinv  18881  gsummptfzsplitl  19903  ablsimpgfindlem1  20079  srgbinomlem4  20205  pzriprng1ALT  21475  psdmvr  22161  pmatcollpw3fi1lem1  22773  cpmadugsumlemF  22863  dvn1  25915  c1lip2  25987  dvply1  26272  iaa  26313  dvtaylp  26357  cos02pilt1  26512  advlogexp  26641  leibpi  26928  log2ublem3  26934  fsumharmonic  26997  lgamgulmlem2  27015  lgamcvg2  27040  bposlem1  27269  lgsne0  27320  gausslemma2dlem4  27354  lgsquadlem2  27366  axlowdimlem16  29048  wlkl1loop  29728  uhgrwkspthlem2  29844  crctcshwlkn0lem6  29905  wwlksn0s  29951  clwwlkccatlem  30081  umgr2cwwk2dif  30156  1wlkdlem4  30232  konigsberglem1  30344  konigsberglem2  30345  konigsberglem3  30346  numclwwlk5  30480  numclwwlk7  30483  nndiffz1  32882  f1ocnt  32896  nn0min  32917  sgnneg  32929  0dp2dp  32991  wrdt2ind  33036  cshw1s2  33043  xrsmulgzz  33092  cyc2fv1  33206  cycpmco2lem4  33214  cycpmco2lem5  33215  cycpmco2lem7  33217  cyc3fv1  33222  cycpmrn  33228  vietadeg1  33774  vietalem  33775  cos9thpiminplylem2  33979  lmat22e12  34015  lmat22e21  34016  fib2  34598  spthcycl  35372  usgrgt2cycl  35373  subfacp1lem6  35428  subfacval2  35430  bccolsum  35982  poimirlem5  38007  poimirlem18  38020  poimirlem21  38023  poimirlem22  38024  poimirlem27  38029  poimirlem28  38030  areacirclem4  38093  420gcd8e4  42506  3lexlogpow5ineq1  42554  3lexlogpow5ineq5  42560  aks4d1p1  42576  sticksstones9  42654  sticksstones10  42655  aks6d1c6lem3  42672  fzsplit1nn0  43218  diophren  43273  jm2.17a  43420  jm2.17b  43421  k0004val0  44613  hashnzfz2  44780  bccn1  44803  dvradcnv2  44806  binomcxplemdvbinom  44812  binomcxplemnotnn0  44815  dvnmul  46400  stoweidlem26  46483  fourierdlem11  46575  fourierdlem24  46588  fourierdlem28  46592  fourierdlem30  46594  fourierdlem41  46605  fourierdlem60  46623  fourierdlem61  46624  fourierdlem73  46636  fourierdlem79  46642  fourierdlem81  46644  etransclem4  46695  etransclem24  46715  etransclem31  46722  etransclem32  46723  etransclem35  46726  ormklocald  47333  natlocalincr  47335  chnerlem1  47341  1fzopredsuc  47802  m1mod0mod1  47837  iccpartigtl  47912  iccpartltu  47914  iccpartgt  47916  iccpartgel  47918  fmtnorec2  48035  fmtno5lem1  48045  fmtnofac2  48061  fmtnofac1  48062  fmtno5faclem1  48071  2exp340mod341  48238  8exp8mod9  48241  gpgprismgriedgdmss  48557  gpg5edgnedg  48635  altgsumbcALT  48858  blen1  49089  blen1b  49093  nn0sumshdiglemA  49124  nn0sumshdiglemB  49125  nn0sumshdiglem1  49126  ackvalsuc0val  49192  ackval0012  49194