![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0le0 | Structured version Visualization version GIF version |
Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
0le0 | ⊢ 0 ≤ 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 10494 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | leidi 11027 | 1 ⊢ 0 ≤ 0 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4966 0cc0 10388 ≤ cle 10527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-resscn 10445 ax-1cn 10446 ax-addrcl 10449 ax-rnegex 10459 ax-cnre 10461 ax-pre-lttri 10462 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-er 8144 df-en 8363 df-dom 8364 df-sdom 8365 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 |
This theorem is referenced by: nn0ledivnn 12357 xsubge0 12509 xmulge0 12532 0e0icopnf 12701 0e0iccpnf 12702 0elunit 12710 0mod 13125 sqlecan 13426 discr 13456 cnpart 14438 sqr0lem 14439 resqrex 14449 sqrt00 14462 fsumabs 14994 rpnnen2lem4 15408 divalglem7 15588 pcmptdvds 16064 prmreclem4 16089 prmreclem5 16090 prmreclem6 16091 ramz2 16194 ramz 16195 isabvd 19286 prdsxmetlem 22666 metustto 22851 cfilucfil 22857 nmolb2d 23015 nmoi 23025 nmoix 23026 nmoleub 23028 nmo0 23032 pcoval1 23305 pco0 23306 minveclem7 23726 ovolfiniun 23790 ovolicc1 23805 ioorf 23862 itg1ge0a 24000 mbfi1fseqlem5 24008 itg2const 24029 itg2const2 24030 itg2splitlem 24037 itg2cnlem1 24050 itg2cnlem2 24051 iblss 24093 itgle 24098 ibladdlem 24108 iblabs 24117 iblabsr 24118 iblmulc2 24119 bddmulibl 24127 c1lip1 24282 dveq0 24285 dv11cn 24286 fta1g 24449 abelthlem2 24708 sinq12ge0 24782 cxpge0 24952 abscxp2 24962 log2ublem3 25213 chtwordi 25420 ppiwordi 25426 chpub 25483 bposlem1 25547 bposlem6 25552 dchrisum0flblem2 25772 qabvle 25888 ostth2lem2 25897 colinearalg 26384 eucrct2eupthOLD 27718 eucrct2eupth 27719 ex-po 27911 nvz0 28141 nmlnoubi 28269 nmblolbii 28272 blocnilem 28277 siilem2 28325 minvecolem7 28356 pjneli 29196 nmbdoplbi 29497 nmcoplbi 29501 nmbdfnlbi 29522 nmcfnlbi 29525 nmopcoi 29568 unierri 29577 leoprf2 29600 leoprf 29601 stle0i 29712 xrge0iifcnv 30798 xrge0iifiso 30800 xrge0iifhom 30802 esumrnmpt2 30949 dstfrvclim1 31357 ballotlemrc 31410 signsply0 31443 chtvalz 31522 poimirlem23 34471 mblfinlem2 34486 itg2addnclem 34499 itg2gt0cn 34503 ibladdnclem 34504 itgaddnclem2 34507 iblabsnc 34512 iblmulc2nc 34513 bddiblnc 34518 ftc1anclem5 34527 ftc1anclem7 34529 ftc1anclem8 34530 ftc1anc 34531 areacirclem1 34538 areacirclem4 34541 mettrifi 34589 monotoddzzfi 39049 rmxypos 39054 rmygeid 39071 stoweidlem55 41908 fourierdlem14 41974 fourierdlem20 41980 fourierdlem92 42051 fourierdlem93 42052 fouriersw 42084 isomennd 42381 ovnssle 42411 hoidmvlelem3 42447 ovnhoilem1 42451 nnlog2ge0lt1 44133 dig1 44175 ex-gte 44334 |
Copyright terms: Public domain | W3C validator |