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

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

Proof of Theorem nnuz
StepHypRef Expression
1 nnzrab 10301 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10303 . . 3  |-  1  e.  ZZ
3 uzval 10482 . . 3  |-  ( 1  e.  ZZ  ->  ( ZZ>=
`  1 )  =  { k  e.  ZZ  |  1  <_  k } )
42, 3ax-mp 8 . 2  |-  ( ZZ>= ` 
1 )  =  {
k  e.  ZZ  | 
1  <_  k }
51, 4eqtr4i 2458 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725   {crab 2701   class class class wbr 4204   ` cfv 5446   1c1 8983    <_ cle 9113   NNcn 9992   ZZcz 10274   ZZ>=cuz 10480
This theorem is referenced by:  elnnuz  10514  uznnssnn  10516  nnwo  10534  nninfm  10548  fseq1p1m1  11114  elfzo1  11165  ltwenn  11294  ser1const  11371  expp1  11380  expmulnbnd  11503  digit1  11505  facnn  11560  fac0  11561  facp1  11563  faclbnd4lem1  11576  bcm1k  11598  bcval5  11601  bcpasc  11604  fz1isolem  11702  seqcoll  11704  seqcoll2  11705  climuni  12338  isercolllem1  12450  isercolllem2  12451  isercoll  12453  sumeq2ii  12479  summolem3  12500  summolem2a  12501  fsum  12506  sum0  12507  sumz  12508  fsumcl2lem  12517  fsumadd  12524  fsummulc2  12559  fsumrelem  12578  o1fsum  12584  isumnn0nn  12614  climcndslem1  12621  climcndslem2  12622  climcnds  12623  divcnv  12625  supcvg  12627  trireciplem  12633  trirecip  12634  expcnv  12635  geo2lim  12644  geoisum1  12648  geoisum1c  12649  mertenslem2  12654  ege2le3  12684  rpnnen2lem3  12808  rpnnen2lem5  12810  rpnnen2lem6  12811  rpnnen2lem7  12812  rpnnen2lem8  12813  rpnnen2lem9  12814  rpnnen2lem11  12816  rpnnen2  12817  ruclem6  12826  bezoutlem2  13031  bezoutlem3  13032  isprm3  13080  phicl2  13149  phibndlem  13151  eulerthlem2  13163  odzcllem  13170  odzdvds  13173  iserodd  13201  pcmptcl  13252  pcmpt  13253  pcmpt2  13254  pcmptdvds  13255  pockthlem  13265  pockthg  13266  unbenlem  13268  prmreclem3  13278  prmreclem4  13279  prmreclem5  13280  prmreclem6  13281  prmrec  13282  1arith  13287  4sqlem13  13317  4sqlem14  13318  4sqlem17  13321  4sqlem18  13322  vdwlem1  13341  vdwlem2  13342  vdwlem3  13343  vdwlem6  13346  vdwlem8  13348  vdwlem10  13350  vdw  13354  vdwnnlem1  13355  vdwnnlem2  13356  vdwnnlem3  13357  2expltfac  13418  prmlem1a  13421  mulgnnp1  14890  mulgnnsubcl  14894  mulgnn0z  14902  mulgnndir  14904  mulgpropd  14915  odlem1  15165  odlem2  15169  gexlem1  15205  gexlem2  15208  gexcl3  15213  sylow1lem1  15224  efgsdmi  15356  efgsrel  15358  efgs1b  15360  efgsp1  15361  mulgnn0di  15440  lt6abl  15496  gsumval3eu  15505  gsumval3  15506  gsumzcl  15510  gsumzaddlem  15518  gsumconst  15524  gsumzmhm  15525  gsumzoppg  15531  zlpirlem2  16761  zlpirlem3  16762  lmcnp  17360  lmmo  17436  1stcelcls  17516  1stccnp  17517  1stckgenlem  17577  1stckgen  17578  imasdsf1olem  18395  lmnn  19208  cmetcaulem  19233  iscmet2  19239  causs  19243  caubl  19252  caublcls  19253  iscmet3i  19256  bcthlem5  19273  ovolsf  19361  ovollb2lem  19376  ovolctb  19378  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliun  19393  ovoliun2  19394  ovoliunnul  19395  ovolscalem1  19401  ovolicc1  19404  ovolicc2lem2  19406  ovolicc2lem3  19407  ovolicc2lem4  19408  iundisj  19434  iundisj2  19435  voliunlem1  19436  voliunlem2  19437  voliunlem3  19438  iunmbl  19439  volsuplem  19441  volsup  19442  ioombl1lem4  19447  uniioovol  19463  uniioombllem2  19467  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  vitalilem4  19495  vitalilem5  19496  itg1climres  19598  mbfi1fseqlem6  19604  mbfi1flimlem  19606  mbfmullem2  19608  itg2monolem1  19634  itg2i1fseqle  19638  itg2i1fseq  19639  itg2i1fseq2  19640  itg2addlem  19642  plyeq0lem  20121  vieta1lem2  20220  elqaalem1  20228  elqaalem3  20230  aaliou3lem4  20255  aaliou3lem7  20258  dvtaylp  20278  taylthlem2  20282  pserdvlem2  20336  pserdv2  20338  abelthlem6  20344  abelthlem9  20348  logtayl  20543  logtaylsum  20544  logtayl2  20545  atantayl  20769  leibpilem2  20773  leibpi  20774  birthdaylem2  20783  dfef2  20801  divsqrsumlem  20810  emcllem2  20827  emcllem4  20829  emcllem5  20830  emcllem6  20831  emcllem7  20832  harmonicbnd4  20841  fsumharmonic  20842  wilthlem3  20845  ftalem2  20848  ftalem4  20850  ftalem5  20851  basellem5  20859  basellem6  20860  basellem7  20861  basellem8  20862  basellem9  20863  ppiprm  20926  ppinprm  20927  chtprm  20928  chtnprm  20929  chpp1  20930  vma1  20941  ppiltx  20952  prmorcht  20953  chtlepsi  20982  chtub  20988  fsumvma2  20990  chpchtsum  20995  chpub  20996  logfacbnd3  20999  logexprlim  21001  bclbnd  21056  bposlem3  21062  bposlem4  21063  bposlem5  21064  bposlem6  21065  lgscllem  21079  lgsval2lem  21082  lgsval4a  21094  lgsneg  21095  lgsdir  21106  lgsdilem2  21107  lgsdi  21108  lgsne0  21109  lgsquadlem2  21131  chebbnd1lem1  21155  chebbnd1lem2  21156  chebbnd1lem3  21157  chtppilimlem1  21159  rplogsumlem1  21170  rplogsumlem2  21171  rpvmasumlem  21173  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  dchrmusum2  21180  dchrvmasum2lem  21182  dchrvmasumiflem1  21187  dchrvmaeq0  21190  dchrisum0flblem2  21195  dchrisum0flb  21196  dchrisum0re  21199  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2a  21203  dchrisum0lem2  21204  dchrisum0lem3  21205  mudivsum  21216  mulogsum  21218  logdivsum  21219  mulog2sumlem2  21221  log2sumbnd  21230  selberg2lem  21236  logdivbnd  21242  pntrsumo1  21251  pntrsumbnd2  21253  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  pntrlog2bndlem6a  21268  pntpbnd1  21272  pntpbnd2  21273  pntlemh  21285  pntlemq  21287  pntlemr  21288  pntlemj  21289  pntlemf  21291  eupath2lem3  21693  gxnn0suc  21844  nvlmle  22180  ipval2  22195  minvecolem3  22370  minvecolem4b  22372  minvecolem4  22374  h2hcau  22474  h2hlm  22475  hlimadd  22687  hlim0  22730  hhsscms  22771  occllem  22797  chscllem2  23132  nlelchi  23556  opsqrlem4  23638  hmopidmchi  23646  iundisjf  24021  iundisj2f  24022  fzssnn  24139  ssnnssfz  24140  iundisjfi  24144  iundisj2fi  24145  lmlim  24325  rge0scvg  24327  lmxrge0  24329  lmdvg  24330  rnlogblem  24391  esumfzf  24451  esumfsup  24452  esumpcvgval  24460  esumpmono  24461  esumcvg  24468  rrvsum  24704  dstfrvclim1  24727  ballotlemsup  24754  ballotlem1ri  24784  zetacvg  24791  lgamgulmlem4  24808  lgamgulmlem6  24810  lgamgulm2  24812  lgamcvglem  24816  lgamcvg2  24831  gamcvg  24832  gamcvg2lem  24835  regamcl  24837  relgamcl  24838  lgam1  24840  subfacp1lem1  24857  subfacp1lem5  24862  subfacp1lem6  24863  erdszelem7  24875  cvmliftlem5  24968  cvmliftlem7  24970  cvmliftlem10  24973  cvmliftlem13  24975  sinccvglem  25101  sinccvg  25102  circum  25103  divcnvshft  25203  divcnvlin  25204  prodeq2ii  25231  prodmolem3  25251  prodmolem2a  25252  fprod  25259  prod0  25261  prod1  25262  fprodss  25266  fprodser  25267  fprodcl2lem  25268  fprodmul  25276  fproddiv  25277  fprodn0  25295  iprodgam  25311  fallfacval4  25351  faclimlem1  25354  faclimlem2  25355  faclim  25357  iprodfac  25358  faclim2  25359  prednn  25468  eedimeq  25829  axlowdimlem6  25878  axlowdimlem16  25888  axlowdimlem17  25889  axlowdim  25892  bpoly4  26097  mblfinlem  26234  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  lmclim2  26455  geomcau  26456  heibor1lem  26509  heibor1  26510  bfplem1  26522  bfplem2  26523  rrncmslem  26532  rrncms  26533  eldioph3b  26814  diophin  26822  diophun  26823  diophren  26865  jm3.1lem2  27080  dgraalem  27318  dgraaub  27321  clim1fr1  27694  stoweidlem7  27723  stoweidlem14  27730  stoweidlem20  27736  stoweidlem34  27750  wallispilem5  27785  wallispi  27786  stirlinglem1  27790  stirlinglem5  27794  stirlinglem7  27796  stirlinglem8  27797  stirlinglem10  27799  stirlinglem11  27800  stirlinglem12  27801  stirlinglem13  27802  stirlinglem14  27803  stirlinglem15  27804  stirlingr  27806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-mulcom 9046  ax-addass 9047  ax-mulass 9048  ax-distr 9049  ax-i2m1 9050  ax-1ne0 9051  ax-1rid 9052  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055  ax-pre-lttri 9056  ax-pre-lttrn 9057  ax-pre-ltadd 9058  ax-pre-mulgt0 9059
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-riota 6541  df-recs 6625  df-rdg 6660  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-sub 9285  df-neg 9286  df-nn 9993  df-z 10275  df-uz 10481
  Copyright terms: Public domain W3C validator