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

Theorem remulcld 7263
Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1 (𝜑𝐴 ∈ ℝ)
readdcld.2 (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
remulcld (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 readdcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 remulcl 7215 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  (class class class)co 5563  cr 7094   · cmul 7100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulrcl 7189
This theorem is referenced by:  rimul  7804  ltmul1a  7810  ltmul1  7811  lemul1  7812  reapmul1lem  7813  reapmul1  7814  remulext1  7818  mulext1  7831  recexaplem2  7861  redivclap  7938  prodgt0gt0  8048  prodgt0  8049  prodge0  8051  lemul1a  8055  ltmuldiv  8071  ledivmul  8074  lt2mul2div  8076  lemuldiv  8078  lt2msq1  8082  lt2msq  8083  ltdiv23  8089  lediv23  8090  le2msq  8098  msq11  8099  div4p1lem1div2  8403  lincmb01cmp  9153  iccf1o  9154  qbtwnrelemcalc  9394  qbtwnre  9395  flhalf  9436  modqval  9458  modqge0  9466  modqmulnn  9476  bernneq  9742  bernneq3  9744  expnbnd  9745  nn0opthlem2d  9797  faclbnd  9817  faclbnd6  9820  remullem  9959  cvg1nlemres  10072  resqrexlemover  10097  resqrexlemnm  10105  resqrexlemglsq  10109  sqrtmul  10122  abstri  10191  maxabslemlub  10294  maxltsup  10305  mulcn2  10352  dvdslelemd  10451  divalglemnqt  10527  oddennn  10812
  Copyright terms: Public domain W3C validator