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

Theorem nnuz 11127
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 10899 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10901 . . 3  |-  1  e.  ZZ
3 uzval 11094 . . 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 2475 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    e. wcel 1804   {crab 2797   class class class wbr 4437   ` cfv 5578   1c1 9496    <_ cle 9632   NNcn 10543   ZZcz 10871   ZZ>=cuz 11092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-z 10872  df-uz 11093
This theorem is referenced by:  elnnuz  11128  eluz2nn  11130  uznnssnn  11139  nnwo  11158  eluznn  11163  nninfm  11173  fseq1p1m1  11763  elfzo1  11853  ltwenn  12055  ser1const  12145  expp1  12155  digit1  12282  facnn  12337  fac0  12338  facp1  12340  faclbnd4lem1  12353  bcm1k  12375  bcval5  12378  bcpasc  12381  fz1isolem  12492  seqcoll  12494  seqcoll2  12495  climuni  13357  isercolllem2  13470  isercoll  13472  sumeq2ii  13497  summolem3  13518  summolem2a  13519  fsum  13524  sum0  13525  sumz  13526  fsumcl2lem  13535  fsumadd  13543  fsummulc2  13581  fsumrelem  13603  isumnn0nn  13636  climcndslem1  13643  climcndslem2  13644  climcnds  13645  divcnv  13647  supcvg  13649  trireciplem  13655  trirecip  13656  expcnv  13657  geo2lim  13666  geoisum1  13670  geoisum1c  13671  mertenslem2  13676  prodeq2ii  13702  prodmolem3  13722  prodmolem2a  13723  fprod  13730  prod0  13732  prod1  13733  fprodss  13737  fprodser  13738  fprodcl2lem  13739  fprodmul  13747  fproddiv  13748  fprodn0  13765  ege2le3  13807  rpnnen2lem3  13932  rpnnen2lem5  13934  rpnnen2lem8  13937  rpnnen2  13941  ruclem6  13950  bezoutlem2  14159  bezoutlem3  14160  isprm3  14208  phicl2  14280  phibndlem  14282  eulerthlem2  14294  odzcllem  14301  odzdvds  14304  iserodd  14341  pcmptcl  14392  pcmpt  14393  pockthlem  14405  pockthg  14406  unbenlem  14408  prmreclem3  14418  prmreclem5  14420  prmreclem6  14421  prmrec  14422  1arith  14427  4sqlem13  14457  4sqlem14  14458  4sqlem17  14461  4sqlem18  14462  vdwlem1  14481  vdwlem2  14482  vdwlem3  14483  vdwlem6  14486  vdwlem8  14488  vdwlem10  14490  vdw  14494  vdwnnlem1  14495  vdwnnlem3  14497  prmlem1a  14574  mulgnnp1  16129  mulgnnsubcl  16133  mulgnn0z  16141  mulgnndir  16143  mulgpropd  16154  odlem1  16538  odlem2  16542  gexlem1  16578  gexlem2  16581  gexcl3  16586  sylow1lem1  16597  efgsdmi  16729  efgsrel  16731  efgs1b  16733  efgsp1  16734  mulgnn0di  16813  lt6abl  16876  gsumval3eu  16886  gsumval3OLD  16887  gsumval3  16890  gsumzcl2  16894  gsumzclOLD  16898  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  gsumzoppg  16946  gsumzoppgOLD  16947  zringlpirlem2  18488  zringlpirlem3  18489  zlpirlem2  18493  zlpirlem3  18494  lmcnp  19783  lmmo  19859  1stcelcls  19940  1stccnp  19941  1stckgenlem  20032  1stckgen  20033  imasdsf1olem  20854  lmnn  21680  cmetcaulem  21705  iscmet2  21711  causs  21715  caubl  21724  iscmet3i  21728  bcthlem5  21745  ovolsf  21862  ovollb2lem  21877  ovolctb  21879  ovolunlem1a  21885  ovolunlem1  21886  ovoliunlem1  21891  ovoliun  21894  ovoliun2  21895  ovoliunnul  21896  ovolscalem1  21902  ovolicc1  21905  ovolicc2lem2  21907  ovolicc2lem3  21908  ovolicc2lem4  21909  iundisj  21936  iundisj2  21937  voliunlem1  21938  voliunlem2  21939  voliunlem3  21940  volsup  21944  ioombl1lem4  21949  uniioovol  21966  uniioombllem2  21970  uniioombllem3  21972  uniioombllem4  21973  uniioombllem6  21975  vitalilem4  21998  vitalilem5  21999  itg1climres  22099  mbfi1fseqlem6  22105  mbfi1flimlem  22107  mbfmullem2  22109  itg2monolem1  22135  itg2i1fseqle  22139  itg2i1fseq  22140  itg2i1fseq2  22141  itg2addlem  22143  plyeq0lem  22585  vieta1lem2  22685  elqaalem1  22693  elqaalem3  22695  aaliou3lem4  22720  aaliou3lem7  22723  dvtaylp  22743  taylthlem2  22747  pserdvlem2  22801  pserdv2  22803  abelthlem6  22809  abelthlem9  22813  logtayl  23019  logtaylsum  23020  logtayl2  23021  atantayl  23246  leibpilem2  23250  leibpi  23251  birthdaylem2  23260  dfef2  23278  divsqrtsumlem  23287  emcllem2  23304  emcllem4  23306  emcllem5  23307  emcllem6  23308  emcllem7  23309  harmonicbnd4  23318  fsumharmonic  23319  wilthlem3  23322  ftalem2  23325  ftalem4  23327  ftalem5  23328  basellem5  23336  basellem6  23337  basellem7  23338  basellem8  23339  basellem9  23340  ppiprm  23403  ppinprm  23404  chtprm  23405  chtnprm  23406  chpp1  23407  vma1  23418  ppiltx  23429  fsumvma2  23467  chpchtsum  23472  logfacbnd3  23476  logexprlim  23478  bposlem5  23541  lgscllem  23556  lgsval2lem  23559  lgsval4a  23571  lgsneg  23572  lgsdir  23583  lgsdilem2  23584  lgsdi  23585  lgsne0  23586  lgsquadlem2  23608  chebbnd1lem1  23632  chtppilimlem1  23636  rplogsumlem1  23647  rplogsumlem2  23648  rpvmasumlem  23650  dchrisumlema  23651  dchrisumlem2  23653  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasum2lem  23659  dchrvmasumiflem1  23664  dchrvmaeq0  23667  dchrisum0flblem2  23672  dchrisum0flb  23673  dchrisum0re  23676  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  dchrisum0lem2  23681  dchrisum0lem3  23682  mudivsum  23693  mulogsum  23695  logdivsum  23696  mulog2sumlem2  23698  log2sumbnd  23707  selberg2lem  23713  logdivbnd  23719  pntrsumo1  23728  pntrsumbnd2  23730  pntrlog2bndlem2  23741  pntrlog2bndlem4  23743  pntrlog2bndlem6a  23745  pntlemf  23768  eedimeq  24179  axlowdimlem6  24228  axlowdimlem16  24238  axlowdimlem17  24239  eupath2lem3  24957  gxnn0suc  25244  nvlmle  25580  ipval2  25595  minvecolem3  25770  minvecolem4b  25772  minvecolem4  25774  h2hcau  25874  h2hlm  25875  hlimadd  26088  hlim0  26131  hhsscms  26173  occllem  26199  nlelchi  26958  opsqrlem4  27040  hmopidmchi  27048  iundisjf  27426  iundisj2f  27427  fzssnn  27573  ssnnssfz  27575  iundisjfi  27579  iundisj2fi  27580  lmlim  27907  rge0scvg  27909  lmxrge0  27912  lmdvg  27913  esumfzf  28053  esumfsup  28054  esumpcvgval  28062  esumpmono  28063  esumcvg  28070  eulerpartlemsv2  28275  eulerpartlems  28277  eulerpartlemsv3  28278  eulerpartlemv  28281  eulerpartlemb  28285  fiblem  28315  fibp1  28318  rrvsum  28371  dstfrvclim1  28394  ballotlemsup  28421  ballotlem1ri  28451  signsvfn  28517  zetacvg  28535  lgamgulmlem4  28552  lgamgulmlem6  28554  lgamgulm2  28556  lgamcvglem  28560  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  regamcl  28581  relgamcl  28582  lgam1  28584  subfacp1lem1  28601  subfacp1lem5  28606  subfacp1lem6  28607  erdszelem7  28619  cvmliftlem5  28712  cvmliftlem7  28714  cvmliftlem10  28717  cvmliftlem13  28719  sinccvg  29017  circum  29018  divcnvshft  29095  divcnvlin  29096  iprodgam  29101  fallfacval4  29141  faclimlem1  29144  faclimlem2  29145  faclim  29147  iprodfac  29148  faclim2  29149  prednn  29257  bpoly4  29797  mblfinlem2  30028  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  lmclim2  30227  geomcau  30228  heibor1lem  30281  heibor1  30282  bfplem1  30294  bfplem2  30295  rrncmslem  30304  rrncms  30305  eldioph3b  30674  diophin  30682  diophun  30683  diophren  30723  jm3.1lem2  30936  dgraalem  31070  dgraaub  31073  lcmcllem  31178  lcmledvds  31181  hashnzfz2  31202  hashnzfzclim  31203  clim1fr1  31561  sumnnodd  31590  stoweidlem7  31743  stoweidlem14  31750  stoweidlem20  31756  stoweidlem34  31770  wallispilem5  31805  wallispi  31806  stirlinglem1  31810  stirlinglem5  31814  stirlinglem7  31816  stirlinglem8  31817  stirlinglem10  31819  stirlinglem11  31820  stirlinglem12  31821  stirlinglem13  31822  stirlinglem14  31823  stirlinglem15  31824  stirlingr  31826  dirkertrigeqlem2  31835  dirkertrigeqlem3  31836  fourierdlem11  31854  fourierdlem31  31874  fourierdlem48  31891  fourierdlem49  31892  fourierdlem69  31912  fourierdlem73  31916  fourierdlem81  31924  fourierdlem93  31936  fourierdlem103  31946  fourierdlem104  31947  fourierdlem112  31955  fouriersw  31968
  Copyright terms: Public domain W3C validator