![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpmulcl | Structured version Visualization version GIF version |
Description: Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
rpmulcl | ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpre 12210 | . . 3 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | rpre 12210 | . . 3 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ) | |
3 | remulcl 10418 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | syl2an 586 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ) |
5 | elrp 12204 | . . 3 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | |
6 | elrp 12204 | . . 3 ⊢ (𝐵 ∈ ℝ+ ↔ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) | |
7 | mulgt0 10516 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵)) | |
8 | 5, 6, 7 | syl2anb 588 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → 0 < (𝐴 · 𝐵)) |
9 | elrp 12204 | . 2 ⊢ ((𝐴 · 𝐵) ∈ ℝ+ ↔ ((𝐴 · 𝐵) ∈ ℝ ∧ 0 < (𝐴 · 𝐵))) | |
10 | 4, 8, 9 | sylanbrc 575 | 1 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 class class class wbr 4925 (class class class)co 6974 ℝcr 10332 0cc0 10333 · cmul 10338 < clt 10472 ℝ+crp 12202 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-resscn 10390 ax-1cn 10391 ax-addrcl 10394 ax-mulrcl 10396 ax-rnegex 10404 ax-cnre 10406 ax-pre-mulgt0 10410 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-pnf 10474 df-mnf 10475 df-ltxr 10477 df-rp 12203 |
This theorem is referenced by: rpmtmip 12228 rpmulcld 12262 moddi 13120 rpexpcl 13261 discr 13414 reccn2 14812 expcnv 15077 fprodrpcl 15168 rprisefaccl 15235 rpmsubg 20323 ovolscalem2 23830 aaliou3lem7 24653 aaliou3lem9 24654 cosordlem 24828 logfac 24897 loglesqrt 25052 divsqrtsumlem 25271 basellem1 25372 pclogsum 25505 bclbnd 25570 bposlem7 25580 bposlem8 25581 bposlem9 25582 chebbnd1lem2 25760 dchrisum0lem3 25809 chpdifbndlem2 25844 pntrsumbnd2 25857 pntpbnd1a 25875 pntpbnd2 25877 pntibnd 25883 pntlemd 25884 pntlema 25886 pntlemb 25887 pntlemf 25895 pntlemo 25897 minvecolem3 28443 knoppndvlem18 33417 taupilem1 34073 taupilem2 34074 taupi 34075 ftc1anclem7 34443 ftc1anc 34445 isbnd2 34532 wallispilem4 41809 wallispi 41811 dirker2re 41833 dirkerdenne0 41834 dirkerper 41837 dirkertrigeq 41842 dirkercncflem2 41845 fourierdlem24 41872 sqwvfoura 41969 sqwvfourb 41970 amgmlemALT 44296 |
Copyright terms: Public domain | W3C validator |