Theorem 3nn0 11523

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

Assertion

Ref	Expression
3nn0	⊢ 3 ∈ ℕ0

Proof of Theorem 3nn0

Step	Hyp	Ref	Expression
1		3nn 11399	. 2 ⊢ 3 ∈ ℕ
2	1	nnnn0i 11513	1 ⊢ 3 ∈ ℕ0

Syntax hints:   ∈ wcel 2140  3c3 11284  ℕ₀cn0 11505

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 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-1cn 10207

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 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-ov 6818  df-om 7233  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-nn 11234  df-2 11292  df-3 11293  df-n0 11506

This theorem is referenced by:  7p4e11  11818  7p4e11OLD  11819  7p7e14  11822  8p4e12  11827  8p6e14  11829  9p4e13  11835  9p5e14  11836  4t4e16  11846  5t4e20  11850  5t4e20OLD  11851  6t4e24  11856  6t6e36  11859  6t6e36OLD  11860  7t4e28  11863  7t6e42  11865  8t4e32  11869  8t5e40  11870  8t5e40OLD  11871  9t4e36  11878  9t5e45  11879  9t7e63  11881  9t8e72  11882  fz0to3un2pr  12656  4fvwrd4  12674  fldiv4p1lem1div2  12851  expnass  13185  binom3  13200  fac4  13283  4bc2eq6  13331  hash3tr  13485  bpoly3  15009  bpoly4  15010  fsumcube  15011  ef4p  15063  efi4p  15087  resin4p  15088  recos4p  15089  ef01bndlem  15134  sin01bnd  15135  sin01gt0  15140  2exp6  16018  2exp8  16019  2exp16  16020  3exp3  16021  7prm  16040  11prm  16045  13prm  16046  17prm  16047  23prm  16049  prmlem2  16050  37prm  16051  43prm  16052  83prm  16053  139prm  16054  163prm  16055  317prm  16056  631prm  16057  1259lem1  16061  1259lem2  16062  1259lem3  16063  1259lem4  16064  1259lem5  16065  1259prm  16066  2503lem1  16067  2503lem2  16068  2503lem3  16069  2503prm  16070  4001lem1  16071  4001lem2  16072  4001lem3  16073  4001lem4  16074  4001prm  16075  cnfldfun  19981  ressunif  22288  tuslem  22293  tangtx  24478  1cubrlem  24789  dcubic1lem  24791  dcubic2  24792  dcubic1  24793  dcubic  24794  mcubic  24795  cubic2  24796  cubic  24797  binom4  24798  dquartlem2  24800  quart1cl  24802  quart1lem  24803  quart1  24804  quartlem1  24805  quartlem2  24806  quart  24809  log2ublem1  24894  log2ublem3  24896  log2ub  24897  log2le1  24898  birthday  24902  ppiublem2  25149  bclbnd  25226  bpos1  25229  bposlem8  25237  gausslemma2dlem4  25315  2lgslem3b  25343  2lgslem3d  25345  pntlemd  25504  pntlema  25506  pntlemb  25507  pntlemf  25515  pntlemo  25517  pntlem3  25519  tgcgr4  25647  iscgra  25922  isinag  25950  isleag  25954  iseqlg  25968  usgrexmplef  26372  upgr3v3e3cycl  27354  upgr4cycl4dv4e  27359  konigsbergiedgw  27422  konigsberglem1  27426  konigsberglem2  27427  konigsberglem3  27428  konigsberglem4  27429  ex-prmo  27649  threehalves  29954  circlemethhgt  31052  hgt750lemd  31057  hgt750lem  31060  hgt750lem2  31061  hgt750lemb  31065  hgt750lema  31066  hgt750leme  31067  tgoldbachgtde  31069  tgoldbachgtda  31070  tgoldbachgt  31072  kur14lem8  31524  jm2.23  38084  jm2.20nn  38085  rmydioph  38102  rmxdioph  38104  expdiophlem2  38110  expdioph  38111  amgm3d  39023  lhe4.4ex1a  39049  fmtno3  41992  fmtno4  41993  fmtno5lem1  41994  fmtno5lem2  41995  fmtno5lem3  41996  fmtno5lem4  41997  fmtno5  41998  257prm  42002  fmtnoprmfac2lem1  42007  fmtno4prmfac  42013  fmtno4prmfac193  42014  fmtno4nprmfac193  42015  fmtno5faclem2  42021  2exp5  42036  139prmALT  42040  31prm  42041  m5prm  42042  127prm  42044  2exp11  42046  m11nprm  42047  mod42tp1mod8  42048  tgoldbachlt  42233  tgoldbach  42234  tgoldbachltOLD  42239  tgoldbachOLD  42241  zlmodzxzldeplem1  42818