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

Theorem nnuz 10997
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 10775 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10777 . . 3  |-  1  e.  ZZ
3 uzval 10964 . . 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 2483 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758   {crab 2799   class class class wbr 4390   ` cfv 5516   1c1 9384    <_ cle 9520   NNcn 10423   ZZcz 10747   ZZ>=cuz 10962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-recs 6932  df-rdg 6966  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-nn 10424  df-z 10748  df-uz 10963
This theorem is referenced by:  elnnuz  10998  uznnssnn  11003  nnwo  11021  eluznn  11026  nninfm  11036  fseq1p1m1  11635  elfzo1  11696  ltwenn  11886  ser1const  11963  expp1  11973  digit1  12099  facnn  12154  fac0  12155  facp1  12157  faclbnd4lem1  12170  bcm1k  12192  bcval5  12195  bcpasc  12198  fz1isolem  12316  seqcoll  12318  seqcoll2  12319  climuni  13132  isercolllem2  13245  isercoll  13247  sumeq2ii  13272  summolem3  13293  summolem2a  13294  fsum  13299  sum0  13300  sumz  13301  fsumcl2lem  13310  fsumadd  13317  fsummulc2  13353  fsumrelem  13372  isumnn0nn  13407  climcndslem1  13414  climcndslem2  13415  climcnds  13416  divcnv  13418  supcvg  13420  trireciplem  13426  trirecip  13427  expcnv  13428  geo2lim  13437  geoisum1  13441  geoisum1c  13442  mertenslem2  13447  ege2le3  13477  rpnnen2lem3  13601  rpnnen2lem5  13603  rpnnen2lem8  13606  rpnnen2  13610  ruclem6  13619  bezoutlem2  13825  bezoutlem3  13826  isprm3  13874  phicl2  13945  phibndlem  13947  eulerthlem2  13959  odzcllem  13966  odzdvds  13969  iserodd  14004  pcmptcl  14055  pcmpt  14056  pockthlem  14068  pockthg  14069  unbenlem  14071  prmreclem3  14081  prmreclem5  14083  prmreclem6  14084  prmrec  14085  1arith  14090  4sqlem13  14120  4sqlem14  14121  4sqlem17  14124  4sqlem18  14125  vdwlem1  14144  vdwlem2  14145  vdwlem3  14146  vdwlem6  14149  vdwlem8  14151  vdwlem10  14153  vdw  14157  vdwnnlem1  14158  vdwnnlem3  14160  prmlem1a  14236  mulgnnp1  15737  mulgnnsubcl  15741  mulgnn0z  15749  mulgnndir  15751  mulgpropd  15762  odlem1  16142  odlem2  16146  gexlem1  16182  gexlem2  16185  gexcl3  16190  sylow1lem1  16201  efgsdmi  16333  efgsrel  16335  efgs1b  16337  efgsp1  16338  mulgnn0di  16417  lt6abl  16475  gsumval3eu  16485  gsumval3OLD  16486  gsumval3  16489  gsumzcl2  16493  gsumzclOLD  16497  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumconst  16532  gsumzmhm  16535  gsumzmhmOLD  16536  gsumzoppg  16545  gsumzoppgOLD  16546  zringlpirlem2  18013  zringlpirlem3  18014  zlpirlem2  18018  zlpirlem3  18019  lmcnp  19024  lmmo  19100  1stcelcls  19181  1stccnp  19182  1stckgenlem  19242  1stckgen  19243  imasdsf1olem  20064  lmnn  20890  cmetcaulem  20915  iscmet2  20921  causs  20925  caubl  20934  iscmet3i  20938  bcthlem5  20955  ovolsf  21072  ovollb2lem  21087  ovolctb  21089  ovolunlem1a  21095  ovolunlem1  21096  ovoliunlem1  21101  ovoliun  21104  ovoliun2  21105  ovoliunnul  21106  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem2  21117  ovolicc2lem3  21118  ovolicc2lem4  21119  iundisj  21145  iundisj2  21146  voliunlem1  21147  voliunlem2  21148  voliunlem3  21149  iunmbl  21150  volsup  21153  ioombl1lem4  21158  uniioovol  21175  uniioombllem2  21179  uniioombllem3  21181  uniioombllem4  21182  uniioombllem6  21184  vitalilem4  21207  vitalilem5  21208  itg1climres  21308  mbfi1fseqlem6  21314  mbfi1flimlem  21316  mbfmullem2  21318  itg2monolem1  21344  itg2i1fseqle  21348  itg2i1fseq  21349  itg2i1fseq2  21350  itg2addlem  21352  plyeq0lem  21794  vieta1lem2  21893  elqaalem1  21901  elqaalem3  21903  aaliou3lem4  21928  aaliou3lem7  21931  dvtaylp  21951  taylthlem2  21955  pserdvlem2  22009  pserdv2  22011  abelthlem6  22017  abelthlem9  22021  logtayl  22221  logtaylsum  22222  logtayl2  22223  atantayl  22448  leibpilem2  22452  leibpi  22453  birthdaylem2  22462  dfef2  22480  divsqrsumlem  22489  emcllem2  22506  emcllem4  22508  emcllem5  22509  emcllem6  22510  emcllem7  22511  harmonicbnd4  22520  fsumharmonic  22521  wilthlem3  22524  ftalem2  22527  ftalem4  22529  ftalem5  22530  basellem5  22538  basellem6  22539  basellem7  22540  basellem8  22541  basellem9  22542  ppiprm  22605  ppinprm  22606  chtprm  22607  chtnprm  22608  chpp1  22609  vma1  22620  ppiltx  22631  prmorcht  22632  chtlepsi  22661  fsumvma2  22669  chpchtsum  22674  chpub  22675  logfacbnd3  22678  logexprlim  22680  bposlem5  22743  lgscllem  22758  lgsval2lem  22761  lgsval4a  22773  lgsneg  22774  lgsdir  22785  lgsdilem2  22786  lgsdi  22787  lgsne0  22788  lgsquadlem2  22810  chebbnd1lem1  22834  chtppilimlem1  22838  rplogsumlem1  22849  rplogsumlem2  22850  rpvmasumlem  22852  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusum2  22859  dchrvmasum2lem  22861  dchrvmasumiflem1  22866  dchrvmaeq0  22869  dchrisum0flblem2  22874  dchrisum0flb  22875  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  mudivsum  22895  mulogsum  22897  logdivsum  22898  mulog2sumlem2  22900  log2sumbnd  22909  selberg2lem  22915  logdivbnd  22921  pntrsumo1  22930  pntrsumbnd2  22932  pntrlog2bndlem2  22943  pntrlog2bndlem4  22945  pntrlog2bndlem6a  22947  pntlemf  22970  eedimeq  23279  axlowdimlem6  23328  axlowdimlem16  23338  axlowdimlem17  23339  axlowdim  23342  eupath2lem3  23735  gxnn0suc  23886  nvlmle  24222  ipval2  24237  minvecolem3  24412  minvecolem4b  24414  minvecolem4  24416  h2hcau  24516  h2hlm  24517  hlimadd  24730  hlim0  24773  hhsscms  24815  occllem  24841  nlelchi  25600  opsqrlem4  25682  hmopidmchi  25690  iundisjf  26065  iundisj2f  26066  fzssnn  26208  ssnnssfz  26210  iundisjfi  26214  iundisj2fi  26215  lmlim  26511  rge0scvg  26513  lmxrge0  26516  lmdvg  26517  rnlogblem  26592  esumfzf  26652  esumfsup  26653  esumpcvgval  26661  esumpmono  26662  esumcvg  26669  eulerpartlemsv2  26875  eulerpartlems  26877  eulerpartlemsv3  26878  eulerpartlemv  26881  eulerpartlemb  26885  fiblem  26915  fibp1  26918  rrvsum  26971  dstfrvclim1  26994  ballotlemsup  27021  ballotlem1ri  27051  signsvfn  27117  zetacvg  27135  lgamgulmlem4  27152  lgamgulmlem6  27154  lgamgulm2  27156  lgamcvglem  27160  lgamcvg2  27175  gamcvg  27176  gamcvg2lem  27179  regamcl  27181  relgamcl  27182  lgam1  27184  subfacp1lem1  27201  subfacp1lem5  27206  subfacp1lem6  27207  erdszelem7  27219  cvmliftlem5  27312  cvmliftlem7  27314  cvmliftlem10  27317  cvmliftlem13  27319  sinccvglem  27451  sinccvg  27452  circum  27453  divcnvshft  27532  divcnvlin  27533  prodeq2ii  27560  prodmolem3  27580  prodmolem2a  27581  fprod  27588  prod0  27590  prod1  27591  fprodss  27595  fprodser  27596  fprodcl2lem  27597  fprodmul  27605  fproddiv  27606  fprodn0  27624  iprodgam  27640  fallfacval4  27680  faclimlem1  27683  faclimlem2  27684  faclim  27686  iprodfac  27687  faclim2  27688  prednn  27796  bpoly4  28336  mblfinlem2  28567  ovoliunnfl  28571  voliunnfl  28573  volsupnfl  28574  lmclim2  28792  geomcau  28793  heibor1lem  28846  heibor1  28847  bfplem1  28859  bfplem2  28860  rrncmslem  28869  rrncms  28870  eldioph3b  29241  diophin  29249  diophun  29250  diophren  29290  jm3.1lem2  29505  dgraalem  29640  dgraaub  29643  clim1fr1  29912  stoweidlem7  29940  stoweidlem14  29947  stoweidlem20  29953  stoweidlem34  29967  wallispilem5  30002  wallispi  30003  stirlinglem1  30007  stirlinglem5  30011  stirlinglem7  30013  stirlinglem8  30014  stirlinglem10  30016  stirlinglem11  30017  stirlinglem12  30018  stirlinglem13  30019  stirlinglem14  30020  stirlinglem15  30021  stirlingr  30023  uz2nn  30329
  Copyright terms: Public domain W3C validator