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

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

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 11113 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  (class class class)co 7358  cr 11051   + caddc 11055
This theorem was proved from axioms:  ax-addrcl 11113
This theorem is referenced by:  0re  11158  readdcli  11171  readdcld  11185  axltadd  11229  peano2re  11329  00id  11331  0cnALT  11390  resubcl  11466  ltaddsub  11630  leaddsub  11632  ltleadd  11639  ltaddsublt  11783  recex  11788  recp1lt1  12054  recreclt  12055  supadd  12124  cju  12150  nnge1  12182  addltmul  12390  avglt1  12392  avglt2  12393  avgle1  12394  avgle2  12395  nzadd  12552  irradd  12899  rpnnen1lem5  12907  rpaddcl  12938  xaddf  13144  xaddnemnf  13156  xaddnepnf  13157  xnegdi  13168  xaddass  13169  xadddilem  13214  iooshf  13344  ge0addcl  13378  icoshft  13391  icoshftf1o  13392  iccshftr  13404  difelfznle  13556  elfzodifsumelfzo  13639  subfzo0  13695  flbi2  13723  modcyc  13812  modadd1  13814  modsumfzodifsn  13850  serfre  13938  sermono  13941  serge0  13963  serle  13964  bernneq  14133  faclbnd6  14200  hashfun  14338  ccatsymb  14471  swrdswrdlem  14593  swrdccatin2  14618  cshweqrep  14710  cshwcsh2id  14718  readd  15012  imadd  15020  elicc4abs  15205  rddif  15226  absrdbnd  15227  caubnd2  15243  mulcn2  15479  o1add  15497  o1sub  15499  lo1add  15510  fsumrecl  15620  rerisefaccl  15901  rprisefaccl  15907  efgt1  15999  pythagtriplem12  16699  pythagtriplem14  16701  pythagtriplem16  16703  remulg  21014  resubdrg  21015  prdsxmetlem  23724  xmeter  23789  bl2ioo  24158  ioo2bl  24159  ioo2blex  24160  blssioo  24161  reperf  24185  reconnlem2  24193  opnreen  24197  icopnfcnv  24308  pcoass  24390  pjthlem1  24804  ovolun  24866  shft2rab  24875  volun  24912  mbfaddlem  25027  i1fadd  25062  itg1addlem4  25066  itg1addlem4OLD  25067  itg2monolem1  25118  ply1divex  25504  psercnlem1  25787  reefgim  25812  tangtx  25865  efif1olem1  25901  efif1olem2  25902  efif1o  25905  relogmul  25950  argimgt0  25970  logimul  25972  ang180lem1  26162  atanlogaddlem  26266  atanlogsublem  26268  atantan  26276  ressatans  26287  emcllem6  26353  basellem9  26441  ppiub  26555  bposlem5  26639  bposlem6  26640  bposlem9  26643  chpchtlim  26830  mulog2sumlem1  26885  mulog2sumlem2  26886  selberglem2  26897  pntrmax  26915  pntpbnd1a  26936  pntpbnd2  26938  pntibndlem3  26943  pntlemb  26948  pntlemk  26957  axsegconlem7  27875  axsegconlem9  27877  axsegconlem10  27878  clwwisshclwwslemlem  28960  eucrctshift  29190  pjhthlem1  30336  staddi  31191  stadd3i  31193  cdj1i  31378  cdj3lem2b  31382  cdj3i  31386  addltmulALT  31391  dp2cl  31739  rpdp2cl  31741  raddcn  32513  subfacval3  33786  dnicld1  34938  dnibndlem2  34945  dnibndlem3  34946  dnibndlem5  34948  dnibndlem7  34950  iooelexlt  35836  cos2h  36072  tan2h  36073  poimir  36114  heicant  36116  mblfinlem2  36119  mblfinlem3  36120  ismblfin  36122  ftc1anclem3  36156  ftc1anclem4  36157  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  cntotbnd  36258  2xp3dxp2ge1d  40617  elre0re  40780  repncan2  40854  readdsub  40856  reltsubadd2  40859  resubsub4  40861  repnpcan  40864  reppncan  40865  pellexlem5  41159  ioomidp  43759  stoweidlem59  44307  stirlinglem10  44331  fourierdlem103  44457  fourierdlem104  44458  fouriersw  44479  sge0isum  44675  sge0seq  44694  hoidmvlelem2  44844  smflimlem4  45022  smfmullem1  45039  leaddsuble  45536  2leaddle2  45537  2elfz2melfz  45557  elfzelfzlble  45560  fmtnodvds  45743  gbegt5  45960  ltsubaddb  46602  ltsubadd2b  46604
  Copyright terms: Public domain W3C validator