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

Theorem remulcld 7115
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 7067 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
41, 2, 3syl2anc 397 1  |-  ( ph  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1409  (class class class)co 5540   RRcr 6946    x. cmul 6952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105  ax-mulrcl 7041
This theorem is referenced by:  rimul  7650  ltmul1a  7656  ltmul1  7657  lemul1  7658  reapmul1lem  7659  reapmul1  7660  remulext1  7664  mulext1  7677  recexaplem2  7707  redivclap  7782  prodgt0gt0  7892  prodgt0  7893  prodge0  7895  lemul1a  7899  ltmuldiv  7915  ledivmul  7918  lt2mul2div  7920  lemuldiv  7922  lt2msq1  7926  lt2msq  7927  ltdiv23  7933  lediv23  7934  le2msq  7942  msq11  7943  div4p1lem1div2  8235  lincmb01cmp  8972  iccf1o  8973  qbtwnrelemcalc  9212  qbtwnre  9213  flhalf  9252  modqval  9274  modqge0  9282  modqmulnn  9292  bernneq  9537  bernneq3  9539  expnbnd  9540  nn0opthlem2d  9589  faclbnd  9609  faclbnd6  9612  remullem  9699  cvg1nlemres  9812  resqrexlemover  9837  resqrexlemnm  9845  resqrexlemglsq  9849  sqrtmul  9862  abstri  9931  mulcn2  10064  dvdslelemd  10155  divalglemnqt  10232
  Copyright terms: Public domain W3C validator