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

Theorem nnuz 11228
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 10999 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 11001 . . 3  |-  1  e.  ZZ
3 uzval 11195 . . 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 2487 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455    e. wcel 1898   {crab 2753   class class class wbr 4418   ` cfv 5605   1c1 9571    <_ cle 9707   NNcn 10642   ZZcz 10971   ZZ>=cuz 11193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-z 10972  df-uz 11194
This theorem is referenced by:  elnnuz  11229  eluz2nn  11231  uznnssnn  11240  nnwo  11258  eluznn  11263  nninf  11274  nninfmOLD  11276  fzssnn  11877  fseq1p1m1  11903  prednn  11949  elfzo1  12002  ltwenn  12214  ser1const  12307  expp1  12317  digit1  12444  facnn  12499  fac0  12500  facp1  12502  faclbnd4lem1  12516  bcm1k  12538  bcval5  12541  bcpasc  12544  fz1isolem  12663  seqcoll  12666  seqcoll2  12667  climuni  13671  isercolllem2  13784  isercoll  13786  sumeq2ii  13814  summolem3  13835  summolem2a  13836  fsum  13841  sum0  13842  sumz  13843  fsumcl2lem  13852  fsumadd  13860  fsummulc2  13900  fsumrelem  13922  isumnn0nn  13955  climcndslem1  13962  climcndslem2  13963  climcnds  13964  divcnv  13966  divcnvshft  13968  supcvg  13969  trireciplem  13975  trirecip  13976  expcnv  13977  geo2lim  13986  geoisum1  13990  geoisum1c  13991  mertenslem2  13996  prodeq2ii  14022  prodmolem3  14042  prodmolem2a  14043  fprod  14050  prod0  14052  prod1  14053  fprodss  14057  fprodser  14058  fprodcl2lem  14059  fprodmul  14069  fproddiv  14070  fprodn0  14088  fallfacval4  14151  bpoly4  14167  ege2le3  14199  rpnnen2lem3  14324  rpnnen2lem5  14326  rpnnen2lem8  14329  rpnnen2  14333  ruclem6  14342  bezoutlem2OLD  14559  bezoutlem3OLD  14560  bezoutlem2  14562  bezoutlem3  14563  lcmcllem  14616  lcmledvds  14619  lcmscllemOLD  14637  lcmsledvdsOLD  14640  lcmfval  14646  lcmfvalOLD  14650  lcmfcllem  14653  lcmfledvds  14660  isprm3  14688  phicl2  14771  phibndlem  14773  eulerthlem2  14785  odzcllem  14792  odzdvds  14795  odzcllemOLD  14798  odzdvdsOLD  14801  iserodd  14840  pcmptcl  14891  pcmpt  14892  pockthlem  14904  pockthg  14905  unbenlem  14907  prmreclem3  14917  prmreclem5  14919  prmreclem6  14920  prmrec  14921  1arith  14926  4sqlem13OLD  14956  4sqlem14OLD  14957  4sqlem17OLD  14960  4sqlem18OLD  14961  4sqlem13  14962  4sqlem14  14963  4sqlem17  14966  4sqlem18  14967  vdwlem1  14986  vdwlem2  14987  vdwlem3  14988  vdwlem6  14991  vdwlem8  14993  vdwlem10  14995  vdw  14999  vdwnnlem1  15000  vdwnnlem3  15002  prmlem1a  15133  mulgnnp1  16821  mulgnnsubcl  16825  mulgnn0z  16833  mulgnndir  16835  mulgpropd  16846  odlem1  17236  odlem1OLD  17239  odlem2  17243  odlem2OLD  17259  gexlem1  17283  gexlem1OLD  17285  gexlem2  17288  gexlem2OLD  17291  gexcl3  17294  sylow1lem1  17305  efgsdmi  17437  efgsrel  17439  efgs1b  17441  efgsp1  17442  mulgnn0di  17521  lt6abl  17584  gsumval3eu  17593  gsumval3  17596  gsumzcl2  17599  gsumzaddlem  17609  gsumconst  17622  gsumzmhm  17625  gsumzoppg  17632  zringlpirlem2OLD  19109  zringlpirlem3OLD  19110  zringlpirlem2  19111  zringlpirlem3  19112  lmcnp  20375  lmmo  20451  1stcelcls  20531  1stccnp  20532  1stckgenlem  20623  1stckgen  20624  imasdsf1olem  21443  lmnn  22288  cmetcaulem  22313  iscmet2  22319  causs  22323  caubl  22332  iscmet3i  22336  bcthlem5  22351  ovolsf  22480  ovollb2lem  22496  ovolctb  22498  ovolunlem1a  22504  ovolunlem1  22505  ovoliunlem1  22510  ovoliun  22513  ovoliun2  22514  ovoliunnul  22515  ovolscalem1  22521  ovolicc1  22524  ovolicc2lem2  22526  ovolicc2lem3  22527  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  iundisj  22557  iundisj2  22558  voliunlem1  22559  voliunlem2  22560  voliunlem3  22561  volsup  22565  ioombl1lem4  22570  uniioovol  22592  uniioombllem2  22596  uniioombllem2OLD  22597  uniioombllem3  22599  uniioombllem4  22600  uniioombllem6  22602  vitalilem4  22625  vitalilem5  22626  itg1climres  22728  mbfi1fseqlem6  22734  mbfi1flimlem  22736  mbfmullem2  22738  itg2monolem1  22764  itg2i1fseqle  22768  itg2i1fseq  22769  itg2i1fseq2  22770  itg2addlem  22772  plyeq0lem  23220  vieta1lem2  23320  elqaalem1  23328  elqaalem3  23330  elqaalem1OLD  23331  elqaalem3OLD  23333  aaliou3lem4  23358  aaliou3lem7  23361  dvtaylp  23381  taylthlem2  23385  pserdvlem2  23439  pserdv2  23441  abelthlem6  23447  abelthlem9  23451  logtayl  23661  logtaylsum  23662  logtayl2  23663  atantayl  23919  leibpilem2  23923  leibpi  23924  birthdaylem2  23934  dfef2  23952  divsqrtsumlem  23961  emcllem2  23978  emcllem4  23980  emcllem5  23981  emcllem6  23982  emcllem7  23983  harmonicbnd4  23992  fsumharmonic  23993  zetacvg  23996  lgamgulmlem4  24013  lgamgulmlem6  24015  lgamgulm2  24017  lgamcvglem  24021  lgamcvg2  24036  gamcvg  24037  gamcvg2lem  24040  regamcl  24042  relgamcl  24043  lgam1  24045  wilthlem3  24051  ftalem2  24054  ftalem4  24056  ftalem5  24057  ftalem4OLD  24058  ftalem5OLD  24059  basellem5  24067  basellem6  24068  basellem7  24069  basellem8  24070  basellem9  24071  ppiprm  24134  ppinprm  24135  chtprm  24136  chtnprm  24137  chpp1  24138  vma1  24149  ppiltx  24160  fsumvma2  24198  chpchtsum  24203  logfacbnd3  24207  logexprlim  24209  bposlem5  24272  lgscllem  24287  lgsval2lem  24290  lgsval4a  24302  lgsneg  24303  lgsdir  24314  lgsdilem2  24315  lgsdi  24316  lgsne0  24317  lgsquadlem2  24339  chebbnd1lem1  24363  chtppilimlem1  24367  rplogsumlem1  24378  rplogsumlem2  24379  rpvmasumlem  24381  dchrisumlema  24382  dchrisumlem2  24384  dchrisumlem3  24385  dchrmusum2  24388  dchrvmasum2lem  24390  dchrvmasumiflem1  24395  dchrvmaeq0  24398  dchrisum0flblem2  24403  dchrisum0flb  24404  dchrisum0re  24407  dchrisum0lem1b  24409  dchrisum0lem1  24410  dchrisum0lem2a  24411  dchrisum0lem2  24412  dchrisum0lem3  24413  mudivsum  24424  mulogsum  24426  logdivsum  24427  mulog2sumlem2  24429  log2sumbnd  24438  selberg2lem  24444  logdivbnd  24450  pntrsumo1  24459  pntrsumbnd2  24461  pntrlog2bndlem2  24472  pntrlog2bndlem4  24474  pntrlog2bndlem6a  24476  pntlemf  24499  eedimeq  24984  axlowdimlem6  25033  axlowdimlem16  25043  axlowdimlem17  25044  eupath2lem3  25763  gxnn0suc  26048  nvlmle  26384  ipval2  26399  minvecolem3  26574  minvecolem4b  26576  minvecolem4  26578  minvecolem3OLD  26584  minvecolem4bOLD  26586  minvecolem4OLD  26588  h2hcau  26688  h2hlm  26689  hlimadd  26902  hlim0  26944  hhsscms  26986  occllem  27012  nlelchi  27770  opsqrlem4  27852  hmopidmchi  27860  iundisjf  28253  iundisj2f  28254  ssnnssfz  28419  iundisjfi  28424  iundisj2fi  28425  1smat1  28681  submat1n  28682  submatres  28683  submateqlem2  28685  lmatfval  28691  madjusmdetlem1  28704  madjusmdetlem2  28705  madjusmdetlem3  28706  madjusmdetlem4  28707  lmlim  28804  rge0scvg  28806  lmxrge0  28809  lmdvg  28810  esumfzf  28941  esumfsup  28942  esumpcvgval  28950  esumpmono  28951  esumcvg  28958  esumcvgsum  28960  esumsup  28961  fiunelros  29047  eulerpartlemsv2  29241  eulerpartlems  29243  eulerpartlemsv3  29244  eulerpartlemv  29247  eulerpartlemb  29251  fiblem  29281  fibp1  29284  rrvsum  29337  dstfrvclim1  29360  ballotlem1ri  29417  ballotlemsupOLD  29425  ballotlem1riOLD  29455  signsvfn  29521  subfacp1lem1  29952  subfacp1lem5  29957  subfacp1lem6  29958  erdszelem7  29970  cvmliftlem5  30062  cvmliftlem7  30064  cvmliftlem10  30067  cvmliftlem13  30069  sinccvg  30367  circum  30368  divcnvlin  30417  iprodgam  30428  faclimlem1  30429  faclimlem2  30430  faclim  30432  iprodfac  30433  faclim2  30434  poimirlem3  31989  poimirlem4  31990  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem12  31998  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem22  32008  poimirlem23  32009  poimirlem24  32010  poimirlem25  32011  poimirlem27  32013  poimirlem28  32014  poimirlem29  32015  poimirlem30  32016  poimirlem31  32017  mblfinlem2  32024  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  lmclim2  32133  geomcau  32134  heibor1lem  32187  heibor1  32188  bfplem1  32200  bfplem2  32201  rrncmslem  32210  rrncms  32211  eldioph3b  35653  diophin  35661  diophun  35662  diophren  35702  jm3.1lem2  35919  dgraalem  36053  dgraalemOLD  36054  dgraaub  36059  dgraaubOLD  36060  dftrcl3  36358  trclfvdecomr  36366  hashnzfz2  36715  hashnzfzclim  36716  dvradcnv2  36741  binomcxplemnotnn0  36750  nnnfi  37448  nnsplit  37656  clim1fr1  37765  sumnnodd  37796  stoweidlem7  37968  stoweidlem14  37975  stoweidlem20  37981  stoweidlem34  37996  wallispilem5  38032  wallispi  38033  stirlinglem1  38037  stirlinglem5  38041  stirlinglem7  38043  stirlinglem8  38044  stirlinglem10  38046  stirlinglem11  38047  stirlinglem12  38048  stirlinglem13  38049  stirlinglem14  38050  stirlinglem15  38051  stirlingr  38053  dirkertrigeqlem2  38062  dirkertrigeqlem3  38063  fourierdlem11  38081  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem48  38119  fourierdlem49  38120  fourierdlem69  38140  fourierdlem73  38144  fourierdlem81  38152  fourierdlem93  38164  fourierdlem103  38174  fourierdlem104  38175  fourierdlem112  38183  fouriersw  38196  sge0ad2en  38376  voliunsge0lem  38415  caragenunicl  38453  caratheodorylem2  38456  hoidmvlelem3  38526  ovolval2lem  38572  ovolval2  38573
  Copyright terms: Public domain W3C validator