Theorem 4nn0 11523

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 11399	. 2 ⊢ 4 ∈ ℕ
2	1	nnnn0i 11512	1 ⊢ 4 ∈ ℕ0

Syntax hints:   ∈ wcel 2139  4c4 11284  ℕ₀cn0 11504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-1cn 10206

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-n0 11505

This theorem is referenced by:  6p5e11  11812  6p5e11OLD  11813  7p5e12  11819  8p5e13  11827  8p7e15  11829  9p5e14  11835  9p6e15  11836  4t3e12  11844  4t4e16  11845  5t5e25  11851  5t5e25OLD  11852  6t4e24  11855  6t5e30  11856  6t5e30OLD  11857  7t3e21  11861  7t5e35  11863  7t7e49  11865  8t3e24  11867  8t4e32  11868  8t5e40  11869  8t5e40OLD  11870  8t6e48  11871  8t6e48OLD  11872  8t7e56  11873  8t8e64  11874  9t5e45  11878  9t6e54  11879  9t7e63  11880  decbin3  11896  fzo0to42pr  12769  4bc3eq4  13329  bpoly4  15009  fsumcube  15010  resin4p  15087  recos4p  15088  ef01bndlem  15133  sin01bnd  15134  cos01bnd  15135  prm23lt5  15741  decexp2  16001  2exp8  16018  2exp16  16019  2expltfac  16021  13prm  16045  19prm  16047  prmlem2  16049  37prm  16050  43prm  16051  83prm  16052  139prm  16053  163prm  16054  317prm  16055  631prm  16056  1259lem1  16060  1259lem2  16061  1259lem3  16062  1259lem4  16063  1259lem5  16064  1259prm  16065  2503lem1  16066  2503lem2  16067  2503lem3  16068  2503prm  16069  4001lem1  16070  4001lem2  16071  4001lem3  16072  4001lem4  16073  4001prm  16074  resshom  16300  slotsbhcdif  16302  prdsvalstr  16335  oppchomfval  16595  oppcbas  16599  rescbas  16710  rescco  16713  rescabs  16714  catstr  16838  lt6abl  18516  cnfldfun  19980  binom4  24797  dquart  24800  quart1cl  24801  quart1lem  24802  quart1  24803  log2ublem3  24895  log2ub  24896  ppiublem2  25148  bclbnd  25225  bpos1  25228  bposlem8  25236  bposlem9  25237  bpos  25238  2lgslem3a  25341  2lgslem3b  25342  2lgslem3c  25343  2lgslem3d  25344  usgrexmplef  26371  upgr4cycl4dv4e  27358  ex-exp  27639  ex-fac  27640  ex-bc  27641  ex-ind-dvds  27650  hgt750lemd  31056  hgt750lem  31059  hgt750lem2  31060  hgt750leme  31066  tgoldbachgtde  31068  kur14lem9  31524  rmxdioph  38103  inductionexd  38973  amgm4d  39023  wallispi2lem1  40809  wallispi2lem2  40810  wallispi2  40811  stirlinglem3  40814  stirlinglem8  40819  stirlinglem15  40826  smfmullem2  41523  fmtno4  41992  fmtno5lem4  41996  fmtno5  41997  257prm  42001  fmtno4prmfac  42012  fmtno4prmfac193  42013  fmtno4nprmfac193  42014  fmtno4prm  42015  fmtnofz04prm  42017  fmtnole4prm  42018  fmtno5faclem1  42019  fmtno5faclem2  42020  fmtno5faclem3  42021  fmtno5fac  42022  fmtno5nprm  42023  139prmALT  42039  2exp7  42042  127prm  42043  2exp11  42045  m11nprm  42046  3exp4mod41  42061  41prothprmlem2  42063