ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2nn0 Unicode version

Theorem 2nn0 8892
Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
2nn0  |-  2  e.  NN0

Proof of Theorem 2nn0
StepHypRef Expression
1 2nn 8779 . 2  |-  2  e.  NN
21nnnn0i 8883 1  |-  2  e.  NN0
Colors of variables: wff set class
Syntax hints:    e. wcel 1461   2c2 8675   NN0cn0 8875
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-cnex 7630  ax-resscn 7631  ax-1re 7633  ax-addrcl 7636
This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-br 3894  df-iota 5044  df-fv 5087  df-ov 5729  df-inn 8625  df-2 8683  df-n0 8876
This theorem is referenced by:  nn0n0n1ge2  9019  7p6e13  9157  8p3e11  9160  8p5e13  9162  9p3e12  9167  9p4e13  9168  4t3e12  9177  4t4e16  9178  5t3e15  9180  5t5e25  9182  6t3e18  9184  6t5e30  9186  7t3e21  9189  7t4e28  9190  7t5e35  9191  7t6e42  9192  7t7e49  9193  8t3e24  9195  8t4e32  9196  8t5e40  9197  9t3e27  9202  9t4e36  9203  9t8e72  9207  9t9e81  9208  decbin3  9221  2eluzge0  9266  nn01to3  9305  xnn0le2is012  9536  fzo0to42pr  9884  nn0sqcl  10207  sqmul  10242  resqcl  10247  zsqcl  10250  cu2  10278  i3  10281  i4  10282  binom3  10296  nn0opthlem1d  10353  fac3  10365  faclbnd2  10375  abssq  10739  sqabs  10740  ef4p  11245  efgt1p2  11246  efi4p  11269  ef01bndlem  11308  cos01bnd  11310  oexpneg  11416  oddge22np1  11420  setsmsdsg  12463  1kp2ke3k  12620  ex-exp  12623  ex-fac  12624
  Copyright terms: Public domain W3C validator