Theorem 3nn0 12073

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 11874	. 2 ⊢ 3 ∈ ℕ
2	1	nnnn0i 12063	1 ⊢ 3 ∈ ℕ0

Syntax hints:   ∈ wcel 2112  3c3 11851  ℕ₀cn0 12055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501  ax-1cn 10752

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-nn 11796  df-2 11858  df-3 11859  df-n0 12056

This theorem is referenced by:  7p4e11  12334  7p7e14  12337  8p4e12  12340  8p6e14  12342  9p4e13  12347  9p5e14  12348  4t4e16  12357  5t4e20  12360  6t4e24  12364  6t6e36  12366  7t4e28  12369  7t6e42  12371  8t4e32  12375  8t5e40  12376  9t4e36  12382  9t5e45  12383  9t7e63  12385  9t8e72  12386  fz0to3un2pr  13179  4fvwrd4  13197  fldiv4p1lem1div2  13375  expnass  13741  binom3  13756  fac4  13812  4bc2eq6  13860  hash3tr  14021  bpoly3  15583  bpoly4  15584  fsumcube  15585  ef4p  15637  efi4p  15661  resin4p  15662  recos4p  15663  ef01bndlem  15708  sin01bnd  15709  sin01gt0  15714  2exp5  16602  2exp6  16603  2exp8  16605  2exp11  16606  2exp16  16607  3exp3  16608  7prm  16627  11prm  16631  13prm  16632  17prm  16633  23prm  16635  prmlem2  16636  37prm  16637  43prm  16638  83prm  16639  139prm  16640  163prm  16641  317prm  16642  631prm  16643  1259lem1  16647  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  1259prm  16652  2503lem1  16653  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001lem3  16659  4001lem4  16660  4001prm  16661  ressunif  16863  cnfldfun  20329  tuslem  23118  tangtx  25349  1cubrlem  25678  dcubic1lem  25680  dcubic2  25681  dcubic1  25682  dcubic  25683  mcubic  25684  cubic2  25685  cubic  25686  binom4  25687  dquartlem2  25689  quart1cl  25691  quart1lem  25692  quart1  25693  quartlem1  25694  quartlem2  25695  quart  25698  log2ublem1  25783  log2ublem3  25785  log2ub  25786  log2le1  25787  birthday  25791  ppiublem2  26038  bclbnd  26115  bpos1  26118  bposlem8  26126  gausslemma2dlem4  26204  2lgslem3b  26232  2lgslem3d  26234  pntlemd  26429  pntlema  26431  pntlemb  26432  pntlemf  26440  pntlemo  26442  pntlem3  26444  tgcgr4  26576  iscgra  26854  isinag  26883  isleag  26892  iseqlg  26912  usgrexmplef  27301  upgr3v3e3cycl  28217  upgr4cycl4dv4e  28222  konigsbergiedgw  28285  konigsberglem1  28289  konigsberglem2  28290  konigsberglem3  28291  konigsberglem4  28292  ex-prmo  28496  threehalves  30863  circlemethhgt  32289  hgt750lemd  32294  hgt750lem  32297  hgt750lem2  32298  hgt750lemb  32302  hgt750lema  32303  hgt750leme  32304  tgoldbachgtde  32306  tgoldbachgtda  32307  tgoldbachgt  32309  cusgracyclt3v  32785  kur14lem8  32842  3exp7  39744  3lexlogpow5ineq1  39745  3lexlogpow2ineq1  39749  3lexlogpow5ineq5  39751  aks4d1p1p7  39764  aks4d1p1p5  39765  aks4d1p1  39766  235t711  39967  ex-decpmul  39968  3cubeslem3l  40152  3cubeslem3r  40153  3cubeslem4  40155  3cubes  40156  jm2.23  40462  jm2.20nn  40463  rmydioph  40480  rmxdioph  40482  expdiophlem2  40488  expdioph  40489  resqrtvalex  40870  amgm3d  41429  lhe4.4ex1a  41561  fmtno3  44619  fmtno4  44620  fmtno5lem1  44621  fmtno5lem2  44622  fmtno5lem3  44623  fmtno5lem4  44624  fmtno5  44625  257prm  44629  fmtnoprmfac2lem1  44634  fmtno4prmfac  44640  fmtno4prmfac193  44641  fmtno4nprmfac193  44642  fmtno5faclem2  44648  139prmALT  44664  31prm  44665  m5prm  44666  127prm  44667  m11nprm  44669  mod42tp1mod8  44670  11t31e341  44800  2exp340mod341  44801  341fppr2  44802  8exp8mod9  44804  nfermltl2rev  44811  tgoldbachlt  44884  tgoldbach  44885  zlmodzxzldeplem1  45457  itcoval3  45627  ackval3  45645  ackval0012  45651  ackval1012  45652  ackval2012  45653  ackval3012  45654  ackval40  45655  ackval41a  45656  ackval41  45657  ackval42  45658