![]() |
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 10328 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | leidi 10852 | 1 ⊢ 0 ≤ 0 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 4841 0cc0 10222 ≤ cle 10362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-resscn 10279 ax-1cn 10280 ax-addrcl 10283 ax-rnegex 10293 ax-cnre 10295 ax-pre-lttri 10296 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-nel 3073 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-er 7980 df-en 8194 df-dom 8195 df-sdom 8196 df-pnf 10363 df-mnf 10364 df-xr 10365 df-ltxr 10366 df-le 10367 |
This theorem is referenced by: nn0ledivnn 12184 xsubge0 12336 xmulge0 12359 0e0icopnf 12529 0e0iccpnf 12530 0elunit 12538 0mod 12952 sqlecan 13221 discr 13251 cnpart 14318 sqr0lem 14319 resqrex 14329 sqrt00 14342 fsumabs 14868 rpnnen2lem4 15279 divalglem7 15455 pcmptdvds 15928 prmreclem4 15953 prmreclem5 15954 prmreclem6 15955 ramz2 16058 ramz 16059 isabvd 19135 prdsxmetlem 22498 metustto 22683 cfilucfil 22689 nmolb2d 22847 nmoi 22857 nmoix 22858 nmoleub 22860 nmo0 22864 pcoval1 23137 pco0 23138 minveclem7 23542 ovolfiniun 23606 ovolicc1 23621 ioorf 23678 itg1ge0a 23816 mbfi1fseqlem5 23824 itg2const 23845 itg2const2 23846 itg2splitlem 23853 itg2cnlem1 23866 itg2cnlem2 23867 iblss 23909 itgle 23914 ibladdlem 23924 iblabs 23933 iblabsr 23934 iblmulc2 23935 bddmulibl 23943 c1lip1 24098 dveq0 24101 dv11cn 24102 fta1g 24265 abelthlem2 24524 sinq12ge0 24599 cxpge0 24767 abscxp2 24777 log2ublem3 25024 chtwordi 25231 ppiwordi 25237 chpub 25294 bposlem1 25358 bposlem6 25363 dchrisum0flblem2 25547 qabvle 25663 ostth2lem2 25672 colinearalg 26139 eucrct2eupthOLD 27583 eucrct2eupth 27584 ex-po 27812 nvz0 28040 nmlnoubi 28168 nmblolbii 28171 blocnilem 28176 siilem2 28224 minvecolem7 28256 pjneli 29099 nmbdoplbi 29400 nmcoplbi 29404 nmbdfnlbi 29425 nmcfnlbi 29428 nmopcoi 29471 unierri 29480 leoprf2 29503 leoprf 29504 stle0i 29615 xrge0iifcnv 30487 xrge0iifiso 30489 xrge0iifhom 30491 esumrnmpt2 30638 dstfrvclim1 31048 ballotlemrc 31101 signsply0 31138 chtvalz 31219 poimirlem23 33913 mblfinlem2 33928 itg2addnclem 33941 itg2gt0cn 33945 ibladdnclem 33946 itgaddnclem2 33949 iblabsnc 33954 iblmulc2nc 33955 bddiblnc 33960 ftc1anclem5 33969 ftc1anclem7 33971 ftc1anclem8 33972 ftc1anc 33973 areacirclem1 33980 areacirclem4 33983 mettrifi 34032 monotoddzzfi 38280 rmxypos 38287 rmygeid 38304 stoweidlem55 41003 fourierdlem14 41069 fourierdlem20 41075 fourierdlem92 41146 fourierdlem93 41147 fouriersw 41179 isomennd 41479 ovnssle 41509 hoidmvlelem3 41545 ovnhoilem1 41549 nnlog2ge0lt1 43147 dig1 43189 ex-gte 43260 |
Copyright terms: Public domain | W3C validator |