Theorem 2nn0 9196

Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
2nn0	⊢ 2 ∈ ℕ0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 9083	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 9187	1 ⊢ 2 ∈ ℕ0

Syntax hints:   ∈ wcel 2148  2c2 8973  ℕ₀cn0 9179

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-sep 4123  ax-cnex 7905  ax-resscn 7906  ax-1re 7908  ax-addrcl 7911

This theorem depends on definitions:  df-bi 117  df-3an 980  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-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5881  df-inn 8923  df-2 8981  df-n0 9180

This theorem is referenced by:  nn0n0n1ge2  9326  7p6e13  9464  8p3e11  9467  8p5e13  9469  9p3e12  9474  9p4e13  9475  4t3e12  9484  4t4e16  9485  5t3e15  9487  5t5e25  9489  6t3e18  9491  6t5e30  9493  7t3e21  9496  7t4e28  9497  7t5e35  9498  7t6e42  9499  7t7e49  9500  8t3e24  9502  8t4e32  9503  8t5e40  9504  9t3e27  9509  9t4e36  9510  9t8e72  9514  9t9e81  9515  decbin3  9528  2eluzge0  9578  nn01to3  9620  xnn0le2is012  9869  fzo0to42pr  10223  nn0sqcl  10550  sqmul  10585  resqcl  10591  zsqcl  10594  cu2  10622  i3  10625  i4  10626  binom3  10641  nn0opthlem1d  10703  fac3  10715  faclbnd2  10725  abssq  11093  sqabs  11094  ef4p  11705  efgt1p2  11706  efi4p  11728  ef01bndlem  11767  cos01bnd  11769  oexpneg  11885  oddge22np1  11889  isprm5  12145  pythagtriplem4  12271  oddprmdvds  12355  basendxltdsndx  12676  dsndxnplusgndx  12678  dsndxnmulrndx  12679  slotsdnscsi  12680  dsndxntsetndx  12681  slotsdifdsndx  12682  slotsdifunifndx  12689  setsmsdsg  14168  dveflem  14375  tangtx  14447  2logb9irr  14577  2logb9irrap  14583  binom4  14585  lgslem1  14589  1kp2ke3k  14664  ex-exp  14667  ex-fac  14668