| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rphalfcl | Structured version Visualization version GIF version | ||
| Description: Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.) |
| Ref | Expression |
|---|---|
| rphalfcl | ⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2rp 12932 | . 2 ⊢ 2 ∈ ℝ+ | |
| 2 | rpdivcl 12954 | . 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 2 ∈ ℝ+) → (𝐴 / 2) ∈ ℝ+) | |
| 3 | 1, 2 | mpan2 691 | 1 ⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2109 (class class class)co 7369 / cdiv 11811 2c2 12217 ℝ+crp 12927 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-2 12225 df-rp 12928 |
| This theorem is referenced by: rphalfcld 12983 rpltrp 13278 cau3lem 15297 2clim 15514 addcn2 15536 mulcn2 15538 climcau 15613 metcnpi3 24410 ngptgp 24500 iccntr 24686 reconnlem2 24692 opnreen 24696 xmetdcn2 24702 cnllycmp 24831 iscfil3 25149 cfilfcls 25150 iscmet3lem3 25166 iscmet3lem1 25167 iscmet3lem2 25168 iscmet3 25169 lmcau 25189 bcthlem5 25204 ivthlem2 25329 uniioombl 25466 dvcnvre 25900 aaliou 26222 ulmcaulem 26279 ulmcau 26280 ulmcn 26284 ulmdvlem3 26287 tanregt0 26424 argregt0 26495 argrege0 26496 logimul 26499 resqrtcn 26635 asin1 26780 reasinsin 26782 atanbnd 26812 atan1 26814 sqrtlim 26859 basellem4 26970 chpchtlim 27366 mulog2sumlem2 27422 pntlem3 27496 vacn 30596 ubthlem1 30772 nmcexi 31928 poimirlem29 37616 heicant 37622 ftc1anclem6 37665 ftc1anclem7 37666 ftc1anc 37668 heibor1lem 37776 heiborlem8 37785 bfplem2 37790 supxrge 45307 suplesup 45308 infleinflem1 45339 infleinf 45341 addlimc 45619 fourierdlem103 46180 fourierdlem104 46181 sge0xaddlem2 46405 smflimlem4 46745 |
| Copyright terms: Public domain | W3C validator |