Theorem 1nn0 9590

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

This proof depends on syntax axioms:   ∈ wcel 2209  1c1 8186  ℕ₀cn0 9574

This proof depends on 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 8279

This proof 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 3971  df-inn 9314  df-n0 9575

This theorem is used by:  peano2nn0  9614  deccl  9801  11nn0  9802  12nn0  9803  16nn0  9804  10nn0  9808  11nn  9811  numsucc  9831  numadd  9838  numaddc  9839  11multnc  9859  6p5lem  9861  6p6e12  9865  7p5e12  9868  8p4e12  9873  9p2e11  9878  9p3e12  9879  10p10e20  9886  4t4e16  9890  5t2e10  9891  5t4e20  9893  6t3e18  9896  6t4e24  9897  7t3e21  9901  7t4e28  9902  8t3e24  9907  9t3e27  9914  9t9e81  9920  nn01to3  10032  fz0to3un2pr  10546  elfzom1elp1fzo  10636  fzo0sn0fzo1  10655  fldiv4lem1div2  10762  1tonninf  10898  expn1ap0  11006  nn0expcl  11010  sqval  11054  sq10  11171  nn0opthlem1d  11179  fac2  11190  bccl  11226  hashsng  11258  1elfz0hash  11268  snopiswrd  11335  wrdred1hash  11369  pfx1  11496  s3fv1g  11585  bcxmas  12280  arisum  12289  geoisum1  12310  geoisum1c  12311  cvgratnnlemsumlt  12319  mertenslem2  12327  fprodnn0cl  12403  ege2le3  12462  ef4p  12485  efgt1p2  12486  efgt1p  12487  sin01gt0  12553  dvds1  12644  3dvds2dec  12657  5ndvds6  12726  bitsmod  12747  bitsinv1lem  12752  isprm5  12945  pcelnn  13128  pockthg  13164  dec5nprm  13221  dec2nprm  13222  modxp1i  13225  2exp8  13243  2exp11  13244  2exp16  13245  2expltfac  13247  5prm  13251  11prm  13257  13prm  13258  17prm  13259  19prm  13260  23prm  13261  prmlem2  13262  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  ennnfonelemhom  13363  ocndx  13623  ocid  13624  basendxnocndx  13625  plendxnocndx  13626  dsndx  13627  dsid  13628  dsslid  13629  dsndxnn  13630  basendxltdsndx  13631  slotsdifdsndx  13637  unifndx  13638  unifid  13639  unifndxnn  13640  basendxltunifndx  13641  slotsdifunifndx  13644  homndx  13645  homid  13646  homslid  13647  ccondx  13648  ccoid  13649  ccoslid  13650  imasvalstrd  13677  prdsvalstrd  13678  cnfldstr  15003  mvridfi  15217  mvrffi  15218  mvrf1fi  15219  mvrclfi  15226  dveflem  15969  plyid  15989  log2ublem3  16240  log2ublog2  16241  birthdaylog2  16245  ppi2  16291  1sgmprm  16305  ppiublem2  16309  chtublem  16312  perfectlem1  16316  perfectlem2  16317  bclbnd  16324  bpos1  16327  bposlem6  16333  2lgslem3a  16434  2lgslem3c  16436  edgfid  16469  edgfndx  16470  edgfndxnn  16471  basendxltedgfndx  16473  clwwlkccatlem  16863  umgr2cwwkdifex  16888  konigsbergiedgwen  16947  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem4  16954  konigsberglem5  16955  konigsberg  16956  1kp2ke3k  16960  ex-exp  16963  ex-fac  16964  012of  17245  isomninnlem  17302  trilpolemisumle  17311  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326