MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  9nn0 Structured version   Visualization version   GIF version

Theorem 9nn0 11564
Description: 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
Assertion
Ref Expression
9nn0 9 ∈ ℕ0

Proof of Theorem 9nn0
StepHypRef Expression
1 9nn 11376 . 2 9 ∈ ℕ
21nnnn0i 11547 1 9 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  9c9 11334  0cn0 11538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-1cn 10247
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-om 7264  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539
This theorem is referenced by:  deccl  11755  le9lt10  11768  decsucc  11782  9p2e11  11828  9p3e12  11829  9p4e13  11830  9p5e14  11831  9p6e15  11832  9p7e16  11833  9p8e17  11834  9p9e18  11835  9t3e27  11864  9t4e36  11865  9t5e45  11866  9t6e54  11867  9t7e63  11868  9t8e72  11869  9t9e81  11870  sq10e99m1  13256  3dvds2dec  15341  2exp8  16072  19prm  16100  prmlem2  16102  37prm  16103  83prm  16105  139prm  16106  163prm  16107  317prm  16108  631prm  16109  1259lem1  16113  1259lem2  16114  1259lem3  16115  1259lem4  16116  1259lem5  16117  1259prm  16118  2503lem1  16119  2503lem2  16120  2503lem3  16121  2503prm  16122  4001lem1  16123  4001lem2  16124  4001lem3  16125  4001lem4  16126  cnfldfun  20031  tuslem  22350  setsmsds  22560  tnglem  22723  tngds  22731  log2ublem3  24966  log2ub  24967  bposlem8  25307  dp2lt10  29974  1mhdrd  30006  hgt750lem2  31113  hgt750leme  31119  kur14lem8  31575  fmtno5lem1  42073  fmtno5lem3  42075  fmtno5lem4  42076  fmtno5  42077  257prm  42081  fmtno4prmfac  42092  fmtno4prmfac193  42093  fmtno4nprmfac193  42094  fmtno5fac  42102  139prmALT  42119  127prm  42123  m11nprm  42126  tgblthelfgott  42311  tgoldbachlt  42312
  Copyright terms: Public domain W3C validator