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

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

Proof of Theorem 5nn0
StepHypRef Expression
1 5nn 11711 . 2 5 ∈ ℕ
21nnnn0i 11893 1 5 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  5c5 11683  0cn0 11885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-1cn 10584
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-om 7566  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-n0 11886
This theorem is referenced by:  6p6e12  12160  7p6e13  12164  8p6e14  12170  8p8e16  12172  9p6e15  12177  9p7e16  12178  5t2e10  12186  5t3e15  12187  5t4e20  12188  5t5e25  12189  6t6e36  12194  7t5e35  12198  7t6e42  12199  8t6e48  12205  8t8e64  12207  9t5e45  12211  9t6e54  12212  9t7e63  12213  dec2dvds  16388  dec5dvds2  16390  2exp8  16414  2exp16  16415  prmlem1  16432  5prm  16433  7prm  16435  11prm  16439  13prm  16440  17prm  16441  19prm  16442  prmlem2  16444  37prm  16445  139prm  16448  163prm  16449  317prm  16450  631prm  16451  1259lem1  16455  1259lem2  16456  1259lem3  16457  1259lem4  16458  1259lem5  16459  1259prm  16460  2503lem1  16461  2503lem2  16462  2503lem3  16463  2503prm  16464  4001lem1  16465  4001lem2  16466  4001lem3  16467  4001lem4  16468  4001prm  16469  ressco  16683  slotsbhcdif  16684  quart1cl  25438  quart1lem  25439  quart1  25440  log2ublem1  25530  log2ublem3  25532  log2ub  25533  log2le1  25534  birthday  25538  ppiublem2  25785  bpos1  25865  bposlem8  25873  ex-fac  28234  threehalves  30601  zlmds  31279  hgt750lemd  31993  hgt750lem2  31997  hgt750leme  32003  kur14lem8  32534  420gcd8e4  39255  12lcm5e60  39257  lcmineqlem  39301  3lexlogpow5ineq1  39302  3lexlogpow5ineq2  39303  3lexlogpow5ineq3  39304  sqn5i  39423  235t711  39429  ex-decpmul  39430  3cubeslem3l  39557  3cubeslem3r  39558  resqrtvalex  40275  imsqrtvalex  40276  inductionexd  40791  fmtno3  44007  fmtno4  44008  fmtno5lem1  44009  fmtno5lem2  44010  fmtno5lem3  44011  fmtno5lem4  44012  fmtno5  44013  257prm  44017  fmtno4prmfac  44028  fmtno4prmfac193  44029  fmtno4nprmfac193  44030  fmtno5faclem3  44037  flsqrt5  44050  139prmALT  44052  31prm  44053  127prm  44055  2exp11  44057  41prothprmlem2  44075  2exp340mod341  44190  linevalexample  44743  ackval2012  45044  ackval3012  45045  ackval41  45048
  Copyright terms: Public domain W3C validator