| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nn0ge0 | Structured version Visualization version GIF version | ||
| Description: A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.) |
| Ref | Expression |
|---|---|
| nn0ge0 | ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elnn0 12378 | . . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) | |
| 2 | nngt0 12151 | . . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁) | |
| 3 | id 22 | . . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0) | |
| 4 | 3 | eqcomd 2737 | . . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁) |
| 5 | 2, 4 | orim12i 908 | . . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁)) |
| 6 | 1, 5 | sylbi 217 | . 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁)) |
| 7 | 0re 11109 | . . 3 ⊢ 0 ∈ ℝ | |
| 8 | nn0re 12385 | . . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ) | |
| 9 | leloe 11194 | . . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) | |
| 10 | 7, 8, 9 | sylancr 587 | . 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) |
| 11 | 6, 10 | mpbird 257 | 1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∨ wo 847 = wceq 1541 ∈ wcel 2111 class class class wbr 5086 ℝcr 11000 0cc0 11001 < clt 11141 ≤ cle 11142 ℕcn 12120 ℕ0cn0 12376 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-nn 12121 df-n0 12377 |
| This theorem is referenced by: nn0nlt0 12402 nn0ge0i 12403 nn0le0eq0 12404 nn0p1gt0 12405 0mnnnnn0 12408 nn0addge1 12422 nn0addge2 12423 nn0negleid 12428 nn0ge0d 12440 nn0ge0div 12537 xnn0ge0 13028 xnn0xadd0 13141 nn0rp0 13350 xnn0xrge0 13401 0elfz 13519 fz0fzelfz0 13529 fz0fzdiffz0 13532 fzctr 13535 difelfzle 13536 fzoun 13591 nn0p1elfzo 13597 elfzodifsumelfzo 13626 fvinim0ffz 13684 subfzo0 13687 adddivflid 13717 modmuladdnn0 13817 addmodid 13821 modifeq2int 13835 modfzo0difsn 13845 nn0sq11 14034 zzlesq 14108 bernneq 14131 bernneq3 14133 faclbnd 14192 faclbnd6 14201 facubnd 14202 bcval5 14220 hashneq0 14266 fi1uzind 14409 ccat0 14478 ccat2s1fvw 14541 repswswrd 14686 nn0sqeq1 15178 nn0absid 15332 rprisefaccl 15925 dvdseq 16220 evennn02n 16256 nn0ehalf 16284 nn0oddm1d2 16291 bitsinv1 16348 smuval2 16388 gcdn0gt0 16424 nn0gcdid0 16427 absmulgcd 16455 algcvgblem 16483 algcvga 16485 lcmgcdnn 16517 lcmfun 16551 lcmfass 16552 2mulprm 16599 nonsq 16665 hashgcdlem 16694 odzdvds 16702 pcfaclem 16805 prmirredlem 21404 prmirred 21406 coe1sclmul 22191 coe1sclmul2 22193 fvmptnn04ifb 22761 mdegle0 26004 plypf1 26139 dgrlt 26194 fta1 26238 taylfval 26288 logbgcd1irr 26726 eldmgm 26954 basellem3 27015 bcmono 27210 lgsdinn0 27278 2sq2 27366 2sqnn0 27371 2sqreulem1 27379 dchrisumlem1 27422 dchrisumlem2 27423 wwlksnextwrd 29870 wwlksnextfun 29871 wwlksnextinj 29872 wwlksnextproplem2 29883 wwlksnextproplem3 29884 wrdt2ind 32926 xrsmulgzz 32982 hashf2 34089 hasheuni 34090 reprinfz1 34627 0nn0m1nnn0 35149 faclimlem1 35779 rrntotbnd 37876 gcdnn0id 42362 pell14qrgt0 42892 pell1qrgaplem 42906 monotoddzzfi 42975 jm2.17a 42993 jm2.22 43028 rmxdiophlem 43048 rexanuz2nf 45530 wallispilem3 46105 stirlinglem7 46118 elfz2z 47346 fz0addge0 47350 elfzlble 47351 2ffzoeq 47358 addmodne 47375 iccpartigtl 47454 sqrtpwpw2p 47569 flsqrt 47624 nn0e 47728 nn0sumltlt 48381 nn0eo 48560 fllog2 48600 dignn0fr 48633 dignnld 48635 dig1 48640 itcovalt2lem2lem1 48705 |
| Copyright terms: Public domain | W3C validator |