Theorem 1nn0 9126

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	|- 1 e. NN0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 8864	. 2 |- 1 e. NN
2	1	nnnn0i 9118	1 |- 1 e. NN0

Syntax hints:   e. wcel 2136   1c1 7750   NN0cn0 9110

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7843

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-int 3824  df-inn 8854  df-n0 9111

This theorem is referenced by:  peano2nn0  9150  deccl  9332  10nn0  9335  numsucc  9357  numadd  9364  numaddc  9365  11multnc  9385  6p5lem  9387  6p6e12  9391  7p5e12  9394  8p4e12  9399  9p2e11  9404  9p3e12  9405  10p10e20  9412  4t4e16  9416  5t2e10  9417  5t4e20  9419  6t3e18  9422  6t4e24  9423  7t3e21  9427  7t4e28  9428  8t3e24  9433  9t3e27  9440  9t9e81  9446  nn01to3  9551  fz0to3un2pr  10054  elfzom1elp1fzo  10133  fzo0sn0fzo1  10152  1tonninf  10371  expn1ap0  10461  nn0expcl  10465  sqval  10509  sq10  10621  nn0opthlem1d  10629  fac2  10640  bccl  10676  hashsng  10707  1elfz0hash  10715  bcxmas  11426  arisum  11435  geoisum1  11456  geoisum1c  11457  cvgratnnlemsumlt  11465  mertenslem2  11473  fprodnn0cl  11549  ege2le3  11608  ef4p  11631  efgt1p2  11632  efgt1p  11633  sin01gt0  11698  dvds1  11787  3dvds2dec  11799  isprm5  12070  pcelnn  12248  pockthg  12283  ennnfonelemhom  12344  dsndx  12548  dsid  12549  dsslid  12550  dveflem  13287  1kp2ke3k  13565  ex-exp  13568  ex-fac  13569  012of  13835  isomninnlem  13869  trilpolemisumle  13877  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891