MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0p1e1 Structured version   Visualization version   GIF version

Theorem 0p1e1 11738
Description: 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
0p1e1 (0 + 1) = 1

Proof of Theorem 0p1e1
StepHypRef Expression
1 ax-1cn 10573 . 2 1 ∈ ℂ
21addid2i 10806 1 (0 + 1) = 1
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  (class class class)co 7133  0cc0 10515  1c1 10516   + caddc 10518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-po 5450  df-so 5451  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-er 8267  df-en 8488  df-dom 8489  df-sdom 8490  df-pnf 10655  df-mnf 10656  df-ltxr 10658
This theorem is referenced by:  fv0p1e1  11739  zgt0ge1  12015  gtndiv  12038  nn0ind-raph  12061  1e0p1  12119  fz01en  12919  fz0tp  12992  fz0to3un2pr  12993  fz0sn0fz1  13008  fz0add1fz1  13091  elfzonlteqm1  13097  fzo0to2pr  13106  fzo0to3tp  13107  elfz0lmr  13136  fldiv4p1lem1div2  13189  mulp1mod1  13264  expp1  13421  facp1  13623  faclbnd  13635  bcval5  13663  bcpasc  13666  hash1  13750  hashge2el2dif  13823  relexpsucr  14368  relexpsucl  14372  relexpaddg  14392  binomlem  15164  isumnn0nn  15177  climcndslem1  15184  pwdif  15203  risefacval2  15344  fallfacval2  15345  risefac1  15367  fallfac1  15368  fallfacfwd  15370  bpolysum  15387  bpolydiflem  15388  bpoly2  15391  bpoly3  15392  bpoly4  15393  ege2le3  15423  ef4p  15446  eirrlem  15537  ruclem6  15568  p1modz1  15594  mod2eq1n2dvds  15676  nn0o1gt2  15710  pwp1fsum  15720  divalglem6  15727  bitsfzo  15762  pcfaclem  16212  4sqlem19  16277  vdwapun  16288  2exp16  16403  37prm  16433  631prm  16439  1259lem3  16445  1259lem4  16446  2503lem2  16450  4001lem1  16453  4001lem4  16456  smndex2dnrinv  18059  gsummptfzsplitl  19032  ablsimpgfindlem1  19208  srgbinomlem4  19272  pmatcollpw3fi1lem1  21370  cpmadugsumlemF  21460  dvn1  24508  c1lip2  24580  dvply1  24859  iaa  24900  dvtaylp  24944  cos02pilt1  25097  advlogexp  25225  leibpi  25507  log2ublem3  25513  fsumharmonic  25576  lgamgulmlem2  25594  lgamcvg2  25619  bposlem1  25847  lgsne0  25898  gausslemma2dlem4  25932  lgsquadlem2  25944  axlowdimlem16  26730  wlkl1loop  27406  uhgrwkspthlem2  27522  crctcshwlkn0lem6  27580  wwlksn0s  27626  clwwlkccatlem  27753  umgr2cwwk2dif  27828  1wlkdlem4  27904  konigsberglem1  28016  konigsberglem2  28017  konigsberglem3  28018  numclwwlk5  28152  numclwwlk7  28155  nndiffz1  30496  f1ocnt  30512  nn0min  30523  0dp2dp  30572  wrdt2ind  30614  cshw1s2  30621  xrsmulgzz  30673  cyc2fv1  30771  cycpmco2lem4  30779  cycpmco2lem5  30780  cycpmco2lem7  30782  cyc3fv1  30787  cycpmrn  30793  lmat22e12  31095  lmat22e21  31096  fib2  31668  sgnneg  31806  spthcycl  32384  usgrgt2cycl  32385  subfacp1lem6  32440  subfacval2  32442  bccolsum  32979  poimirlem5  34938  poimirlem18  34951  poimirlem21  34954  poimirlem22  34955  poimirlem27  34960  poimirlem28  34961  areacirclem4  35024  420gcd8e4  39158  fzsplit1nn0  39488  diophren  39547  jm2.17a  39694  jm2.17b  39695  k0004val0  40639  hashnzfz2  40808  bccn1  40831  dvradcnv2  40834  binomcxplemdvbinom  40840  binomcxplemnotnn0  40843  dvnmul  42376  stoweidlem26  42459  fourierdlem11  42551  fourierdlem24  42564  fourierdlem28  42568  fourierdlem30  42570  fourierdlem41  42581  fourierdlem60  42599  fourierdlem61  42600  fourierdlem73  42612  fourierdlem79  42618  fourierdlem81  42620  etransclem4  42671  etransclem24  42691  etransclem31  42698  etransclem32  42699  etransclem35  42702  1fzopredsuc  43672  m1mod0mod1  43677  iccpartigtl  43731  iccpartltu  43733  iccpartgt  43735  iccpartgel  43737  fmtnorec2  43851  fmtno5lem1  43861  fmtnofac2  43877  fmtnofac1  43878  fmtno5faclem1  43887  2exp340mod341  44043  8exp8mod9  44046  altgsumbcALT  44546  blen1  44789  blen1b  44793  nn0sumshdiglemA  44824  nn0sumshdiglemB  44825  nn0sumshdiglem1  44826  ackvalsuc0val  44861  ackval0012  44863
  Copyright terms: Public domain W3C validator