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

Theorem nnuz 10477
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 10265 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10267 . . 3  |-  1  e.  ZZ
3 uzval 10446 . . 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 2427 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   {crab 2670   class class class wbr 4172   ` cfv 5413   1c1 8947    <_ cle 9077   NNcn 9956   ZZcz 10238   ZZ>=cuz 10444
This theorem is referenced by:  elnnuz  10478  uznnssnn  10480  nnwo  10498  nninfm  10512  fseq1p1m1  11077  elfzo1  11128  ltwenn  11257  ser1const  11334  expp1  11343  expmulnbnd  11466  digit1  11468  facnn  11523  fac0  11524  facp1  11526  faclbnd4lem1  11539  bcm1k  11561  bcval5  11564  bcpasc  11567  fz1isolem  11665  seqcoll  11667  seqcoll2  11668  climuni  12301  isercolllem1  12413  isercolllem2  12414  isercoll  12416  sumeq2ii  12442  summolem3  12463  summolem2a  12464  fsum  12469  sum0  12470  sumz  12471  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumrelem  12541  o1fsum  12547  isumnn0nn  12577  climcndslem1  12584  climcndslem2  12585  climcnds  12586  divcnv  12588  supcvg  12590  trireciplem  12596  trirecip  12597  expcnv  12598  geo2lim  12607  geoisum1  12611  geoisum1c  12612  mertenslem2  12617  ege2le3  12647  rpnnen2lem3  12771  rpnnen2lem5  12773  rpnnen2lem6  12774  rpnnen2lem7  12775  rpnnen2lem8  12776  rpnnen2lem9  12777  rpnnen2lem11  12779  rpnnen2  12780  ruclem6  12789  bezoutlem2  12994  bezoutlem3  12995  isprm3  13043  phicl2  13112  phibndlem  13114  eulerthlem2  13126  odzcllem  13133  odzdvds  13136  iserodd  13164  pcmptcl  13215  pcmpt  13216  pcmpt2  13217  pcmptdvds  13218  pockthlem  13228  pockthg  13229  unbenlem  13231  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  prmrec  13245  1arith  13250  4sqlem13  13280  4sqlem14  13281  4sqlem17  13284  4sqlem18  13285  vdwlem1  13304  vdwlem2  13305  vdwlem3  13306  vdwlem6  13309  vdwlem8  13311  vdwlem10  13313  vdw  13317  vdwnnlem1  13318  vdwnnlem2  13319  vdwnnlem3  13320  2expltfac  13381  prmlem1a  13384  mulgnnp1  14853  mulgnnsubcl  14857  mulgnn0z  14865  mulgnndir  14867  mulgpropd  14878  odlem1  15128  odlem2  15132  gexlem1  15168  gexlem2  15171  gexcl3  15176  sylow1lem1  15187  efgsdmi  15319  efgsrel  15321  efgs1b  15323  efgsp1  15324  mulgnn0di  15403  lt6abl  15459  gsumval3eu  15468  gsumval3  15469  gsumzcl  15473  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  zlpirlem2  16724  zlpirlem3  16725  lmcnp  17322  lmmo  17398  1stcelcls  17477  1stccnp  17478  1stckgenlem  17538  1stckgen  17539  imasdsf1olem  18356  lmnn  19169  cmetcaulem  19194  iscmet2  19200  causs  19204  caubl  19213  caublcls  19214  iscmet3i  19217  bcthlem5  19234  ovolsf  19322  ovollb2lem  19337  ovolctb  19339  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliun  19354  ovoliun2  19355  ovoliunnul  19356  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem4  19369  iundisj  19395  iundisj2  19396  voliunlem1  19397  voliunlem2  19398  voliunlem3  19399  iunmbl  19400  volsuplem  19402  volsup  19403  ioombl1lem4  19408  uniioovol  19424  uniioombllem2  19428  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  vitalilem4  19456  vitalilem5  19457  itg1climres  19559  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfmullem2  19569  itg2monolem1  19595  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  plyeq0lem  20082  vieta1lem2  20181  elqaalem1  20189  elqaalem3  20191  aaliou3lem4  20216  aaliou3lem7  20219  dvtaylp  20239  taylthlem2  20243  pserdvlem2  20297  pserdv2  20299  abelthlem6  20305  abelthlem9  20309  logtayl  20504  logtaylsum  20505  logtayl2  20506  atantayl  20730  leibpilem2  20734  leibpi  20735  birthdaylem2  20744  dfef2  20762  divsqrsumlem  20771  emcllem2  20788  emcllem4  20790  emcllem5  20791  emcllem6  20792  emcllem7  20793  harmonicbnd4  20802  fsumharmonic  20803  wilthlem3  20806  ftalem2  20809  ftalem4  20811  ftalem5  20812  basellem5  20820  basellem6  20821  basellem7  20822  basellem8  20823  basellem9  20824  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  chpp1  20891  vma1  20902  ppiltx  20913  prmorcht  20914  chtlepsi  20943  chtub  20949  fsumvma2  20951  chpchtsum  20956  chpub  20957  logfacbnd3  20960  logexprlim  20962  bclbnd  21017  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  lgscllem  21040  lgsval2lem  21043  lgsval4a  21055  lgsneg  21056  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgsquadlem2  21092  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  chtppilimlem1  21120  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasum2lem  21143  dchrvmasumiflem1  21148  dchrvmaeq0  21151  dchrisum0flblem2  21156  dchrisum0flb  21157  dchrisum0re  21160  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  mudivsum  21177  mulogsum  21179  logdivsum  21180  mulog2sumlem2  21182  log2sumbnd  21191  selberg2lem  21197  logdivbnd  21203  pntrsumo1  21212  pntrsumbnd2  21214  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem6a  21229  pntpbnd1  21233  pntpbnd2  21234  pntlemh  21246  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemf  21252  eupath2lem3  21654  gxnn0suc  21805  nvlmle  22141  ipval2  22156  minvecolem3  22331  minvecolem4b  22333  minvecolem4  22335  h2hcau  22435  h2hlm  22436  hlimadd  22648  hlim0  22691  hhsscms  22732  occllem  22758  chscllem2  23093  nlelchi  23517  opsqrlem4  23599  hmopidmchi  23607  iundisjf  23982  iundisj2f  23983  fzssnn  24100  ssnnssfz  24101  iundisjfi  24105  iundisj2fi  24106  lmlim  24286  rge0scvg  24288  lmxrge0  24290  lmdvg  24291  rnlogblem  24352  esumfzf  24412  esumfsup  24413  esumpcvgval  24421  esumpmono  24422  esumcvg  24429  rrvsum  24665  dstfrvclim1  24688  ballotlemsup  24715  ballotlem1ri  24745  zetacvg  24752  lgamgulmlem4  24769  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvglem  24777  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  regamcl  24798  relgamcl  24799  lgam1  24801  subfacp1lem1  24818  subfacp1lem5  24823  subfacp1lem6  24824  erdszelem7  24836  cvmliftlem5  24929  cvmliftlem7  24931  cvmliftlem10  24934  cvmliftlem13  24936  sinccvglem  25062  sinccvg  25063  circum  25064  divcnvshft  25164  divcnvlin  25165  prodeq2ii  25192  prodmolem3  25212  prodmolem2a  25213  fprod  25220  prod0  25222  prod1  25223  fprodss  25227  fprodser  25228  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodn0  25256  iprodgam  25272  faclimlem1  25310  faclimlem2  25311  faclim  25313  iprodfac  25314  faclim2  25315  prednn  25415  eedimeq  25741  axlowdimlem6  25790  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  bpoly4  26009  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  lmclim2  26354  geomcau  26355  heibor1lem  26408  heibor1  26409  bfplem1  26421  bfplem2  26422  rrncmslem  26431  rrncms  26432  eldioph3b  26713  diophin  26721  diophun  26722  diophren  26764  jm3.1lem2  26979  dgraalem  27218  dgraaub  27221  clim1fr1  27594  stoweidlem7  27623  stoweidlem14  27630  stoweidlem20  27636  stoweidlem34  27650  wallispilem5  27685  wallispi  27686  stirlinglem1  27690  stirlinglem5  27694  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  stirlingr  27706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-z 10239  df-uz 10445
  Copyright terms: Public domain W3C validator