Theorem rpmulcld 12999

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 12964	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7364   · cmul 11040  ℝ⁺crp 12939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-addrcl 11096  ax-mulrcl 11098  ax-rnegex 11106  ax-cnre 11108  ax-pre-mulgt0 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-ltxr 11181  df-rp 12940

This theorem is referenced by:  reccn2  15556  eirrlem  16168  nrginvrcnlem  24672  ovolscalem1  25496  itg2gt0  25743  aaliou3lem1  26325  aaliou3lem2  26326  aaliou3lem8  26328  cosordlem  26513  logcnlem2  26626  cxp2limlem  26959  lgamgulmlem3  27014  lgamgulmlem4  27015  lgamgulmlem5  27016  lgamgulmlem6  27017  lgsquadlem2  27364  2sqmod  27419  chtppilimlem1  27456  chtppilim  27458  chebbnd2  27460  chto1lb  27461  rplogsumlem1  27467  dchrvmasumlem1  27478  chpdifbndlem1  27536  chpdifbndlem2  27537  selberg3lem1  27540  selberg4lem1  27543  selberg4  27544  pntrlog2bndlem2  27561  pntrlog2bndlem3  27562  pntrlog2bndlem4  27563  pntrlog2bndlem5  27564  pntpbnd2  27570  pntlemd  27577  pntlema  27579  pntlemb  27580  pntlemq  27584  pntlemr  27585  pntlemj  27586  pntlemf  27588  pntlemo  27590  pntlem3  27592  pntleml  27594  pnt  27597  ttgcontlem1  28973  hgt750leme  34824  faclimlem1  35947  faclimlem3  35949  faclim  35950  unbdqndv2  36793  knoppndvlem17  36810  rrndstprj2  38174  aks4d1p1p7  42535  pellfund14  43352  0ellimcdiv  46103  wallispilem3  46521  wallispilem4  46522  wallispi  46524  wallispi2lem1  46525  stirlinglem2  46529  stirlinglem3  46530  stirlinglem4  46531  stirlinglem6  46533  stirlinglem7  46534  stirlinglem10  46537  stirlinglem11  46538  stirlinglem12  46539  stirlinglem13  46540  stirlinglem14  46541  stirlinglem15  46542  stirlingr  46544  dirkertrigeqlem1  46552  dirkercncflem1  46557  dirkercncflem4  46560  hoiqssbllem1  47076  hoiqssbllem2  47077  hoiqssbllem3  47078  gpg3kgrtriexlem2  48580  amgmwlem  50297  amgmw2d  50299