Theorem rpmulcl 12962

Description: Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
rpmulcl	⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)

Proof of Theorem rpmulcl

Step	Hyp	Ref	Expression
1		rpre 12946	. . 3 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2		rpre 12946	. . 3 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ)
3		remulcl 11118	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	syl2an 603	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ)
5		elrp 12939	. . 3 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
6		elrp 12939	. . 3 ⊢ (𝐵 ∈ ℝ+ ↔ (𝐵 ∈ ℝ ∧ 0 < 𝐵))
7		mulgt0 11218	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵))
8	5, 6, 7	syl2anb 605	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → 0 < (𝐴 · 𝐵))
9		elrp 12939	. 2 ⊢ ((𝐴 · 𝐵) ∈ ℝ+ ↔ ((𝐴 · 𝐵) ∈ ℝ ∧ 0 < (𝐴 · 𝐵)))
10	4, 8, 9	sylanbrc 590	1 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121   class class class wbr 5075  (class class class)co 7360  ℝcr 11032  0cc0 11033   · cmul 11038   < clt 11174  ℝ⁺crp 12937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-resscn 11090  ax-1cn 11091  ax-addrcl 11094  ax-mulrcl 11096  ax-rnegex 11104  ax-cnre 11106  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-ltxr 11179  df-rp 12938

This theorem is referenced by:  rpmtmip  12963  rpmulcld  12997  moddi  13896  rpexpcl  14037  discr  14197  reccn2  15554  expcnv  15824  fprodrpcl  15916  rprisefaccl  15983  rpmsubg  21410  ovolscalem2  25503  aaliou3lem7  26337  aaliou3lem9  26338  cos02pilt1  26512  cosordlem  26516  logfac  26587  loglesqrt  26747  divsqrtsumlem  26965  basellem1  27066  pclogsum  27200  bclbnd  27265  bposlem7  27275  bposlem8  27276  bposlem9  27277  chebbnd1lem2  27455  dchrisum0lem3  27504  chpdifbndlem2  27539  pntrsumbnd2  27552  pntpbnd1a  27570  pntpbnd2  27572  pntibnd  27578  pntlemd  27579  pntlema  27581  pntlemb  27582  pntlemf  27590  pntlemo  27592  minvecolem3  30969  knoppndvlem18  36850  taupilem1  37696  taupilem2  37697  taupi  37698  ftc1anclem7  38081  ftc1anc  38083  isbnd2  38165  wallispilem4  46525  wallispi  46527  dirker2re  46549  dirkerdenne0  46550  dirkerper  46553  dirkertrigeq  46558  dirkercncflem2  46561  fourierdlem24  46588  sqwvfoura  46685  sqwvfourb  46686  amgmlemALT  50307