Theorem 0p1e1 12487

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7440  0cc0 11224  1c1 11225   + caddc 11227

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-ltxr 11372

This theorem is used by:  fv0p1e1  12488  zgt0ge1  12776  gtndiv  12800  nn0ind-raph  12823  1e0p1  12885  fz01en  13710  fz0dif1  13764  fz0tp  13786  fz0to3un2pr  13787  fz0sn0fz1  13803  fz0add1fz1  13894  elfzonlteqm1  13900  fzo0to2pr  13909  fz01pr  13910  fzo0to3tp  13911  elfz0lmr  13942  fldiv4p1lem1div2  13999  mulp1mod1  14078  expp1  14235  facp1  14446  faclbnd  14458  bcval5  14486  bcpasc  14489  hash1  14572  hashge2el2dif  14649  relexpsucl  15210  relexpsucr  15211  relexpaddg  15232  sgnneg  15279  binomlem  16024  isumnn0nn  16037  climcndslem1  16044  pwdif  16063  risefacval2  16203  fallfacval2  16204  risefac1  16225  fallfac1  16226  fallfacfwd  16228  bpolysum  16245  bpolydiflem  16246  bpoly2  16249  bpoly3  16250  bpoly4  16251  ege2le3  16282  ef4p  16307  eirrlem  16398  ruclem6  16429  p1modz1  16455  mod2eq1n2dvds  16543  nn0o1gt2  16577  pwp1fsum  16587  divalglem6  16594  bitsfzo  16631  pcfaclem  17102  4sqlem19  17167  vdwapun  17178  2exp16  17294  37prm  17325  631prm  17331  1259lem3  17337  1259lem4  17338  2503lem2  17342  4001lem1  17345  4001lem4  17348  chnub  18822  smndex2dnrinv  19140  gsummptfzsplitl  20174  ablsimpgfindlem1  20350  srgbinomlem4  20482  pzriprng1ALT  21829  psdmvr  22517  pmatcollpw3fi1lem1  23131  cpmadugsumlemF  23221  dvn1  26273  c1lip2  26345  dvply1  26632  iaaOLD  26679  dvtaylp  26724  cos02pilt1  26881  advlogexp  27010  leibpi  27297  log2ublem3  27303  fsumharmonic  27366  lgamgulmlem2  27384  lgamcvg2  27409  bposlem1  27638  lgsne0  27689  gausslemma2dlem4  27723  lgsquadlem2  27735  axlowdimlem16  29562  wlkl1loop  30245  spthcycl  30419  crctcshwlkn0lem6  30431  wwlksn0s  30477  clwwlkccatlem  30607  umgr2cwwk2dif  30682  1wlkdlem4  30758  konigsberglem1  30880  konigsberglem2  30881  konigsberglem3  30882  numclwwlk5  31016  numclwwlk7  31019  nndiffz1  33445  f1ocnt  33459  nn0min  33479  0dp2dp  33542  wrdt2ind  33583  cshw1s2  33588  xrsmulgzz  33637  cyc2fv1  33749  cycpmco2lem4  33757  cycpmco2lem5  33758  cycpmco2lem7  33760  cyc3fv1  33765  cycpmrn  33771  vietadeg1  34277  vietalem  34278  cos9thpiminplylem2  34482  lmat22e12  34518  lmat22e21  34519  fib2  35101  usgrgt2cycl  36065  subfacp1lem6  36116  subfacval2  36118  bccolsum  36681  poimirlem5  38734  poimirlem18  38747  poimirlem21  38750  poimirlem22  38751  poimirlem27  38756  poimirlem28  38757  areacirclem4  38820  420gcd8e4  43247  3lexlogpow5ineq1  43295  3lexlogpow5ineq5  43301  aks4d1p1  43317  sticksstones9  43395  sticksstones10  43396  aks6d1c6lem3  43413  fzsplit1nn0  43956  diophren  44011  jm2.17a  44158  jm2.17b  44159  hashnzfz2  45495  bccn1  45518  dvradcnv2  45521  binomcxplemdvbinom  45527  binomcxplemnotnn0  45530  dvnmul  47156  stoweidlem26  47239  fourierdlem11  47331  fourierdlem24  47344  fourierdlem28  47348  fourierdlem30  47350  fourierdlem41  47361  fourierdlem60  47379  fourierdlem61  47380  fourierdlem73  47392  fourierdlem79  47398  fourierdlem81  47400  etransclem4  47451  etransclem24  47471  etransclem31  47478  etransclem32  47479  etransclem35  47482  ormklocald  48089  chnerlem1  48095  1fzopredsuc  48598  m1mod0mod1  48633  iccpartigtl  48708  iccpartltu  48710  iccpartgt  48712  iccpartgel  48714  fmtnorec2  48831  fmtno5lem1  48841  fmtnofac2  48857  fmtnofac1  48858  fmtno5faclem1  48867  2exp340mod341  49034  8exp8mod9  49037  gpgprismgriedgdmss  49353  gpg5edgnedg  49431  altgsumbcALT  49668  blen1  49899  blen1b  49903  nn0sumshdiglemA  49934  nn0sumshdiglemB  49935  nn0sumshdiglem1  49936  ackvalsuc0val  50002  ackval0012  50004