Theorem nn0uz 11119

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 10894	. 2 |- NN0 = { k e. ZZ | 0 <_ k }
2		0z 10876	. . 3 |- 0 e. ZZ
3		uzval 11087	. . 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 2473	1 |- NN0 = ( ZZ>= ` 0 )

Syntax hints:   = wceq 1381   e. wcel 1802   {crab 2795   class class class wbr 4433   ` cfv 5574   0cc0 9490   <_ cle 9627   NN0cn0 10796   ZZcz 10865   ZZ>=cuz 11085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-recs 7040  df-rdg 7074  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-nn 10538  df-n0 10797  df-z 10866  df-uz 11086

This theorem is referenced by:  elnn0uz  11122  2eluzge0  11130  eluznn0  11155  nn0infm  11167  fseq1p1m1  11756  fznn0sub2  11784  nn0split  11793  fzossnn0  11830  fzennn  12052  hashgf1o  12055  exple1  12199  faclbnd4lem1  12345  bcval5  12370  bcpasc  12373  hashfzo0  12462  hashf1  12480  ccatval2  12570  ccatass  12579  ccatrn  12580  swrdid  12626  swrdccat1  12656  swrdccat2  12657  wrdeqcats1  12673  wrdeqs1cat  12674  cats1un  12675  splfv2a  12706  splval2  12707  revccat  12714  cats1fv  12798  binom1dif  13619  isumnn0nn  13628  climcndslem1  13635  climcnds  13637  harmonic  13644  arisum2  13646  explecnv  13650  geoser  13652  geolim  13653  geolim2  13654  geomulcvg  13659  geoisum  13660  geoisumr  13661  mertenslem1  13667  mertenslem2  13668  mertens  13669  efcllem  13686  ef0lem  13687  eff  13690  efcvg  13693  efcvgfsum  13694  reefcl  13695  ege2le3  13698  efcj  13700  eftlcvg  13713  eftlub  13716  effsumlt  13718  ef4p  13720  efgt1p2  13721  efgt1p  13722  eflegeo  13728  eirrlem  13809  ruclem6  13840  ruclem7  13841  divalglem2  13925  divalglem5  13927  bitsfzolem  13956  bitsfzo  13957  bitsfi  13959  bitsinv1lem  13963  bitsinv1  13964  bitsinvp1  13971  sadcf  13975  sadcp1  13977  sadadd  13989  sadass  13993  bitsres  13995  smupf  14000  smupp1  14002  smuval2  14004  smupval  14010  smueqlem  14012  smumul  14015  alginv  14076  algcvg  14077  algcvga  14080  algfx  14081  eucalgcvga  14087  eucalg  14088  phiprmpw  14178  prmdiv  14187  iserodd  14231  pcfac  14290  prmreclem2  14307  prmreclem4  14309  vdwapun  14364  vdwlem1  14371  ramcl2lem  14399  ramtcl  14400  ramtub  14402  gsumwsubmcl  15875  gsumws1  15876  gsumccat  15878  gsumwmhm  15882  psgnunilem2  16389  psgnunilem4  16391  sylow1lem1  16487  efginvrel2  16614  efgredleme  16630  efgredlemc  16632  efgcpbllemb  16642  frgpuplem  16659  nn0gsumfz  16881  telgsumfz0s  16889  telgsums  16891  pgpfaclem1  17000  psrbaglefi  17891  psrbaglefiOLD  17892  ltbwe  18005  pmatcollpw3fi  19153  pmatcollpw3fi1lem1  19154  chfacfisf  19222  chfacfisfcpmat  19223  iscmet3lem3  21595  dyadmax  21873  mbfi1fseqlem3  21990  itgcnlem  22062  dvnff  22192  dvnp1  22194  dvn2bss  22199  cpncn  22205  dveflem  22246  ig1peu  22438  ig1pdvds  22443  ply1termlem  22466  plyeq0lem  22473  plyaddlem1  22476  plymullem1  22477  coeeulem  22487  dgrcl  22496  dgrub  22497  dgrlb  22499  coeid3  22503  plyco  22504  coeeq2  22505  coefv0  22510  coemulhi  22516  coemulc  22517  dvply1  22545  vieta1lem2  22572  vieta1  22573  elqaalem2  22581  elqaalem3  22582  geolim3  22600  dvntaylp  22631  taylthlem1  22633  radcnvlem1  22673  radcnvlem2  22674  radcnvlem3  22675  radcnv0  22676  radcnvlt2  22679  dvradcnv  22681  pserulm  22682  psercn2  22683  pserdvlem2  22688  pserdv2  22690  abelthlem4  22694  abelthlem5  22695  abelthlem6  22696  abelthlem7  22698  abelthlem8  22699  abelthlem9  22700  advlogexp  22901  logtayllem  22905  logtayl  22906  cxpeq  22996  leibpi  23138  leibpisum  23139  log2cnv  23140  log2tlbnd  23141  log2ublem2  23143  birthdaylem3  23148  wilthlem2  23208  ftalem1  23211  ftalem5  23215  basellem2  23220  basellem3  23221  basellem5  23223  musum  23332  0sgmppw  23338  1sgmprm  23339  chtublem  23351  logexprlim  23365  lgseisenlem1  23489  lgsquadlem2  23495  dchrisumlem1  23539  dchrisumlem2  23540  dchrisum0flblem1  23558  ostth2lem3  23685  eupares  24840  eupap1  24841  eupath2lem3  24844  eupath2  24845  konigsberg  24852  oddpwdc  28159  eulerpartlemb  28173  sseqfn  28195  sseqf  28197  signsplypnf  28373  signstcl  28388  signstf  28389  signstfvn  28392  signstfvneq0  28395  subfacval2  28497  subfaclim  28498  cvmliftlem7  28602  relexpsucr  28919  fallfacfwd  29126  0fallfac  29127  binomfallfaclem2  29130  prednn0  29250  bpolylem  29778  bpolysum  29783  bpolydiflem  29784  fsumkthpow  29786  bpoly2  29787  bpoly3  29788  bpoly4  29789  heiborlem4  30278  heiborlem6  30280  mapfzcons  30616  irrapxlem1  30726  ltrmynn0  30854  ltrmxnn0  30855  acongeq  30889  jm2.23  30906  jm2.26lem3  30911  radcnvrat  31164  stoweidlem17  31684  stoweidlem34  31701  stirlinglem5  31745  stirlinglem7  31747  fourierdlem15  31789  fourierdlem25  31799  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem52  31826  fourierdlem54  31828  fourierdlem64  31838  fourierdlem65  31839  fourierdlem81  31855  fourierdlem92  31866  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem113  31887  fourierdlem114  31888  ssnn0ssfz  32646