Theorem 3nn0 12436

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

Syntax hints:   ∈ wcel 2109  3c3 12218  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419

This theorem is referenced by:  7p4e11  12701  7p7e14  12704  8p4e12  12707  8p6e14  12709  9p4e13  12714  9p5e14  12715  4t4e16  12724  5t4e20  12727  6t4e24  12731  6t6e36  12733  7t4e28  12736  7t6e42  12738  8t4e32  12742  8t5e40  12743  9t4e36  12749  9t5e45  12750  9t7e63  12752  9t8e72  12753  fz0to3un2pr  13566  4fvwrd4  13585  fldiv4p1lem1div2  13773  expnass  14149  binom3  14165  fac4  14222  4bc2eq6  14270  hash3tr  14432  tpf1o  14442  bpoly3  16000  bpoly4  16001  fsumcube  16002  ef4p  16057  efi4p  16081  resin4p  16082  recos4p  16083  ef01bndlem  16128  sin01bnd  16129  sin01gt0  16134  2exp5  17032  2exp6  17033  2exp8  17035  2exp11  17036  2exp16  17037  3exp3  17038  7prm  17057  11prm  17061  13prm  17062  17prm  17063  23prm  17065  prmlem2  17066  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  dsndxnmulrndx  17330  basendxltunifndx  17337  unifndxntsetndx  17339  slotsdifunifndx  17340  tangtx  26390  1cubrlem  26727  dcubic1lem  26729  dcubic2  26730  dcubic1  26731  dcubic  26732  mcubic  26733  cubic2  26734  cubic  26735  binom4  26736  dquartlem2  26738  quart1cl  26740  quart1lem  26741  quart1  26742  quartlem1  26743  quartlem2  26744  quart  26747  log2ublem1  26832  log2ublem3  26834  log2ub  26835  log2le1  26836  birthday  26840  ppiublem2  27090  bclbnd  27167  bpos1  27170  bposlem8  27178  gausslemma2dlem4  27256  2lgslem3b  27284  2lgslem3d  27286  pntlemd  27481  pntlema  27483  pntlemb  27484  pntlemf  27492  pntlemo  27494  pntlem3  27496  tgcgr4  28434  iscgra  28712  isinag  28741  isleag  28750  iseqlg  28770  usgrexmplef  29162  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  konigsbergiedgw  30150  konigsberglem1  30154  konigsberglem2  30155  konigsberglem3  30156  konigsberglem4  30157  ex-prmo  30361  threehalves  32808  evl1deg2  33519  evl1deg3  33520  ply1dg3rt0irred  33524  iconstr  33729  2sqr3minply  33743  2sqr3nconstr  33744  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminplylem4  33748  cos9thpiminplylem5  33749  cos9thpiminplylem6  33750  cos9thpiminply  33751  cos9thpinconstrlem2  33753  circlemethhgt  34607  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  hgt750lemb  34620  hgt750lema  34621  hgt750leme  34622  tgoldbachgtde  34624  tgoldbachgtda  34625  tgoldbachgt  34627  cusgracyclt3v  35116  kur14lem8  35173  3exp7  42014  3lexlogpow5ineq1  42015  3lexlogpow2ineq1  42019  3lexlogpow5ineq5  42021  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  235t711  42266  ex-decpmul  42267  nicomachus  42273  3cubeslem3l  42647  3cubeslem3r  42648  3cubeslem4  42650  3cubes  42651  jm2.23  42958  jm2.20nn  42959  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  expdioph  42985  resqrtvalex  43607  amgm3d  44161  lhe4.4ex1a  44291  8mod5e3  47334  modm2nep1  47340  modm1nep2  47342  fmtno3  47525  fmtno4  47526  fmtno5lem1  47527  fmtno5lem2  47528  fmtno5lem3  47529  fmtno5lem4  47530  fmtno5  47531  257prm  47535  fmtnoprmfac2lem1  47540  fmtno4prmfac  47546  fmtno4prmfac193  47547  fmtno4nprmfac193  47548  fmtno5faclem2  47554  139prmALT  47570  31prm  47571  m5prm  47572  127prm  47573  m11nprm  47575  mod42tp1mod8  47576  11t31e341  47706  2exp340mod341  47707  341fppr2  47708  8exp8mod9  47710  nfermltl2rev  47717  tgoldbachlt  47790  tgoldbach  47791  grtriprop  47913  grtriclwlk3  47917  cycl3grtri  47919  usgrexmpl1lem  47985  usgrexmpl2lem  47990  usgrexmpl2nb2  47997  gpg5gricstgr3  48054  gpg5grlic  48057  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem10  48067  zlmodzxzldeplem1  48462  itcoval3  48627  ackval3  48645  ackval0012  48651  ackval1012  48652  ackval2012  48653  ackval3012  48654  ackval40  48655  ackval41a  48656  ackval41  48657  ackval42  48658