Theorem rpmulcld 11283

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	|- ( ph -> A e. RR+ )
rpaddcld.1	|- ( ph -> B e. RR+ )

Assertion

Ref	Expression
rpmulcld	|- ( ph -> ( A x. B ) e. RR+ )

Proof of Theorem rpmulcld

Step	Hyp	Ref	Expression
1		rpred.1	. 2 |- ( ph -> A e. RR+ )
2		rpaddcld.1	. 2 |- ( ph -> B e. RR+ )
3		rpmulcl 11252	. 2 |- ( ( A e. RR+ /\ B e. RR+ ) -> ( A x. B ) e. RR+ )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( A x. B ) e. RR+ )

Syntax hints:   -> wi 4   e. wcel 1804  (class class class)co 6281   x. cmul 9500   RR+crp 11231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-mulgt0 9572

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-ltxr 9636  df-rp 11232

This theorem is referenced by:  reccn2  13401  eirrlem  13919  nrginvrcnlem  21177  ovolscalem1  21902  itg2gt0  22145  aaliou3lem1  22716  aaliou3lem2  22717  aaliou3lem8  22719  cosordlem  22896  logcnlem2  23002  cxp2limlem  23283  lgsquadlem2  23608  chtppilimlem1  23636  chtppilim  23638  chebbnd2  23640  chto1lb  23641  rplogsumlem1  23647  dchrvmasumlem1  23658  chpdifbndlem1  23716  chpdifbndlem2  23717  selberg3lem1  23720  selberg4lem1  23723  selberg4  23724  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntpbnd2  23750  pntlemd  23757  pntlema  23759  pntlemb  23760  pntlemq  23764  pntlemr  23765  pntlemj  23766  pntlemf  23768  pntlemo  23770  pntlem3  23772  pntleml  23774  pnt  23777  ttgcontlem1  24166  2sqmod  27614  lgamgulmlem3  28551  lgamgulmlem4  28552  lgamgulmlem5  28553  lgamgulmlem6  28554  faclimlem1  29144  faclimlem3  29146  faclim  29147  rrndstprj2  30303  pellfund14  30810  0ellimcdiv  31609  wallispilem3  31803  wallispilem4  31804  wallispi  31806  wallispi2lem1  31807  stirlinglem2  31811  stirlinglem3  31812  stirlinglem4  31813  stirlinglem6  31815  stirlinglem7  31816  stirlinglem10  31819  stirlinglem11  31820  stirlinglem12  31821  stirlinglem13  31822  stirlinglem14  31823  stirlinglem15  31824  stirlingr  31826  dirkertrigeqlem1  31834  dirkercncflem1  31839  dirkercncflem4  31842