Theorem 1nn0 9558

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

Syntax hints:   ∈ wcel 2209  1c1 8170  ℕ₀cn0 9542

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8263

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-int 3966  df-inn 9284  df-n0 9543

This theorem is referenced by:  peano2nn0  9582  deccl  9770  10nn0  9773  numsucc  9795  numadd  9802  numaddc  9803  11multnc  9823  6p5lem  9825  6p6e12  9829  7p5e12  9832  8p4e12  9837  9p2e11  9842  9p3e12  9843  10p10e20  9850  4t4e16  9854  5t2e10  9855  5t4e20  9857  6t3e18  9860  6t4e24  9861  7t3e21  9865  7t4e28  9866  8t3e24  9871  9t3e27  9878  9t9e81  9884  nn01to3  9996  fz0to3un2pr  10508  elfzom1elp1fzo  10598  fzo0sn0fzo1  10617  fldiv4lem1div2  10720  1tonninf  10856  expn1ap0  10964  nn0expcl  10968  sqval  11012  sq10  11128  nn0opthlem1d  11136  fac2  11147  bccl  11183  hashsng  11215  1elfz0hash  11225  snopiswrd  11292  wrdred1hash  11326  pfx1  11453  s3fv1g  11542  bcxmas  12234  arisum  12243  geoisum1  12264  geoisum1c  12265  cvgratnnlemsumlt  12273  mertenslem2  12281  fprodnn0cl  12357  ege2le3  12416  ef4p  12439  efgt1p2  12440  efgt1p  12441  sin01gt0  12507  dvds1  12598  3dvds2dec  12611  5ndvds6  12680  bitsmod  12701  bitsinv1lem  12706  isprm5  12898  pcelnn  13078  pockthg  13114  dec5nprm  13171  dec2nprm  13172  modxp1i  13175  2exp8  13192  2exp11  13193  2exp16  13194  2expltfac  13196  ennnfonelemhom  13284  ocndx  13542  ocid  13543  basendxnocndx  13544  plendxnocndx  13545  dsndx  13546  dsid  13547  dsslid  13548  dsndxnn  13549  basendxltdsndx  13550  slotsdifdsndx  13556  unifndx  13557  unifid  13558  unifndxnn  13559  basendxltunifndx  13560  slotsdifunifndx  13563  homndx  13564  homid  13565  homslid  13566  ccondx  13567  ccoid  13568  ccoslid  13569  imasvalstrd  13596  prdsvalstrd  13597  cnfldstr  14867  dveflem  15750  plyid  15770  1sgmprm  16022  perfectlem1  16027  perfectlem2  16028  2lgslem3a  16126  2lgslem3c  16128  edgfid  16161  edgfndx  16162  edgfndxnn  16163  basendxltedgfndx  16165  clwwlkccatlem  16555  umgr2cwwkdifex  16580  konigsbergiedgwen  16639  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem4  16646  konigsberglem5  16647  konigsberg  16648  1kp2ke3k  16652  ex-exp  16655  ex-fac  16656  012of  16937  isomninnlem  16984  trilpolemisumle  16992  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007