![]() |
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 12474 | . . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) | |
2 | nngt0 12243 | . . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁) | |
3 | id 22 | . . . . 5 ⊢ (𝑁 = 0 → 𝑁 = 0) | |
4 | 3 | eqcomd 2739 | . . . 4 ⊢ (𝑁 = 0 → 0 = 𝑁) |
5 | 2, 4 | orim12i 908 | . . 3 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁)) |
6 | 1, 5 | sylbi 216 | . 2 ⊢ (𝑁 ∈ ℕ0 → (0 < 𝑁 ∨ 0 = 𝑁)) |
7 | 0re 11216 | . . 3 ⊢ 0 ∈ ℝ | |
8 | nn0re 12481 | . . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ) | |
9 | leloe 11300 | . . 3 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) | |
10 | 7, 8, 9 | sylancr 588 | . 2 ⊢ (𝑁 ∈ ℕ0 → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) |
11 | 6, 10 | mpbird 257 | 1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 846 = wceq 1542 ∈ wcel 2107 class class class wbr 5149 ℝcr 11109 0cc0 11110 < clt 11248 ≤ cle 11249 ℕcn 12212 ℕ0cn0 12472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-n0 12473 |
This theorem is referenced by: nn0nlt0 12498 nn0ge0i 12499 nn0le0eq0 12500 nn0p1gt0 12501 0mnnnnn0 12504 nn0addge1 12518 nn0addge2 12519 nn0negleid 12524 nn0ge0d 12535 nn0ge0div 12631 xnn0ge0 13113 xnn0xadd0 13226 nn0rp0 13432 xnn0xrge0 13483 0elfz 13598 fz0fzelfz0 13607 fz0fzdiffz0 13610 fzctr 13613 difelfzle 13614 fzoun 13669 nn0p1elfzo 13675 elfzodifsumelfzo 13698 fvinim0ffz 13751 subfzo0 13754 adddivflid 13783 modmuladdnn0 13880 addmodid 13884 modifeq2int 13898 modfzo0difsn 13908 nn0sq11 14097 zzlesq 14170 bernneq 14192 bernneq3 14194 faclbnd 14250 faclbnd6 14259 facubnd 14260 bcval5 14278 hashneq0 14324 fi1uzind 14458 ccat0 14526 ccat2s1fvw 14588 repswswrd 14734 nn0sqeq1 15223 rprisefaccl 15967 dvdseq 16257 evennn02n 16293 nn0ehalf 16321 nn0oddm1d2 16328 bitsinv1 16383 smuval2 16423 gcdn0gt0 16459 nn0gcdid0 16462 absmulgcd 16491 algcvgblem 16514 algcvga 16516 lcmgcdnn 16548 lcmfun 16582 lcmfass 16583 2mulprm 16630 nonsq 16695 hashgcdlem 16721 odzdvds 16728 pcfaclem 16831 prmirredlem 21042 prmirred 21044 coe1sclmul 21804 coe1sclmul2 21806 fvmptnn04ifb 22353 mdegle0 25595 plypf1 25726 dgrlt 25780 fta1 25821 taylfval 25871 logbgcd1irr 26299 eldmgm 26526 basellem3 26587 bcmono 26780 lgsdinn0 26848 2sq2 26936 2sqnn0 26941 2sqreulem1 26949 dchrisumlem1 26992 dchrisumlem2 26993 wwlksnextwrd 29182 wwlksnextfun 29183 wwlksnextinj 29184 wwlksnextproplem2 29195 wwlksnextproplem3 29196 wrdt2ind 32148 xrsmulgzz 32210 hashf2 33113 hasheuni 33114 reprinfz1 33665 0nn0m1nnn0 34133 faclimlem1 34744 rrntotbnd 36752 factwoffsmonot 41071 gcdnn0id 41268 pell14qrgt0 41645 pell1qrgaplem 41659 monotoddzzfi 41729 jm2.17a 41747 jm2.22 41782 rmxdiophlem 41802 rexanuz2nf 44251 wallispilem3 44831 stirlinglem7 44844 elfz2z 46071 fz0addge0 46075 elfzlble 46076 2ffzoeq 46084 iccpartigtl 46139 sqrtpwpw2p 46254 flsqrt 46309 nn0e 46413 nn0sumltlt 47074 nn0eo 47262 fllog2 47302 dignn0fr 47335 dignnld 47337 dig1 47342 itcovalt2lem2lem1 47407 |
Copyright terms: Public domain | W3C validator |