Theorem 0p1e1 12284

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

Syntax hints:   = wceq 1541  (class class class)co 7362  0cc0 11060  1c1 11061   + caddc 11063

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-ltxr 11203

This theorem is referenced by:  fv0p1e1  12285  zgt0ge1  12566  gtndiv  12589  nn0ind-raph  12612  1e0p1  12669  fz01en  13479  fz0tp  13552  fz0to3un2pr  13553  fz0sn0fz1  13568  fz0add1fz1  13652  elfzonlteqm1  13658  fzo0to2pr  13667  fzo0to3tp  13668  elfz0lmr  13697  fldiv4p1lem1div2  13750  mulp1mod1  13827  expp1  13984  facp1  14188  faclbnd  14200  bcval5  14228  bcpasc  14231  hash1  14314  hashge2el2dif  14391  relexpsucl  14928  relexpsucr  14929  relexpaddg  14950  binomlem  15725  isumnn0nn  15738  climcndslem1  15745  pwdif  15764  risefacval2  15904  fallfacval2  15905  risefac1  15927  fallfac1  15928  fallfacfwd  15930  bpolysum  15947  bpolydiflem  15948  bpoly2  15951  bpoly3  15952  bpoly4  15953  ege2le3  15983  ef4p  16006  eirrlem  16097  ruclem6  16128  p1modz1  16154  mod2eq1n2dvds  16240  nn0o1gt2  16274  pwp1fsum  16284  divalglem6  16291  bitsfzo  16326  pcfaclem  16781  4sqlem19  16846  vdwapun  16857  2exp16  16974  37prm  17004  631prm  17010  1259lem3  17016  1259lem4  17017  2503lem2  17021  4001lem1  17024  4001lem4  17027  smndex2dnrinv  18739  gsummptfzsplitl  19724  ablsimpgfindlem1  19900  srgbinomlem4  19974  pmatcollpw3fi1lem1  22172  cpmadugsumlemF  22262  dvn1  25327  c1lip2  25399  dvply1  25681  iaa  25722  dvtaylp  25766  cos02pilt1  25919  advlogexp  26047  leibpi  26329  log2ublem3  26335  fsumharmonic  26398  lgamgulmlem2  26416  lgamcvg2  26441  bposlem1  26669  lgsne0  26720  gausslemma2dlem4  26754  lgsquadlem2  26766  axlowdimlem16  27969  wlkl1loop  28649  uhgrwkspthlem2  28765  crctcshwlkn0lem6  28823  wwlksn0s  28869  clwwlkccatlem  28996  umgr2cwwk2dif  29071  1wlkdlem4  29147  konigsberglem1  29259  konigsberglem2  29260  konigsberglem3  29261  numclwwlk5  29395  numclwwlk7  29398  nndiffz1  31757  f1ocnt  31773  nn0min  31786  0dp2dp  31835  wrdt2ind  31877  cshw1s2  31884  xrsmulgzz  31939  cyc2fv1  32040  cycpmco2lem4  32048  cycpmco2lem5  32049  cycpmco2lem7  32051  cyc3fv1  32056  cycpmrn  32062  lmat22e12  32489  lmat22e21  32490  fib2  33091  sgnneg  33229  spthcycl  33810  usgrgt2cycl  33811  subfacp1lem6  33866  subfacval2  33868  bccolsum  34398  poimirlem5  36156  poimirlem18  36169  poimirlem21  36172  poimirlem22  36173  poimirlem27  36178  poimirlem28  36179  areacirclem4  36242  420gcd8e4  40536  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1  40606  sticksstones9  40635  sticksstones10  40636  metakunt2  40651  fzsplit1nn0  41135  diophren  41194  jm2.17a  41342  jm2.17b  41343  k0004val0  42548  hashnzfz2  42723  bccn1  42746  dvradcnv2  42749  binomcxplemdvbinom  42755  binomcxplemnotnn0  42758  dvnmul  44304  stoweidlem26  44387  fourierdlem11  44479  fourierdlem24  44492  fourierdlem28  44496  fourierdlem30  44498  fourierdlem41  44509  fourierdlem60  44527  fourierdlem61  44528  fourierdlem73  44540  fourierdlem79  44546  fourierdlem81  44548  etransclem4  44599  etransclem24  44619  etransclem31  44626  etransclem32  44627  etransclem35  44630  natlocalincr  45235  1fzopredsuc  45676  m1mod0mod1  45681  iccpartigtl  45735  iccpartltu  45737  iccpartgt  45739  iccpartgel  45741  fmtnorec2  45855  fmtno5lem1  45865  fmtnofac2  45881  fmtnofac1  45882  fmtno5faclem1  45891  2exp340mod341  46045  8exp8mod9  46048  altgsumbcALT  46549  blen1  46790  blen1b  46794  nn0sumshdiglemA  46825  nn0sumshdiglemB  46826  nn0sumshdiglem1  46827  ackvalsuc0val  46893  ackval0012  46895