Theorem nn0uz 10996

Description: Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)

Assertion

Ref	Expression
nn0uz	|- NN0 = ( ZZ>= ` 0 )

Proof of Theorem nn0uz

Step	Hyp	Ref	Expression
1		nn0zrab 10776	. 2 |- NN0 = { k e. ZZ | 0 <_ k }
2		0z 10758	. . 3 |- 0 e. ZZ
3		uzval 10964	. . 3 |- ( 0 e. ZZ -> ( ZZ>= ` 0 ) = { k e. ZZ | 0 <_ k } )
4	2, 3	ax-mp 5	. 2 |- ( ZZ>= ` 0 ) = { k e. ZZ | 0 <_ k }
5	1, 4	eqtr4i 2483	1 |- NN0 = ( ZZ>= ` 0 )

Syntax hints:   = wceq 1370   e. wcel 1758   {crab 2799   class class class wbr 4390   ` cfv 5516   0cc0 9383   <_ cle 9520   NN0cn0 10680   ZZcz 10747   ZZ>=cuz 10962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-recs 6932  df-rdg 6966  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-nn 10424  df-n0 10681  df-z 10748  df-uz 10963

This theorem is referenced by:  elnn0uz  10999  eluznn0  11025  nn0infm  11037  fznn0sub2  11589  fseq1p1m1  11635  fzossnn0  11681  fzennn  11891  hashgf1o  11894  exple1  12024  faclbnd4lem1  12170  bcn0  12187  bcn1  12190  bcval5  12195  bcpasc  12198  hashfzo0  12293  hashf1  12312  ccatval2  12379  ccatass  12388  swrdid  12423  swrdccat1  12453  swrdccat2  12454  wrdeqcats1  12470  wrdeqs1cat  12471  cats1un  12472  splfv2a  12500  splval2  12501  revccat  12508  cats1fv  12588  binom1dif  13398  isumnn0nn  13407  climcndslem1  13414  climcnds  13416  harmonic  13423  arisum2  13425  explecnv  13429  geoser  13431  geolim  13432  geolim2  13433  geomulcvg  13438  geoisum  13439  geoisumr  13440  mertenslem1  13446  mertenslem2  13447  mertens  13448  efcllem  13465  ef0lem  13466  eff  13469  efcvg  13472  efcvgfsum  13473  reefcl  13474  ege2le3  13477  efcj  13479  eftlcvg  13492  eftlub  13495  effsumlt  13497  ef4p  13499  efgt1p2  13500  efgt1p  13501  eflegeo  13507  eirrlem  13588  ruclem6  13619  ruclem7  13620  divalglem2  13701  divalglem5  13703  bitsfzolem  13732  bitsfzo  13733  bitsfi  13735  bitsinv1lem  13739  bitsinv1  13740  bitsinvp1  13747  sadcf  13751  sadcp1  13753  sadadd  13765  sadass  13769  bitsres  13771  smupf  13776  smupp1  13778  smuval2  13780  smupval  13786  smueqlem  13788  smumul  13791  alginv  13852  algcvg  13853  algcvga  13856  algfx  13857  eucalgcvga  13863  eucalg  13864  dfphi2  13951  phiprmpw  13953  prmdiv  13962  iserodd  14004  pcfac  14063  prmreclem2  14080  prmreclem4  14082  vdwapun  14137  vdwlem1  14144  ramcl2lem  14172  ramtcl  14173  ramtub  14175  gsumwsubmcl  15618  gsumws1  15619  gsumccat  15621  gsumwmhm  15625  psgnunilem2  16103  psgnunilem4  16105  sylow1lem1  16201  efginvrel2  16328  efgsp1  16338  efgsres  16339  efgredleme  16344  efgredlemd  16345  efgredlemc  16346  efgredlem  16348  efgcpbllemb  16356  frgpuplem  16373  pgpfaclem1  16687  psrbaglefi  17547  psrbaglefiOLD  17548  ltbwe  17661  iscmet3lem3  20917  dyadmax  21194  mbfi1fseqlem3  21311  iblcnlem1  21381  itgcnlem  21383  dvnff  21513  dvnp1  21515  dvn2bss  21520  cpncn  21526  dveflem  21567  c1lip2  21586  ig1peu  21759  ig1pdvds  21764  ply1termlem  21787  plyeq0lem  21794  plyaddlem1  21797  plymullem1  21798  coeeulem  21808  dgrcl  21817  dgrub  21818  dgrlb  21820  coeid3  21824  plyco  21825  coeeq2  21826  coefv0  21831  coemulhi  21837  coemulc  21838  dvply1  21866  vieta1lem2  21893  vieta1  21894  elqaalem2  21902  elqaalem3  21903  geolim3  21921  dvtaylp  21951  dvntaylp  21952  taylthlem1  21954  taylthlem2  21955  radcnvlem1  21994  radcnvlem2  21995  radcnvlem3  21996  radcnv0  21997  radcnvlt2  22000  dvradcnv  22002  pserulm  22003  psercn2  22004  pserdvlem2  22009  pserdv2  22011  abelthlem4  22015  abelthlem5  22016  abelthlem6  22017  abelthlem7  22019  abelthlem8  22020  abelthlem9  22021  advlogexp  22216  logtayllem  22220  logtayl  22221  cxpeq  22311  leibpilem2  22452  leibpi  22453  leibpisum  22454  log2cnv  22455  log2tlbnd  22456  log2ublem2  22458  birthdaylem3  22463  wilthlem2  22523  ftalem1  22526  ftalem5  22530  basellem2  22535  basellem3  22536  basellem5  22538  musum  22647  0sgmppw  22653  1sgmprm  22654  chtublem  22666  logexprlim  22680  lgseisenlem1  22804  lgsquadlem2  22810  dchrisumlem1  22854  dchrisumlem2  22855  dchrisum0flblem1  22873  ostth2lem3  23000  eupares  23731  eupap1  23732  eupath2lem3  23735  eupath2  23736  konigsberg  23743  oddpwdc  26871  eulerpartlemb  26885  sseqfn  26907  sseqf  26909  ballotlemfrci  27044  ballotlemfrceq  27045  signsplypnf  27085  signstcl  27100  signstf  27101  signstfvn  27104  signstfvneq0  27107  signsvfn  27117  subfacval2  27209  subfaclim  27210  cvmliftlem7  27314  relexpsucr  27466  fallfacfwd  27673  0fallfac  27674  binomfallfaclem2  27677  prednn0  27797  bpolylem  28325  bpolysum  28330  bpolydiflem  28331  fsumkthpow  28333  bpoly2  28334  bpoly3  28335  bpoly4  28336  heiborlem4  28851  heiborlem6  28853  mapfzcons  29190  irrapxlem1  29301  ltrmynn0  29429  ltrmxnn0  29430  acongeq  29464  jm2.23  29483  jm2.26lem3  29488  stoweidlem17  29950  stoweidlem34  29967  stirlinglem5  30011  stirlinglem7  30013  nn0split  30875  ssnn0ssfz  30879  nn0gsumfz  30945  telescfzgsum0  30953  telescgsum  30955  pmatcollpw4fi  31241  pmatcollpw4fi1lem1  31242  chfacfisf  31308  chfacfisfcpmat  31309