Theorem 1nn0 9284

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

Syntax hints:   ∈ wcel 2167  1c1 7899  ℕ₀cn0 9268

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7992

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-int 3876  df-inn 9010  df-n0 9269

This theorem is referenced by:  peano2nn0  9308  deccl  9490  10nn0  9493  numsucc  9515  numadd  9522  numaddc  9523  11multnc  9543  6p5lem  9545  6p6e12  9549  7p5e12  9552  8p4e12  9557  9p2e11  9562  9p3e12  9563  10p10e20  9570  4t4e16  9574  5t2e10  9575  5t4e20  9577  6t3e18  9580  6t4e24  9581  7t3e21  9585  7t4e28  9586  8t3e24  9591  9t3e27  9598  9t9e81  9604  nn01to3  9710  fz0to3un2pr  10217  elfzom1elp1fzo  10297  fzo0sn0fzo1  10316  fldiv4lem1div2  10416  1tonninf  10552  expn1ap0  10660  nn0expcl  10664  sqval  10708  sq10  10823  nn0opthlem1d  10831  fac2  10842  bccl  10878  hashsng  10909  1elfz0hash  10917  snopiswrd  10964  wrdred1hash  10997  bcxmas  11673  arisum  11682  geoisum1  11703  geoisum1c  11704  cvgratnnlemsumlt  11712  mertenslem2  11720  fprodnn0cl  11796  ege2le3  11855  ef4p  11878  efgt1p2  11879  efgt1p  11880  sin01gt0  11946  dvds1  12037  3dvds2dec  12050  5ndvds6  12119  bitsmod  12140  bitsinv1lem  12145  isprm5  12337  pcelnn  12517  pockthg  12553  dec5nprm  12610  dec2nprm  12611  modxp1i  12614  2exp8  12631  2exp11  12632  2exp16  12633  2expltfac  12635  ennnfonelemhom  12659  ocndx  12915  ocid  12916  basendxnocndx  12917  plendxnocndx  12918  dsndx  12919  dsid  12920  dsslid  12921  dsndxnn  12922  basendxltdsndx  12923  slotsdifdsndx  12929  unifndx  12930  unifid  12931  unifndxnn  12932  basendxltunifndx  12933  slotsdifunifndx  12936  homndx  12937  homid  12938  homslid  12939  ccondx  12940  ccoid  12941  ccoslid  12942  imasvalstrd  12974  prdsvalstrd  12975  cnfldstr  14192  dveflem  15070  plyid  15090  1sgmprm  15338  perfectlem1  15343  perfectlem2  15344  2lgslem3a  15442  2lgslem3c  15444  1kp2ke3k  15478  ex-exp  15481  ex-fac  15482  012of  15748  isomninnlem  15787  trilpolemisumle  15795  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809