| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rprege0d | Structured version Visualization version GIF version | ||
| Description: A positive real is real and greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
| Ref | Expression |
|---|---|
| rpred.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ+) |
| Ref | Expression |
|---|---|
| rprege0d | ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rpred.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+) | |
| 2 | 1 | rpred 13002 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 3 | 1 | rpge0d 13006 | . 2 ⊢ (𝜑 → 0 ≤ 𝐴) |
| 4 | 2, 3 | jca 511 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2109 class class class wbr 5110 ℝcr 11074 0cc0 11075 ≤ cle 11216 ℝ+crp 12958 |
| 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 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-resscn 11132 ax-1cn 11133 ax-addrcl 11136 ax-rnegex 11146 ax-cnre 11148 ax-pre-lttri 11149 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-rp 12959 |
| This theorem is referenced by: eirrlem 16179 prmreclem3 16896 prmreclem6 16899 cxprec 26602 cxpsqrt 26619 cxpcn3lem 26664 cxplim 26889 cxploglim2 26896 divsqrtsumlem 26897 divsqrtsumo1 26901 fsumharmonic 26929 zetacvg 26932 logfacubnd 27139 logfacbnd3 27141 bposlem1 27202 bposlem4 27205 bposlem7 27208 bposlem9 27210 2sqmod 27354 dchrmusum2 27412 dchrvmasumlem3 27417 dchrisum0flblem2 27427 dchrisum0fno1 27429 dchrisum0lema 27432 dchrisum0lem1b 27433 dchrisum0lem1 27434 dchrisum0lem2a 27435 dchrisum0lem2 27436 dchrisum0lem3 27437 chpdifbndlem2 27472 selberg3lem1 27475 pntrsumo1 27483 pntrlog2bndlem2 27496 pntrlog2bndlem4 27498 pntrlog2bndlem6a 27500 pntpbnd2 27505 pntibndlem2 27509 pntlemb 27515 pntlemg 27516 pntlemh 27517 pntlemn 27518 pntlemr 27520 pntlemj 27521 pntlemf 27523 pntlemk 27524 pntlemo 27525 blocnilem 30740 ubthlem2 30807 minvecolem4 30816 eulerpartlemgc 34360 irrapxlem4 42820 irrapxlem5 42821 stirlinglem3 46081 stirlinglem15 46093 inlinecirc02plem 48779 amgmlemALT 49796 |
| Copyright terms: Public domain | W3C validator |