Theorem 1nn0 9584

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

This proof depends on syntax axioms:   ∈ wcel 2209  1c1 8181  ℕ₀cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8274

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-int 3971  df-inn 9308  df-n0 9569

This theorem is used by:  peano2nn0  9608  deccl  9796  11nn0  9797  12nn0  9798  16nn0  9799  10nn0  9803  11nn  9806  numsucc  9826  numadd  9833  numaddc  9834  11multnc  9854  6p5lem  9856  6p6e12  9860  7p5e12  9863  8p4e12  9868  9p2e11  9873  9p3e12  9874  10p10e20  9881  4t4e16  9885  5t2e10  9886  5t4e20  9888  6t3e18  9891  6t4e24  9892  7t3e21  9896  7t4e28  9897  8t3e24  9902  9t3e27  9909  9t9e81  9915  nn01to3  10027  fz0to3un2pr  10541  elfzom1elp1fzo  10631  fzo0sn0fzo1  10650  fldiv4lem1div2  10757  1tonninf  10893  expn1ap0  11001  nn0expcl  11005  sqval  11049  sq10  11166  nn0opthlem1d  11174  fac2  11185  bccl  11221  hashsng  11253  1elfz0hash  11263  snopiswrd  11330  wrdred1hash  11364  pfx1  11491  s3fv1g  11580  bcxmas  12275  arisum  12284  geoisum1  12305  geoisum1c  12306  cvgratnnlemsumlt  12314  mertenslem2  12322  fprodnn0cl  12398  ege2le3  12457  ef4p  12480  efgt1p2  12481  efgt1p  12482  sin01gt0  12548  dvds1  12639  3dvds2dec  12652  5ndvds6  12721  bitsmod  12742  bitsinv1lem  12747  isprm5  12940  pcelnn  13123  pockthg  13159  dec5nprm  13216  dec2nprm  13217  modxp1i  13220  2exp8  13238  2exp11  13239  2exp16  13240  2expltfac  13242  5prm  13246  11prm  13252  13prm  13253  17prm  13254  19prm  13255  23prm  13256  prmlem2  13257  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ennnfonelemhom  13358  ocndx  13618  ocid  13619  basendxnocndx  13620  plendxnocndx  13621  dsndx  13622  dsid  13623  dsslid  13624  dsndxnn  13625  basendxltdsndx  13626  slotsdifdsndx  13632  unifndx  13633  unifid  13634  unifndxnn  13635  basendxltunifndx  13636  slotsdifunifndx  13639  homndx  13640  homid  13641  homslid  13642  ccondx  13643  ccoid  13644  ccoslid  13645  imasvalstrd  13672  prdsvalstrd  13673  cnfldstr  14979  dveflem  15918  plyid  15938  log2ublem3  16184  log2ublog2  16185  birthdaylog2  16189  ppi2  16235  1sgmprm  16249  ppiublem2  16253  chtublem  16256  perfectlem1  16260  perfectlem2  16261  bclbnd  16268  bpos1  16271  bposlem6  16277  2lgslem3a  16378  2lgslem3c  16380  edgfid  16413  edgfndx  16414  edgfndxnn  16415  basendxltedgfndx  16417  clwwlkccatlem  16807  umgr2cwwkdifex  16832  konigsbergiedgwen  16891  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem4  16898  konigsberglem5  16899  konigsberg  16900  1kp2ke3k  16904  ex-exp  16907  ex-fac  16908  012of  17189  isomninnlem  17245  trilpolemisumle  17254  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269