MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnuz Structured version   Unicode version

Theorem nnuz 11201
Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
nnuz  |-  NN  =  ( ZZ>= `  1 )

Proof of Theorem nnuz
StepHypRef Expression
1 nnzrab 10972 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10974 . . 3  |-  1  e.  ZZ
3 uzval 11168 . . 3  |-  ( 1  e.  ZZ  ->  ( ZZ>=
`  1 )  =  { k  e.  ZZ  |  1  <_  k } )
42, 3ax-mp 5 . 2  |-  ( ZZ>= ` 
1 )  =  {
k  e.  ZZ  | 
1  <_  k }
51, 4eqtr4i 2454 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872   {crab 2775   class class class wbr 4423   ` cfv 5601   1c1 9547    <_ cle 9683   NNcn 10616   ZZcz 10944   ZZ>=cuz 11166
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 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623
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 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-z 10945  df-uz 11167
This theorem is referenced by:  elnnuz  11202  eluz2nn  11204  uznnssnn  11213  nnwo  11231  eluznn  11236  nninf  11247  nninfmOLD  11249  fzssnn  11849  fseq1p1m1  11875  prednn  11919  elfzo1  11971  ltwenn  12182  ser1const  12275  expp1  12285  digit1  12412  facnn  12467  fac0  12468  facp1  12470  faclbnd4lem1  12484  bcm1k  12506  bcval5  12509  bcpasc  12512  fz1isolem  12628  seqcoll  12631  seqcoll2  12632  climuni  13615  isercolllem2  13728  isercoll  13730  sumeq2ii  13758  summolem3  13779  summolem2a  13780  fsum  13785  sum0  13786  sumz  13787  fsumcl2lem  13796  fsumadd  13804  fsummulc2  13844  fsumrelem  13866  isumnn0nn  13899  climcndslem1  13906  climcndslem2  13907  climcnds  13908  divcnv  13910  divcnvshft  13912  supcvg  13913  trireciplem  13919  trirecip  13920  expcnv  13921  geo2lim  13930  geoisum1  13934  geoisum1c  13935  mertenslem2  13940  prodeq2ii  13966  prodmolem3  13986  prodmolem2a  13987  fprod  13994  prod0  13996  prod1  13997  fprodss  14001  fprodser  14002  fprodcl2lem  14003  fprodmul  14013  fproddiv  14014  fprodn0  14032  fallfacval4  14095  bpoly4  14111  ege2le3  14143  rpnnen2lem3  14268  rpnnen2lem5  14270  rpnnen2lem8  14273  rpnnen2  14277  ruclem6  14286  bezoutlem2OLD  14503  bezoutlem3OLD  14504  bezoutlem2  14506  bezoutlem3  14507  lcmcllem  14560  lcmledvds  14563  lcmscllemOLD  14581  lcmsledvdsOLD  14584  lcmfval  14590  lcmfvalOLD  14594  lcmfcllem  14597  lcmfledvds  14604  isprm3  14632  phicl2  14715  phibndlem  14717  eulerthlem2  14729  odzcllem  14736  odzdvds  14739  odzcllemOLD  14742  odzdvdsOLD  14745  iserodd  14784  pcmptcl  14835  pcmpt  14836  pockthlem  14848  pockthg  14849  unbenlem  14851  prmreclem3  14861  prmreclem5  14863  prmreclem6  14864  prmrec  14865  1arith  14870  4sqlem13OLD  14900  4sqlem14OLD  14901  4sqlem17OLD  14904  4sqlem18OLD  14905  4sqlem13  14906  4sqlem14  14907  4sqlem17  14910  4sqlem18  14911  vdwlem1  14930  vdwlem2  14931  vdwlem3  14932  vdwlem6  14935  vdwlem8  14937  vdwlem10  14939  vdw  14943  vdwnnlem1  14944  vdwnnlem3  14946  prmlem1a  15077  mulgnnp1  16765  mulgnnsubcl  16769  mulgnn0z  16777  mulgnndir  16779  mulgpropd  16790  odlem1  17180  odlem1OLD  17183  odlem2  17187  odlem2OLD  17203  gexlem1  17227  gexlem1OLD  17229  gexlem2  17232  gexlem2OLD  17235  gexcl3  17238  sylow1lem1  17249  efgsdmi  17381  efgsrel  17383  efgs1b  17385  efgsp1  17386  mulgnn0di  17465  lt6abl  17528  gsumval3eu  17537  gsumval3  17540  gsumzcl2  17543  gsumzaddlem  17553  gsumconst  17566  gsumzmhm  17569  gsumzoppg  17576  zringlpirlem2OLD  19052  zringlpirlem3OLD  19053  zringlpirlem2  19054  zringlpirlem3  19055  lmcnp  20318  lmmo  20394  1stcelcls  20474  1stccnp  20475  1stckgenlem  20566  1stckgen  20567  imasdsf1olem  21386  lmnn  22231  cmetcaulem  22256  iscmet2  22262  causs  22266  caubl  22275  iscmet3i  22279  bcthlem5  22294  ovolsf  22423  ovollb2lem  22439  ovolctb  22441  ovolunlem1a  22447  ovolunlem1  22448  ovoliunlem1  22453  ovoliun  22456  ovoliun2  22457  ovoliunnul  22458  ovolscalem1  22464  ovolicc1  22467  ovolicc2lem2  22469  ovolicc2lem3  22470  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  iundisj  22499  iundisj2  22500  voliunlem1  22501  voliunlem2  22502  voliunlem3  22503  volsup  22507  ioombl1lem4  22512  uniioovol  22534  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem3  22541  uniioombllem4  22542  uniioombllem6  22544  vitalilem4  22567  vitalilem5  22568  itg1climres  22670  mbfi1fseqlem6  22676  mbfi1flimlem  22678  mbfmullem2  22680  itg2monolem1  22706  itg2i1fseqle  22710  itg2i1fseq  22711  itg2i1fseq2  22712  itg2addlem  22714  plyeq0lem  23162  vieta1lem2  23262  elqaalem1  23270  elqaalem3  23272  elqaalem1OLD  23273  elqaalem3OLD  23275  aaliou3lem4  23300  aaliou3lem7  23303  dvtaylp  23323  taylthlem2  23327  pserdvlem2  23381  pserdv2  23383  abelthlem6  23389  abelthlem9  23393  logtayl  23603  logtaylsum  23604  logtayl2  23605  atantayl  23861  leibpilem2  23865  leibpi  23866  birthdaylem2  23876  dfef2  23894  divsqrtsumlem  23903  emcllem2  23920  emcllem4  23922  emcllem5  23923  emcllem6  23924  emcllem7  23925  harmonicbnd4  23934  fsumharmonic  23935  zetacvg  23938  lgamgulmlem4  23955  lgamgulmlem6  23957  lgamgulm2  23959  lgamcvglem  23963  lgamcvg2  23978  gamcvg  23979  gamcvg2lem  23982  regamcl  23984  relgamcl  23985  lgam1  23987  wilthlem3  23993  ftalem2  23996  ftalem4  23998  ftalem5  23999  ftalem4OLD  24000  ftalem5OLD  24001  basellem5  24009  basellem6  24010  basellem7  24011  basellem8  24012  basellem9  24013  ppiprm  24076  ppinprm  24077  chtprm  24078  chtnprm  24079  chpp1  24080  vma1  24091  ppiltx  24102  fsumvma2  24140  chpchtsum  24145  logfacbnd3  24149  logexprlim  24151  bposlem5  24214  lgscllem  24229  lgsval2lem  24232  lgsval4a  24244  lgsneg  24245  lgsdir  24256  lgsdilem2  24257  lgsdi  24258  lgsne0  24259  lgsquadlem2  24281  chebbnd1lem1  24305  chtppilimlem1  24309  rplogsumlem1  24320  rplogsumlem2  24321  rpvmasumlem  24323  dchrisumlema  24324  dchrisumlem2  24326  dchrisumlem3  24327  dchrmusum2  24330  dchrvmasum2lem  24332  dchrvmasumiflem1  24337  dchrvmaeq0  24340  dchrisum0flblem2  24345  dchrisum0flb  24346  dchrisum0re  24349  dchrisum0lem1b  24351  dchrisum0lem1  24352  dchrisum0lem2a  24353  dchrisum0lem2  24354  dchrisum0lem3  24355  mudivsum  24366  mulogsum  24368  logdivsum  24369  mulog2sumlem2  24371  log2sumbnd  24380  selberg2lem  24386  logdivbnd  24392  pntrsumo1  24401  pntrsumbnd2  24403  pntrlog2bndlem2  24414  pntrlog2bndlem4  24416  pntrlog2bndlem6a  24418  pntlemf  24441  eedimeq  24926  axlowdimlem6  24975  axlowdimlem16  24985  axlowdimlem17  24986  eupath2lem3  25705  gxnn0suc  25990  nvlmle  26326  ipval2  26341  minvecolem3  26516  minvecolem4b  26518  minvecolem4  26520  minvecolem3OLD  26526  minvecolem4bOLD  26528  minvecolem4OLD  26530  h2hcau  26630  h2hlm  26631  hlimadd  26844  hlim0  26886  hhsscms  26928  occllem  26954  nlelchi  27712  opsqrlem4  27794  hmopidmchi  27802  iundisjf  28201  iundisj2f  28202  ssnnssfz  28373  iundisjfi  28378  iundisj2fi  28379  1smat1  28638  submat1n  28639  submatres  28640  submateqlem2  28642  lmatfval  28648  madjusmdetlem1  28661  madjusmdetlem2  28662  madjusmdetlem3  28663  madjusmdetlem4  28664  lmlim  28761  rge0scvg  28763  lmxrge0  28766  lmdvg  28767  esumfzf  28898  esumfsup  28899  esumpcvgval  28907  esumpmono  28908  esumcvg  28915  esumcvgsum  28917  esumsup  28918  fiunelros  29004  eulerpartlemsv2  29199  eulerpartlems  29201  eulerpartlemsv3  29202  eulerpartlemv  29205  eulerpartlemb  29209  fiblem  29239  fibp1  29242  rrvsum  29295  dstfrvclim1  29318  ballotlem1ri  29375  ballotlemsupOLD  29383  ballotlem1riOLD  29413  signsvfn  29479  subfacp1lem1  29910  subfacp1lem5  29915  subfacp1lem6  29916  erdszelem7  29928  cvmliftlem5  30020  cvmliftlem7  30022  cvmliftlem10  30025  cvmliftlem13  30027  sinccvg  30325  circum  30326  divcnvlin  30374  iprodgam  30385  faclimlem1  30386  faclimlem2  30387  faclim  30389  iprodfac  30390  faclim2  30391  poimirlem3  31907  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem12  31916  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  poimirlem25  31929  poimirlem27  31931  poimirlem28  31932  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  mblfinlem2  31942  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  lmclim2  32051  geomcau  32052  heibor1lem  32105  heibor1  32106  bfplem1  32118  bfplem2  32119  rrncmslem  32128  rrncms  32129  eldioph3b  35576  diophin  35584  diophun  35585  diophren  35625  jm3.1lem2  35843  dgraalem  35977  dgraalemOLD  35978  dgraaub  35983  dgraaubOLD  35984  dftrcl3  36282  trclfvdecomr  36290  hashnzfz2  36640  hashnzfzclim  36641  dvradcnv2  36666  binomcxplemnotnn0  36675  nnnfi  37382  nnsplit  37535  clim1fr1  37619  sumnnodd  37650  stoweidlem7  37807  stoweidlem14  37814  stoweidlem20  37820  stoweidlem34  37835  wallispilem5  37871  wallispi  37872  stirlinglem1  37876  stirlinglem5  37880  stirlinglem7  37882  stirlinglem8  37883  stirlinglem10  37885  stirlinglem11  37886  stirlinglem12  37887  stirlinglem13  37888  stirlinglem14  37889  stirlinglem15  37890  stirlingr  37892  dirkertrigeqlem2  37901  dirkertrigeqlem3  37902  fourierdlem11  37920  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem48  37958  fourierdlem49  37959  fourierdlem69  37979  fourierdlem73  37983  fourierdlem81  37991  fourierdlem93  38003  fourierdlem103  38013  fourierdlem104  38014  fourierdlem112  38022  fouriersw  38035  sge0ad2en  38181  caragenunicl  38253  caratheodorylem2  38256  hoidmvlelem3  38323
  Copyright terms: Public domain W3C validator