| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > nn0p1nn | GIF version | ||
| Description: A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.) |
| Ref | Expression |
|---|---|
| nn0p1nn | ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn 9197 | . 2 ⊢ 1 ∈ ℕ | |
| 2 | nn0nnaddcl 9476 | . 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ) → (𝑁 + 1) ∈ ℕ) | |
| 3 | 1, 2 | mpan2 425 | 1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2202 (class class class)co 6028 1c1 8076 + caddc 8078 ℕcn 9186 ℕ0cn0 9445 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2213 ax-sep 4212 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-addcom 8175 ax-addass 8177 ax-i2m1 8180 ax-0id 8183 ax-rnegex 8184 |
| This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ral 2516 df-rex 2517 df-rab 2520 df-v 2805 df-un 3205 df-in 3207 df-ss 3214 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-br 4094 df-iota 5293 df-fv 5341 df-ov 6031 df-inn 9187 df-n0 9446 |
| This theorem is referenced by: elnn0nn 9487 elz2 9594 peano5uzti 9631 fseq1p1m1 10372 fzonn0p1 10500 nn0ennn 10739 faccl 11041 facdiv 11044 facwordi 11046 faclbnd 11047 facubnd 11051 bcm1k 11066 bcp1n 11067 bcp1nk 11068 bcpasc 11072 ccats1pfxeqrex 11343 wrdind 11350 wrd2ind 11351 ccats1pfxeqbi 11370 bcxmas 12111 efcllemp 12280 uzwodc 12669 prmfac1 12785 pcfac 12984 4sqlem12 13036 gsumfzconst 13989 plycolemc 15549 gausslemma2dlem3 15859 2lgslem1a 15884 depindlem1 16424 gfsump1 16792 |
| Copyright terms: Public domain | W3C validator |