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

Theorem 9nn0 8588
Description: 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
Assertion
Ref Expression
9nn0  |-  9  e.  NN0

Proof of Theorem 9nn0
StepHypRef Expression
1 9nn 8476 . 2  |-  9  e.  NN
21nnnn0i 8572 1  |-  9  e.  NN0
Colors of variables: wff set class
Syntax hints:    e. wcel 1434   9c9 8372   NN0cn0 8564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-cnex 7338  ax-resscn 7339  ax-1re 7341  ax-addrcl 7344
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-br 3812  df-iota 4933  df-fv 4976  df-ov 5593  df-inn 8316  df-2 8374  df-3 8375  df-4 8376  df-5 8377  df-6 8378  df-7 8379  df-8 8380  df-9 8381  df-n0 8565
This theorem is referenced by:  deccl  8785  le9lt10  8797  decsucc  8811  9p2e11  8857  9p3e12  8858  9p4e13  8859  9p5e14  8860  9p6e15  8861  9p7e16  8862  9p8e17  8863  9p9e18  8864  9t3e27  8893  9t4e36  8894  9t5e45  8895  9t6e54  8896  9t7e63  8897  9t8e72  8898  9t9e81  8899  sq10e99m1  9956  3dvds2dec  10645
  Copyright terms: Public domain W3C validator