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

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

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 10035 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  (class class class)co 6690  cr 9973   + caddc 9977
This theorem was proved from axioms:  ax-addrcl 10035
This theorem is referenced by:  0re  10078  readdcli  10091  readdcld  10107  axltadd  10149  peano2re  10247  00id  10249  resubcl  10383  ltaddsub  10540  leaddsub  10542  ltleadd  10549  ltaddsublt  10692  recex  10697  recp1lt1  10959  recreclt  10960  supadd  11029  cju  11054  nnge1  11084  addltmul  11306  avglt1  11308  avglt2  11309  avgle1  11310  avgle2  11311  nzadd  11463  irradd  11850  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  rpaddcl  11892  xaddf  12093  xaddnemnf  12105  xaddnepnf  12106  xnegdi  12116  xaddass  12117  xadddilem  12162  iooshf  12290  ge0addcl  12322  icoshft  12332  icoshftf1o  12333  iccshftr  12344  difelfznle  12492  elfzodifsumelfzo  12573  subfzo0  12630  flbi2  12658  modcyc  12745  modadd1  12747  modsumfzodifsn  12783  serfre  12870  sermono  12873  serge0  12895  serle  12896  bernneq  13030  faclbnd6  13126  hashfun  13262  ccatsymb  13400  swrdswrdlem  13505  swrdccatin2  13533  cshweqrep  13613  cshwcsh2id  13620  readd  13910  imadd  13918  elicc4abs  14103  rddif  14124  absrdbnd  14125  caubnd2  14141  mulcn2  14370  o1add  14388  o1sub  14390  lo1add  14401  fsumrecl  14509  rerisefaccl  14792  rprisefaccl  14798  efgt1  14890  pythagtriplem12  15578  pythagtriplem14  15580  pythagtriplem16  15582  remulg  20001  resubdrg  20002  prdsxmetlem  22220  xmeter  22285  bl2ioo  22642  ioo2bl  22643  ioo2blex  22644  blssioo  22645  reperf  22669  reconnlem2  22677  opnreen  22681  icopnfcnv  22788  pcoass  22870  pjthlem1  23254  ovolun  23313  shft2rab  23322  volun  23359  mbfaddlem  23472  i1fadd  23507  itg1addlem4  23511  itg2monolem1  23562  ply1divex  23941  psercnlem1  24224  reefgim  24249  tangtx  24302  efif1olem1  24333  efif1olem2  24334  efif1o  24337  relogmul  24383  argimgt0  24403  logimul  24405  ang180lem1  24584  atanlogaddlem  24685  atanlogsublem  24687  atantan  24695  ressatans  24706  emcllem6  24772  basellem9  24860  ppiub  24974  bposlem5  25058  bposlem6  25059  bposlem9  25062  chpchtlim  25213  mulog2sumlem1  25268  mulog2sumlem2  25269  selberglem2  25280  pntrmax  25298  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem3  25326  pntlemb  25331  pntlemk  25340  axsegconlem7  25848  axsegconlem9  25850  axsegconlem10  25851  clwwisshclwwslemlem  26970  eucrctshift  27221  pjhthlem1  28378  staddi  29233  stadd3i  29235  cdj1i  29420  cdj3lem2b  29424  cdj3i  29428  addltmulALT  29433  dp2cl  29715  rpdp2cl  29717  raddcn  30103  subfacval3  31297  dnicld1  32587  dnibndlem2  32594  dnibndlem3  32595  dnibndlem5  32597  dnibndlem7  32599  iooelexlt  33340  cos2h  33530  tan2h  33531  poimir  33572  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  ismblfin  33580  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  cntotbnd  33725  pellexlem5  37714  ioomidp  40058  stoweidlem59  40594  stirlinglem10  40618  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  sge0isum  40962  sge0seq  40981  hoidmvlelem2  41131  smflimlem4  41303  smfmullem1  41319  leaddsuble  41636  2leaddle2  41637  2elfz2melfz  41653  elfzelfzlble  41656  fmtnodvds  41781  gbegt5  41974  ltsubaddb  42629  ltsubadd2b  42631
  Copyright terms: Public domain W3C validator