![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rpge0 | Structured version Visualization version GIF version |
Description: A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.) |
Ref | Expression |
---|---|
rpge0 | ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpre 12212 | . 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | |
2 | rpgt0 12218 | . 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | |
3 | 0re 10441 | . . 3 ⊢ 0 ∈ ℝ | |
4 | ltle 10529 | . . 3 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) | |
5 | 3, 4 | mpan 677 | . 2 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴)) |
6 | 1, 2, 5 | sylc 65 | 1 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 class class class wbr 4929 ℝcr 10334 0cc0 10335 < clt 10474 ≤ cle 10475 ℝ+crp 12204 |
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 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-resscn 10392 ax-1cn 10393 ax-addrcl 10396 ax-rnegex 10406 ax-cnre 10408 ax-pre-lttri 10409 |
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 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-mpt 5009 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-rp 12205 |
This theorem is referenced by: rprege0 12221 rpge0d 12252 xralrple 12415 xlemul1 12499 infmrp1 12553 sqrlem1 14463 rpsqrtcl 14485 divrcnv 15067 ef01bndlem 15397 stdbdmet 22829 reconnlem2 23138 cphsqrtcl3 23494 iscmet3lem3 23596 minveclem3 23735 itg2const2 24045 itg2mulclem 24050 aalioulem2 24625 pige3ALT 24808 argregt0 24894 argrege0 24895 2irrexpq 25014 cxpcn3 25030 cxplim 25251 cxp2lim 25256 divsqrtsumlem 25259 logdiflbnd 25274 basellem4 25363 ppiltx 25456 bposlem8 25569 bposlem9 25570 chebbnd1 25750 mulog2sumlem2 25813 selbergb 25827 selberg2b 25830 nmcexi 29584 nmcopexi 29585 nmcfnexi 29609 sqsscirc1 30801 divsqrtid 31519 logdivsqrle 31575 hgt750lem2 31577 subfacval3 32027 ptrecube 34339 heicant 34374 itg2addnclem 34390 itg2gt0cn 34394 areacirclem1 34429 areacirclem4 34432 areacirc 34434 cntotbnd 34522 xralrple4 41076 xralrple3 41077 fourierdlem103 41931 blenre 44008 itscnhlinecirc02plem3 44145 itscnhlinecirc02p 44146 |
Copyright terms: Public domain | W3C validator |