| 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 9244 | . 2 ⊢ 1 ∈ ℕ | |
| 2 | nn0nnaddcl 9523 | . 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ) → (𝑁 + 1) ∈ ℕ) | |
| 3 | 1, 2 | mpan2 425 | 1 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2203 (class class class)co 6049 1c1 8124 + caddc 8126 ℕcn 9233 ℕ0cn0 9492 |
| 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 2214 ax-sep 4227 ax-cnex 8214 ax-resscn 8215 ax-1cn 8216 ax-1re 8217 ax-icn 8218 ax-addcl 8219 ax-addrcl 8220 ax-mulcl 8221 ax-addcom 8223 ax-addass 8225 ax-i2m1 8228 ax-0id 8231 ax-rnegex 8232 |
| This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ral 2525 df-rex 2526 df-rab 2529 df-v 2814 df-un 3214 df-in 3216 df-ss 3223 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-int 3949 df-br 4109 df-iota 5311 df-fv 5359 df-ov 6052 df-inn 9234 df-n0 9493 |
| This theorem is referenced by: elnn0nn 9534 elz2 9645 peano5uzti 9682 fseq1p1m1 10424 fzonn0p1 10552 nn0ennn 10791 faccl 11093 facdiv 11096 facwordi 11098 faclbnd 11099 facubnd 11103 bcm1k 11118 bcp1n 11119 bcp1nk 11120 bcpasc 11124 ccats1pfxeqrex 11400 wrdind 11407 wrd2ind 11408 ccats1pfxeqbi 11427 bcxmas 12168 efcllemp 12337 uzwodc 12726 prmfac1 12842 pcfac 13041 4sqlem12 13093 gsumfzconst 14047 plycolemc 15610 gausslemma2dlem3 15923 2lgslem1a 15948 depindlem1 16488 gfsump1 16854 |
| Copyright terms: Public domain | W3C validator |