Theorem 1nn0 9017

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 8755	. 2 |- 1 e. NN
2	1	nnnn0i 9009	1 |- 1 e. NN0

Syntax hints:   e. wcel 1481   1c1 7645   NN0cn0 9001

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7738

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-int 3780  df-inn 8745  df-n0 9002

This theorem is referenced by:  peano2nn0  9041  deccl  9220  10nn0  9223  numsucc  9245  numadd  9252  numaddc  9253  11multnc  9273  6p5lem  9275  6p6e12  9279  7p5e12  9282  8p4e12  9287  9p2e11  9292  9p3e12  9293  10p10e20  9300  4t4e16  9304  5t2e10  9305  5t4e20  9307  6t3e18  9310  6t4e24  9311  7t3e21  9315  7t4e28  9316  8t3e24  9321  9t3e27  9328  9t9e81  9334  nn01to3  9436  elfzom1elp1fzo  10010  fzo0sn0fzo1  10029  1tonninf  10244  expn1ap0  10334  nn0expcl  10338  sqval  10382  sq10  10490  nn0opthlem1d  10498  fac2  10509  bccl  10545  hashsng  10576  1elfz0hash  10584  bcxmas  11290  arisum  11299  geoisum1  11320  geoisum1c  11321  cvgratnnlemsumlt  11329  mertenslem2  11337  ege2le3  11414  ef4p  11437  efgt1p2  11438  efgt1p  11439  sin01gt0  11504  dvds1  11587  3dvds2dec  11599  ennnfonelemhom  11964  dsndx  12156  dsid  12157  dsslid  12158  dveflem  12895  1kp2ke3k  13107  ex-exp  13110  ex-fac  13111  012of  13363  isomninnlem  13400  trilpolemisumle  13406  iswomninnlem  13417  ismkvnnlem  13419