MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpmulcl Structured version   Visualization version   GIF version

Theorem rpmulcl 12939
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
StepHypRef Expression
1 rpre 12924 . . 3 (๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„)
2 rpre 12924 . . 3 (๐ต โˆˆ โ„+ โ†’ ๐ต โˆˆ โ„)
3 remulcl 11137 . . 3 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
41, 2, 3syl2an 597 . 2 ((๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
5 elrp 12918 . . 3 (๐ด โˆˆ โ„+ โ†” (๐ด โˆˆ โ„ โˆง 0 < ๐ด))
6 elrp 12918 . . 3 (๐ต โˆˆ โ„+ โ†” (๐ต โˆˆ โ„ โˆง 0 < ๐ต))
7 mulgt0 11233 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ 0 < (๐ด ยท ๐ต))
85, 6, 7syl2anb 599 . 2 ((๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+) โ†’ 0 < (๐ด ยท ๐ต))
9 elrp 12918 . 2 ((๐ด ยท ๐ต) โˆˆ โ„+ โ†” ((๐ด ยท ๐ต) โˆˆ โ„ โˆง 0 < (๐ด ยท ๐ต)))
104, 8, 9sylanbrc 584 1 ((๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+) โ†’ (๐ด ยท ๐ต) โˆˆ โ„+)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆˆ wcel 2107   class class class wbr 5106  (class class class)co 7358  โ„cr 11051  0cc0 11052   ยท cmul 11057   < clt 11190  โ„+crp 12916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-addrcl 11113  ax-mulrcl 11115  ax-rnegex 11123  ax-cnre 11125  ax-pre-mulgt0 11129
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195  df-rp 12917
This theorem is referenced by:  rpmtmip  12940  rpmulcld  12974  moddi  13845  rpexpcl  13987  discr  14144  reccn2  15480  expcnv  15750  fprodrpcl  15840  rprisefaccl  15907  rpmsubg  20864  ovolscalem2  24881  aaliou3lem7  25712  aaliou3lem9  25713  cos02pilt1  25885  cosordlem  25889  logfac  25959  loglesqrt  26114  divsqrtsumlem  26332  basellem1  26433  pclogsum  26566  bclbnd  26631  bposlem7  26641  bposlem8  26642  bposlem9  26643  chebbnd1lem2  26821  dchrisum0lem3  26870  chpdifbndlem2  26905  pntrsumbnd2  26918  pntpbnd1a  26936  pntpbnd2  26938  pntibnd  26944  pntlemd  26945  pntlema  26947  pntlemb  26948  pntlemf  26956  pntlemo  26958  minvecolem3  29821  knoppndvlem18  34995  taupilem1  35795  taupilem2  35796  taupi  35797  ftc1anclem7  36160  ftc1anc  36162  isbnd2  36245  wallispilem4  44316  wallispi  44318  dirker2re  44340  dirkerdenne0  44341  dirkerper  44344  dirkertrigeq  44349  dirkercncflem2  44352  fourierdlem24  44379  sqwvfoura  44476  sqwvfourb  44477  amgmlemALT  47257
  Copyright terms: Public domain W3C validator