Theorem 0p1e1 12388

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416  0cc0 11127  1c1 11128   + caddc 11130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275

This theorem is used by:  fv0p1e1  12389  zgt0ge1  12677  gtndiv  12701  nn0ind-raph  12724  1e0p1  12786  fz01en  13609  fz0dif1  13663  fz0tp  13685  fz0to3un2pr  13686  fz0sn0fz1  13702  fz0add1fz1  13793  elfzonlteqm1  13799  fzo0to2pr  13808  fz01pr  13809  fzo0to3tp  13810  elfz0lmr  13841  fldiv4p1lem1div2  13898  mulp1mod1  13977  expp1  14134  facp1  14344  faclbnd  14356  bcval5  14384  bcpasc  14387  hash1  14470  hashge2el2dif  14547  relexpsucl  15106  relexpsucr  15107  relexpaddg  15128  sgnneg  15175  binomlem  15920  isumnn0nn  15933  climcndslem1  15940  pwdif  15959  risefacval2  16101  fallfacval2  16102  risefac1  16123  fallfac1  16124  fallfacfwd  16126  bpolysum  16143  bpolydiflem  16144  bpoly2  16147  bpoly3  16148  bpoly4  16149  ege2le3  16180  ef4p  16205  eirrlem  16296  ruclem6  16327  p1modz1  16353  mod2eq1n2dvds  16441  nn0o1gt2  16475  pwp1fsum  16485  divalglem6  16492  bitsfzo  16529  pcfaclem  16994  4sqlem19  17059  vdwapun  17070  2exp16  17186  37prm  17217  631prm  17223  1259lem3  17229  1259lem4  17230  2503lem2  17234  4001lem1  17237  4001lem4  17240  chnub  18714  smndex2dnrinv  19028  gsummptfzsplitl  20061  ablsimpgfindlem1  20237  srgbinomlem4  20369  pzriprng1ALT  21710  psdmvr  22398  pmatcollpw3fi1lem1  23012  cpmadugsumlemF  23102  dvn1  26155  c1lip2  26227  dvply1  26515  iaa  26558  dvtaylp  26603  cos02pilt1  26761  advlogexp  26890  leibpi  27177  log2ublem3  27183  fsumharmonic  27246  lgamgulmlem2  27264  lgamcvg2  27289  bposlem1  27518  lgsne0  27569  gausslemma2dlem4  27603  lgsquadlem2  27615  axlowdimlem16  29400  wlkl1loop  30083  uhgrwkspthlem2  30205  spthcycl  30257  crctcshwlkn0lem6  30269  wwlksn0s  30315  clwwlkccatlem  30445  umgr2cwwk2dif  30520  1wlkdlem4  30596  konigsberglem1  30718  konigsberglem2  30719  konigsberglem3  30720  numclwwlk5  30854  numclwwlk7  30857  nndiffz1  33244  f1ocnt  33258  nn0min  33278  0dp2dp  33341  wrdt2ind  33382  cshw1s2  33387  xrsmulgzz  33436  cyc2fv1  33548  cycpmco2lem4  33556  cycpmco2lem5  33557  cycpmco2lem7  33559  cyc3fv1  33564  cycpmrn  33570  vietadeg1  34075  vietalem  34076  cos9thpiminplylem2  34280  lmat22e12  34316  lmat22e21  34317  fib2  34900  usgrgt2cycl  35710  subfacp1lem6  35751  subfacval2  35753  bccolsum  36305  poimirlem5  38361  poimirlem18  38374  poimirlem21  38377  poimirlem22  38378  poimirlem27  38383  poimirlem28  38384  areacirclem4  38447  420gcd8e4  42859  3lexlogpow5ineq1  42907  3lexlogpow5ineq5  42913  aks4d1p1  42929  sticksstones9  43007  sticksstones10  43008  aks6d1c6lem3  43025  fzsplit1nn0  43586  diophren  43641  jm2.17a  43788  jm2.17b  43789  k0004val0  44981  hashnzfz2  45132  bccn1  45155  dvradcnv2  45158  binomcxplemdvbinom  45164  binomcxplemnotnn0  45167  dvnmul  46758  stoweidlem26  46841  fourierdlem11  46933  fourierdlem24  46946  fourierdlem28  46950  fourierdlem30  46952  fourierdlem41  46963  fourierdlem60  46981  fourierdlem61  46982  fourierdlem73  46994  fourierdlem79  47000  fourierdlem81  47002  etransclem4  47053  etransclem24  47073  etransclem31  47080  etransclem32  47081  etransclem35  47084  ormklocald  47691  chnerlem1  47697  1fzopredsuc  48200  m1mod0mod1  48235  iccpartigtl  48310  iccpartltu  48312  iccpartgt  48314  iccpartgel  48316  fmtnorec2  48433  fmtno5lem1  48443  fmtnofac2  48459  fmtnofac1  48460  fmtno5faclem1  48469  2exp340mod341  48636  8exp8mod9  48639  gpgprismgriedgdmss  48955  gpg5edgnedg  49033  altgsumbcALT  49270  blen1  49501  blen1b  49505  nn0sumshdiglemA  49536  nn0sumshdiglemB  49537  nn0sumshdiglem1  49538  ackvalsuc0val  49604  ackval0012  49606