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

Theorem 4nn0 10708
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 10591 . 2  |-  4  e.  NN
21nnnn0i 10697 1  |-  4  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   4c4 10483   NN0cn0 10689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-1cn 9450
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-reu 2805  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-om 6586  df-recs 6941  df-rdg 6975  df-nn 10433  df-2 10490  df-3 10491  df-4 10492  df-n0 10690
This theorem is referenced by:  6p5e11  10915  7p5e12  10918  8p5e13  10923  8p7e15  10925  9p5e14  10930  9p6e15  10931  4t3e12  10937  4t4e16  10938  5t5e25  10941  6t4e24  10944  6t5e30  10945  7t3e21  10948  7t5e35  10950  7t7e49  10952  8t3e24  10954  8t4e32  10955  8t5e40  10956  8t6e48  10957  8t7e56  10958  8t8e64  10959  9t5e45  10963  9t6e54  10964  9t7e63  10965  decbin3  10970  fzo0to42pr  11732  resin4p  13539  recos4p  13540  ef01bndlem  13585  sin01bnd  13586  cos01bnd  13587  decexp2  14221  2exp6  14232  2exp8  14233  2exp16  14234  2expltfac  14236  13prm  14260  19prm  14262  prmlem2  14264  37prm  14265  43prm  14266  83prm  14267  139prm  14268  163prm  14269  317prm  14270  631prm  14271  1259lem1  14272  1259lem2  14273  1259lem3  14274  1259lem4  14275  1259lem5  14276  1259prm  14277  2503lem1  14278  2503lem2  14279  2503lem3  14280  2503prm  14281  4001lem1  14282  4001lem2  14283  4001lem3  14284  4001lem4  14285  4001prm  14286  resshom  14475  prdsvalstr  14509  oppchomfval  14771  oppcbas  14775  rescbas  14860  rescco  14863  rescabs  14864  catstr  14985  lt6abl  16491  binom4  22377  dquart  22380  quart1cl  22381  quart1lem  22382  quart1  22383  log2ublem3  22475  log2ub  22476  ppiublem2  22674  bclbnd  22751  bpos1  22754  bposlem8  22762  bposlem9  22763  bpos  22764  usgraex0elv  23465  usgraex1elv  23466  usgraex2elv  23467  usgraex3elv  23468  4cycl4v4e  23703  4cycl4dv4e  23705  kur14lem9  27245  4bc3eq4  27533  bpoly4  28345  fsumcube  28346  rmxdioph  29512  wallispi2lem1  30013  wallispi2lem2  30014  wallispi2  30015  stirlinglem3  30018  stirlinglem8  30023  stirlinglem15  30030
  Copyright terms: Public domain W3C validator