Theorem 0p1e1 12282

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

Syntax hints:   = wceq 1540  (class class class)co 7370  0cc0 11047  1c1 11048   + caddc 11050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7692  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7373  df-er 8649  df-en 8897  df-dom 8898  df-sdom 8899  df-pnf 11189  df-mnf 11190  df-ltxr 11192

This theorem is referenced by:  fv0p1e1  12283  zgt0ge1  12567  gtndiv  12590  nn0ind-raph  12613  1e0p1  12670  fz01en  13492  fz0dif1  13546  fz0tp  13568  fz0to3un2pr  13569  fz0sn0fz1  13585  fz0add1fz1  13675  elfzonlteqm1  13681  fzo0to2pr  13690  fz01pr  13691  fzo0to3tp  13692  elfz0lmr  13722  fldiv4p1lem1div2  13776  mulp1mod1  13855  expp1  14012  facp1  14222  faclbnd  14234  bcval5  14262  bcpasc  14265  hash1  14348  hashge2el2dif  14424  relexpsucl  14975  relexpsucr  14976  relexpaddg  14997  binomlem  15773  isumnn0nn  15786  climcndslem1  15793  pwdif  15812  risefacval2  15954  fallfacval2  15955  risefac1  15977  fallfac1  15978  fallfacfwd  15980  bpolysum  15997  bpolydiflem  15998  bpoly2  16001  bpoly3  16002  bpoly4  16003  ege2le3  16034  ef4p  16059  eirrlem  16150  ruclem6  16181  p1modz1  16207  mod2eq1n2dvds  16295  nn0o1gt2  16329  pwp1fsum  16339  divalglem6  16346  bitsfzo  16383  pcfaclem  16847  4sqlem19  16912  vdwapun  16923  2exp16  17039  37prm  17069  631prm  17075  1259lem3  17081  1259lem4  17082  2503lem2  17086  4001lem1  17089  4001lem4  17092  smndex2dnrinv  18826  gsummptfzsplitl  19849  ablsimpgfindlem1  20025  srgbinomlem4  20151  pzriprng1ALT  21440  psdmvr  22091  pmatcollpw3fi1lem1  22708  cpmadugsumlemF  22798  dvn1  25863  c1lip2  25938  dvply1  26226  iaa  26268  dvtaylp  26313  cos02pilt1  26470  advlogexp  26599  leibpi  26887  log2ublem3  26893  fsumharmonic  26957  lgamgulmlem2  26975  lgamcvg2  27000  bposlem1  27230  lgsne0  27281  gausslemma2dlem4  27315  lgsquadlem2  27327  axlowdimlem16  28939  wlkl1loop  29620  uhgrwkspthlem2  29736  crctcshwlkn0lem6  29797  wwlksn0s  29843  clwwlkccatlem  29970  umgr2cwwk2dif  30045  1wlkdlem4  30121  konigsberglem1  30233  konigsberglem2  30234  konigsberglem3  30235  numclwwlk5  30369  numclwwlk7  30372  nndiffz1  32761  f1ocnt  32777  nn0min  32797  sgnneg  32810  0dp2dp  32881  wrdt2ind  32927  cshw1s2  32934  chnub  32986  xrsmulgzz  32995  cyc2fv1  33095  cycpmco2lem4  33103  cycpmco2lem5  33104  cycpmco2lem7  33106  cyc3fv1  33111  cycpmrn  33117  cos9thpiminplylem2  33768  lmat22e12  33804  lmat22e21  33805  fib2  34388  spthcycl  35111  usgrgt2cycl  35112  subfacp1lem6  35167  subfacval2  35169  bccolsum  35721  poimirlem5  37614  poimirlem18  37627  poimirlem21  37630  poimirlem22  37631  poimirlem27  37636  poimirlem28  37637  areacirclem4  37700  420gcd8e4  41989  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  aks4d1p1  42059  sticksstones9  42137  sticksstones10  42138  aks6d1c6lem3  42155  fzsplit1nn0  42737  diophren  42796  jm2.17a  42944  jm2.17b  42945  k0004val0  44138  hashnzfz2  44305  bccn1  44328  dvradcnv2  44331  binomcxplemdvbinom  44337  binomcxplemnotnn0  44340  dvnmul  45936  stoweidlem26  46019  fourierdlem11  46111  fourierdlem24  46124  fourierdlem28  46128  fourierdlem30  46130  fourierdlem41  46141  fourierdlem60  46159  fourierdlem61  46160  fourierdlem73  46172  fourierdlem79  46178  fourierdlem81  46180  etransclem4  46231  etransclem24  46251  etransclem31  46258  etransclem32  46259  etransclem35  46262  ormklocald  46867  natlocalincr  46869  1fzopredsuc  47320  m1mod0mod1  47350  iccpartigtl  47419  iccpartltu  47421  iccpartgt  47423  iccpartgel  47425  fmtnorec2  47539  fmtno5lem1  47549  fmtnofac2  47565  fmtnofac1  47566  fmtno5faclem1  47575  2exp340mod341  47729  8exp8mod9  47732  gpgprismgriedgdmss  48038  altgsumbcALT  48336  blen1  48568  blen1b  48572  nn0sumshdiglemA  48603  nn0sumshdiglemB  48604  nn0sumshdiglem1  48605  ackvalsuc0val  48671  ackval0012  48673