Theorem 3nn0 12546

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

This proof depends on syntax axioms:   ∈ wcel 2145  3c3 12320  ℕ₀cn0 12528

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12258  df-2 12327  df-3 12328  df-n0 12529

This theorem is used by:  7p4e11  12817  7p7e14  12820  8p4e12  12823  8p6e14  12825  9p4e13  12830  9p5e14  12831  4t4e16  12840  5t4e20  12843  6t4e24  12847  6t6e36  12849  7t4e28  12852  7t6e42  12854  8t4e32  12858  8t5e40  12859  9t4e36  12865  9t5e45  12866  9t7e63  12868  9t8e72  12869  3lt10  12879  fz0to3un2pr  13684  4fvwrd4  13703  fldiv4p1lem1div2  13896  expnass  14272  binom3  14288  fac4  14345  4bc2eq6  14393  hash3tr  14556  tpf1o  14566  s3rex  15021  bpoly3  16144  bpoly4  16145  fsumcube  16146  ef4p  16201  efi4p  16225  resin4p  16226  recos4p  16227  ef01bndlem  16272  sin01bnd  16273  sin01gt0  16278  2exp5  17177  2exp6  17178  2exp8  17180  2exp11  17181  2exp16  17182  3exp3  17183  7prm  17202  11prm  17207  13prm  17208  17prm  17209  23prm  17211  prmlem2  17212  37prm  17213  43prm  17214  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem1  17229  2503lem2  17230  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  4001prm  17237  dsndxnmulrndx  17476  basendxltunifndx  17483  unifndxntsetndx  17485  slotsdifunifndx  17486  tangtx  26743  1cubrlem  27078  dcubic1lem  27080  dcubic2  27081  dcubic1  27082  dcubic  27083  mcubic  27084  cubic2  27085  cubic  27086  binom4  27087  dquartlem2  27089  quart1cl  27091  quart1lem  27092  quart1  27093  quartlem1  27094  quartlem2  27095  quart  27098  log2ublem1  27183  log2ublem3  27185  log2ub  27186  log2le1  27187  birthday  27191  ppiublem2  27439  bclbnd  27516  bpos1  27519  bposlem8  27527  gausslemma2dlem4  27605  2lgslem3b  27633  2lgslem3d  27635  pntlemd  27830  pntlema  27832  pntlemb  27833  pntlemf  27841  pntlemo  27843  pntlem3  27845  tgcgr4  28873  iscgra  29195  isinag  29236  isleag  29245  elcgrabasi  29254  iseqlg  29291  usgrexmplef  29719  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  konigsbergiedgw  30728  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  konigsberglem4  30735  ex-prmo  30939  threehalves  33360  evl1deg2  33987  evl1deg3  33988  ply1dg3rt0irred  33994  iconstr  34276  2sqr3minply  34290  2sqr3nconstr  34291  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminplylem4  34295  cos9thpiminplylem5  34296  cos9thpiminplylem6  34297  cos9thpiminply  34298  cos9thpinconstrlem2  34300  circlemethhgt  35151  hgt750lemd  35156  hgt750lem  35159  hgt750lem2  35160  hgt750lemb  35164  hgt750lema  35165  hgt750leme  35166  tgoldbachgtde  35168  tgoldbachgtda  35169  tgoldbachgt  35171  cusgracyclt3v  35735  kur14lem8  35792  3exp7  42919  3lexlogpow5ineq1  42920  3lexlogpow2ineq1  42924  3lexlogpow5ineq5  42926  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  25or6to4  43072  235t711  43180  ex-decpmul  43181  nicomachus  43187  3cubeslem3l  43531  3cubeslem3r  43532  3cubeslem4  43534  3cubes  43535  jm2.23  43837  jm2.20nn  43838  rmydioph  43855  rmxdioph  43857  expdiophlem2  43863  expdioph  43864  resqrtvalex  44485  amgm3d  45039  lhe4.4ex1a  45153  sin3t  47735  cos3t  47736  sin5tlem1  47737  sin5tlem2  47738  sin5tlem3  47739  sin5tlem4  47740  sin5tlem5  47741  goldpolyfactor  47745  goldratmolem2  47751  goldratmolem3  47752  8mod5e3  48254  modm2nep1  48260  modm1nep2  48262  fmtno3  48454  fmtno4  48455  fmtno5lem1  48456  fmtno5lem2  48457  fmtno5lem3  48458  fmtno5lem4  48459  fmtno5  48460  257prm  48464  fmtnoprmfac2lem1  48469  fmtno4prmfac  48475  fmtno4prmfac193  48476  fmtno4nprmfac193  48477  fmtno5faclem2  48483  139prmALT  48499  31prm  48500  m5prm  48501  127prm  48502  m11nprm  48504  mod42tp1mod8  48505  ppivalnn4  48530  11t31e341  48648  2exp340mod341  48649  341fppr2  48650  8exp8mod9  48652  nfermltl2rev  48659  tgoldbachlt  48732  tgoldbach  48733  grtriprop  48857  grtriclwlk3  48861  cycl3grtri  48863  usgrexmpl1lem  48937  usgrexmpl2lem  48942  usgrexmpl2nb2  48949  gpg5gricstgr3  49006  gpg5grlim  49009  gpg5grlic  49010  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem10  49020  gpg5edgnedg  49046  zlmodzxzldeplem1  49430  itcoval3  49595  ackval3  49613  ackval0012  49619  ackval1012  49620  ackval2012  49621  ackval3012  49622  ackval40  49623  ackval41a  49624  ackval41  49625  ackval42  49626