Theorem 5nn0 11669

Description: 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Assertion

Ref	Expression
5nn0	⊢ 5 ∈ ℕ0

Proof of Theorem 5nn0

Step	Hyp	Ref	Expression
1		5nn 11468	. 2 ⊢ 5 ∈ ℕ
2	1	nnnn0i 11656	1 ⊢ 5 ∈ ℕ0

Syntax hints:   ∈ wcel 2107  5c5 11438  ℕ₀cn0 11647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-1cn 10332

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-ov 6927  df-om 7346  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-nn 11380  df-2 11443  df-3 11444  df-4 11445  df-5 11446  df-n0 11648

This theorem is referenced by:  6p6e12  11926  7p6e13  11930  8p6e14  11936  8p8e16  11938  9p6e15  11943  9p7e16  11944  5t2e10  11952  5t3e15  11953  5t4e20  11954  5t5e25  11955  6t6e36  11960  7t5e35  11964  7t6e42  11965  8t6e48  11971  8t8e64  11973  9t5e45  11977  9t6e54  11978  9t7e63  11979  dec2dvds  16182  dec5dvds2  16184  2exp8  16206  2exp16  16207  prmlem1  16224  5prm  16225  7prm  16227  11prm  16231  13prm  16232  17prm  16233  19prm  16234  prmlem2  16236  37prm  16237  139prm  16240  163prm  16241  317prm  16242  631prm  16243  1259lem1  16247  1259lem2  16248  1259lem3  16249  1259lem4  16250  1259lem5  16251  1259prm  16252  2503lem1  16253  2503lem2  16254  2503lem3  16255  2503prm  16256  4001lem1  16257  4001lem2  16258  4001lem3  16259  4001lem4  16260  4001prm  16261  ressco  16476  slotsbhcdif  16477  quart1cl  25043  quart1lem  25044  quart1  25045  log2ublem1  25136  log2ublem3  25138  log2ub  25139  log2le1  25140  birthday  25144  ppiublem2  25391  bpos1  25471  bposlem8  25479  ex-fac  27900  threehalves  30199  zlmds  30614  hgt750lemd  31336  hgt750lem2  31340  hgt750leme  31346  kur14lem8  31802  sqn5i  38161  235t711  38167  ex-decpmul  38168  inductionexd  39423  fmtno3  42498  fmtno4  42499  fmtno5lem1  42500  fmtno5lem2  42501  fmtno5lem3  42502  fmtno5lem4  42503  fmtno5  42504  257prm  42508  fmtno4prmfac  42519  fmtno4prmfac193  42520  fmtno4nprmfac193  42521  fmtno5faclem3  42528  flsqrt5  42544  139prmALT  42546  31prm  42547  127prm  42550  2exp11  42552  41prothprmlem2  42570  linevalexample  43213