Theorem rpmulcld 13093

Description: Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)
rpaddcld.1	⊢ (𝜑 → 𝐵 ∈ ℝ+)

Assertion

Ref	Expression
rpmulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ+)

Proof of Theorem rpmulcld

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpaddcld.1	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
3		rpmulcl 13058	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431   · cmul 11160  ℝ⁺crp 13034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-addrcl 11216  ax-mulrcl 11218  ax-rnegex 11226  ax-cnre 11228  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-rp 13035

This theorem is referenced by:  reccn2  15633  eirrlem  16240  nrginvrcnlem  24712  ovolscalem1  25548  itg2gt0  25795  aaliou3lem1  26384  aaliou3lem2  26385  aaliou3lem8  26387  cosordlem  26572  logcnlem2  26685  cxp2limlem  27019  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgsquadlem2  27425  2sqmod  27480  chtppilimlem1  27517  chtppilim  27519  chebbnd2  27521  chto1lb  27522  rplogsumlem1  27528  dchrvmasumlem1  27539  chpdifbndlem1  27597  chpdifbndlem2  27598  selberg3lem1  27601  selberg4lem1  27604  selberg4  27605  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntpbnd2  27631  pntlemd  27638  pntlema  27640  pntlemb  27641  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemf  27649  pntlemo  27651  pntlem3  27653  pntleml  27655  pnt  27658  ttgcontlem1  28899  hgt750leme  34673  faclimlem1  35743  faclimlem3  35745  faclim  35746  unbdqndv2  36512  knoppndvlem17  36529  rrndstprj2  37838  aks4d1p1p7  42075  pellfund14  42909  0ellimcdiv  45664  wallispilem3  46082  wallispilem4  46083  wallispi  46085  wallispi2lem1  46086  stirlinglem2  46090  stirlinglem3  46091  stirlinglem4  46092  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  dirkertrigeqlem1  46113  dirkercncflem1  46118  dirkercncflem4  46121  hoiqssbllem1  46637  hoiqssbllem2  46638  hoiqssbllem3  46639  gpg3kgrtriexlem2  48040  amgmwlem  49321  amgmw2d  49323