Theorem 5nn0 12498

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

Syntax hints:   ∈ wcel 2104  5c5 12276  ℕ₀cn0 12478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729  ax-1cn 11172

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-n0 12479

This theorem is referenced by:  6p6e12  12757  7p6e13  12761  8p6e14  12767  8p8e16  12769  9p6e15  12774  9p7e16  12775  5t2e10  12783  5t3e15  12784  5t4e20  12785  5t5e25  12786  6t6e36  12791  7t5e35  12795  7t6e42  12796  8t6e48  12802  8t8e64  12804  9t5e45  12808  9t6e54  12809  9t7e63  12810  dec2dvds  17002  dec5dvds2  17004  2exp8  17028  2exp11  17029  2exp16  17030  prmlem1  17047  5prm  17048  7prm  17050  11prm  17054  13prm  17055  17prm  17056  19prm  17057  prmlem2  17059  37prm  17060  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  slotsdnscsi  17343  slotsbhcdif  17366  slotsbhcdifOLD  17367  quart1cl  26593  quart1lem  26594  quart1  26595  log2ublem1  26685  log2ublem3  26687  log2ub  26688  log2le1  26689  birthday  26693  ppiublem2  26940  bpos1  27020  bposlem8  27028  ex-fac  29969  threehalves  32346  zlmdsOLD  33239  hgt750lemd  33956  hgt750lem2  33960  hgt750leme  33966  kur14lem8  34500  420gcd8e4  41179  12lcm5e60  41181  lcmineqlem  41225  3lexlogpow5ineq1  41227  3lexlogpow5ineq2  41228  3lexlogpow5ineq4  41229  3lexlogpow5ineq3  41230  3lexlogpow2ineq2  41232  3lexlogpow5ineq5  41233  aks4d1lem1  41235  aks4d1p1p3  41242  aks4d1p1p2  41243  aks4d1p1p4  41244  aks4d1p1p6  41246  aks4d1p1p7  41247  aks4d1p1p5  41248  aks4d1p1  41249  aks4d1p2  41250  aks4d1p3  41251  aks4d1p5  41253  aks4d1p6  41254  aks4d1p7d1  41255  aks4d1p7  41256  aks4d1p8  41260  sqn5i  41501  235t711  41509  ex-decpmul  41510  sq45  41717  sum9cubes  41718  3cubeslem3l  41728  3cubeslem3r  41729  resqrtvalex  42700  imsqrtvalex  42701  inductionexd  43210  fmtno3  46519  fmtno4  46520  fmtno5lem1  46521  fmtno5lem2  46522  fmtno5lem3  46523  fmtno5lem4  46524  fmtno5  46525  257prm  46529  fmtno4prmfac  46540  fmtno4prmfac193  46541  fmtno4nprmfac193  46542  fmtno5faclem3  46549  flsqrt5  46562  139prmALT  46564  31prm  46565  127prm  46567  41prothprmlem2  46586  2exp340mod341  46701  linevalexample  47165  ackval2012  47466  ackval3012  47467  ackval41  47470