Theorem rpmulcld 13135

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7409   · cmul 11162  ℝ⁺crp 13075

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-resscn 11214  ax-1cn 11215  ax-addrcl 11218  ax-mulrcl 11220  ax-rnegex 11228  ax-cnre 11230  ax-pre-mulgt0 11234

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-ltxr 11305  df-rp 13076

This theorem is used by:  reccn2  15717  eirrlem  16325  nrginvrcnlem  24957  ovolscalem1  25781  itg2gt0  26028  aaliou3lem1  26618  aaliou3lem2  26619  aaliou3lem8  26621  cosordlem  26807  logcnlem2  26920  cxp2limlem  27252  lgamgulmlem3  27307  lgamgulmlem4  27308  lgamgulmlem5  27309  lgamgulmlem6  27310  lgsquadlem2  27657  2sqmod  27712  chtppilimlem1  27749  chtppilim  27751  chebbnd2  27753  chto1lb  27754  rplogsumlem1  27760  dchrvmasumlem1  27771  chpdifbndlem1  27829  chpdifbndlem2  27830  selberg3lem1  27833  selberg4lem1  27836  selberg4  27837  pntrlog2bndlem2  27854  pntrlog2bndlem3  27855  pntrlog2bndlem4  27856  pntrlog2bndlem5  27857  pntpbnd2  27863  pntlemd  27870  pntlema  27872  pntlemb  27873  pntlemq  27877  pntlemr  27878  pntlemj  27879  pntlemf  27881  pntlemo  27883  pntlem3  27885  pntleml  27887  pnt  27890  ttgcontlem1  29381  hgt750leme  35207  faclimlem1  36423  faclimlem3  36425  faclim  36426  unbdqndv2  37293  knoppndvlem17  37310  rrndstprj2  38679  aks4d1p1p7  43038  pellfund14  43837  0ellimcdiv  46575  wallispilem3  46993  wallispilem4  46994  wallispi  46996  wallispi2lem1  46997  stirlinglem2  47001  stirlinglem3  47002  stirlinglem4  47003  stirlinglem6  47005  stirlinglem7  47006  stirlinglem10  47009  stirlinglem11  47010  stirlinglem12  47011  stirlinglem13  47012  stirlinglem14  47013  stirlinglem15  47014  stirlingr  47016  dirkertrigeqlem1  47024  dirkercncflem1  47029  dirkercncflem4  47032  hoiqssbllem1  47548  hoiqssbllem2  47549  hoiqssbllem3  47550  gpg3kgrtriexlem2  49098  amgmwlem  50903  amgmw2d  50905