Theorem 1nn0 9385

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 9121	. 2 |- 1 e. NN
2	1	nnnn0i 9377	1 |- 1 e. NN0

Syntax hints:   e. wcel 2200   1c1 8000   NN0cn0 9369

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8093

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-int 3924  df-inn 9111  df-n0 9370

This theorem is referenced by:  peano2nn0  9409  deccl  9592  10nn0  9595  numsucc  9617  numadd  9624  numaddc  9625  11multnc  9645  6p5lem  9647  6p6e12  9651  7p5e12  9654  8p4e12  9659  9p2e11  9664  9p3e12  9665  10p10e20  9672  4t4e16  9676  5t2e10  9677  5t4e20  9679  6t3e18  9682  6t4e24  9683  7t3e21  9687  7t4e28  9688  8t3e24  9693  9t3e27  9700  9t9e81  9706  nn01to3  9812  fz0to3un2pr  10319  elfzom1elp1fzo  10408  fzo0sn0fzo1  10427  fldiv4lem1div2  10527  1tonninf  10663  expn1ap0  10771  nn0expcl  10775  sqval  10819  sq10  10934  nn0opthlem1d  10942  fac2  10953  bccl  10989  hashsng  11020  1elfz0hash  11028  snopiswrd  11081  wrdred1hash  11115  pfx1  11235  s3fv1g  11324  bcxmas  12000  arisum  12009  geoisum1  12030  geoisum1c  12031  cvgratnnlemsumlt  12039  mertenslem2  12047  fprodnn0cl  12123  ege2le3  12182  ef4p  12205  efgt1p2  12206  efgt1p  12207  sin01gt0  12273  dvds1  12364  3dvds2dec  12377  5ndvds6  12446  bitsmod  12467  bitsinv1lem  12472  isprm5  12664  pcelnn  12844  pockthg  12880  dec5nprm  12937  dec2nprm  12938  modxp1i  12941  2exp8  12958  2exp11  12959  2exp16  12960  2expltfac  12962  ennnfonelemhom  12986  ocndx  13244  ocid  13245  basendxnocndx  13246  plendxnocndx  13247  dsndx  13248  dsid  13249  dsslid  13250  dsndxnn  13251  basendxltdsndx  13252  slotsdifdsndx  13258  unifndx  13259  unifid  13260  unifndxnn  13261  basendxltunifndx  13262  slotsdifunifndx  13265  homndx  13266  homid  13267  homslid  13268  ccondx  13269  ccoid  13270  ccoslid  13271  imasvalstrd  13303  prdsvalstrd  13304  cnfldstr  14522  dveflem  15400  plyid  15420  1sgmprm  15668  perfectlem1  15673  perfectlem2  15674  2lgslem3a  15772  2lgslem3c  15774  edgfid  15807  edgfndx  15808  edgfndxnn  15809  basendxltedgfndx  15811  1kp2ke3k  16088  ex-exp  16091  ex-fac  16092  012of  16357  isomninnlem  16398  trilpolemisumle  16406  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420