Theorem 1nn0 9396

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

Syntax hints:   ∈ wcel 2200  1c1 8011  ℕ₀cn0 9380

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 8104

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-int 3924  df-inn 9122  df-n0 9381

This theorem is referenced by:  peano2nn0  9420  deccl  9603  10nn0  9606  numsucc  9628  numadd  9635  numaddc  9636  11multnc  9656  6p5lem  9658  6p6e12  9662  7p5e12  9665  8p4e12  9670  9p2e11  9675  9p3e12  9676  10p10e20  9683  4t4e16  9687  5t2e10  9688  5t4e20  9690  6t3e18  9693  6t4e24  9694  7t3e21  9698  7t4e28  9699  8t3e24  9704  9t3e27  9711  9t9e81  9717  nn01to3  9824  fz0to3un2pr  10331  elfzom1elp1fzo  10420  fzo0sn0fzo1  10439  fldiv4lem1div2  10539  1tonninf  10675  expn1ap0  10783  nn0expcl  10787  sqval  10831  sq10  10946  nn0opthlem1d  10954  fac2  10965  bccl  11001  hashsng  11032  1elfz0hash  11041  snopiswrd  11094  wrdred1hash  11128  pfx1  11250  s3fv1g  11339  bcxmas  12015  arisum  12024  geoisum1  12045  geoisum1c  12046  cvgratnnlemsumlt  12054  mertenslem2  12062  fprodnn0cl  12138  ege2le3  12197  ef4p  12220  efgt1p2  12221  efgt1p  12222  sin01gt0  12288  dvds1  12379  3dvds2dec  12392  5ndvds6  12461  bitsmod  12482  bitsinv1lem  12487  isprm5  12679  pcelnn  12859  pockthg  12895  dec5nprm  12952  dec2nprm  12953  modxp1i  12956  2exp8  12973  2exp11  12974  2exp16  12975  2expltfac  12977  ennnfonelemhom  13001  ocndx  13259  ocid  13260  basendxnocndx  13261  plendxnocndx  13262  dsndx  13263  dsid  13264  dsslid  13265  dsndxnn  13266  basendxltdsndx  13267  slotsdifdsndx  13273  unifndx  13274  unifid  13275  unifndxnn  13276  basendxltunifndx  13277  slotsdifunifndx  13280  homndx  13281  homid  13282  homslid  13283  ccondx  13284  ccoid  13285  ccoslid  13286  imasvalstrd  13318  prdsvalstrd  13319  cnfldstr  14537  dveflem  15415  plyid  15435  1sgmprm  15683  perfectlem1  15688  perfectlem2  15689  2lgslem3a  15787  2lgslem3c  15789  edgfid  15822  edgfndx  15823  edgfndxnn  15824  basendxltedgfndx  15826  clwwlkccatlem  16137  1kp2ke3k  16143  ex-exp  16146  ex-fac  16147  012of  16416  isomninnlem  16458  trilpolemisumle  16466  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480