Theorem 0p1e1 12389

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7417  0cc0 11128  1c1 11129   + caddc 11131

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 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

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 7420  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276

This theorem is used by:  fv0p1e1  12390  zgt0ge1  12678  gtndiv  12702  nn0ind-raph  12725  1e0p1  12787  fz01en  13611  fz0dif1  13665  fz0tp  13687  fz0to3un2pr  13688  fz0sn0fz1  13704  fz0add1fz1  13795  elfzonlteqm1  13801  fzo0to2pr  13810  fz01pr  13811  fzo0to3tp  13812  elfz0lmr  13843  fldiv4p1lem1div2  13900  mulp1mod1  13979  expp1  14136  facp1  14346  faclbnd  14358  bcval5  14386  bcpasc  14389  hash1  14472  hashge2el2dif  14549  relexpsucl  15108  relexpsucr  15109  relexpaddg  15130  sgnneg  15177  binomlem  15922  isumnn0nn  15935  climcndslem1  15942  pwdif  15961  risefacval2  16103  fallfacval2  16104  risefac1  16125  fallfac1  16126  fallfacfwd  16128  bpolysum  16145  bpolydiflem  16146  bpoly2  16149  bpoly3  16150  bpoly4  16151  ege2le3  16182  ef4p  16207  eirrlem  16298  ruclem6  16329  p1modz1  16355  mod2eq1n2dvds  16443  nn0o1gt2  16477  pwp1fsum  16487  divalglem6  16494  bitsfzo  16531  pcfaclem  16996  4sqlem19  17061  vdwapun  17072  2exp16  17188  37prm  17219  631prm  17225  1259lem3  17231  1259lem4  17232  2503lem2  17236  4001lem1  17239  4001lem4  17242  chnub  18716  smndex2dnrinv  19033  gsummptfzsplitl  20066  ablsimpgfindlem1  20242  srgbinomlem4  20374  pzriprng1ALT  21715  psdmvr  22403  pmatcollpw3fi1lem1  23017  cpmadugsumlemF  23107  dvn1  26160  c1lip2  26232  dvply1  26521  iaaOLD  26568  dvtaylp  26613  cos02pilt1  26771  advlogexp  26900  leibpi  27187  log2ublem3  27193  fsumharmonic  27256  lgamgulmlem2  27274  lgamcvg2  27299  bposlem1  27528  lgsne0  27579  gausslemma2dlem4  27613  lgsquadlem2  27625  axlowdimlem16  29422  wlkl1loop  30105  uhgrwkspthlem2  30227  spthcycl  30279  crctcshwlkn0lem6  30291  wwlksn0s  30337  clwwlkccatlem  30467  umgr2cwwk2dif  30542  1wlkdlem4  30618  konigsberglem1  30740  konigsberglem2  30741  konigsberglem3  30742  numclwwlk5  30876  numclwwlk7  30879  nndiffz1  33265  f1ocnt  33279  nn0min  33299  0dp2dp  33362  wrdt2ind  33403  cshw1s2  33408  xrsmulgzz  33457  cyc2fv1  33569  cycpmco2lem4  33577  cycpmco2lem5  33578  cycpmco2lem7  33580  cyc3fv1  33585  cycpmrn  33591  vietadeg1  34096  vietalem  34097  cos9thpiminplylem2  34301  lmat22e12  34337  lmat22e21  34338  fib2  34921  usgrgt2cycl  35731  subfacp1lem6  35772  subfacval2  35774  bccolsum  36326  poimirlem5  38382  poimirlem18  38395  poimirlem21  38398  poimirlem22  38399  poimirlem27  38404  poimirlem28  38405  areacirclem4  38468  420gcd8e4  42880  3lexlogpow5ineq1  42928  3lexlogpow5ineq5  42934  aks4d1p1  42950  sticksstones9  43028  sticksstones10  43029  aks6d1c6lem3  43046  fzsplit1nn0  43607  diophren  43662  jm2.17a  43809  jm2.17b  43810  k0004val0  45002  hashnzfz2  45153  bccn1  45176  dvradcnv2  45179  binomcxplemdvbinom  45185  binomcxplemnotnn0  45188  dvnmul  46779  stoweidlem26  46862  fourierdlem11  46954  fourierdlem24  46967  fourierdlem28  46971  fourierdlem30  46973  fourierdlem41  46984  fourierdlem60  47002  fourierdlem61  47003  fourierdlem73  47015  fourierdlem79  47021  fourierdlem81  47023  etransclem4  47074  etransclem24  47094  etransclem31  47101  etransclem32  47102  etransclem35  47105  ormklocald  47712  chnerlem1  47718  1fzopredsuc  48221  m1mod0mod1  48256  iccpartigtl  48331  iccpartltu  48333  iccpartgt  48335  iccpartgel  48337  fmtnorec2  48454  fmtno5lem1  48464  fmtnofac2  48480  fmtnofac1  48481  fmtno5faclem1  48490  2exp340mod341  48657  8exp8mod9  48660  gpgprismgriedgdmss  48976  gpg5edgnedg  49054  altgsumbcALT  49291  blen1  49522  blen1b  49526  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  nn0sumshdiglem1  49559  ackvalsuc0val  49625  ackval0012  49627