Theorem 4nn0 11663

Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Assertion

Ref	Expression
4nn0	⊢ 4 ∈ ℕ0

Proof of Theorem 4nn0

Step	Hyp	Ref	Expression
1		4nn 11459	. 2 ⊢ 4 ∈ ℕ
2	1	nnnn0i 11651	1 ⊢ 4 ∈ ℕ0

Syntax hints:   ∈ wcel 2107  4c4 11432  ℕ₀cn0 11642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-1cn 10330

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-n0 11643

This theorem is referenced by:  6p5e11  11920  7p5e12  11924  8p5e13  11930  8p7e15  11932  9p5e14  11937  9p6e15  11938  4t3e12  11945  4t4e16  11946  5t5e25  11950  6t4e24  11953  6t5e30  11954  7t3e21  11957  7t5e35  11959  7t7e49  11961  8t3e24  11963  8t4e32  11964  8t5e40  11965  8t6e48  11966  8t7e56  11967  8t8e64  11968  9t5e45  11972  9t6e54  11973  9t7e63  11974  decbin3  11989  fzo0to42pr  12874  4bc3eq4  13433  bpoly4  15192  fsumcube  15193  resin4p  15270  recos4p  15271  ef01bndlem  15316  sin01bnd  15317  cos01bnd  15318  prm23lt5  15923  decexp2  16183  2exp8  16195  2exp16  16196  2expltfac  16198  13prm  16221  19prm  16223  prmlem2  16225  37prm  16226  43prm  16227  83prm  16228  139prm  16229  163prm  16230  317prm  16231  631prm  16232  1259lem1  16236  1259lem2  16237  1259lem3  16238  1259lem4  16239  1259lem5  16240  1259prm  16241  2503lem1  16242  2503lem2  16243  2503lem3  16244  2503prm  16245  4001lem1  16246  4001lem2  16247  4001lem3  16248  4001lem4  16249  4001prm  16250  resshom  16464  slotsbhcdif  16466  prdsvalstr  16499  oppchomfval  16759  oppcbas  16763  rescbas  16874  rescco  16877  rescabs  16878  catstr  17002  lt6abl  18682  cnfldfun  20154  binom4  25028  dquart  25031  quart1cl  25032  quart1lem  25033  quart1  25034  log2ublem3  25127  log2ub  25128  ppiublem2  25380  bclbnd  25457  bpos1  25460  bposlem8  25468  bposlem9  25469  bpos  25470  2lgslem3a  25573  2lgslem3b  25574  2lgslem3c  25575  2lgslem3d  25576  usgrexmplef  26606  upgr4cycl4dv4e  27588  ex-exp  27882  ex-fac  27883  ex-bc  27884  ex-ind-dvds  27893  hgt750lemd  31328  hgt750lem  31331  hgt750lem2  31332  hgt750leme  31338  tgoldbachgtde  31340  kur14lem9  31795  235t711  38159  ex-decpmul  38160  rmxdioph  38546  inductionexd  39413  amgm4d  39463  wallispi2lem1  41219  wallispi2lem2  41220  wallispi2  41221  stirlinglem3  41224  stirlinglem8  41229  stirlinglem15  41236  smfmullem2  41930  fmtno4  42489  fmtno5lem4  42493  fmtno5  42494  257prm  42498  fmtno4prmfac  42509  fmtno4prmfac193  42510  fmtno4nprmfac193  42511  fmtno4prm  42512  fmtnofz04prm  42514  fmtnole4prm  42515  fmtno5faclem1  42516  fmtno5faclem2  42517  fmtno5faclem3  42518  fmtno5fac  42519  fmtno5nprm  42520  139prmALT  42536  2exp7  42539  127prm  42540  2exp11  42542  m11nprm  42543  3exp4mod41  42558  41prothprmlem2  42560