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

Theorem remulcld 6813
Description: Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1 (φA ℝ)
readdcld.2 (φB ℝ)
Assertion
Ref Expression
remulcld (φ → (A · B) ℝ)

Proof of Theorem remulcld
StepHypRef Expression
1 recnd.1 . 2 (φA ℝ)
2 readdcld.2 . 2 (φB ℝ)
3 remulcl 6767 . 2 ((A B ℝ) → (A · B) ℝ)
41, 2, 3syl2anc 391 1 (φ → (A · B) ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  (class class class)co 5455  cr 6670   · cmul 6676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-mulrcl 6742
This theorem is referenced by:  rimul  7329  ltmul1a  7335  ltmul1  7336  lemul1  7337  reapmul1lem  7338  reapmul1  7339  remulext1  7343  mulext1  7356  recexaplem2  7375  redivclap  7449  prodgt0gt0  7558  prodgt0  7559  prodge0  7561  lemul1a  7565  ltmuldiv  7581  ledivmul  7584  lt2mul2div  7586  lemuldiv  7588  lt2msq1  7592  lt2msq  7593  ltdiv23  7599  lediv23  7600  le2msq  7608  msq11  7609  lincmb01cmp  8601  iccf1o  8602  bernneq  8982  bernneq3  8984  expnbnd  8985  remullem  9059
  Copyright terms: Public domain W3C validator