Theorem 1nn0 9590

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

This proof depends on syntax axioms:   ∈ wcel 2209  1c1 8186  ℕ₀cn0 9574

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 8279

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 9314  df-n0 9575

This theorem is used by:  peano2nn0  9614  deccl  9802  11nn0  9803  12nn0  9804  16nn0  9805  10nn0  9809  11nn  9812  numsucc  9832  numadd  9839  numaddc  9840  11multnc  9860  6p5lem  9862  6p6e12  9866  7p5e12  9869  8p4e12  9874  9p2e11  9879  9p3e12  9880  10p10e20  9887  4t4e16  9891  5t2e10  9892  5t4e20  9894  6t3e18  9897  6t4e24  9898  7t3e21  9902  7t4e28  9903  8t3e24  9908  9t3e27  9915  9t9e81  9921  nn01to3  10033  fz0to3un2pr  10547  elfzom1elp1fzo  10637  fzo0sn0fzo1  10656  fldiv4lem1div2  10763  1tonninf  10899  expn1ap0  11007  nn0expcl  11011  sqval  11055  sq10  11172  nn0opthlem1d  11180  fac2  11191  bccl  11227  hashsng  11259  1elfz0hash  11269  snopiswrd  11336  wrdred1hash  11370  pfx1  11497  s3fv1g  11586  bcxmas  12281  arisum  12290  geoisum1  12311  geoisum1c  12312  cvgratnnlemsumlt  12320  mertenslem2  12328  fprodnn0cl  12404  ege2le3  12463  ef4p  12486  efgt1p2  12487  efgt1p  12488  sin01gt0  12554  dvds1  12645  3dvds2dec  12658  5ndvds6  12727  bitsmod  12748  bitsinv1lem  12753  isprm5  12946  pcelnn  13129  pockthg  13165  dec5nprm  13222  dec2nprm  13223  modxp1i  13226  2exp8  13244  2exp11  13245  2exp16  13246  2expltfac  13248  5prm  13252  11prm  13258  13prm  13259  17prm  13260  19prm  13261  23prm  13262  prmlem2  13263  37prm  13264  43prm  13265  83prm  13266  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem3  13273  1259lem4  13274  1259lem5  13275  1259prm  13276  ennnfonelemhom  13364  ocndx  13624  ocid  13625  basendxnocndx  13626  plendxnocndx  13627  dsndx  13628  dsid  13629  dsslid  13630  dsndxnn  13631  basendxltdsndx  13632  slotsdifdsndx  13638  unifndx  13639  unifid  13640  unifndxnn  13641  basendxltunifndx  13642  slotsdifunifndx  13645  homndx  13646  homid  13647  homslid  13648  ccondx  13649  ccoid  13650  ccoslid  13651  imasvalstrd  13678  prdsvalstrd  13679  cnfldstr  15004  dveflem  15952  plyid  15972  log2ublem3  16223  log2ublog2  16224  birthdaylog2  16228  ppi2  16274  1sgmprm  16288  ppiublem2  16292  chtublem  16295  perfectlem1  16299  perfectlem2  16300  bclbnd  16307  bpos1  16310  bposlem6  16316  2lgslem3a  16417  2lgslem3c  16419  edgfid  16452  edgfndx  16453  edgfndxnn  16454  basendxltedgfndx  16456  clwwlkccatlem  16846  umgr2cwwkdifex  16871  konigsbergiedgwen  16930  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem4  16937  konigsberglem5  16938  konigsberg  16939  1kp2ke3k  16943  ex-exp  16946  ex-fac  16947  012of  17228  isomninnlem  17285  trilpolemisumle  17294  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309