Theorem remulcld 8356

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

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		remulcl 8307	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 8278

This theorem is used by:  rimul  8913  ltmul1a  8919  ltmul1  8920  lemul1  8921  reapmul1lem  8922  reapmul1  8923  remulext1  8927  mulext1  8940  recexaplem2  8980  redivclap  9061  prodgt0gt0  9181  prodgt0  9182  prodge0  9184  lemul1a  9188  ltmuldiv  9204  ledivmul  9207  lt2mul2div  9209  lemuldiv  9211  lt2msq1  9215  lt2msq  9216  ltdiv23  9222  lediv23  9223  le2msq  9231  msq11  9232  div4p1lem1div2  9559  mul2lt0rlt0  10160  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  qbtwnrelemcalc  10690  qbtwnre  10691  flhalf  10737  modqval  10761  modqge0  10769  modqmulnn  10779  bernneq  11098  bernneq3  11100  expnbnd  11101  nn0opthlem2d  11159  faclbnd  11179  faclbnd6  11182  remullem  11636  sq01  11660  cvg1nlemres  11751  resqrexlemover  11776  resqrexlemnm  11784  resqrexlemglsq  11788  sqrtmul  11801  abstri  11870  maxabslemlub  11973  maxltsup  11984  bdtrilem  12005  mulcn2  12078  reccn2ap  12079  cvgratnnlembern  12290  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemabsle  12294  cvgratnnlemfm  12296  cvgratnnlemrate  12297  mertenslemi1  12302  fprodge1  12406  efcllem  12426  ege2le3  12438  eftlub  12457  sin02gt0  12531  cos12dec  12535  eirraplem  12544  dvdslelemd  12610  divalglemnqt  12687  bitsp1o  12720  2expltfac  13218  oddennn  13283  metss2lem  15598  dveflem  15827  sin0pilem1  15882  sin0pilem2  15883  tangtx  15939  logdivlti  15982  rpcxpcl  16005  cxpmul  16014  cxplt  16018  rpcxple2  16020  rpcxplt2  16021  apcxp2  16041  rpabscxpbnd  16042  log2tlbndlog2  16082  pellexlem2  16092  perfectlem2  16114  lgsdilem  16146  gausslemma2dlem0c  16170  gausslemma2dlem2  16181  gausslemma2dlem3  16182  lgsquadlem1  16196  lgsquadlem2  16197  dichmul0orlem1  16753  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  nconstwlpolemgt0  17114