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

Theorem remulcld 7764
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 7716 . 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 1465  (class class class)co 5742   RRcr 7587    x. cmul 7593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulrcl 7687
This theorem is referenced by:  rimul  8315  ltmul1a  8321  ltmul1  8322  lemul1  8323  reapmul1lem  8324  reapmul1  8325  remulext1  8329  mulext1  8342  recexaplem2  8381  redivclap  8459  prodgt0gt0  8577  prodgt0  8578  prodge0  8580  lemul1a  8584  ltmuldiv  8600  ledivmul  8603  lt2mul2div  8605  lemuldiv  8607  lt2msq1  8611  lt2msq  8612  ltdiv23  8618  lediv23  8619  le2msq  8627  msq11  8628  div4p1lem1div2  8941  mul2lt0rlt0  9514  lincmb01cmp  9754  iccf1o  9755  qbtwnrelemcalc  10001  qbtwnre  10002  flhalf  10043  modqval  10065  modqge0  10073  modqmulnn  10083  bernneq  10380  bernneq3  10382  expnbnd  10383  nn0opthlem2d  10435  faclbnd  10455  faclbnd6  10458  remullem  10611  cvg1nlemres  10725  resqrexlemover  10750  resqrexlemnm  10758  resqrexlemglsq  10762  sqrtmul  10775  abstri  10844  maxabslemlub  10947  maxltsup  10958  bdtrilem  10978  mulcn2  11049  reccn2ap  11050  cvgratnnlembern  11260  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemabsle  11264  cvgratnnlemfm  11266  cvgratnnlemrate  11267  mertenslemi1  11272  efcllem  11292  ege2le3  11304  eftlub  11323  sin02gt0  11397  cos12dec  11401  eirraplem  11410  dvdslelemd  11468  divalglemnqt  11544  oddennn  11832  metss2lem  12593  dveflem  12782  sin0pilem1  12789  sin0pilem2  12790  tangtx  12846  trilpolemclim  13156  trilpolemcl  13157  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator