MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4nn0 Structured version   Unicode version

Theorem 4nn0 10586
Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
Assertion
Ref Expression
4nn0  |-  4  e.  NN0

Proof of Theorem 4nn0
StepHypRef Expression
1 4nn 10469 . 2  |-  4  e.  NN
21nnnn0i 10575 1  |-  4  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   4c4 10361   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-1cn 9328
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-n0 10568
This theorem is referenced by:  6p5e11  10793  7p5e12  10796  8p5e13  10801  8p7e15  10803  9p5e14  10808  9p6e15  10809  4t3e12  10815  4t4e16  10816  5t5e25  10819  6t4e24  10822  6t5e30  10823  7t3e21  10826  7t5e35  10828  7t7e49  10830  8t3e24  10832  8t4e32  10833  8t5e40  10834  8t6e48  10835  8t7e56  10836  8t8e64  10837  9t5e45  10841  9t6e54  10842  9t7e63  10843  decbin3  10848  fzo0to42pr  11600  resin4p  13405  recos4p  13406  ef01bndlem  13451  sin01bnd  13452  cos01bnd  13453  decexp2  14087  2exp6  14098  2exp8  14099  2exp16  14100  2expltfac  14102  13prm  14126  19prm  14128  prmlem2  14130  37prm  14131  43prm  14132  83prm  14133  139prm  14134  163prm  14135  317prm  14136  631prm  14137  1259lem1  14138  1259lem2  14139  1259lem3  14140  1259lem4  14141  1259lem5  14142  1259prm  14143  2503lem1  14144  2503lem2  14145  2503lem3  14146  2503prm  14147  4001lem1  14148  4001lem2  14149  4001lem3  14150  4001lem4  14151  4001prm  14152  resshom  14340  prdsvalstr  14374  oppchomfval  14636  oppcbas  14640  rescbas  14725  rescco  14728  rescabs  14729  catstr  14850  lt6abl  16351  binom4  22130  dquart  22133  quart1cl  22134  quart1lem  22135  quart1  22136  log2ublem3  22228  log2ub  22229  ppiublem2  22427  bclbnd  22504  bpos1  22507  bposlem8  22515  bposlem9  22516  bpos  22517  usgraex0elv  23137  usgraex1elv  23138  usgraex2elv  23139  usgraex3elv  23140  4cycl4v4e  23375  4cycl4dv4e  23377  kur14lem9  26950  4bc3eq4  27237  bpoly4  28049  fsumcube  28050  rmxdioph  29210  wallispi2lem1  29712  wallispi2lem2  29713  wallispi2  29714  stirlinglem3  29717  stirlinglem8  29722  stirlinglem15  29729
  Copyright terms: Public domain W3C validator