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

Theorem nnuz 11113
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 10888 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10890 . . 3  |-  1  e.  ZZ
3 uzval 11080 . . 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 2499 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767   {crab 2818   class class class wbr 4447   ` cfv 5586   1c1 9489    <_ cle 9625   NNcn 10532   ZZcz 10860   ZZ>=cuz 11078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-recs 7039  df-rdg 7073  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-z 10861  df-uz 11079
This theorem is referenced by:  elnnuz  11114  eluz2nn  11116  uznnssnn  11124  nnwo  11143  eluznn  11148  nninfm  11158  fseq1p1m1  11748  elfzo1  11835  ltwenn  12036  ser1const  12126  expp1  12136  digit1  12262  facnn  12317  fac0  12318  facp1  12320  faclbnd4lem1  12333  bcm1k  12355  bcval5  12358  bcpasc  12361  fz1isolem  12470  seqcoll  12472  seqcoll2  12473  climuni  13331  isercolllem2  13444  isercoll  13446  sumeq2ii  13471  summolem3  13492  summolem2a  13493  fsum  13498  sum0  13499  sumz  13500  fsumcl2lem  13509  fsumadd  13517  fsummulc2  13555  fsumrelem  13577  isumnn0nn  13610  climcndslem1  13617  climcndslem2  13618  climcnds  13619  divcnv  13621  supcvg  13623  trireciplem  13629  trirecip  13630  expcnv  13631  geo2lim  13640  geoisum1  13644  geoisum1c  13645  mertenslem2  13650  ege2le3  13680  rpnnen2lem3  13804  rpnnen2lem5  13806  rpnnen2lem8  13809  rpnnen2  13813  ruclem6  13822  bezoutlem2  14029  bezoutlem3  14030  isprm3  14078  phicl2  14150  phibndlem  14152  eulerthlem2  14164  odzcllem  14171  odzdvds  14174  iserodd  14211  pcmptcl  14262  pcmpt  14263  pockthlem  14275  pockthg  14276  unbenlem  14278  prmreclem3  14288  prmreclem5  14290  prmreclem6  14291  prmrec  14292  1arith  14297  4sqlem13  14327  4sqlem14  14328  4sqlem17  14331  4sqlem18  14332  vdwlem1  14351  vdwlem2  14352  vdwlem3  14353  vdwlem6  14356  vdwlem8  14358  vdwlem10  14360  vdw  14364  vdwnnlem1  14365  vdwnnlem3  14367  prmlem1a  14443  mulgnnp1  15947  mulgnnsubcl  15951  mulgnn0z  15959  mulgnndir  15961  mulgpropd  15972  odlem1  16352  odlem2  16356  gexlem1  16392  gexlem2  16395  gexcl3  16400  sylow1lem1  16411  efgsdmi  16543  efgsrel  16545  efgs1b  16547  efgsp1  16548  mulgnn0di  16627  lt6abl  16685  gsumval3eu  16695  gsumval3OLD  16696  gsumval3  16699  gsumzcl2  16703  gsumzclOLD  16707  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumconst  16742  gsumzmhm  16745  gsumzmhmOLD  16746  gsumzoppg  16755  gsumzoppgOLD  16756  zringlpirlem2  18274  zringlpirlem3  18275  zlpirlem2  18279  zlpirlem3  18280  lmcnp  19568  lmmo  19644  1stcelcls  19725  1stccnp  19726  1stckgenlem  19786  1stckgen  19787  imasdsf1olem  20608  lmnn  21434  cmetcaulem  21459  iscmet2  21465  causs  21469  caubl  21478  iscmet3i  21482  bcthlem5  21499  ovolsf  21616  ovollb2lem  21631  ovolctb  21633  ovolunlem1a  21639  ovolunlem1  21640  ovoliunlem1  21645  ovoliun  21648  ovoliun2  21649  ovoliunnul  21650  ovolscalem1  21656  ovolicc1  21659  ovolicc2lem2  21661  ovolicc2lem3  21662  ovolicc2lem4  21663  iundisj  21690  iundisj2  21691  voliunlem1  21692  voliunlem2  21693  voliunlem3  21694  iunmbl  21695  volsup  21698  ioombl1lem4  21703  uniioovol  21720  uniioombllem2  21724  uniioombllem3  21726  uniioombllem4  21727  uniioombllem6  21729  vitalilem4  21752  vitalilem5  21753  itg1climres  21853  mbfi1fseqlem6  21859  mbfi1flimlem  21861  mbfmullem2  21863  itg2monolem1  21889  itg2i1fseqle  21893  itg2i1fseq  21894  itg2i1fseq2  21895  itg2addlem  21897  plyeq0lem  22339  vieta1lem2  22438  elqaalem1  22446  elqaalem3  22448  aaliou3lem4  22473  aaliou3lem7  22476  dvtaylp  22496  taylthlem2  22500  pserdvlem2  22554  pserdv2  22556  abelthlem6  22562  abelthlem9  22566  logtayl  22766  logtaylsum  22767  logtayl2  22768  atantayl  22993  leibpilem2  22997  leibpi  22998  birthdaylem2  23007  dfef2  23025  divsqrtsumlem  23034  emcllem2  23051  emcllem4  23053  emcllem5  23054  emcllem6  23055  emcllem7  23056  harmonicbnd4  23065  fsumharmonic  23066  wilthlem3  23069  ftalem2  23072  ftalem4  23074  ftalem5  23075  basellem5  23083  basellem6  23084  basellem7  23085  basellem8  23086  basellem9  23087  ppiprm  23150  ppinprm  23151  chtprm  23152  chtnprm  23153  chpp1  23154  vma1  23165  ppiltx  23176  prmorcht  23177  chtlepsi  23206  fsumvma2  23214  chpchtsum  23219  chpub  23220  logfacbnd3  23223  logexprlim  23225  bposlem5  23288  lgscllem  23303  lgsval2lem  23306  lgsval4a  23318  lgsneg  23319  lgsdir  23330  lgsdilem2  23331  lgsdi  23332  lgsne0  23333  lgsquadlem2  23355  chebbnd1lem1  23379  chtppilimlem1  23383  rplogsumlem1  23394  rplogsumlem2  23395  rpvmasumlem  23397  dchrisumlema  23398  dchrisumlem2  23400  dchrisumlem3  23401  dchrmusum2  23404  dchrvmasum2lem  23406  dchrvmasumiflem1  23411  dchrvmaeq0  23414  dchrisum0flblem2  23419  dchrisum0flb  23420  dchrisum0re  23423  dchrisum0lem1b  23425  dchrisum0lem1  23426  dchrisum0lem2a  23427  dchrisum0lem2  23428  dchrisum0lem3  23429  mudivsum  23440  mulogsum  23442  logdivsum  23443  mulog2sumlem2  23445  log2sumbnd  23454  selberg2lem  23460  logdivbnd  23466  pntrsumo1  23475  pntrsumbnd2  23477  pntrlog2bndlem2  23488  pntrlog2bndlem4  23490  pntrlog2bndlem6a  23492  pntlemf  23515  eedimeq  23874  axlowdimlem6  23923  axlowdimlem16  23933  axlowdimlem17  23934  axlowdim  23937  eupath2lem3  24652  gxnn0suc  24939  nvlmle  25275  ipval2  25290  minvecolem3  25465  minvecolem4b  25467  minvecolem4  25469  h2hcau  25569  h2hlm  25570  hlimadd  25783  hlim0  25826  hhsscms  25868  occllem  25894  nlelchi  26653  opsqrlem4  26735  hmopidmchi  26743  iundisjf  27118  iundisj2f  27119  fzssnn  27260  ssnnssfz  27262  iundisjfi  27266  iundisj2fi  27267  lmlim  27562  rge0scvg  27564  lmxrge0  27567  lmdvg  27568  rnlogblem  27652  esumfzf  27712  esumfsup  27713  esumpcvgval  27721  esumpmono  27722  esumcvg  27729  eulerpartlemsv2  27934  eulerpartlems  27936  eulerpartlemsv3  27937  eulerpartlemv  27940  eulerpartlemb  27944  fiblem  27974  fibp1  27977  rrvsum  28030  dstfrvclim1  28053  ballotlemsup  28080  ballotlem1ri  28110  signsvfn  28176  zetacvg  28194  lgamgulmlem4  28211  lgamgulmlem6  28213  lgamgulm2  28215  lgamcvglem  28219  lgamcvg2  28234  gamcvg  28235  gamcvg2lem  28238  regamcl  28240  relgamcl  28241  lgam1  28243  subfacp1lem1  28260  subfacp1lem5  28265  subfacp1lem6  28266  erdszelem7  28278  cvmliftlem5  28371  cvmliftlem7  28373  cvmliftlem10  28376  cvmliftlem13  28378  sinccvglem  28510  sinccvg  28511  circum  28512  divcnvshft  28591  divcnvlin  28592  prodeq2ii  28619  prodmolem3  28639  prodmolem2a  28640  fprod  28647  prod0  28649  prod1  28650  fprodss  28654  fprodser  28655  fprodcl2lem  28656  fprodmul  28664  fproddiv  28665  fprodn0  28683  iprodgam  28699  fallfacval4  28739  faclimlem1  28742  faclimlem2  28743  faclim  28745  iprodfac  28746  faclim2  28747  prednn  28855  bpoly4  29395  mblfinlem2  29627  ovoliunnfl  29631  voliunnfl  29633  volsupnfl  29634  lmclim2  29852  geomcau  29853  heibor1lem  29906  heibor1  29907  bfplem1  29919  bfplem2  29920  rrncmslem  29929  rrncms  29930  eldioph3b  30300  diophin  30308  diophun  30309  diophren  30349  jm3.1lem2  30564  dgraalem  30699  dgraaub  30702  lcmcllem  30802  lcmledvds  30805  hashnzfz2  30826  hashnzfzclim  30827  clim1fr1  31143  sumnnodd  31172  stoweidlem7  31307  stoweidlem14  31314  stoweidlem20  31320  stoweidlem34  31334  wallispilem5  31369  wallispi  31370  stirlinglem1  31374  stirlinglem5  31378  stirlinglem7  31380  stirlinglem8  31381  stirlinglem10  31383  stirlinglem11  31384  stirlinglem12  31385  stirlinglem13  31386  stirlinglem14  31387  stirlinglem15  31388  stirlingr  31390  dirkertrigeqlem2  31399  dirkertrigeqlem3  31400  fourierdlem11  31418  fourierdlem31  31438  fourierdlem48  31455  fourierdlem49  31456  fourierdlem69  31476  fourierdlem73  31480  fourierdlem81  31488  fourierdlem93  31500  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fouriersw  31532
  Copyright terms: Public domain W3C validator