Theorem nn0p1nn 9444

Description: A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)

Assertion

Ref	Expression
nn0p1nn	|- ( N e. NN0 -> ( N + 1 ) e. NN )

Proof of Theorem nn0p1nn

Step	Hyp	Ref	Expression
1		1nn 9157	. 2 |- 1 e. NN
2		nn0nnaddcl 9436	. 2 |- ( ( N e. NN0 /\ 1 e. NN ) -> ( N + 1 ) e. NN )
3	1, 2	mpan2 425	1 |- ( N e. NN0 -> ( N + 1 ) e. NN )

Syntax hints:   -> wi 4   e. wcel 2202  (class class class)co 6021   1c1 8036   + caddc 8038   NNcn 9146   NN0cn0 9405

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8126  ax-resscn 8127  ax-1cn 8128  ax-1re 8129  ax-icn 8130  ax-addcl 8131  ax-addrcl 8132  ax-mulcl 8133  ax-addcom 8135  ax-addass 8137  ax-i2m1 8140  ax-0id 8143  ax-rnegex 8144

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6024  df-inn 9147  df-n0 9406

This theorem is referenced by:  elnn0nn  9447  elz2  9554  peano5uzti  9591  fseq1p1m1  10332  fzonn0p1  10460  nn0ennn  10699  faccl  11001  facdiv  11004  facwordi  11006  faclbnd  11007  facubnd  11011  bcm1k  11026  bcp1n  11027  bcp1nk  11028  bcpasc  11032  ccats1pfxeqrex  11303  wrdind  11310  wrd2ind  11311  ccats1pfxeqbi  11330  bcxmas  12071  efcllemp  12240  uzwodc  12629  prmfac1  12745  pcfac  12944  4sqlem12  12996  gsumfzconst  13949  plycolemc  15509  gausslemma2dlem3  15819  2lgslem1a  15844  depindlem1  16384  gfsump1  16746