| 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 12383 | . . 3 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) | |
| 2 | nngt0 12156 | . . . 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 11114 | . . 3 ⊢ 0 ∈ ℝ | |
| 8 | nn0re 12390 | . . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ) | |
| 9 | leloe 11199 | . . 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 5091 ℝcr 11005 0cc0 11006 < clt 11146 ≤ cle 11147 ℕcn 12125 ℕ0cn0 12381 |
| 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 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 |
| 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 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-n0 12382 |
| This theorem is referenced by: nn0nlt0 12407 nn0ge0i 12408 nn0le0eq0 12409 nn0p1gt0 12410 0mnnnnn0 12413 nn0addge1 12427 nn0addge2 12428 nn0negleid 12433 nn0ge0d 12445 nn0ge0div 12542 xnn0ge0 13033 xnn0xadd0 13146 nn0rp0 13355 xnn0xrge0 13406 0elfz 13524 fz0fzelfz0 13534 fz0fzdiffz0 13537 fzctr 13540 difelfzle 13541 fzoun 13596 nn0p1elfzo 13602 elfzodifsumelfzo 13631 fvinim0ffz 13689 subfzo0 13692 adddivflid 13722 modmuladdnn0 13822 addmodid 13826 modifeq2int 13840 modfzo0difsn 13850 nn0sq11 14039 zzlesq 14113 bernneq 14136 bernneq3 14138 faclbnd 14197 faclbnd6 14206 facubnd 14207 bcval5 14225 hashneq0 14271 fi1uzind 14414 ccat0 14483 ccat2s1fvw 14546 repswswrd 14691 nn0sqeq1 15183 nn0absid 15337 rprisefaccl 15930 dvdseq 16225 evennn02n 16261 nn0ehalf 16289 nn0oddm1d2 16296 bitsinv1 16353 smuval2 16393 gcdn0gt0 16429 nn0gcdid0 16432 absmulgcd 16460 algcvgblem 16488 algcvga 16490 lcmgcdnn 16522 lcmfun 16556 lcmfass 16557 2mulprm 16604 nonsq 16670 hashgcdlem 16699 odzdvds 16707 pcfaclem 16810 prmirredlem 21410 prmirred 21412 coe1sclmul 22197 coe1sclmul2 22199 fvmptnn04ifb 22767 mdegle0 26010 plypf1 26145 dgrlt 26200 fta1 26244 taylfval 26294 logbgcd1irr 26732 eldmgm 26960 basellem3 27021 bcmono 27216 lgsdinn0 27284 2sq2 27372 2sqnn0 27377 2sqreulem1 27385 dchrisumlem1 27428 dchrisumlem2 27429 wwlksnextwrd 29876 wwlksnextfun 29877 wwlksnextinj 29878 wwlksnextproplem2 29889 wwlksnextproplem3 29890 wrdt2ind 32932 xrsmulgzz 32988 hashf2 34095 hasheuni 34096 reprinfz1 34633 0nn0m1nnn0 35155 faclimlem1 35785 rrntotbnd 37882 gcdnn0id 42368 pell14qrgt0 42898 pell1qrgaplem 42912 monotoddzzfi 42981 jm2.17a 42999 jm2.22 43034 rmxdiophlem 43054 rexanuz2nf 45536 wallispilem3 46111 stirlinglem7 46124 elfz2z 47352 fz0addge0 47356 elfzlble 47357 2ffzoeq 47364 addmodne 47381 iccpartigtl 47460 sqrtpwpw2p 47575 flsqrt 47630 nn0e 47734 nn0sumltlt 48387 nn0eo 48566 fllog2 48606 dignn0fr 48639 dignnld 48641 dig1 48646 itcovalt2lem2lem1 48711 |
| Copyright terms: Public domain | W3C validator |