Theorem rpmulcld 12448

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156   · cmul 10542  ℝ⁺crp 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-addrcl 10598  ax-mulrcl 10600  ax-rnegex 10608  ax-cnre 10610  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-rp 12391

This theorem is referenced by:  reccn2  14953  eirrlem  15557  nrginvrcnlem  23300  ovolscalem1  24114  itg2gt0  24361  aaliou3lem1  24931  aaliou3lem2  24932  aaliou3lem8  24934  cosordlem  25115  logcnlem2  25226  cxp2limlem  25553  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgsquadlem2  25957  2sqmod  26012  chtppilimlem1  26049  chtppilim  26051  chebbnd2  26053  chto1lb  26054  rplogsumlem1  26060  dchrvmasumlem1  26071  chpdifbndlem1  26129  chpdifbndlem2  26130  selberg3lem1  26133  selberg4lem1  26136  selberg4  26137  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntpbnd2  26163  pntlemd  26170  pntlema  26172  pntlemb  26173  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemo  26183  pntlem3  26185  pntleml  26187  pnt  26190  ttgcontlem1  26671  hgt750leme  31929  faclimlem1  32975  faclimlem3  32977  faclim  32978  unbdqndv2  33850  knoppndvlem17  33867  rrndstprj2  35124  pellfund14  39544  0ellimcdiv  41979  wallispilem3  42401  wallispilem4  42402  wallispi  42404  wallispi2lem1  42405  stirlinglem2  42409  stirlinglem3  42410  stirlinglem4  42411  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  stirlinglem14  42421  stirlinglem15  42422  stirlingr  42424  dirkertrigeqlem1  42432  dirkercncflem1  42437  dirkercncflem4  42440  hoiqssbllem1  42953  hoiqssbllem2  42954  hoiqssbllem3  42955  amgmwlem  44952  amgmw2d  44954