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

Theorem remulcld 7114
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 7066 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 397 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  (class class class)co 5539  cr 6945   · cmul 6951
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105  ax-mulrcl 7040
This theorem is referenced by:  rimul  7649  ltmul1a  7655  ltmul1  7656  lemul1  7657  reapmul1lem  7658  reapmul1  7659  remulext1  7663  mulext1  7676  recexaplem2  7706  redivclap  7781  prodgt0gt0  7891  prodgt0  7892  prodge0  7894  lemul1a  7898  ltmuldiv  7914  ledivmul  7917  lt2mul2div  7919  lemuldiv  7921  lt2msq1  7925  lt2msq  7926  ltdiv23  7932  lediv23  7933  le2msq  7941  msq11  7942  div4p1lem1div2  8234  lincmb01cmp  8971  iccf1o  8972  qbtwnrelemcalc  9211  qbtwnre  9212  flhalf  9246  modqval  9268  modqge0  9276  modqmulnn  9286  bernneq  9530  bernneq3  9532  expnbnd  9533  nn0opthlem2d  9582  faclbnd  9602  faclbnd6  9605  remullem  9692  cvg1nlemres  9805  resqrexlemover  9829  resqrexlemnm  9837  resqrexlemglsq  9841  sqrtmul  9854  abstri  9923  mulcn2  10056  dvdslelemd  10147
  Copyright terms: Public domain W3C validator