Theorem nn0uz 11139

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

Syntax hints:   = wceq 1437   e. wcel 1872   {crab 2713   class class class wbr 4361   ` cfv 5539   0cc0 9485   <_ cle 9622   NN0cn0 10815   ZZcz 10883   ZZ>=cuz 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-n0 10816  df-z 10884  df-uz 11106

This theorem is referenced by:  elnn0uz  11142  2eluzge0  11149  eluznn0  11174  nn0inf  11187  nn0infmOLD  11189  fseq1p1m1  11814  fznn0sub2  11843  nn0split  11852  prednn0  11859  fzossnn0  11895  fzennn  12126  hashgf1o  12129  exple1  12277  faclbnd4lem1  12423  bcval5  12448  bcpasc  12451  hashfzo0  12545  hashf1  12563  ccatval2  12666  ccatass  12675  ccatrn  12676  swrdccat1  12754  swrdccat2  12755  wrdeqs1cat  12772  cats1un  12773  splfv2a  12804  splval2  12805  revccat  12812  cats1fv  12896  binom1dif  13829  isumnn0nn  13838  climcndslem1  13845  climcnds  13847  harmonic  13855  arisum2  13857  explecnv  13861  geoser  13863  geolim  13864  geolim2  13865  geomulcvg  13870  geoisum  13871  geoisumr  13872  mertenslem1  13878  mertenslem2  13879  mertens  13880  fallfacfwd  14027  0fallfac  14028  binomfallfaclem2  14031  bpolylem  14039  bpolysum  14044  bpolydiflem  14045  fsumkthpow  14047  bpoly2  14048  bpoly3  14049  bpoly4  14050  efcllem  14070  ef0lem  14071  eff  14074  efcvg  14077  efcvgfsum  14078  reefcl  14079  ege2le3  14082  efcj  14084  eftlcvg  14098  eftlub  14101  effsumlt  14103  ef4p  14105  efgt1p2  14106  efgt1p  14107  eflegeo  14113  eirrlem  14194  ruclem6  14225  ruclem7  14226  divalglem2  14311  divalglem2OLD  14312  divalglem5OLD  14314  divalglem5  14315  bitsfzolem  14345  bitsfzolemOLD  14346  bitsfzo  14347  bitsfi  14349  bitsinv1lem  14353  bitsinv1  14354  bitsinvp1  14361  sadcf  14365  sadcp1  14367  sadadd  14379  sadass  14383  bitsres  14385  smupf  14390  smupp1  14392  smuval2  14394  smupval  14400  smueqlem  14402  smumul  14405  alginv  14472  algcvg  14473  algcvga  14476  algfx  14477  eucalgcvga  14483  eucalg  14484  phiprmpw  14662  prmdiv  14671  iserodd  14723  pcfac  14782  prmreclem2  14799  prmreclem4  14801  vdwapun  14862  vdwlem1  14869  ramcl2lem  14900  ramcl2lemOLD  14901  ramtcl  14902  ramtclOLD  14903  ramtub  14906  ramtubOLD  14907  gsumwsubmcl  16560  gsumws1  16561  gsumccat  16563  gsumwmhm  16567  psgnunilem2  17074  psgnunilem4  17076  sylow1lem1  17188  efginvrel2  17315  efgredleme  17331  efgredlemc  17333  efgcpbllemb  17343  frgpuplem  17360  nn0gsumfz  17551  telgsumfz0s  17559  telgsums  17561  pgpfaclem1  17652  psrbaglefi  18534  ltbwe  18634  pmatcollpw3fi  19746  pmatcollpw3fi1lem1  19747  chfacfisf  19815  chfacfisfcpmat  19816  iscmet3lem3  22197  dyadmax  22493  mbfi1fseqlem3  22612  itgcnlem  22684  dvnff  22814  dvnp1  22816  dvn2bss  22821  cpncn  22827  dveflem  22868  ig1peu  23059  ig1peuOLD  23060  ig1pdvds  23065  ig1pdvdsOLD  23071  ply1termlem  23094  plyeq0lem  23101  plyaddlem1  23104  plymullem1  23105  coeeulem  23115  dgrcl  23124  dgrub  23125  dgrlb  23127  coeid3  23131  plyco  23132  coeeq2  23133  coefv0  23139  coemulhi  23145  coemulc  23146  dvply1  23174  vieta1lem2  23201  vieta1  23202  elqaalem2  23210  elqaalem3  23211  elqaalem2OLD  23213  elqaalem3OLD  23214  geolim3  23232  dvntaylp  23263  taylthlem1  23265  radcnvlem1  23305  radcnvlem2  23306  radcnvlem3  23307  radcnv0  23308  radcnvlt2  23311  dvradcnv  23313  pserulm  23314  psercn2  23315  pserdvlem2  23320  pserdv2  23322  abelthlem4  23326  abelthlem5  23327  abelthlem6  23328  abelthlem7  23330  abelthlem8  23331  abelthlem9  23332  advlogexp  23537  logtayllem  23541  logtayl  23542  cxpeq  23634  leibpi  23805  leibpisum  23806  log2cnv  23807  log2tlbnd  23808  log2ublem2  23810  birthdaylem3  23816  wilthlem2  23931  ftalem1  23934  ftalem5  23938  ftalem5OLD  23940  basellem2  23945  basellem3  23946  basellem5  23948  musum  24057  0sgmppw  24063  1sgmprm  24064  chtublem  24076  logexprlim  24090  lgseisenlem1  24214  lgsquadlem2  24220  dchrisumlem1  24264  dchrisumlem2  24265  dchrisum0flblem1  24283  ostth2lem3  24410  tgcgr4  24513  eupares  25640  eupap1  25641  eupath2lem3  25644  eupath2  25645  konigsberg  25652  oddpwdc  29134  eulerpartlemb  29148  sseqfn  29170  sseqf  29172  signsplypnf  29386  signstcl  29401  signstf  29402  signstfvn  29405  signstfvneq0  29408  subfacval2  29857  subfaclim  29858  cvmliftlem7  29961  fwddifnp1  30876  poimirlem3  31850  poimirlem4  31851  poimirlem18  31865  poimirlem21  31868  poimirlem22  31869  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  heiborlem4  32053  heiborlem6  32055  mapfzcons  35470  irrapxlem1  35579  ltrmynn0  35711  ltrmxnn0  35712  acongeq  35746  jm2.23  35764  jm2.26lem3  35769  dfrtrcl3  36238  radcnvrat  36576  bcc0  36602  dvradcnv2  36609  binomcxplemnn0  36611  binomcxplemrat  36612  binomcxplemradcnv  36614  binomcxplemnotnn0  36618  fzssnn0  37436  expfac  37621  dvnmptdivc  37696  dvnmul  37701  dvnprodlem3  37706  stoweidlem17  37760  stoweidlem34  37778  stirlinglem5  37823  stirlinglem7  37825  fourierdlem15  37867  fourierdlem25  37877  fourierdlem48  37901  fourierdlem49  37902  fourierdlem50  37903  fourierdlem52  37905  fourierdlem54  37907  fourierdlem64  37917  fourierdlem65  37918  fourierdlem81  37934  fourierdlem92  37945  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem113  37966  fourierdlem114  37967  elaa2lem  37980  elaa2lemOLD  37981  etransclem4  37986  etransclem10  37992  etransclem14  37996  etransclem15  37997  etransclem23  38005  etransclem24  38006  etransclem31  38013  etransclem32  38014  etransclem35  38017  etransclem44  38026  etransclem46  38028  etransclem48OLD  38030  etransclem48  38031  ssnn0ssfz  39723  aacllem  40133