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

Theorem readdcl 9876
Description: Alias for ax-addrcl 9854, for naming consistency with readdcli 9910. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 9854 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  (class class class)co 6527  cr 9792   + caddc 9796
This theorem was proved from axioms:  ax-addrcl 9854
This theorem is referenced by:  0re  9897  readdcli  9910  readdcld  9926  axltadd  9963  peano2re  10061  00id  10063  resubcl  10197  ltaddsub  10354  leaddsub  10356  ltleadd  10363  ltaddsublt  10506  recex  10511  recp1lt1  10773  recreclt  10774  supadd  10841  cju  10866  nnge1  10896  addltmul  11118  avglt1  11120  avglt2  11121  avgle1  11122  avgle2  11123  nzadd  11261  irradd  11647  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  rpaddcl  11689  xaddf  11891  xaddnemnf  11902  xaddnepnf  11903  xnegdi  11910  xaddass  11911  xadddilem  11956  iooshf  12082  ge0addcl  12114  icoshft  12124  icoshftf1o  12125  iccshftr  12136  difelfznle  12280  elfzodifsumelfzo  12359  subfzo0  12410  flbi2  12438  modcyc  12525  modadd1  12527  modsumfzodifsn  12563  serfre  12650  sermono  12653  serge0  12675  serle  12676  bernneq  12810  faclbnd6  12906  hashfun  13039  ccatsymb  13168  swrdswrdlem  13260  swrdccatin2  13287  cshweqrep  13367  cshwcsh2id  13374  readd  13663  imadd  13671  elicc4abs  13856  rddif  13877  absrdbnd  13878  caubnd2  13894  mulcn2  14123  o1add  14141  o1sub  14143  lo1add  14154  fsumrecl  14261  rerisefaccl  14536  rprisefaccl  14542  efgt1  14634  pythagtriplem12  15318  pythagtriplem14  15320  pythagtriplem16  15322  remulg  19720  resubdrg  19721  prdsxmetlem  21931  xmeter  21996  bl2ioo  22351  ioo2bl  22352  ioo2blex  22353  blssioo  22354  reperf  22378  reconnlem2  22386  opnreen  22390  icopnfcnv  22497  pcoass  22580  pjthlem1  22961  ovolun  23019  shft2rab  23028  volun  23065  mbfaddlem  23178  i1fadd  23213  itg1addlem4  23217  itg2monolem1  23268  ply1divex  23645  psercnlem1  23928  reefgim  23953  tangtx  24006  efif1olem1  24037  efif1olem2  24038  efif1o  24041  relogmul  24087  argimgt0  24107  logimul  24109  ang180lem1  24284  atanlogaddlem  24385  atanlogsublem  24387  atantan  24395  ressatans  24406  emcllem6  24472  basellem9  24560  ppiub  24674  bposlem5  24758  bposlem6  24759  bposlem9  24762  chpchtlim  24913  mulog2sumlem1  24968  mulog2sumlem2  24969  selberglem2  24980  pntrmax  24998  pntpbnd1a  25019  pntpbnd2  25021  pntibndlem3  25026  pntlemb  25031  pntlemk  25040  axsegconlem7  25549  axsegconlem9  25551  axsegconlem10  25552  clwwisshclwwlem1  26127  pjhthlem1  27468  staddi  28323  stadd3i  28325  cdj1i  28510  cdj3lem2b  28514  cdj3i  28518  addltmulALT  28523  raddcn  29137  subfacval3  30259  dnicld1  31466  dnibndlem2  31473  dnibndlem3  31474  dnibndlem5  31476  dnibndlem7  31478  iooelexlt  32210  cos2h  32394  tan2h  32395  poimir  32436  heicant  32438  mblfinlem2  32441  mblfinlem3  32442  ismblfin  32444  ftc1anclem3  32481  ftc1anclem4  32482  ftc1anclem6  32484  ftc1anclem7  32485  ftc1anclem8  32486  cntotbnd  32589  pellexlem5  36239  ioomidp  38411  stoweidlem59  38776  stirlinglem10  38800  fourierdlem103  38926  fourierdlem104  38927  fouriersw  38948  sge0isum  39144  sge0seq  39163  hoidmvlelem2  39310  smflimlem4  39484  smfmullem1  39500  fmtnodvds  39819  gbegt5  40008  leaddsuble  40190  2leaddle2  40191  2elfz2melfz  40202  elfzelfzlble  40205  clwwisshclwwslemlem  41255  eucrctshift  41433  ltsubaddb  42120  ltsubadd2b  42122  dp2cl  42292
  Copyright terms: Public domain W3C validator