Theorem 1nn0 9406

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

Syntax hints:   ∈ wcel 2200  1c1 8021  ℕ₀cn0 9390

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8114

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-int 3925  df-inn 9132  df-n0 9391

This theorem is referenced by:  peano2nn0  9430  deccl  9613  10nn0  9616  numsucc  9638  numadd  9645  numaddc  9646  11multnc  9666  6p5lem  9668  6p6e12  9672  7p5e12  9675  8p4e12  9680  9p2e11  9685  9p3e12  9686  10p10e20  9693  4t4e16  9697  5t2e10  9698  5t4e20  9700  6t3e18  9703  6t4e24  9704  7t3e21  9708  7t4e28  9709  8t3e24  9714  9t3e27  9721  9t9e81  9727  nn01to3  9839  fz0to3un2pr  10346  elfzom1elp1fzo  10435  fzo0sn0fzo1  10454  fldiv4lem1div2  10555  1tonninf  10691  expn1ap0  10799  nn0expcl  10803  sqval  10847  sq10  10962  nn0opthlem1d  10970  fac2  10981  bccl  11017  hashsng  11048  1elfz0hash  11057  snopiswrd  11110  wrdred1hash  11144  pfx1  11271  s3fv1g  11360  bcxmas  12037  arisum  12046  geoisum1  12067  geoisum1c  12068  cvgratnnlemsumlt  12076  mertenslem2  12084  fprodnn0cl  12160  ege2le3  12219  ef4p  12242  efgt1p2  12243  efgt1p  12244  sin01gt0  12310  dvds1  12401  3dvds2dec  12414  5ndvds6  12483  bitsmod  12504  bitsinv1lem  12509  isprm5  12701  pcelnn  12881  pockthg  12917  dec5nprm  12974  dec2nprm  12975  modxp1i  12978  2exp8  12995  2exp11  12996  2exp16  12997  2expltfac  12999  ennnfonelemhom  13023  ocndx  13281  ocid  13282  basendxnocndx  13283  plendxnocndx  13284  dsndx  13285  dsid  13286  dsslid  13287  dsndxnn  13288  basendxltdsndx  13289  slotsdifdsndx  13295  unifndx  13296  unifid  13297  unifndxnn  13298  basendxltunifndx  13299  slotsdifunifndx  13302  homndx  13303  homid  13304  homslid  13305  ccondx  13306  ccoid  13307  ccoslid  13308  imasvalstrd  13340  prdsvalstrd  13341  cnfldstr  14559  dveflem  15437  plyid  15457  1sgmprm  15705  perfectlem1  15710  perfectlem2  15711  2lgslem3a  15809  2lgslem3c  15811  edgfid  15844  edgfndx  15845  edgfndxnn  15846  basendxltedgfndx  15848  clwwlkccatlem  16185  umgr2cwwkdifex  16210  1kp2ke3k  16230  ex-exp  16233  ex-fac  16234  012of  16502  isomninnlem  16544  trilpolemisumle  16552  iswomninnlem  16563  iswomni0  16565  ismkvnnlem  16566