Theorem rpmulcld 12990

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7370   · cmul 11052  ℝ⁺crp 12930

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7692  ax-resscn 11104  ax-1cn 11105  ax-addrcl 11108  ax-mulrcl 11110  ax-rnegex 11118  ax-cnre 11120  ax-pre-mulgt0 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8649  df-en 8897  df-dom 8898  df-sdom 8899  df-pnf 11189  df-mnf 11190  df-ltxr 11192  df-rp 12931

This theorem is referenced by:  reccn2  15541  eirrlem  16150  nrginvrcnlem  24614  ovolscalem1  25449  itg2gt0  25696  aaliou3lem1  26285  aaliou3lem2  26286  aaliou3lem8  26288  cosordlem  26474  logcnlem2  26587  cxp2limlem  26921  lgamgulmlem3  26976  lgamgulmlem4  26977  lgamgulmlem5  26978  lgamgulmlem6  26979  lgsquadlem2  27327  2sqmod  27382  chtppilimlem1  27419  chtppilim  27421  chebbnd2  27423  chto1lb  27424  rplogsumlem1  27430  dchrvmasumlem1  27441  chpdifbndlem1  27499  chpdifbndlem2  27500  selberg3lem1  27503  selberg4lem1  27506  selberg4  27507  pntrlog2bndlem2  27524  pntrlog2bndlem3  27525  pntrlog2bndlem4  27526  pntrlog2bndlem5  27527  pntpbnd2  27533  pntlemd  27540  pntlema  27542  pntlemb  27543  pntlemq  27547  pntlemr  27548  pntlemj  27549  pntlemf  27551  pntlemo  27553  pntlem3  27555  pntleml  27557  pnt  27560  ttgcontlem1  28867  hgt750leme  34644  faclimlem1  35725  faclimlem3  35727  faclim  35728  unbdqndv2  36494  knoppndvlem17  36511  rrndstprj2  37820  aks4d1p1p7  42057  pellfund14  42881  0ellimcdiv  45642  wallispilem3  46060  wallispilem4  46061  wallispi  46063  wallispi2lem1  46064  stirlinglem2  46068  stirlinglem3  46069  stirlinglem4  46070  stirlinglem6  46072  stirlinglem7  46073  stirlinglem10  46076  stirlinglem11  46077  stirlinglem12  46078  stirlinglem13  46079  stirlinglem14  46080  stirlinglem15  46081  stirlingr  46083  dirkertrigeqlem1  46091  dirkercncflem1  46096  dirkercncflem4  46099  hoiqssbllem1  46615  hoiqssbllem2  46616  hoiqssbllem3  46617  gpg3kgrtriexlem2  48070  amgmwlem  49786  amgmw2d  49788