Theorem 3nn0 12664

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

This proof depends on syntax axioms:   ∈ wcel 2147  3c3 12438  ℕ₀cn0 12646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376  df-2 12445  df-3 12446  df-n0 12647

This theorem is used by:  7p4e11  12935  7p7e14  12938  8p4e12  12941  8p6e14  12943  9p4e13  12948  9p5e14  12949  4t4e16  12958  5t4e20  12961  6t4e24  12965  6t6e36  12967  7t4e28  12970  7t6e42  12972  8t4e32  12976  8t5e40  12977  9t4e36  12983  9t5e45  12984  9t7e63  12986  9t8e72  12987  3lt10  12997  fz0to3un2pr  13803  4fvwrd4  13822  fldiv4p1lem1div2  14015  expnass  14392  binom3  14409  fac4  14466  4bc2eq6  14514  hash3tr  14677  tpf1o  14687  s3rex  15144  bpoly3  16268  bpoly4  16269  fsumcube  16270  ef4p  16325  efi4p  16349  resin4p  16350  recos4p  16351  ef01bndlem  16396  sin01bnd  16397  sin01gt0  16402  2exp5  17307  2exp6  17308  2exp8  17310  2exp11  17311  2exp16  17312  3exp3  17313  7prm  17332  11prm  17337  13prm  17338  17prm  17339  23prm  17341  prmlem2  17342  37prm  17343  43prm  17344  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  dsndxnmulrndx  17608  basendxltunifndx  17615  unifndxntsetndx  17617  slotsdifunifndx  17618  cnfldfunALT  21745  tangtx  26891  1cubrlem  27226  dcubic1lem  27228  dcubic2  27229  dcubic1  27230  dcubic  27231  mcubic  27232  cubic2  27233  cubic  27234  binom4  27235  dquartlem2  27237  quart1cl  27239  quart1lem  27240  quart1  27241  quartlem1  27242  quartlem2  27243  quart  27246  log2ublem1  27331  log2ublem3  27333  log2ub  27334  log2le1  27335  birthday  27339  ppiublem2  27587  bclbnd  27664  bpos1  27667  bposlem8  27675  gausslemma2dlem4  27753  2lgslem3b  27781  2lgslem3d  27783  pntlemd  27978  pntlema  27980  pntlemb  27981  pntlemf  27989  pntlemo  27991  pntlem3  27993  tgcgr4  29051  iscgra  29373  isinag  29414  isleag  29423  elcgrabasi  29432  iseqlg  29469  usgrexmplef  29897  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  konigsbergiedgw  30906  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  konigsberglem4  30913  ex-prmo  31117  threehalves  33577  evl1deg2  34212  evl1deg3  34213  ply1dg3rt0irred  34219  iconstr  34509  2sqr3minply  34523  2sqr3nconstr  34524  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminplylem4  34528  cos9thpiminplylem5  34529  cos9thpiminplylem6  34530  cos9thpiminply  34531  cos9thpinconstrlem2  34533  circlemethhgt  35383  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  hgt750lemb  35396  hgt750lema  35397  hgt750leme  35398  tgoldbachgtde  35400  tgoldbachgtda  35401  tgoldbachgt  35403  cusgracyclt3v  36119  kur14lem8  36186  3exp7  43369  3lexlogpow5ineq1  43370  3lexlogpow2ineq1  43374  3lexlogpow5ineq5  43376  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  25or6to4  43522  235t711  43628  ex-decpmul  43629  nicomachus  43635  3cubeslem3l  43962  3cubeslem3r  43963  3cubeslem4  43965  3cubes  43966  jm2.23  44269  jm2.20nn  44270  rmydioph  44287  rmxdioph  44289  expdiophlem2  44295  expdioph  44296  resqrtvalex  44906  amgm3d  45460  lhe4.4ex1a  45574  sin3t  48190  cos3t  48191  sin5tlem1  48192  sin5tlem2  48193  sin5tlem3  48194  sin5tlem4  48195  sin5tlem5  48196  goldpolyfactor  48200  goldratmolem2  48206  goldratmolem3  48207  8mod5e3  48709  modm2nep1  48715  modm1nep2  48717  fmtno3  48909  fmtno4  48910  fmtno5lem1  48911  fmtno5lem2  48912  fmtno5lem3  48913  fmtno5lem4  48914  fmtno5  48915  257prm  48919  fmtnoprmfac2lem1  48924  fmtno4prmfac  48930  fmtno4prmfac193  48931  fmtno4nprmfac193  48932  fmtno5faclem2  48938  139prmALT  48954  31prm  48955  m5prm  48956  127prm  48957  m11nprm  48959  mod42tp1mod8  48960  ppivalnn4  48985  11t31e341  49103  2exp340mod341  49104  341fppr2  49105  8exp8mod9  49107  nfermltl2rev  49114  tgoldbachlt  49187  tgoldbach  49188  grtriprop  49312  grtriclwlk3  49316  cycl3grtri  49318  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb2  49404  gpg5gricstgr3  49461  gpg5grlim  49464  gpg5grlic  49465  gpgprismgr4cycllem7  49472  gpgprismgr4cycllem10  49475  gpg5edgnedg  49501  zlmodzxzldeplem1  49943  itcoval3  50108  ackval3  50126  ackval0012  50132  ackval1012  50133  ackval2012  50134  ackval3012  50135  ackval40  50136  ackval41a  50137  ackval41  50138  ackval42  50139