Theorem 0p1e1 12303

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

Syntax hints:   = wceq 1540  (class class class)co 7387  0cc0 11068  1c1 11069   + caddc 11071

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  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 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  fv0p1e1  12304  zgt0ge1  12588  gtndiv  12611  nn0ind-raph  12634  1e0p1  12691  fz01en  13513  fz0dif1  13567  fz0tp  13589  fz0to3un2pr  13590  fz0sn0fz1  13606  fz0add1fz1  13696  elfzonlteqm1  13702  fzo0to2pr  13711  fz01pr  13712  fzo0to3tp  13713  elfz0lmr  13743  fldiv4p1lem1div2  13797  mulp1mod1  13876  expp1  14033  facp1  14243  faclbnd  14255  bcval5  14283  bcpasc  14286  hash1  14369  hashge2el2dif  14445  relexpsucl  14997  relexpsucr  14998  relexpaddg  15019  binomlem  15795  isumnn0nn  15808  climcndslem1  15815  pwdif  15834  risefacval2  15976  fallfacval2  15977  risefac1  15999  fallfac1  16000  fallfacfwd  16002  bpolysum  16019  bpolydiflem  16020  bpoly2  16023  bpoly3  16024  bpoly4  16025  ege2le3  16056  ef4p  16081  eirrlem  16172  ruclem6  16203  p1modz1  16229  mod2eq1n2dvds  16317  nn0o1gt2  16351  pwp1fsum  16361  divalglem6  16368  bitsfzo  16405  pcfaclem  16869  4sqlem19  16934  vdwapun  16945  2exp16  17061  37prm  17091  631prm  17097  1259lem3  17103  1259lem4  17104  2503lem2  17108  4001lem1  17111  4001lem4  17114  smndex2dnrinv  18842  gsummptfzsplitl  19863  ablsimpgfindlem1  20039  srgbinomlem4  20138  pzriprng1ALT  21406  psdmvr  22056  pmatcollpw3fi1lem1  22673  cpmadugsumlemF  22763  dvn1  25828  c1lip2  25903  dvply1  26191  iaa  26233  dvtaylp  26278  cos02pilt1  26435  advlogexp  26564  leibpi  26852  log2ublem3  26858  fsumharmonic  26922  lgamgulmlem2  26940  lgamcvg2  26965  bposlem1  27195  lgsne0  27246  gausslemma2dlem4  27280  lgsquadlem2  27292  axlowdimlem16  28884  wlkl1loop  29566  uhgrwkspthlem2  29684  crctcshwlkn0lem6  29745  wwlksn0s  29791  clwwlkccatlem  29918  umgr2cwwk2dif  29993  1wlkdlem4  30069  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  numclwwlk5  30317  numclwwlk7  30320  nndiffz1  32709  f1ocnt  32725  nn0min  32745  sgnneg  32758  0dp2dp  32829  wrdt2ind  32875  cshw1s2  32882  chnub  32938  xrsmulgzz  32947  cyc2fv1  33078  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem7  33089  cyc3fv1  33094  cycpmrn  33100  cos9thpiminplylem2  33773  lmat22e12  33809  lmat22e21  33810  fib2  34393  spthcycl  35116  usgrgt2cycl  35117  subfacp1lem6  35172  subfacval2  35174  bccolsum  35726  poimirlem5  37619  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem27  37641  poimirlem28  37642  areacirclem4  37705  420gcd8e4  41994  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1  42064  sticksstones9  42142  sticksstones10  42143  aks6d1c6lem3  42160  fzsplit1nn0  42742  diophren  42801  jm2.17a  42949  jm2.17b  42950  k0004val0  44143  hashnzfz2  44310  bccn1  44333  dvradcnv2  44336  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  dvnmul  45941  stoweidlem26  46024  fourierdlem11  46116  fourierdlem24  46129  fourierdlem28  46133  fourierdlem30  46135  fourierdlem41  46146  fourierdlem60  46164  fourierdlem61  46165  fourierdlem73  46177  fourierdlem79  46183  fourierdlem81  46185  etransclem4  46236  etransclem24  46256  etransclem31  46263  etransclem32  46264  etransclem35  46267  ormklocald  46872  natlocalincr  46874  1fzopredsuc  47325  m1mod0mod1  47355  iccpartigtl  47424  iccpartltu  47426  iccpartgt  47428  iccpartgel  47430  fmtnorec2  47544  fmtno5lem1  47554  fmtnofac2  47570  fmtnofac1  47571  fmtno5faclem1  47580  2exp340mod341  47734  8exp8mod9  47737  gpgprismgriedgdmss  48043  altgsumbcALT  48341  blen1  48573  blen1b  48577  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  ackvalsuc0val  48676  ackval0012  48678