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

Theorem nnuz 10884
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 10662 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10664 . . 3  |-  1  e.  ZZ
3 uzval 10851 . . 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 2456 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755   {crab 2709   class class class wbr 4280   ` cfv 5406   1c1 9271    <_ cle 9407   NNcn 10310   ZZcz 10634   ZZ>=cuz 10849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-recs 6818  df-rdg 6852  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-nn 10311  df-z 10635  df-uz 10850
This theorem is referenced by:  elnnuz  10885  uznnssnn  10890  nnwo  10908  eluznn  10913  nninfm  10923  fseq1p1m1  11518  elfzo1  11579  ltwenn  11769  ser1const  11846  expp1  11856  digit1  11982  facnn  12037  fac0  12038  facp1  12040  faclbnd4lem1  12053  bcm1k  12075  bcval5  12078  bcpasc  12081  fz1isolem  12198  seqcoll  12200  seqcoll2  12201  climuni  13014  isercolllem2  13127  isercoll  13129  sumeq2ii  13154  summolem3  13175  summolem2a  13176  fsum  13181  sum0  13182  sumz  13183  fsumcl2lem  13192  fsumadd  13199  fsummulc2  13234  fsumrelem  13253  isumnn0nn  13288  climcndslem1  13295  climcndslem2  13296  climcnds  13297  divcnv  13299  supcvg  13301  trireciplem  13307  trirecip  13308  expcnv  13309  geo2lim  13318  geoisum1  13322  geoisum1c  13323  mertenslem2  13328  ege2le3  13358  rpnnen2lem3  13482  rpnnen2lem5  13484  rpnnen2lem8  13487  rpnnen2  13491  ruclem6  13500  bezoutlem2  13706  bezoutlem3  13707  isprm3  13755  phicl2  13826  phibndlem  13828  eulerthlem2  13840  odzcllem  13847  odzdvds  13850  iserodd  13885  pcmptcl  13936  pcmpt  13937  pockthlem  13949  pockthg  13950  unbenlem  13952  prmreclem3  13962  prmreclem5  13964  prmreclem6  13965  prmrec  13966  1arith  13971  4sqlem13  14001  4sqlem14  14002  4sqlem17  14005  4sqlem18  14006  vdwlem1  14025  vdwlem2  14026  vdwlem3  14027  vdwlem6  14030  vdwlem8  14032  vdwlem10  14034  vdw  14038  vdwnnlem1  14039  vdwnnlem3  14041  prmlem1a  14117  mulgnnp1  15615  mulgnnsubcl  15619  mulgnn0z  15627  mulgnndir  15629  mulgpropd  15640  odlem1  16018  odlem2  16022  gexlem1  16058  gexlem2  16061  gexcl3  16066  sylow1lem1  16077  efgsdmi  16209  efgsrel  16211  efgs1b  16213  efgsp1  16214  mulgnn0di  16293  lt6abl  16351  gsumval3eu  16361  gsumval3OLD  16362  gsumval3  16365  gsumzcl2  16369  gsumzclOLD  16373  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumconst  16406  gsumzmhm  16407  gsumzmhmOLD  16408  gsumzoppg  16416  gsumzoppgOLD  16417  zringlpirlem2  17746  zringlpirlem3  17747  zlpirlem2  17751  zlpirlem3  17752  lmcnp  18750  lmmo  18826  1stcelcls  18907  1stccnp  18908  1stckgenlem  18968  1stckgen  18969  imasdsf1olem  19790  lmnn  20616  cmetcaulem  20641  iscmet2  20647  causs  20651  caubl  20660  iscmet3i  20664  bcthlem5  20681  ovolsf  20798  ovollb2lem  20813  ovolctb  20815  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliun  20830  ovoliun2  20831  ovoliunnul  20832  ovolscalem1  20838  ovolicc1  20841  ovolicc2lem2  20843  ovolicc2lem3  20844  ovolicc2lem4  20845  iundisj  20871  iundisj2  20872  voliunlem1  20873  voliunlem2  20874  voliunlem3  20875  iunmbl  20876  volsup  20879  ioombl1lem4  20884  uniioovol  20901  uniioombllem2  20905  uniioombllem3  20907  uniioombllem4  20908  uniioombllem6  20910  vitalilem4  20933  vitalilem5  20934  itg1climres  21034  mbfi1fseqlem6  21040  mbfi1flimlem  21042  mbfmullem2  21044  itg2monolem1  21070  itg2i1fseqle  21074  itg2i1fseq  21075  itg2i1fseq2  21076  itg2addlem  21078  plyeq0lem  21563  vieta1lem2  21662  elqaalem1  21670  elqaalem3  21672  aaliou3lem4  21697  aaliou3lem7  21700  dvtaylp  21720  taylthlem2  21724  pserdvlem2  21778  pserdv2  21780  abelthlem6  21786  abelthlem9  21790  logtayl  21990  logtaylsum  21991  logtayl2  21992  atantayl  22217  leibpilem2  22221  leibpi  22222  birthdaylem2  22231  dfef2  22249  divsqrsumlem  22258  emcllem2  22275  emcllem4  22277  emcllem5  22278  emcllem6  22279  emcllem7  22280  harmonicbnd4  22289  fsumharmonic  22290  wilthlem3  22293  ftalem2  22296  ftalem4  22298  ftalem5  22299  basellem5  22307  basellem6  22308  basellem7  22309  basellem8  22310  basellem9  22311  ppiprm  22374  ppinprm  22375  chtprm  22376  chtnprm  22377  chpp1  22378  vma1  22389  ppiltx  22400  prmorcht  22401  chtlepsi  22430  fsumvma2  22438  chpchtsum  22443  chpub  22444  logfacbnd3  22447  logexprlim  22449  bposlem5  22512  lgscllem  22527  lgsval2lem  22530  lgsval4a  22542  lgsneg  22543  lgsdir  22554  lgsdilem2  22555  lgsdi  22556  lgsne0  22557  lgsquadlem2  22579  chebbnd1lem1  22603  chtppilimlem1  22607  rplogsumlem1  22618  rplogsumlem2  22619  rpvmasumlem  22621  dchrisumlema  22622  dchrisumlem2  22624  dchrisumlem3  22625  dchrmusum2  22628  dchrvmasum2lem  22630  dchrvmasumiflem1  22635  dchrvmaeq0  22638  dchrisum0flblem2  22643  dchrisum0flb  22644  dchrisum0re  22647  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0lem3  22653  mudivsum  22664  mulogsum  22666  logdivsum  22667  mulog2sumlem2  22669  log2sumbnd  22678  selberg2lem  22684  logdivbnd  22690  pntrsumo1  22699  pntrsumbnd2  22701  pntrlog2bndlem2  22712  pntrlog2bndlem4  22714  pntrlog2bndlem6a  22716  pntlemf  22739  eedimeq  22967  axlowdimlem6  23016  axlowdimlem16  23026  axlowdimlem17  23027  axlowdim  23030  eupath2lem3  23423  gxnn0suc  23574  nvlmle  23910  ipval2  23925  minvecolem3  24100  minvecolem4b  24102  minvecolem4  24104  h2hcau  24204  h2hlm  24205  hlimadd  24418  hlim0  24461  hhsscms  24503  occllem  24529  nlelchi  25288  opsqrlem4  25370  hmopidmchi  25378  iundisjf  25755  iundisj2f  25756  fzssnn  25897  ssnnssfz  25899  iundisjfi  25903  iundisj2fi  25904  lmlim  26231  rge0scvg  26233  lmxrge0  26236  lmdvg  26237  rnlogblem  26312  esumfzf  26372  esumfsup  26373  esumpcvgval  26381  esumpmono  26382  esumcvg  26389  eulerpartlemsv2  26589  eulerpartlems  26591  eulerpartlemsv3  26592  eulerpartlemv  26595  eulerpartlemb  26599  fiblem  26629  fibp1  26632  rrvsum  26685  dstfrvclim1  26708  ballotlemsup  26735  ballotlem1ri  26765  signsvfn  26831  zetacvg  26849  lgamgulmlem4  26866  lgamgulmlem6  26868  lgamgulm2  26870  lgamcvglem  26874  lgamcvg2  26889  gamcvg  26890  gamcvg2lem  26893  regamcl  26895  relgamcl  26896  lgam1  26898  subfacp1lem1  26915  subfacp1lem5  26920  subfacp1lem6  26921  erdszelem7  26933  cvmliftlem5  27026  cvmliftlem7  27028  cvmliftlem10  27031  cvmliftlem13  27033  sinccvglem  27164  sinccvg  27165  circum  27166  divcnvshft  27245  divcnvlin  27246  prodeq2ii  27273  prodmolem3  27293  prodmolem2a  27294  fprod  27301  prod0  27303  prod1  27304  fprodss  27308  fprodser  27309  fprodcl2lem  27310  fprodmul  27318  fproddiv  27319  fprodn0  27337  iprodgam  27353  fallfacval4  27393  faclimlem1  27396  faclimlem2  27397  faclim  27399  iprodfac  27400  faclim2  27401  prednn  27509  bpoly4  28049  mblfinlem2  28273  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  lmclim2  28498  geomcau  28499  heibor1lem  28552  heibor1  28553  bfplem1  28565  bfplem2  28566  rrncmslem  28575  rrncms  28576  eldioph3b  28948  diophin  28956  diophun  28957  diophren  28997  jm3.1lem2  29212  dgraalem  29347  dgraaub  29350  clim1fr1  29620  stoweidlem7  29648  stoweidlem14  29655  stoweidlem20  29661  stoweidlem34  29675  wallispilem5  29710  wallispi  29711  stirlinglem1  29715  stirlinglem5  29719  stirlinglem7  29721  stirlinglem8  29722  stirlinglem10  29724  stirlinglem11  29725  stirlinglem12  29726  stirlinglem13  29727  stirlinglem14  29728  stirlinglem15  29729  stirlingr  29731  uz2nn  30037
  Copyright terms: Public domain W3C validator