Theorem 1nn0 9381

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

Syntax hints:   ∈ wcel 2200  1c1 7996  ℕ₀cn0 9365

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 8089

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 3923  df-inn 9107  df-n0 9366

This theorem is referenced by:  peano2nn0  9405  deccl  9588  10nn0  9591  numsucc  9613  numadd  9620  numaddc  9621  11multnc  9641  6p5lem  9643  6p6e12  9647  7p5e12  9650  8p4e12  9655  9p2e11  9660  9p3e12  9661  10p10e20  9668  4t4e16  9672  5t2e10  9673  5t4e20  9675  6t3e18  9678  6t4e24  9679  7t3e21  9683  7t4e28  9684  8t3e24  9689  9t3e27  9696  9t9e81  9702  nn01to3  9808  fz0to3un2pr  10315  elfzom1elp1fzo  10403  fzo0sn0fzo1  10422  fldiv4lem1div2  10522  1tonninf  10658  expn1ap0  10766  nn0expcl  10770  sqval  10814  sq10  10929  nn0opthlem1d  10937  fac2  10948  bccl  10984  hashsng  11015  1elfz0hash  11023  snopiswrd  11076  wrdred1hash  11110  pfx1  11230  s3fv1g  11319  bcxmas  11995  arisum  12004  geoisum1  12025  geoisum1c  12026  cvgratnnlemsumlt  12034  mertenslem2  12042  fprodnn0cl  12118  ege2le3  12177  ef4p  12200  efgt1p2  12201  efgt1p  12202  sin01gt0  12268  dvds1  12359  3dvds2dec  12372  5ndvds6  12441  bitsmod  12462  bitsinv1lem  12467  isprm5  12659  pcelnn  12839  pockthg  12875  dec5nprm  12932  dec2nprm  12933  modxp1i  12936  2exp8  12953  2exp11  12954  2exp16  12955  2expltfac  12957  ennnfonelemhom  12981  ocndx  13239  ocid  13240  basendxnocndx  13241  plendxnocndx  13242  dsndx  13243  dsid  13244  dsslid  13245  dsndxnn  13246  basendxltdsndx  13247  slotsdifdsndx  13253  unifndx  13254  unifid  13255  unifndxnn  13256  basendxltunifndx  13257  slotsdifunifndx  13260  homndx  13261  homid  13262  homslid  13263  ccondx  13264  ccoid  13265  ccoslid  13266  imasvalstrd  13298  prdsvalstrd  13299  cnfldstr  14516  dveflem  15394  plyid  15414  1sgmprm  15662  perfectlem1  15667  perfectlem2  15668  2lgslem3a  15766  2lgslem3c  15768  edgfid  15801  edgfndx  15802  edgfndxnn  15803  basendxltedgfndx  15805  1kp2ke3k  16046  ex-exp  16049  ex-fac  16050  012of  16316  isomninnlem  16357  trilpolemisumle  16365  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379