Theorem 5nn0 12529

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 12334	. 2 ⊢ 5 ∈ ℕ
2	1	nnnn0i 12517	1 ⊢ 5 ∈ ℕ0

Syntax hints:   ∈ wcel 2107  5c5 12306  ℕ₀cn0 12509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-1cn 11195

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-n0 12510

This theorem is referenced by:  6p6e12  12790  7p6e13  12794  8p6e14  12800  8p8e16  12802  9p6e15  12807  9p7e16  12808  5t2e10  12816  5t3e15  12817  5t4e20  12818  5t5e25  12819  6t6e36  12824  7t5e35  12828  7t6e42  12829  8t6e48  12835  8t8e64  12837  9t5e45  12841  9t6e54  12842  9t7e63  12843  fz0to5un2tp  13653  dec2dvds  17084  dec5dvds2  17086  2exp8  17109  2exp11  17110  2exp16  17111  prmlem1  17128  5prm  17129  7prm  17131  11prm  17135  13prm  17136  17prm  17137  19prm  17138  prmlem2  17140  37prm  17141  139prm  17144  163prm  17145  317prm  17146  631prm  17147  1259lem1  17151  1259lem2  17152  1259lem3  17153  1259lem4  17154  1259lem5  17155  1259prm  17156  2503lem1  17157  2503lem2  17158  2503lem3  17159  2503prm  17160  4001lem1  17161  4001lem2  17162  4001lem3  17163  4001lem4  17164  4001prm  17165  slotsdnscsi  17409  slotsbhcdif  17432  quart1cl  26834  quart1lem  26835  quart1  26836  log2ublem1  26926  log2ublem3  26928  log2ub  26929  log2le1  26930  birthday  26934  ppiublem2  27184  bpos1  27264  bposlem8  27272  ex-fac  30399  threehalves  32842  zlmdsOLD  33937  hgt750lemd  34638  hgt750lem2  34642  hgt750leme  34648  kur14lem8  35193  420gcd8e4  41982  12lcm5e60  41984  lcmineqlem  42028  3lexlogpow5ineq1  42030  3lexlogpow5ineq2  42031  3lexlogpow5ineq4  42032  3lexlogpow5ineq3  42033  3lexlogpow2ineq2  42035  3lexlogpow5ineq5  42036  aks4d1lem1  42038  aks4d1p1p3  42045  aks4d1p1p2  42046  aks4d1p1p4  42047  aks4d1p1p6  42049  aks4d1p1p7  42050  aks4d1p1p5  42051  aks4d1p1  42052  aks4d1p2  42053  aks4d1p3  42054  aks4d1p5  42056  aks4d1p6  42057  aks4d1p7d1  42058  aks4d1p7  42059  aks4d1p8  42063  sqn5i  42299  235t711  42318  ex-decpmul  42319  sq45  42660  sum9cubes  42661  3cubeslem3l  42675  3cubeslem3r  42676  resqrtvalex  43635  imsqrtvalex  43636  inductionexd  44145  fmtno3  47511  fmtno4  47512  fmtno5lem1  47513  fmtno5lem2  47514  fmtno5lem3  47515  fmtno5lem4  47516  fmtno5  47517  257prm  47521  fmtno4prmfac  47532  fmtno4prmfac193  47533  fmtno4nprmfac193  47534  fmtno5faclem3  47541  flsqrt5  47554  139prmALT  47556  31prm  47557  127prm  47559  41prothprmlem2  47578  2exp340mod341  47693  usgrexmpl1lem  47953  usgrexmpl2lem  47958  usgrexmpl2nb0  47963  usgrexmpl2nb1  47964  usgrexmpl2nb2  47965  usgrexmpl2nb3  47966  usgrexmpl2trifr  47969  linevalexample  48285  ackval2012  48585  ackval3012  48586  ackval41  48589