Theorem 2nn0 9127

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

Syntax hints:   ∈ wcel 2136  2c2 8904  ℕ₀cn0 9110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4099  ax-cnex 7840  ax-resscn 7841  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-int 3824  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-inn 8854  df-2 8912  df-n0 9111

This theorem is referenced by:  nn0n0n1ge2  9257  7p6e13  9395  8p3e11  9398  8p5e13  9400  9p3e12  9405  9p4e13  9406  4t3e12  9415  4t4e16  9416  5t3e15  9418  5t5e25  9420  6t3e18  9422  6t5e30  9424  7t3e21  9427  7t4e28  9428  7t5e35  9429  7t6e42  9430  7t7e49  9431  8t3e24  9433  8t4e32  9434  8t5e40  9435  9t3e27  9440  9t4e36  9441  9t8e72  9445  9t9e81  9446  decbin3  9459  2eluzge0  9509  nn01to3  9551  xnn0le2is012  9798  fzo0to42pr  10151  nn0sqcl  10478  sqmul  10513  resqcl  10518  zsqcl  10521  cu2  10549  i3  10552  i4  10553  binom3  10568  nn0opthlem1d  10629  fac3  10641  faclbnd2  10651  abssq  11019  sqabs  11020  ef4p  11631  efgt1p2  11632  efi4p  11654  ef01bndlem  11693  cos01bnd  11695  oexpneg  11810  oddge22np1  11814  isprm5  12070  pythagtriplem4  12196  oddprmdvds  12280  setsmsdsg  13080  dveflem  13287  tangtx  13359  2logb9irr  13489  2logb9irrap  13495  binom4  13497  lgslem1  13501  1kp2ke3k  13565  ex-exp  13568  ex-fac  13569