Theorem 2nn0 12663

Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
2nn0	⊢ 2 ∈ ℕ0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 12456	. 2 ⊢ 2 ∈ ℕ
2	1	nnnn0i 12654	1 ⊢ 2 ∈ ℕ0

This proof depends on syntax axioms:   ∈ wcel 2147  2c2 12437  ℕ₀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-n0 12647

This theorem is used by:  nn0n0n1ge2  12714  12nn0  12871  25nn0  12873  7p6e13  12937  8p3e11  12940  8p5e13  12942  9p3e12  12947  9p4e13  12948  4t3e12  12957  4t4e16  12958  5t3e15  12960  5t5e25  12962  6t3e18  12964  6t5e30  12966  7t3e21  12969  7t4e28  12970  7t5e35  12971  7t6e42  12972  7t7e49  12973  8t3e24  12975  8t4e32  12976  8t5e40  12977  9t3e27  12982  9t4e36  12983  9t8e72  12987  9t9e81  12988  2lt10  12998  decbin3  13003  2eluzge0  13048  xnn0le2is012  13416  fzo0to42pr  13928  fvf1tp  13969  nn0sqcl  14272  sqmul  14302  resqcl  14307  zsqcl  14312  cu2  14383  exp4sqsq  14384  i3  14387  i4  14388  binom3  14409  expmulnbnd  14420  nn0opthlem1  14453  fac3  14465  faclbnd2  14476  faclbnd4lem1  14478  faclbnd4lem3  14480  hash2pr  14655  hashtplei  14670  tpf1ofv2  14684  tpfo  14686  s4fv2  15091  pfx2  15141  repsw3  15147  swrd2lsw  15148  2swrd2eqwrdeq  15149  abssq  15516  sqabs  15517  iseraltlem2  15894  iseraltlem3  15895  bpoly2  16267  bpoly3  16268  bpoly4  16269  fsumcube  16270  ef4p  16325  efgt1p2  16326  efi4p  16349  ef01bndlem  16396  cos01bnd  16398  oexpneg  16559  oddge22np1  16563  bitsinv2  16657  bitsf1ocnv  16658  sadcaddlem  16671  sadadd2lem  16673  pythagtriplem4  17041  iserodd  17057  oddprmdvds  17125  prmreclem2  17139  prmreclem6  17143  vdwlem7  17209  vdwlem10  17212  vdwlem12  17214  dec2dvds  17285  dec5dvds  17286  2exp4  17306  2exp5  17307  2exp6  17308  2exp7  17309  2exp8  17310  2exp11  17311  2exp16  17312  3exp3  17313  2expltfac  17314  5prm  17330  7prm  17332  11prm  17337  13prm  17338  17prm  17339  19prm  17340  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  basendxltdsndx  17605  dsndxnplusgndx  17607  dsndxnmulrndx  17608  slotsdnscsi  17609  dsndxntsetndx  17610  slotsdifdsndx  17611  slotsdifunifndx  17618  eufndx  17632  eufid  17633  prdsvalstr  17673  smndex2dbas  19163  smndex2dlinvh  19166  pmtrprfval  19752  psgnunilem2  19760  efgredleme  20008  lt6abl  20160  cnfldfunALT  21745  sqcn  25250  ehl2eudis  25798  dveflem  26354  iaa  26708  iaaOLD  26709  tangtx  26891  efif1olem3  26929  efif1olem4  26930  root1id  27139  2logb9irr  27180  mcubic  27232  cubic2  27233  cubic  27234  binom4  27235  dquartlem2  27237  dquart  27238  quart1lem  27240  quart1  27241  quartlem1  27242  quartlem2  27243  atandmcj  27294  bndatandm  27314  atansopn  27317  atantayl3  27324  leibpilem2  27326  leibpi  27327  leibpisum  27328  log2cnv  27329  log2tlbnd  27330  log2ublem2  27332  log2ublem3  27333  log2ub  27334  log2le1  27335  birthday  27339  basellem3  27467  basellem4  27468  basellem5  27469  basellem8  27472  issqf  27520  ppi3  27555  ppiublem2  27587  chtublem  27595  mersenne  27611  bcmax  27662  bcp1ctr  27663  bclbnd  27664  bpos1  27667  bposlem6  27673  bposlem8  27675  lgslem1  27681  lgsqrlem2  27731  gausslemma2dlem6  27756  lgseisenlem4  27762  2lgslem1c  27777  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2sq2  27817  2sqreultlem  27831  2sqreunnltlem  27834  chebbnd1lem3  27855  rplogsumlem2  27869  dchrisumlem2  27874  dchrisum0flblem1  27892  dchrisum0flblem2  27893  dchrisum0flb  27894  selberglem2  27930  pntrmax  27948  pntlemo  27991  fltoprmlem2  28051  slotsinbpsd  28960  slotslnbpsd  28961  trkgstr  28963  eengstr  29615  usgrexmplef  29897  upgr2wlk  30304  usgr2pthlem  30406  usgr2pth  30407  wpthswwlks2on  30610  elwspths2spth  30616  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  konigsbergiedgw  30906  konigsberglem1  30910  konigsberglem2  30911  konigsberglem3  30912  clwlknon2num  31026  1kp2ke3k  31104  ex-mod  31107  ex-exp  31108  ex-fac  31109  9p10ne21  31128  ipidsq  31369  strlem3a  32911  xnn01gt  33458  expevenpos  33522  dpmul4  33576  pfxlsw2ccat  33609  wrdt2ind  33612  evl1deg2  34212  evl1deg3  34213  rngunsnply1chr2lem1  34250  rngunsnply1chr2lem2  34251  rngunsnply1chr2lem3  34252  fldext2rspun  34425  rtelextdg2lem  34469  rtelextdg2  34470  constrelextdg2  34490  2sqr3minply  34523  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem4  34528  cos9thpiminplylem5  34529  cos9thpinconstrlem1  34532  madjusmdetlem4  34573  coinflippv  35227  prodfzo03  35343  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  tgoldbachgnn  35399  tgoldbachgtde  35400  tgoldbachgt  35403  cusgredgex  36104  kur14lem8  36186  sinccvglem  36645  dvtan  38856  420gcd8e4  43322  12lcm5e60  43324  60lcm7e420  43326  lcmineqlem17  43361  lcmineqlem18  43362  lcmineqlem20  43364  lcmineqlem21  43365  lcmineqlem22  43366  lcmineqlem  43368  3exp7  43369  3lexlogpow5ineq1  43370  3lexlogpow5ineq2  43371  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  3lexlogpow5ineq5  43376  aks4d1p1p2  43386  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  2np3bcnp1  43460  2ap1caineq  43461  aks6d1c7lem1  43496  25or6to4  43522  sqn5i  43608  235t711  43628  ex-decpmul  43629  nicomachus  43635  dffltz  43936  sum9cubes  43949  3cubeslem2  43961  3cubeslem3l  43962  3cubeslem3r  43963  diophin  44049  irrapxlem5  44099  pellexlem2  44103  pell1qrge1  44143  jm2.22  44268  jm2.20nn  44270  jm2.27c  44280  rmydioph  44287  rmxdioph  44289  expdiophlem2  44295  frlmpwfi  44366  isnumbasgrplem3  44372  resqrtvalex  44906  imsqrtvalex  44907  amgm2d  45459  dvdivbd  47206  itgsinexplem1  47237  itgsinexp  47238  stoweidlem1  47284  wallispilem4  47351  wallispilem5  47352  wallispi2lem2  47355  stirlinglem3  47359  stirlinglem5  47361  stirlinglem7  47363  stirlinglem8  47364  stirlinglem10  47366  stirlinglem11  47367  hoiqssbllem2  47906  sqrtnnaa  48186  sqrtnzqaa  48187  sin3t  48190  cos3t  48191  sin5tlem1  48192  sin5tlem2  48193  sin5tlem4  48195  goldpolyfactor  48200  sqrtnpoly  48216  fmtnoge3  48888  fmtnom1nn  48890  fmtnof1  48893  fmtnorec1  48895  sqrtpwpw2p  48896  fmtnosqrt  48897  fmtnorec2lem  48900  fmtnodvds  48902  fmtnorec3  48906  fmtnorec4  48907  fmtno2  48908  fmtno3  48909  fmtno5lem2  48912  fmtno5lem4  48914  fmtno5  48915  257prm  48919  odz2prm2pw  48921  fmtnoprmfac1lem  48922  fmtnoprmfac2lem1  48924  fmtnofac2lem  48926  fmtnofac2  48927  fmtnofac1  48928  fmtno4prmfac  48930  fmtno4nprmfac193  48932  fmtno4prm  48933  fmtno5faclem1  48937  fmtno5faclem2  48938  fmtno5faclem3  48939  fmtno5fac  48940  flsqrt  48951  139prmALT  48954  31prm  48955  m5prm  48956  127prm  48957  m7prm  48958  m11nprm  48959  sfprmdvdsmersenne  48961  lighneallem2  48964  lighneallem3  48965  lighneallem4a  48966  proththd  48972  3exp4mod41  48974  41prothprmlem1  48975  oexpnegALTV  49048  fppr2odd  49102  2exp340mod341  49104  341fppr2  49105  8exp8mod9  49107  nfermltl2rev  49114  evengpoap3  49170  tgblthelfgott  49186  tgoldbachlt  49187  tgoldbach  49188  cycl3grtri  49318  usgrexmpl1lem  49392  usgrexmpl2lem  49397  gpg3nbgrvtx0  49447  gpgprismgr4cycllem7  49472  gpgprismgr4cycllem10  49475  gpg5edgnedg  49501  pgrple2abl  49808  pgrpgt2nabl  49809  ply1mulgsumlem2  49830  logbpw2m1  50010  blenpw2m1  50022  dignn0ehalf  50060  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0mullong  50068  2aryfvalel  50090  itcoval2  50107  itcoval3  50108  itcovalt2lem2lem2  50117  itcovalt2lem1  50118  ackval2  50125  ackval3  50126  ackval0012  50132  ackval1012  50133  ackval2012  50134  ackval3012  50135  ackval42  50139  prelrrx2bd  50157  2sphere  50192  itscnhlinecirc02plem3  50227  inlinecirc02p  50230  onetansqsecsq  51282  cotsqcscsq  51283