Theorem 1nn0 9408

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

Assertion

Ref	Expression
1nn0	⊢ 1 ∈ ℕ0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 9144	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 9400	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2200  1c1 8023  ℕ₀cn0 9392

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 8116

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-int 3927  df-inn 9134  df-n0 9393

This theorem is referenced by:  peano2nn0  9432  deccl  9615  10nn0  9618  numsucc  9640  numadd  9647  numaddc  9648  11multnc  9668  6p5lem  9670  6p6e12  9674  7p5e12  9677  8p4e12  9682  9p2e11  9687  9p3e12  9688  10p10e20  9695  4t4e16  9699  5t2e10  9700  5t4e20  9702  6t3e18  9705  6t4e24  9706  7t3e21  9710  7t4e28  9711  8t3e24  9716  9t3e27  9723  9t9e81  9729  nn01to3  9841  fz0to3un2pr  10348  elfzom1elp1fzo  10437  fzo0sn0fzo1  10456  fldiv4lem1div2  10557  1tonninf  10693  expn1ap0  10801  nn0expcl  10805  sqval  10849  sq10  10964  nn0opthlem1d  10972  fac2  10983  bccl  11019  hashsng  11050  1elfz0hash  11060  snopiswrd  11113  wrdred1hash  11147  pfx1  11274  s3fv1g  11363  bcxmas  12040  arisum  12049  geoisum1  12070  geoisum1c  12071  cvgratnnlemsumlt  12079  mertenslem2  12087  fprodnn0cl  12163  ege2le3  12222  ef4p  12245  efgt1p2  12246  efgt1p  12247  sin01gt0  12313  dvds1  12404  3dvds2dec  12417  5ndvds6  12486  bitsmod  12507  bitsinv1lem  12512  isprm5  12704  pcelnn  12884  pockthg  12920  dec5nprm  12977  dec2nprm  12978  modxp1i  12981  2exp8  12998  2exp11  12999  2exp16  13000  2expltfac  13002  ennnfonelemhom  13026  ocndx  13284  ocid  13285  basendxnocndx  13286  plendxnocndx  13287  dsndx  13288  dsid  13289  dsslid  13290  dsndxnn  13291  basendxltdsndx  13292  slotsdifdsndx  13298  unifndx  13299  unifid  13300  unifndxnn  13301  basendxltunifndx  13302  slotsdifunifndx  13305  homndx  13306  homid  13307  homslid  13308  ccondx  13309  ccoid  13310  ccoslid  13311  imasvalstrd  13343  prdsvalstrd  13344  cnfldstr  14562  dveflem  15440  plyid  15460  1sgmprm  15708  perfectlem1  15713  perfectlem2  15714  2lgslem3a  15812  2lgslem3c  15814  edgfid  15847  edgfndx  15848  edgfndxnn  15849  basendxltedgfndx  15851  clwwlkccatlem  16195  umgr2cwwkdifex  16220  1kp2ke3k  16256  ex-exp  16259  ex-fac  16260  012of  16528  isomninnlem  16570  trilpolemisumle  16578  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592