Theorem 3nn0 11662

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

Syntax hints:   ∈ wcel 2107  3c3 11431  ℕ₀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-n0 11643

This theorem is referenced by:  7p4e11  11923  7p7e14  11926  8p4e12  11929  8p6e14  11931  9p4e13  11936  9p5e14  11937  4t4e16  11946  5t4e20  11949  6t4e24  11953  6t6e36  11955  7t4e28  11958  7t6e42  11960  8t4e32  11964  8t5e40  11965  9t4e36  11971  9t5e45  11972  9t7e63  11974  9t8e72  11975  fz0to3un2pr  12760  4fvwrd4  12778  fldiv4p1lem1div2  12955  expnass  13289  binom3  13304  fac4  13386  4bc2eq6  13434  hash3tr  13586  bpoly3  15191  bpoly4  15192  fsumcube  15193  ef4p  15245  efi4p  15269  resin4p  15270  recos4p  15271  ef01bndlem  15316  sin01bnd  15317  sin01gt0  15322  2exp6  16194  2exp8  16195  2exp16  16196  3exp3  16197  7prm  16216  11prm  16220  13prm  16221  17prm  16222  23prm  16224  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  cnfldfun  20154  ressunif  22474  tuslem  22479  tangtx  24695  1cubrlem  25019  dcubic1lem  25021  dcubic2  25022  dcubic1  25023  dcubic  25024  mcubic  25025  cubic2  25026  cubic  25027  binom4  25028  dquartlem2  25030  quart1cl  25032  quart1lem  25033  quart1  25034  quartlem1  25035  quartlem2  25036  quart  25039  log2ublem1  25125  log2ublem3  25127  log2ub  25128  log2le1  25129  birthday  25133  ppiublem2  25380  bclbnd  25457  bpos1  25460  bposlem8  25468  gausslemma2dlem4  25546  2lgslem3b  25574  2lgslem3d  25576  pntlemd  25735  pntlema  25737  pntlemb  25738  pntlemf  25746  pntlemo  25748  pntlem3  25750  tgcgr4  25882  iscgra  26157  isinag  26187  isleag  26196  iseqlg  26216  usgrexmplef  26606  upgr3v3e3cycl  27583  upgr4cycl4dv4e  27588  konigsbergiedgw  27654  konigsberglem1  27658  konigsberglem2  27659  konigsberglem3  27660  konigsberglem4  27661  ex-prmo  27891  threehalves  30185  circlemethhgt  31323  hgt750lemd  31328  hgt750lem  31331  hgt750lem2  31332  hgt750lemb  31336  hgt750lema  31337  hgt750leme  31338  tgoldbachgtde  31340  tgoldbachgtda  31341  tgoldbachgt  31343  kur14lem8  31794  235t711  38159  ex-decpmul  38160  jm2.23  38526  jm2.20nn  38527  rmydioph  38544  rmxdioph  38546  expdiophlem2  38552  expdioph  38553  amgm3d  39462  lhe4.4ex1a  39488  fmtno3  42488  fmtno4  42489  fmtno5lem1  42490  fmtno5lem2  42491  fmtno5lem3  42492  fmtno5lem4  42493  fmtno5  42494  257prm  42498  fmtnoprmfac2lem1  42503  fmtno4prmfac  42509  fmtno4prmfac193  42510  fmtno4nprmfac193  42511  fmtno5faclem2  42517  2exp5  42532  139prmALT  42536  31prm  42537  m5prm  42538  127prm  42540  2exp11  42542  m11nprm  42543  mod42tp1mod8  42544  tgoldbachlt  42733  tgoldbach  42734  zlmodzxzldeplem1  43308