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

Theorem rpmulcld 12974
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
StepHypRef Expression
1 rpred.1 . 2 (๐œ‘ โ†’ ๐ด โˆˆ โ„+)
2 rpaddcld.1 . 2 (๐œ‘ โ†’ ๐ต โˆˆ โ„+)
3 rpmulcl 12939 . 2 ((๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+) โ†’ (๐ด ยท ๐ต) โˆˆ โ„+)
41, 2, 3syl2anc 585 1 (๐œ‘ โ†’ (๐ด ยท ๐ต) โˆˆ โ„+)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆˆ wcel 2107  (class class class)co 7358   ยท cmul 11057  โ„+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:  reccn2  15480  eirrlem  16087  nrginvrcnlem  24058  ovolscalem1  24880  itg2gt0  25128  aaliou3lem1  25705  aaliou3lem2  25706  aaliou3lem8  25708  cosordlem  25889  logcnlem2  26001  cxp2limlem  26328  lgamgulmlem3  26383  lgamgulmlem4  26384  lgamgulmlem5  26385  lgamgulmlem6  26386  lgsquadlem2  26732  2sqmod  26787  chtppilimlem1  26824  chtppilim  26826  chebbnd2  26828  chto1lb  26829  rplogsumlem1  26835  dchrvmasumlem1  26846  chpdifbndlem1  26904  chpdifbndlem2  26905  selberg3lem1  26908  selberg4lem1  26911  selberg4  26912  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntpbnd2  26938  pntlemd  26945  pntlema  26947  pntlemb  26948  pntlemq  26952  pntlemr  26953  pntlemj  26954  pntlemf  26956  pntlemo  26958  pntlem3  26960  pntleml  26962  pnt  26965  ttgcontlem1  27836  hgt750leme  33274  faclimlem1  34319  faclimlem3  34321  faclim  34322  unbdqndv2  34977  knoppndvlem17  34994  rrndstprj2  36293  aks4d1p1p7  40534  pellfund14  41224  0ellimcdiv  43897  wallispilem3  44315  wallispilem4  44316  wallispi  44318  wallispi2lem1  44319  stirlinglem2  44323  stirlinglem3  44324  stirlinglem4  44325  stirlinglem6  44327  stirlinglem7  44328  stirlinglem10  44331  stirlinglem11  44332  stirlinglem12  44333  stirlinglem13  44334  stirlinglem14  44335  stirlinglem15  44336  stirlingr  44338  dirkertrigeqlem1  44346  dirkercncflem1  44351  dirkercncflem4  44354  hoiqssbllem1  44870  hoiqssbllem2  44871  hoiqssbllem3  44872  amgmwlem  47256  amgmw2d  47258
  Copyright terms: Public domain W3C validator