Theorem 0p1e1 12245

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

Syntax hints:   = wceq 1540  (class class class)co 7349  0cc0 11009  1c1 11010   + caddc 11012

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

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 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154

This theorem is referenced by:  fv0p1e1  12246  zgt0ge1  12530  gtndiv  12553  nn0ind-raph  12576  1e0p1  12633  fz01en  13455  fz0dif1  13509  fz0tp  13531  fz0to3un2pr  13532  fz0sn0fz1  13548  fz0add1fz1  13638  elfzonlteqm1  13644  fzo0to2pr  13653  fz01pr  13654  fzo0to3tp  13655  elfz0lmr  13685  fldiv4p1lem1div2  13739  mulp1mod1  13818  expp1  13975  facp1  14185  faclbnd  14197  bcval5  14225  bcpasc  14228  hash1  14311  hashge2el2dif  14387  relexpsucl  14938  relexpsucr  14939  relexpaddg  14960  binomlem  15736  isumnn0nn  15749  climcndslem1  15756  pwdif  15775  risefacval2  15917  fallfacval2  15918  risefac1  15940  fallfac1  15941  fallfacfwd  15943  bpolysum  15960  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  bpoly4  15966  ege2le3  15997  ef4p  16022  eirrlem  16113  ruclem6  16144  p1modz1  16170  mod2eq1n2dvds  16258  nn0o1gt2  16292  pwp1fsum  16302  divalglem6  16309  bitsfzo  16346  pcfaclem  16810  4sqlem19  16875  vdwapun  16886  2exp16  17002  37prm  17032  631prm  17038  1259lem3  17044  1259lem4  17045  2503lem2  17049  4001lem1  17052  4001lem4  17055  smndex2dnrinv  18789  gsummptfzsplitl  19812  ablsimpgfindlem1  19988  srgbinomlem4  20114  pzriprng1ALT  21403  psdmvr  22054  pmatcollpw3fi1lem1  22671  cpmadugsumlemF  22761  dvn1  25826  c1lip2  25901  dvply1  26189  iaa  26231  dvtaylp  26276  cos02pilt1  26433  advlogexp  26562  leibpi  26850  log2ublem3  26856  fsumharmonic  26920  lgamgulmlem2  26938  lgamcvg2  26963  bposlem1  27193  lgsne0  27244  gausslemma2dlem4  27278  lgsquadlem2  27290  axlowdimlem16  28906  wlkl1loop  29587  uhgrwkspthlem2  29703  crctcshwlkn0lem6  29764  wwlksn0s  29810  clwwlkccatlem  29937  umgr2cwwk2dif  30012  1wlkdlem4  30088  konigsberglem1  30200  konigsberglem2  30201  konigsberglem3  30202  numclwwlk5  30336  numclwwlk7  30339  nndiffz1  32738  f1ocnt  32754  nn0min  32774  sgnneg  32787  0dp2dp  32858  wrdt2ind  32904  cshw1s2  32911  chnub  32963  xrsmulgzz  32972  cyc2fv1  33072  cycpmco2lem4  33080  cycpmco2lem5  33081  cycpmco2lem7  33083  cyc3fv1  33088  cycpmrn  33094  cos9thpiminplylem2  33766  lmat22e12  33802  lmat22e21  33803  fib2  34386  spthcycl  35122  usgrgt2cycl  35123  subfacp1lem6  35178  subfacval2  35180  bccolsum  35732  poimirlem5  37625  poimirlem18  37638  poimirlem21  37641  poimirlem22  37642  poimirlem27  37647  poimirlem28  37648  areacirclem4  37711  420gcd8e4  41999  3lexlogpow5ineq1  42047  3lexlogpow5ineq5  42053  aks4d1p1  42069  sticksstones9  42147  sticksstones10  42148  aks6d1c6lem3  42165  fzsplit1nn0  42747  diophren  42806  jm2.17a  42953  jm2.17b  42954  k0004val0  44147  hashnzfz2  44314  bccn1  44337  dvradcnv2  44340  binomcxplemdvbinom  44346  binomcxplemnotnn0  44349  dvnmul  45944  stoweidlem26  46027  fourierdlem11  46119  fourierdlem24  46132  fourierdlem28  46136  fourierdlem30  46138  fourierdlem41  46149  fourierdlem60  46167  fourierdlem61  46168  fourierdlem73  46180  fourierdlem79  46186  fourierdlem81  46188  etransclem4  46239  etransclem24  46259  etransclem31  46266  etransclem32  46267  etransclem35  46270  ormklocald  46875  natlocalincr  46877  1fzopredsuc  47328  m1mod0mod1  47358  iccpartigtl  47427  iccpartltu  47429  iccpartgt  47431  iccpartgel  47433  fmtnorec2  47547  fmtno5lem1  47557  fmtnofac2  47573  fmtnofac1  47574  fmtno5faclem1  47583  2exp340mod341  47737  8exp8mod9  47740  gpgprismgriedgdmss  48056  gpg5edgnedg  48134  altgsumbcALT  48357  blen1  48589  blen1b  48593  nn0sumshdiglemA  48624  nn0sumshdiglemB  48625  nn0sumshdiglem1  48626  ackvalsuc0val  48692  ackval0012  48694