Theorem 1nn0 9417

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 9153	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 9409	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2202  1c1 8032  ℕ₀cn0 9401

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8125

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-int 3929  df-inn 9143  df-n0 9402

This theorem is referenced by:  peano2nn0  9441  deccl  9624  10nn0  9627  numsucc  9649  numadd  9656  numaddc  9657  11multnc  9677  6p5lem  9679  6p6e12  9683  7p5e12  9686  8p4e12  9691  9p2e11  9696  9p3e12  9697  10p10e20  9704  4t4e16  9708  5t2e10  9709  5t4e20  9711  6t3e18  9714  6t4e24  9715  7t3e21  9719  7t4e28  9720  8t3e24  9725  9t3e27  9732  9t9e81  9738  nn01to3  9850  fz0to3un2pr  10357  elfzom1elp1fzo  10446  fzo0sn0fzo1  10465  fldiv4lem1div2  10566  1tonninf  10702  expn1ap0  10810  nn0expcl  10814  sqval  10858  sq10  10973  nn0opthlem1d  10981  fac2  10992  bccl  11028  hashsng  11059  1elfz0hash  11069  snopiswrd  11122  wrdred1hash  11156  pfx1  11283  s3fv1g  11372  bcxmas  12049  arisum  12058  geoisum1  12079  geoisum1c  12080  cvgratnnlemsumlt  12088  mertenslem2  12096  fprodnn0cl  12172  ege2le3  12231  ef4p  12254  efgt1p2  12255  efgt1p  12256  sin01gt0  12322  dvds1  12413  3dvds2dec  12426  5ndvds6  12495  bitsmod  12516  bitsinv1lem  12521  isprm5  12713  pcelnn  12893  pockthg  12929  dec5nprm  12986  dec2nprm  12987  modxp1i  12990  2exp8  13007  2exp11  13008  2exp16  13009  2expltfac  13011  ennnfonelemhom  13035  ocndx  13293  ocid  13294  basendxnocndx  13295  plendxnocndx  13296  dsndx  13297  dsid  13298  dsslid  13299  dsndxnn  13300  basendxltdsndx  13301  slotsdifdsndx  13307  unifndx  13308  unifid  13309  unifndxnn  13310  basendxltunifndx  13311  slotsdifunifndx  13314  homndx  13315  homid  13316  homslid  13317  ccondx  13318  ccoid  13319  ccoslid  13320  imasvalstrd  13352  prdsvalstrd  13353  cnfldstr  14571  dveflem  15449  plyid  15469  1sgmprm  15717  perfectlem1  15722  perfectlem2  15723  2lgslem3a  15821  2lgslem3c  15823  edgfid  15856  edgfndx  15857  edgfndxnn  15858  basendxltedgfndx  15860  clwwlkccatlem  16250  umgr2cwwkdifex  16275  1kp2ke3k  16320  ex-exp  16323  ex-fac  16324  012of  16592  isomninnlem  16634  trilpolemisumle  16642  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656