Theorem rpmulcld 12989

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369   · cmul 11051  ℝ⁺crp 12929

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 7691  ax-resscn 11103  ax-1cn 11104  ax-addrcl 11107  ax-mulrcl 11109  ax-rnegex 11117  ax-cnre 11119  ax-pre-mulgt0 11123

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 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11188  df-mnf 11189  df-ltxr 11191  df-rp 12930

This theorem is referenced by:  reccn2  15540  eirrlem  16149  nrginvrcnlem  24613  ovolscalem1  25448  itg2gt0  25695  aaliou3lem1  26284  aaliou3lem2  26285  aaliou3lem8  26287  cosordlem  26473  logcnlem2  26586  cxp2limlem  26920  lgamgulmlem3  26975  lgamgulmlem4  26976  lgamgulmlem5  26977  lgamgulmlem6  26978  lgsquadlem2  27326  2sqmod  27381  chtppilimlem1  27418  chtppilim  27420  chebbnd2  27422  chto1lb  27423  rplogsumlem1  27429  dchrvmasumlem1  27440  chpdifbndlem1  27498  chpdifbndlem2  27499  selberg3lem1  27502  selberg4lem1  27505  selberg4  27506  pntrlog2bndlem2  27523  pntrlog2bndlem3  27524  pntrlog2bndlem4  27525  pntrlog2bndlem5  27526  pntpbnd2  27532  pntlemd  27539  pntlema  27541  pntlemb  27542  pntlemq  27546  pntlemr  27547  pntlemj  27548  pntlemf  27550  pntlemo  27552  pntlem3  27554  pntleml  27556  pnt  27559  ttgcontlem1  28866  hgt750leme  34643  faclimlem1  35724  faclimlem3  35726  faclim  35727  unbdqndv2  36493  knoppndvlem17  36510  rrndstprj2  37819  aks4d1p1p7  42056  pellfund14  42880  0ellimcdiv  45641  wallispilem3  46059  wallispilem4  46060  wallispi  46062  wallispi2lem1  46063  stirlinglem2  46067  stirlinglem3  46068  stirlinglem4  46069  stirlinglem6  46071  stirlinglem7  46072  stirlinglem10  46075  stirlinglem11  46076  stirlinglem12  46077  stirlinglem13  46078  stirlinglem14  46079  stirlinglem15  46080  stirlingr  46082  dirkertrigeqlem1  46090  dirkercncflem1  46095  dirkercncflem4  46098  hoiqssbllem1  46614  hoiqssbllem2  46615  hoiqssbllem3  46616  gpg3kgrtriexlem2  48069  amgmwlem  49785  amgmw2d  49787