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

Theorem remulcld 7497
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 7449 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1438  (class class class)co 5634  cr 7328   · cmul 7334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-mulrcl 7423
This theorem is referenced by:  rimul  8038  ltmul1a  8044  ltmul1  8045  lemul1  8046  reapmul1lem  8047  reapmul1  8048  remulext1  8052  mulext1  8065  recexaplem2  8095  redivclap  8172  prodgt0gt0  8284  prodgt0  8285  prodge0  8287  lemul1a  8291  ltmuldiv  8307  ledivmul  8310  lt2mul2div  8312  lemuldiv  8314  lt2msq1  8318  lt2msq  8319  ltdiv23  8325  lediv23  8326  le2msq  8334  msq11  8335  div4p1lem1div2  8639  lincmb01cmp  9389  iccf1o  9390  qbtwnrelemcalc  9632  qbtwnre  9633  flhalf  9674  modqval  9696  modqge0  9704  modqmulnn  9714  bernneq  10039  bernneq3  10041  expnbnd  10042  nn0opthlem2d  10094  faclbnd  10114  faclbnd6  10117  remullem  10270  cvg1nlemres  10383  resqrexlemover  10408  resqrexlemnm  10416  resqrexlemglsq  10420  sqrtmul  10433  abstri  10502  maxabslemlub  10605  maxltsup  10616  mulcn2  10665  cvgratnnlembern  10878  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  cvgratnnlemabsle  10882  cvgratnnlemfm  10884  cvgratnnlemrate  10885  dvdslelemd  10937  divalglemnqt  11013  oddennn  11298
  Copyright terms: Public domain W3C validator