Theorem 1nn0 9186

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

Syntax hints:   ∈ wcel 2148  1c1 7807  ℕ₀cn0 9170

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7900

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-int 3844  df-inn 8914  df-n0 9171

This theorem is referenced by:  peano2nn0  9210  deccl  9392  10nn0  9395  numsucc  9417  numadd  9424  numaddc  9425  11multnc  9445  6p5lem  9447  6p6e12  9451  7p5e12  9454  8p4e12  9459  9p2e11  9464  9p3e12  9465  10p10e20  9472  4t4e16  9476  5t2e10  9477  5t4e20  9479  6t3e18  9482  6t4e24  9483  7t3e21  9487  7t4e28  9488  8t3e24  9493  9t3e27  9500  9t9e81  9506  nn01to3  9611  fz0to3un2pr  10116  elfzom1elp1fzo  10195  fzo0sn0fzo1  10214  1tonninf  10433  expn1ap0  10523  nn0expcl  10527  sqval  10571  sq10  10683  nn0opthlem1d  10691  fac2  10702  bccl  10738  hashsng  10769  1elfz0hash  10777  bcxmas  11488  arisum  11497  geoisum1  11518  geoisum1c  11519  cvgratnnlemsumlt  11527  mertenslem2  11535  fprodnn0cl  11611  ege2le3  11670  ef4p  11693  efgt1p2  11694  efgt1p  11695  sin01gt0  11760  dvds1  11849  3dvds2dec  11861  isprm5  12132  pcelnn  12310  pockthg  12345  ennnfonelemhom  12406  dsndx  12656  dsid  12657  dsslid  12658  dsndxnn  12659  basendxltdsndx  12660  slotsdifdsndx  12666  unifndx  12667  unifid  12668  unifndxnn  12669  basendxltunifndx  12670  slotsdifunifndx  12673  cnfldstr  13262  dveflem  13969  1kp2ke3k  14247  ex-exp  14250  ex-fac  14251  012of  14516  isomninnlem  14549  trilpolemisumle  14557  iswomninnlem  14568  iswomni0  14570  ismkvnnlem  14571