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

Theorem nnnn0 8952
Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnnn0  |-  ( A  e.  NN  ->  A  e.  NN0 )

Proof of Theorem nnnn0
StepHypRef Expression
1 nnssnn0 8948 . 2  |-  NN  C_  NN0
21sseli 3063 1  |-  ( A  e.  NN  ->  A  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465   NNcn 8688   NN0cn0 8945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-in 3047  df-ss 3054  df-n0 8946
This theorem is referenced by:  nnnn0i  8953  elnnnn0b  8989  elnnnn0c  8990  elnn0z  9035  elz2  9090  nn0ind-raph  9136  zindd  9137  fzo1fzo0n0  9928  ubmelfzo  9945  elfzom1elp1fzo  9947  fzo0sn0fzo1  9966  modqmulnn  10083  expnegap0  10269  expcllem  10272  expcl2lemap  10273  expap0  10291  expeq0  10292  mulexpzap  10301  expnlbnd  10384  facdiv  10452  faclbnd  10455  faclbnd3  10457  faclbnd6  10458  resqrexlemlo  10753  absexpzap  10820  isummolemnm  11116  summodclem2a  11118  fsum3  11124  arisum  11235  expcnvap0  11239  expcnv  11241  geo2sum  11251  geo2lim  11253  geoisum1c  11257  0.999...  11258  mertenslem2  11273  ef0lem  11293  ege2le3  11304  efaddlem  11307  efexp  11315  nn0enne  11526  nnehalf  11528  nno  11530  nn0o  11531  divalg2  11550  ndvdssub  11554  gcddiv  11634  gcdmultiple  11635  gcdmultiplez  11636  rpmulgcd  11641  rplpwr  11642  dvdssqlem  11645  eucalgf  11663  1nprm  11722  isprm6  11752  prmdvdsexp  11753  pw2dvds  11771  oddpwdc  11779  phicl2  11817  phibndlem  11819  phiprmpw  11825  crth  11827  hashgcdlem  11830  ennnfonelemjn  11842  dvexp  12771
  Copyright terms: Public domain W3C validator