![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nn0ge0 | 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 8773 | . 2 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) | |
2 | nnre 8527 | . . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ) | |
3 | nngt0 8545 | . . . 4 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁) | |
4 | 0re 7585 | . . . . 5 ⊢ 0 ∈ ℝ | |
5 | ltle 7669 | . . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 < 𝑁 → 0 ≤ 𝑁)) | |
6 | 4, 5 | mpan 416 | . . . 4 ⊢ (𝑁 ∈ ℝ → (0 < 𝑁 → 0 ≤ 𝑁)) |
7 | 2, 3, 6 | sylc 62 | . . 3 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁) |
8 | 0le0 8609 | . . . 4 ⊢ 0 ≤ 0 | |
9 | breq2 3871 | . . . 4 ⊢ (𝑁 = 0 → (0 ≤ 𝑁 ↔ 0 ≤ 0)) | |
10 | 8, 9 | mpbiri 167 | . . 3 ⊢ (𝑁 = 0 → 0 ≤ 𝑁) |
11 | 7, 10 | jaoi 674 | . 2 ⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → 0 ≤ 𝑁) |
12 | 1, 11 | sylbi 120 | 1 ⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 667 = wceq 1296 ∈ wcel 1445 class class class wbr 3867 ℝcr 7446 0cc0 7447 < clt 7619 ≤ cle 7620 ℕcn 8520 ℕ0cn0 8771 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-cnex 7533 ax-resscn 7534 ax-1cn 7535 ax-1re 7536 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-i2m1 7547 ax-0lt1 7548 ax-0id 7550 ax-rnegex 7551 ax-pre-ltirr 7554 ax-pre-ltwlin 7555 ax-pre-lttrn 7556 ax-pre-ltadd 7558 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-rab 2379 df-v 2635 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-br 3868 df-opab 3922 df-xp 4473 df-cnv 4475 df-iota 5014 df-fv 5057 df-ov 5693 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 df-inn 8521 df-n0 8772 |
This theorem is referenced by: nn0nlt0 8797 nn0ge0i 8798 nn0le0eq0 8799 nn0p1gt0 8800 0mnnnnn0 8803 nn0addge1 8817 nn0addge2 8818 nn0ge0d 8827 elnn0z 8861 nn0lt10b 8925 nn0ge0div 8932 nn0pnfge0 9360 xnn0xadd0 9433 0elfz 9681 fz0fzelfz0 9687 fz0fzdiffz0 9690 fzctr 9693 difelfzle 9694 elfzodifsumelfzo 9761 fvinim0ffz 9801 subfzo0 9802 adddivflid 9848 modqmuladdnn0 9924 modfzo0difsn 9951 bernneq 10205 bernneq3 10207 faclbnd 10280 faclbnd6 10283 facubnd 10284 bcval5 10302 fihashneq0 10334 dvdseq 11292 evennn02n 11325 nn0ehalf 11346 nn0oddm1d2 11352 gcdn0gt0 11412 nn0gcdid0 11415 absmulgcd 11449 algcvgblem 11474 algcvga 11476 lcmgcdnn 11507 hashgcdlem 11646 znnen 11654 |
Copyright terms: Public domain | W3C validator |