ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  remulcld Unicode version

Theorem remulcld 7803
Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
readdcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
remulcld  |-  ( ph  ->  ( A  x.  B
)  e.  RR )

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 remulcl 7755 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3syl2anc 408 1  |-  ( ph  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480  (class class class)co 5774   RRcr 7626    x. cmul 7632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulrcl 7726
This theorem is referenced by:  rimul  8354  ltmul1a  8360  ltmul1  8361  lemul1  8362  reapmul1lem  8363  reapmul1  8364  remulext1  8368  mulext1  8381  recexaplem2  8420  redivclap  8498  prodgt0gt0  8616  prodgt0  8617  prodge0  8619  lemul1a  8623  ltmuldiv  8639  ledivmul  8642  lt2mul2div  8644  lemuldiv  8646  lt2msq1  8650  lt2msq  8651  ltdiv23  8657  lediv23  8658  le2msq  8666  msq11  8667  div4p1lem1div2  8980  mul2lt0rlt0  9553  lincmb01cmp  9793  iccf1o  9794  qbtwnrelemcalc  10040  qbtwnre  10041  flhalf  10082  modqval  10104  modqge0  10112  modqmulnn  10122  bernneq  10419  bernneq3  10421  expnbnd  10422  nn0opthlem2d  10474  faclbnd  10494  faclbnd6  10497  remullem  10650  cvg1nlemres  10764  resqrexlemover  10789  resqrexlemnm  10797  resqrexlemglsq  10801  sqrtmul  10814  abstri  10883  maxabslemlub  10986  maxltsup  10997  bdtrilem  11017  mulcn2  11088  reccn2ap  11089  cvgratnnlembern  11299  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  cvgratnnlemabsle  11303  cvgratnnlemfm  11305  cvgratnnlemrate  11306  mertenslemi1  11311  efcllem  11372  ege2le3  11384  eftlub  11403  sin02gt0  11477  cos12dec  11481  eirraplem  11490  dvdslelemd  11548  divalglemnqt  11624  oddennn  11912  metss2lem  12676  dveflem  12865  sin0pilem1  12875  sin0pilem2  12876  tangtx  12932  trilpolemclim  13259  trilpolemcl  13260  trilpolemisumle  13261  trilpolemeq1  13263  trilpolemlt1  13264
  Copyright terms: Public domain W3C validator