Theorem 1nn0 9282

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

Syntax hints:   ∈ wcel 2167  1c1 7897  ℕ₀cn0 9266

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 7990

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 9008  df-n0 9267

This theorem is referenced by:  peano2nn0  9306  deccl  9488  10nn0  9491  numsucc  9513  numadd  9520  numaddc  9521  11multnc  9541  6p5lem  9543  6p6e12  9547  7p5e12  9550  8p4e12  9555  9p2e11  9560  9p3e12  9561  10p10e20  9568  4t4e16  9572  5t2e10  9573  5t4e20  9575  6t3e18  9578  6t4e24  9579  7t3e21  9583  7t4e28  9584  8t3e24  9589  9t3e27  9596  9t9e81  9602  nn01to3  9708  fz0to3un2pr  10215  elfzom1elp1fzo  10295  fzo0sn0fzo1  10314  fldiv4lem1div2  10414  1tonninf  10550  expn1ap0  10658  nn0expcl  10662  sqval  10706  sq10  10821  nn0opthlem1d  10829  fac2  10840  bccl  10876  hashsng  10907  1elfz0hash  10915  snopiswrd  10962  wrdred1hash  10995  bcxmas  11671  arisum  11680  geoisum1  11701  geoisum1c  11702  cvgratnnlemsumlt  11710  mertenslem2  11718  fprodnn0cl  11794  ege2le3  11853  ef4p  11876  efgt1p2  11877  efgt1p  11878  sin01gt0  11944  dvds1  12035  3dvds2dec  12048  5ndvds6  12117  bitsmod  12138  bitsinv1lem  12143  isprm5  12335  pcelnn  12515  pockthg  12551  dec5nprm  12608  dec2nprm  12609  modxp1i  12612  2exp8  12629  2exp11  12630  2exp16  12631  2expltfac  12633  ennnfonelemhom  12657  ocndx  12913  ocid  12914  basendxnocndx  12915  plendxnocndx  12916  dsndx  12917  dsid  12918  dsslid  12919  dsndxnn  12920  basendxltdsndx  12921  slotsdifdsndx  12927  unifndx  12928  unifid  12929  unifndxnn  12930  basendxltunifndx  12931  slotsdifunifndx  12934  homndx  12935  homid  12936  homslid  12937  ccondx  12938  ccoid  12939  ccoslid  12940  imasvalstrd  12972  prdsvalstrd  12973  cnfldstr  14190  dveflem  15046  plyid  15066  1sgmprm  15314  perfectlem1  15319  perfectlem2  15320  2lgslem3a  15418  2lgslem3c  15420  1kp2ke3k  15454  ex-exp  15457  ex-fac  15458  012of  15724  isomninnlem  15761  trilpolemisumle  15769  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783