Theorem 1nn0 9313

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 9049	. 2 |- 1 e. NN
2	1	nnnn0i 9305	1 |- 1 e. NN0

Syntax hints:   e. wcel 2176   1c1 7928   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8021

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-int 3886  df-inn 9039  df-n0 9298

This theorem is referenced by:  peano2nn0  9337  deccl  9520  10nn0  9523  numsucc  9545  numadd  9552  numaddc  9553  11multnc  9573  6p5lem  9575  6p6e12  9579  7p5e12  9582  8p4e12  9587  9p2e11  9592  9p3e12  9593  10p10e20  9600  4t4e16  9604  5t2e10  9605  5t4e20  9607  6t3e18  9610  6t4e24  9611  7t3e21  9615  7t4e28  9616  8t3e24  9621  9t3e27  9628  9t9e81  9634  nn01to3  9740  fz0to3un2pr  10247  elfzom1elp1fzo  10333  fzo0sn0fzo1  10352  fldiv4lem1div2  10452  1tonninf  10588  expn1ap0  10696  nn0expcl  10700  sqval  10744  sq10  10859  nn0opthlem1d  10867  fac2  10878  bccl  10914  hashsng  10945  1elfz0hash  10953  snopiswrd  11006  wrdred1hash  11039  pfx1  11157  bcxmas  11833  arisum  11842  geoisum1  11863  geoisum1c  11864  cvgratnnlemsumlt  11872  mertenslem2  11880  fprodnn0cl  11956  ege2le3  12015  ef4p  12038  efgt1p2  12039  efgt1p  12040  sin01gt0  12106  dvds1  12197  3dvds2dec  12210  5ndvds6  12279  bitsmod  12300  bitsinv1lem  12305  isprm5  12497  pcelnn  12677  pockthg  12713  dec5nprm  12770  dec2nprm  12771  modxp1i  12774  2exp8  12791  2exp11  12792  2exp16  12793  2expltfac  12795  ennnfonelemhom  12819  ocndx  13076  ocid  13077  basendxnocndx  13078  plendxnocndx  13079  dsndx  13080  dsid  13081  dsslid  13082  dsndxnn  13083  basendxltdsndx  13084  slotsdifdsndx  13090  unifndx  13091  unifid  13092  unifndxnn  13093  basendxltunifndx  13094  slotsdifunifndx  13097  homndx  13098  homid  13099  homslid  13100  ccondx  13101  ccoid  13102  ccoslid  13103  imasvalstrd  13135  prdsvalstrd  13136  cnfldstr  14353  dveflem  15231  plyid  15251  1sgmprm  15499  perfectlem1  15504  perfectlem2  15505  2lgslem3a  15603  2lgslem3c  15605  edgfid  15638  edgfndx  15639  edgfndxnn  15640  basendxltedgfndx  15642  1kp2ke3k  15697  ex-exp  15700  ex-fac  15701  012of  15967  isomninnlem  16006  trilpolemisumle  16014  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028