Theorem nn0uz 11053

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 10828	. 2 |- NN0 = { k e. ZZ | 0 <_ k }
2		0z 10810	. . 3 |- 0 e. ZZ
3		uzval 11021	. . 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 2424	1 |- NN0 = ( ZZ>= ` 0 )

Syntax hints:   = wceq 1399   e. wcel 1836   {crab 2746   class class class wbr 4380   ` cfv 5509   0cc0 9421   <_ cle 9558   NN0cn0 10730   ZZcz 10799   ZZ>=cuz 11019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-cnex 9477  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-recs 6978  df-rdg 7012  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-nn 10471  df-n0 10731  df-z 10800  df-uz 11020

This theorem is referenced by:  elnn0uz  11056  2eluzge0  11063  eluznn0  11088  nn0infm  11100  fseq1p1m1  11692  fznn0sub2  11721  nn0split  11730  fzossnn0  11769  fzennn  12000  hashgf1o  12003  exple1  12147  faclbnd4lem1  12292  bcval5  12317  bcpasc  12320  hashfzo0  12411  hashf1  12429  ccatval2  12524  ccatass  12533  ccatrn  12534  swrdccat1  12612  swrdccat2  12613  wrdeqs1cat  12630  cats1un  12631  splfv2a  12662  splval2  12663  revccat  12670  cats1fv  12754  binom1dif  13666  isumnn0nn  13675  climcndslem1  13682  climcnds  13684  harmonic  13691  arisum2  13693  explecnv  13697  geoser  13699  geolim  13700  geolim2  13701  geomulcvg  13706  geoisum  13707  geoisumr  13708  mertenslem1  13714  mertenslem2  13715  mertens  13716  efcllem  13834  ef0lem  13835  eff  13838  efcvg  13841  efcvgfsum  13842  reefcl  13843  ege2le3  13846  efcj  13848  eftlcvg  13862  eftlub  13865  effsumlt  13867  ef4p  13869  efgt1p2  13870  efgt1p  13871  eflegeo  13877  eirrlem  13958  ruclem6  13989  ruclem7  13990  divalglem2  14074  divalglem5  14076  bitsfzolem  14105  bitsfzo  14106  bitsfi  14108  bitsinv1lem  14112  bitsinv1  14113  bitsinvp1  14120  sadcf  14124  sadcp1  14126  sadadd  14138  sadass  14142  bitsres  14144  smupf  14149  smupp1  14151  smuval2  14153  smupval  14159  smueqlem  14161  smumul  14164  alginv  14225  algcvg  14226  algcvga  14229  algfx  14230  eucalgcvga  14236  eucalg  14237  phiprmpw  14327  prmdiv  14336  iserodd  14380  pcfac  14439  prmreclem2  14456  prmreclem4  14458  vdwapun  14513  vdwlem1  14520  ramcl2lem  14548  ramtcl  14549  ramtub  14551  gsumwsubmcl  16142  gsumws1  16143  gsumccat  16145  gsumwmhm  16149  psgnunilem2  16656  psgnunilem4  16658  sylow1lem1  16754  efginvrel2  16881  efgredleme  16897  efgredlemc  16899  efgcpbllemb  16909  frgpuplem  16926  nn0gsumfz  17144  telgsumfz0s  17152  telgsums  17154  pgpfaclem1  17264  psrbaglefi  18155  psrbaglefiOLD  18156  ltbwe  18269  pmatcollpw3fi  19390  pmatcollpw3fi1lem1  19391  chfacfisf  19459  chfacfisfcpmat  19460  iscmet3lem3  21833  dyadmax  22111  mbfi1fseqlem3  22228  itgcnlem  22300  dvnff  22430  dvnp1  22432  dvn2bss  22437  cpncn  22443  dveflem  22484  ig1peu  22676  ig1pdvds  22681  ply1termlem  22704  plyeq0lem  22711  plyaddlem1  22714  plymullem1  22715  coeeulem  22725  dgrcl  22734  dgrub  22735  dgrlb  22737  coeid3  22741  plyco  22742  coeeq2  22743  coefv0  22749  coemulhi  22755  coemulc  22756  dvply1  22784  vieta1lem2  22811  vieta1  22812  elqaalem2  22820  elqaalem3  22821  geolim3  22839  dvntaylp  22870  taylthlem1  22872  radcnvlem1  22912  radcnvlem2  22913  radcnvlem3  22914  radcnv0  22915  radcnvlt2  22918  dvradcnv  22920  pserulm  22921  psercn2  22922  pserdvlem2  22927  pserdv2  22929  abelthlem4  22933  abelthlem5  22934  abelthlem6  22935  abelthlem7  22937  abelthlem8  22938  abelthlem9  22939  advlogexp  23142  logtayllem  23146  logtayl  23147  cxpeq  23237  leibpi  23408  leibpisum  23409  log2cnv  23410  log2tlbnd  23411  log2ublem2  23413  birthdaylem3  23419  wilthlem2  23479  ftalem1  23482  ftalem5  23486  basellem2  23491  basellem3  23492  basellem5  23494  musum  23603  0sgmppw  23609  1sgmprm  23610  chtublem  23622  logexprlim  23636  lgseisenlem1  23760  lgsquadlem2  23766  dchrisumlem1  23810  dchrisumlem2  23811  dchrisum0flblem1  23829  ostth2lem3  23956  eupares  25117  eupap1  25118  eupath2lem3  25121  eupath2  25122  konigsberg  25129  oddpwdc  28512  eulerpartlemb  28526  sseqfn  28548  sseqf  28550  signsplypnf  28726  signstcl  28741  signstf  28742  signstfvn  28745  signstfvneq0  28748  subfacval2  28856  subfaclim  28857  cvmliftlem7  28961  fallfacfwd  29360  0fallfac  29361  binomfallfaclem2  29364  prednn0  29483  bpolylem  29999  bpolysum  30004  bpolydiflem  30005  fsumkthpow  30007  bpoly2  30008  bpoly3  30009  bpoly4  30010  heiborlem4  30512  heiborlem6  30514  mapfzcons  30850  irrapxlem1  30959  ltrmynn0  31087  ltrmxnn0  31088  acongeq  31122  jm2.23  31140  jm2.26lem3  31145  radcnvrat  31399  bcc0  31449  dvradcnv2  31456  binomcxplemnn0  31458  binomcxplemrat  31459  binomcxplemradcnv  31461  binomcxplemnotnn0  31465  fzssnn0  31723  expfac  31864  dvnmptdivc  31936  dvnmul  31941  dvnprodlem3  31946  stoweidlem17  32000  stoweidlem34  32017  stirlinglem5  32061  stirlinglem7  32063  fourierdlem15  32105  fourierdlem25  32115  fourierdlem48  32138  fourierdlem49  32139  fourierdlem50  32140  fourierdlem52  32142  fourierdlem54  32144  fourierdlem64  32154  fourierdlem65  32155  fourierdlem81  32171  fourierdlem92  32182  fourierdlem102  32192  fourierdlem103  32193  fourierdlem104  32194  fourierdlem113  32203  fourierdlem114  32204  elaa2lem  32217  etransclem4  32222  etransclem10  32228  etransclem14  32232  etransclem15  32233  etransclem23  32241  etransclem24  32242  etransclem31  32249  etransclem32  32250  etransclem35  32253  etransclem44  32262  etransclem46  32264  etransclem48  32266  ssnn0ssfz  33173  aacllem  33585  dfrtrcl3  38267