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

Theorem 0p1e1 10425
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 9332 . 2  |-  1  e.  CC
21addid2i 9549 1  |-  ( 0  +  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369  (class class class)co 6086   0cc0 9274   1c1 9275    + caddc 9277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415
This theorem is referenced by:  zgt0ge1  10690  nn0lt10b  10698  recnz  10709  gtndiv  10711  nn0ind-raph  10734  1e0p1  10775  fz01en  11469  fz0tp  11505  fzo0to2pr  11606  fzo0to3tp  11607  expp1  11864  facp1  12048  faclbnd  12058  bcm1k  12083  bcval5  12086  bcpasc  12089  hash1  12154  hashge2el2dif  12176  wrdeqs1cat  12361  binomlem  13284  isumnn0nn  13297  climcndslem1  13304  mertenslem2  13337  ege2le3  13367  ef4p  13389  eirrlem  13478  ruclem6  13509  divalglem6  13594  bitsfzo  13623  pcfaclem  13952  4sqlem19  14016  vdwapun  14027  37prm  14140  631prm  14146  1259lem3  14149  1259lem4  14150  2503lem2  14154  4001lem1  14157  4001lem4  14160  srgbinomlem4  16629  dvn1  21375  c1lip2  21445  dvply1  21725  iaa  21766  dvtaylp  21810  advlogexp  22075  loglesqr  22171  leibpi  22312  log2ublem3  22318  harmonicbnd3  22376  fsumharmonic  22380  bposlem1  22598  lgslem4  22613  lgsne0  22647  lgsquadlem2  22669  axlowdimlem16  23154  wlkntrllem2  23410  2wlklem  23414  constr1trl  23438  fargshiftlem  23471  usgrcyclnl1  23477  usgrcyclnl2  23478  3v3e3cycl1  23481  constr3trllem3  23489  constr3trllem5  23491  4cycl4v4e  23503  4cycl4dv4e  23505  gxnn0suc  23702  nndiffz1  26026  nn0min  26041  xrsmulgzz  26090  fib2  26737  ballotlemodife  26832  sgnneg  26875  lgamgulmlem2  26968  lgamcvg2  26993  facgam  27004  subfacp1lem6  27025  subfacval2  27027  relexpsucl  27285  risefacval2  27464  fallfacval2  27465  risefac1  27487  fallfac1  27488  fallfacfwd  27490  bpolysum  28147  bpolydiflem  28148  bpoly2  28151  bpoly3  28152  bpoly4  28153  areacirclem4  28440  fzsplit1nn0  29045  diophren  29105  jm2.17a  29256  jm2.17b  29257  stoweidlem26  29774  stoweidlem34  29782  elfzonlteqm1  30178  usgra2pthspth  30248  usgra2wlkspthlem1  30249  usgra2pthlem1  30253  usgra2pth  30254  wwlkn0  30276  wwlkn0s  30292  clwwlkn2  30391  usg2cwwk2dif  30447  rusgranumwlkl1  30512  numclwwlk5  30658  numclwwlk7  30660  altgsumbcALT  30701
  Copyright terms: Public domain W3C validator