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

Theorem 4nn0 10888
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 10769 . 2  |-  4  e.  NN
21nnnn0i 10877 1  |-  4  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   4c4 10661   NN0cn0 10869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-1cn 9597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-n0 10870
This theorem is referenced by:  6p5e11  11101  7p5e12  11104  8p5e13  11109  8p7e15  11111  9p5e14  11116  9p6e15  11117  4t3e12  11123  4t4e16  11124  5t5e25  11127  6t4e24  11130  6t5e30  11131  7t3e21  11134  7t5e35  11136  7t7e49  11138  8t3e24  11140  8t4e32  11141  8t5e40  11142  8t6e48  11143  8t7e56  11144  8t8e64  11145  9t5e45  11149  9t6e54  11150  9t7e63  11151  decbin3  11156  fzo0to42pr  11999  4bc3eq4  12512  bpoly4  14099  fsumcube  14100  resin4p  14179  recos4p  14180  ef01bndlem  14225  sin01bnd  14226  cos01bnd  14227  decexp2  15034  2exp6OLD  15046  2exp8  15047  2exp16  15048  2expltfac  15050  13prm  15074  19prm  15076  prmlem2  15078  37prm  15079  43prm  15080  83prm  15081  139prm  15082  163prm  15083  317prm  15084  631prm  15085  1259lem1  15089  1259lem2  15090  1259lem3  15091  1259lem4  15092  1259lem5  15093  1259prm  15094  2503lem1  15095  2503lem2  15096  2503lem3  15097  2503prm  15098  4001lem1  15099  4001lem2  15100  4001lem3  15101  4001lem4  15102  4001prm  15103  resshom  15303  slotsbhcdif  15305  prdsvalstr  15338  oppchomfval  15606  oppcbas  15610  rescbas  15721  rescco  15724  rescabs  15725  catstr  15849  lt6abl  17516  binom4  23762  dquart  23765  quart1cl  23766  quart1lem  23767  quart1  23768  log2ublem3  23860  log2ub  23861  ppiublem2  24117  bclbnd  24194  bpos1  24197  bposlem8  24205  bposlem9  24206  bpos  24207  usgraex0elv  25109  usgraex1elv  25110  usgraex2elv  25111  usgraex3elv  25112  ex-ind-dvds  25884  kur14lem9  29932  rmxdioph  35790  inductionexd  36450  amgm4d  36509  wallispi2lem1  37752  wallispi2lem2  37753  wallispi2  37754  stirlinglem3  37757  stirlinglem8  37762  stirlinglem15  37769  3exp4mod41  38627  41prothprmlem2  38629
  Copyright terms: Public domain W3C validator