Theorem 1nn0 9460

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

Syntax hints:   ∈ wcel 2202  1c1 8076  ℕ₀cn0 9444

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8169

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-int 3934  df-inn 9186  df-n0 9445

This theorem is referenced by:  peano2nn0  9484  deccl  9669  10nn0  9672  numsucc  9694  numadd  9701  numaddc  9702  11multnc  9722  6p5lem  9724  6p6e12  9728  7p5e12  9731  8p4e12  9736  9p2e11  9741  9p3e12  9742  10p10e20  9749  4t4e16  9753  5t2e10  9754  5t4e20  9756  6t3e18  9759  6t4e24  9760  7t3e21  9764  7t4e28  9765  8t3e24  9770  9t3e27  9777  9t9e81  9783  nn01to3  9895  fz0to3un2pr  10403  elfzom1elp1fzo  10493  fzo0sn0fzo1  10512  fldiv4lem1div2  10613  1tonninf  10749  expn1ap0  10857  nn0expcl  10861  sqval  10905  sq10  11020  nn0opthlem1d  11028  fac2  11039  bccl  11075  hashsng  11106  1elfz0hash  11116  snopiswrd  11172  wrdred1hash  11206  pfx1  11333  s3fv1g  11422  bcxmas  12113  arisum  12122  geoisum1  12143  geoisum1c  12144  cvgratnnlemsumlt  12152  mertenslem2  12160  fprodnn0cl  12236  ege2le3  12295  ef4p  12318  efgt1p2  12319  efgt1p  12320  sin01gt0  12386  dvds1  12477  3dvds2dec  12490  5ndvds6  12559  bitsmod  12580  bitsinv1lem  12585  isprm5  12777  pcelnn  12957  pockthg  12993  dec5nprm  13050  dec2nprm  13051  modxp1i  13054  2exp8  13071  2exp11  13072  2exp16  13073  2expltfac  13075  ennnfonelemhom  13099  ocndx  13357  ocid  13358  basendxnocndx  13359  plendxnocndx  13360  dsndx  13361  dsid  13362  dsslid  13363  dsndxnn  13364  basendxltdsndx  13365  slotsdifdsndx  13371  unifndx  13372  unifid  13373  unifndxnn  13374  basendxltunifndx  13375  slotsdifunifndx  13378  homndx  13379  homid  13380  homslid  13381  ccondx  13382  ccoid  13383  ccoslid  13384  imasvalstrd  13416  prdsvalstrd  13417  cnfldstr  14637  dveflem  15520  plyid  15540  1sgmprm  15791  perfectlem1  15796  perfectlem2  15797  2lgslem3a  15895  2lgslem3c  15897  edgfid  15930  edgfndx  15931  edgfndxnn  15932  basendxltedgfndx  15934  clwwlkccatlem  16324  umgr2cwwkdifex  16349  konigsbergiedgwen  16408  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem4  16415  konigsberglem5  16416  konigsberg  16417  1kp2ke3k  16421  ex-exp  16424  ex-fac  16425  012of  16696  isomninnlem  16745  trilpolemisumle  16753  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768