Theorem nn0uz 11722

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 11406	. 2 |- NN0 = { k e. ZZ | 0 <_ k }
2		0z 11388	. . 3 |- 0 e. ZZ
3		uzval 11689	. . 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 2647	1 |- NN0 = ( ZZ>= ` 0 )

Syntax hints:   = wceq 1483   e. wcel 1990   {crab 2916   class class class wbr 4653   ` cfv 5888   0cc0 9936   <_ cle 10075   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688

This theorem is referenced by:  elnn0uz  11725  2eluzge0  11733  eluznn0  11757  nn0inf  11770  fseq1p1m1  12414  fznn0sub2  12446  nn0split  12454  prednn0  12463  fzossnn0  12499  fzennn  12767  hashgf1o  12770  exple1  12920  faclbnd4lem1  13080  bcval5  13105  bcpasc  13108  hashfzo0  13217  hashf1  13241  ccatval2  13362  ccatass  13371  ccatrn  13372  swrdccat1  13457  swrdccat2  13458  wrdeqs1cat  13474  cats1un  13475  splfv2a  13507  splval2  13508  revccat  13515  cats1fv  13604  binom1dif  14565  isumnn0nn  14574  climcndslem1  14581  climcnds  14583  harmonic  14591  arisum2  14593  explecnv  14597  geoser  14599  geolim  14601  geolim2  14602  geomulcvg  14607  geoisum  14608  geoisumr  14609  mertenslem1  14616  mertenslem2  14617  mertens  14618  fallfacfwd  14767  0fallfac  14768  binomfallfaclem2  14771  bpolylem  14779  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  bpoly2  14788  bpoly3  14789  bpoly4  14790  efcllem  14808  ef0lem  14809  eff  14812  efcvg  14815  efcvgfsum  14816  reefcl  14817  ege2le3  14820  efcj  14822  eftlcvg  14836  eftlub  14839  effsumlt  14841  ef4p  14843  efgt1p2  14844  efgt1p  14845  eflegeo  14851  eirrlem  14932  ruclem6  14964  ruclem7  14965  divalglem2  15118  divalglem5  15120  bitsfzolem  15156  bitsfzo  15157  bitsfi  15159  bitsinv1lem  15163  bitsinv1  15164  bitsinvp1  15171  sadcf  15175  sadcp1  15177  sadadd  15189  sadass  15193  bitsres  15195  smupf  15200  smupp1  15202  smuval2  15204  smupval  15210  smueqlem  15212  smumul  15215  alginv  15288  algcvg  15289  algcvga  15292  algfx  15293  eucalgcvga  15299  eucalg  15300  phiprmpw  15481  prmdiv  15490  iserodd  15540  pcfac  15603  prmreclem2  15621  prmreclem4  15623  vdwapun  15678  vdwlem1  15685  ramcl2lem  15713  ramtcl  15714  ramtub  15716  gsumwsubmcl  17375  gsumws1  17376  gsumccat  17378  gsumwmhm  17382  psgnunilem2  17915  psgnunilem4  17917  sylow1lem1  18013  efginvrel2  18140  efgredleme  18156  efgredlemc  18158  efgcpbllemb  18168  frgpuplem  18185  telgsumfz0s  18388  telgsums  18390  pgpfaclem1  18480  psrbaglefi  19372  ltbwe  19472  pmatcollpw3fi1lem1  20591  chfacfisf  20659  chfacfisfcpmat  20660  iscmet3lem3  23088  dyadmax  23366  mbfi1fseqlem3  23484  itgcnlem  23556  dvnff  23686  dvnp1  23688  dvn2bss  23693  cpncn  23699  dveflem  23742  ig1peu  23931  ig1pdvds  23936  ply1termlem  23959  plyeq0lem  23966  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  dgrcl  23989  dgrub  23990  dgrlb  23992  coeid3  23996  plyco  23997  coeeq2  23998  coefv0  24004  coemulhi  24010  coemulc  24011  dvply1  24039  vieta1lem2  24066  vieta1  24067  elqaalem2  24075  elqaalem3  24076  geolim3  24094  dvntaylp  24125  taylthlem1  24127  radcnvlem1  24167  radcnvlem2  24168  radcnvlem3  24169  radcnv0  24170  radcnvlt2  24173  dvradcnv  24175  pserulm  24176  psercn2  24177  pserdvlem2  24182  pserdv2  24184  abelthlem4  24188  abelthlem5  24189  abelthlem6  24190  abelthlem7  24192  abelthlem8  24193  abelthlem9  24194  advlogexp  24401  logtayllem  24405  logtayl  24406  cxpeq  24498  leibpi  24669  leibpisum  24670  log2cnv  24671  log2tlbnd  24672  log2ublem2  24674  birthdaylem3  24680  wilthlem2  24795  ftalem1  24799  ftalem5  24803  basellem2  24808  basellem3  24809  basellem5  24811  musum  24917  0sgmppw  24923  1sgmprm  24924  chtublem  24936  logexprlim  24950  lgseisenlem1  25100  lgsquadlem2  25106  dchrisumlem1  25178  dchrisumlem2  25179  dchrisum0flblem1  25197  ostth2lem3  25324  tgcgr4  25426  eupth2lems  27098  numclwwlkovf2exlem1  27211  fz2ssnn0  29547  oddpwdc  30416  eulerpartlemb  30430  sseqfn  30452  sseqf  30454  signsplypnf  30627  signstcl  30642  signstf  30643  signstfvn  30646  signstfvneq0  30649  fsum2dsub  30685  reprsuc  30693  breprexplema  30708  breprexplemc  30710  subfacval2  31169  subfaclim  31170  cvmliftlem7  31273  fwddifnp1  32272  knoppcnlem6  32488  knoppcnlem8  32490  knoppcnlem9  32491  knoppcnlem11  32493  knoppcn  32494  knoppndvlem4  32506  knoppndvlem6  32508  knoppf  32526  poimirlem3  33412  poimirlem4  33413  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  heiborlem4  33613  heiborlem6  33615  mapfzcons  37279  irrapxlem1  37386  ltrmynn0  37515  ltrmxnn0  37516  acongeq  37550  jm2.23  37563  jm2.26lem3  37568  dfrtrcl3  38025  radcnvrat  38513  bcc0  38539  dvradcnv2  38546  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemradcnv  38551  binomcxplemnotnn0  38555  fzssnn0  39533  expfac  39889  dvnmptdivc  40153  dvnmul  40158  dvnprodlem3  40163  stoweidlem17  40234  stoweidlem34  40251  stirlinglem5  40295  stirlinglem7  40297  fourierdlem15  40339  fourierdlem25  40349  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem52  40375  fourierdlem54  40377  fourierdlem64  40387  fourierdlem65  40388  fourierdlem81  40404  fourierdlem92  40415  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  fourierdlem114  40437  elaa2lem  40450  etransclem4  40455  etransclem10  40461  etransclem14  40465  etransclem15  40466  etransclem23  40474  etransclem24  40475  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem44  40495  etransclem46  40497  etransclem48  40499  pwdif  41501  ssnn0ssfz  42127  aacllem  42547