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

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

Proof of Theorem 6nn0
StepHypRef Expression
1 6nn 11366 . 2 6 ∈ ℕ
21nnnn0i 11549 1 6 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  6c6 11333  0cn0 11540
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 2070  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 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-1cn 10249
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 2063  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 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6847  df-om 7266  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-n0 11541
This theorem is referenced by:  6p5e11  11817  6p6e12  11818  7p7e14  11823  8p7e15  11829  9p7e16  11836  9p8e17  11837  6t3e18  11849  6t4e24  11850  6t5e30  11851  6t6e36  11852  7t7e49  11858  8t3e24  11860  8t7e56  11864  8t8e64  11865  9t4e36  11868  9t5e45  11869  9t7e63  11871  9t8e72  11872  6lcm4e12  15613  2exp8  16073  2exp16  16074  2expltfac  16076  19prm  16101  prmlem2  16103  37prm  16104  43prm  16105  139prm  16107  163prm  16108  317prm  16109  631prm  16110  1259lem1  16114  1259lem2  16115  1259lem3  16116  1259lem4  16117  1259lem5  16118  2503lem1  16120  2503lem2  16121  2503lem3  16122  2503prm  16123  4001lem1  16124  4001lem2  16125  4001lem3  16126  4001lem4  16127  4001prm  16128  log2ublem2  24968  log2ublem3  24969  log2ub  24970  log2le1  24971  birthday  24975  bclbnd  25299  bpos1  25302  bposlem8  25310  bposlem9  25311  bpos  25312  ttgval  26049  ttglem  26050  ttgbas  26051  ttgplusg  26052  ttgvsca  26054  eengstr  26154  ex-exp  27769  zlmds  30458  hgt750lemd  31180  hgt750lem  31183  hgt750lem2  31184  kur14lem8  31646  expdiophlem2  38269  wallispi2lem2  40929  fmtno2  42141  fmtno3  42142  fmtno4  42143  fmtno5lem1  42144  fmtno5lem2  42145  fmtno5lem3  42146  fmtno5lem4  42147  fmtno5  42148  257prm  42152  fmtno4prmfac  42163  fmtno4nprmfac193  42165  fmtno5faclem1  42170  fmtno5faclem2  42171  fmtno5faclem3  42172  fmtno5fac  42173  fmtno5nprm  42174  139prmALT  42190  2exp7  42193  127prm  42194  2exp11  42196  m11nprm  42197
  Copyright terms: Public domain W3C validator