Theorem rpmulcld 13055

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398   · cmul 11080  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-mulrcl 11138  ax-rnegex 11146  ax-cnre 11148  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-rp 12996

This theorem is referenced by:  reccn2  15626  eirrlem  16238  nrginvrcnlem  24753  ovolscalem1  25577  itg2gt0  25824  aaliou3lem1  26408  aaliou3lem2  26409  aaliou3lem8  26411  cosordlem  26597  logcnlem2  26710  cxp2limlem  27042  lgamgulmlem3  27097  lgamgulmlem4  27098  lgamgulmlem5  27099  lgamgulmlem6  27100  lgsquadlem2  27447  2sqmod  27502  chtppilimlem1  27539  chtppilim  27541  chebbnd2  27543  chto1lb  27544  rplogsumlem1  27550  dchrvmasumlem1  27561  chpdifbndlem1  27619  chpdifbndlem2  27620  selberg3lem1  27623  selberg4lem1  27626  selberg4  27627  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntpbnd2  27653  pntlemd  27660  pntlema  27662  pntlemb  27663  pntlemq  27667  pntlemr  27668  pntlemj  27669  pntlemf  27671  pntlemo  27673  pntlem3  27675  pntleml  27677  pnt  27680  ttgcontlem1  29087  hgt750leme  34954  faclimlem1  36098  faclimlem3  36100  faclim  36101  unbdqndv2  36954  knoppndvlem17  36971  rrndstprj2  38335  aks4d1p1p7  42696  pellfund14  43480  0ellimcdiv  46228  wallispilem3  46646  wallispilem4  46647  wallispi  46649  wallispi2lem1  46650  stirlinglem2  46654  stirlinglem3  46655  stirlinglem4  46656  stirlinglem6  46658  stirlinglem7  46659  stirlinglem10  46662  stirlinglem11  46663  stirlinglem12  46664  stirlinglem13  46665  stirlinglem14  46666  stirlinglem15  46667  stirlingr  46669  dirkertrigeqlem1  46677  dirkercncflem1  46682  dirkercncflem4  46685  hoiqssbllem1  47201  hoiqssbllem2  47202  hoiqssbllem3  47203  gpg3kgrtriexlem2  48711  amgmwlem  50428  amgmw2d  50430