| 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 13059 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 3 | 1 | rpge0d 13063 | . 2 ⊢ (𝜑 → 0 ≤ 𝐴) |
| 4 | 2, 3 | jca 511 | 1 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 class class class wbr 5123 ℝcr 11136 0cc0 11137 ≤ cle 11278 ℝ+crp 13016 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-resscn 11194 ax-1cn 11195 ax-addrcl 11198 ax-rnegex 11208 ax-cnre 11210 ax-pre-lttri 11211 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-br 5124 df-opab 5186 df-mpt 5206 df-id 5558 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-er 8727 df-en 8968 df-dom 8969 df-sdom 8970 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-rp 13017 |
| This theorem is referenced by: eirrlem 16223 prmreclem3 16939 prmreclem6 16942 cxprec 26665 cxpsqrt 26682 cxpcn3lem 26727 cxplim 26952 cxploglim2 26959 divsqrtsumlem 26960 divsqrtsumo1 26964 fsumharmonic 26992 zetacvg 26995 logfacubnd 27202 logfacbnd3 27204 bposlem1 27265 bposlem4 27268 bposlem7 27271 bposlem9 27273 2sqmod 27417 dchrmusum2 27475 dchrvmasumlem3 27480 dchrisum0flblem2 27490 dchrisum0fno1 27492 dchrisum0lema 27495 dchrisum0lem1b 27496 dchrisum0lem1 27497 dchrisum0lem2a 27498 dchrisum0lem2 27499 dchrisum0lem3 27500 chpdifbndlem2 27535 selberg3lem1 27538 pntrsumo1 27546 pntrlog2bndlem2 27559 pntrlog2bndlem4 27561 pntrlog2bndlem6a 27563 pntpbnd2 27568 pntibndlem2 27572 pntlemb 27578 pntlemg 27579 pntlemh 27580 pntlemn 27581 pntlemr 27583 pntlemj 27584 pntlemf 27586 pntlemk 27587 pntlemo 27588 blocnilem 30752 ubthlem2 30819 minvecolem4 30828 eulerpartlemgc 34339 irrapxlem4 42814 irrapxlem5 42815 stirlinglem3 46063 stirlinglem15 46075 inlinecirc02plem 48680 amgmlemALT 49417 |
| Copyright terms: Public domain | W3C validator |