ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nn0p1nn Unicode version

Theorem nn0p1nn 8383
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
StepHypRef Expression
1 1nn 8106 . 2  |-  1  e.  NN
2 nn0nnaddcl 8375 . 2  |-  ( ( N  e.  NN0  /\  1  e.  NN )  ->  ( N  +  1 )  e.  NN )
31, 2mpan2 416 1  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434  (class class class)co 5537   1c1 7033    + caddc 7035   NNcn 8095   NN0cn0 8344
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3898  ax-cnex 7118  ax-resscn 7119  ax-1cn 7120  ax-1re 7121  ax-icn 7122  ax-addcl 7123  ax-addrcl 7124  ax-mulcl 7125  ax-addcom 7127  ax-addass 7129  ax-i2m1 7132  ax-0id 7135  ax-rnegex 7136
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-rab 2358  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3604  df-int 3639  df-br 3788  df-iota 4891  df-fv 4934  df-ov 5540  df-inn 8096  df-n0 8345
This theorem is referenced by:  elnn0nn  8386  elz2  8489  peano5uzti  8525  fseq1p1m1  9176  fzonn0p1  9286  nn0ennn  9504  faccl  9748  facdiv  9751  facwordi  9753  faclbnd  9754  facubnd  9758  bcm1k  9773  bcp1n  9774  bcp1nk  9775  bcpasc  9779  prmfac1  10664
  Copyright terms: Public domain W3C validator