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

Theorem nnuz 11557
Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
nnuz ℕ = (ℤ‘1)

Proof of Theorem nnuz
StepHypRef Expression
1 nnzrab 11240 . 2 ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2 1z 11242 . . 3 1 ∈ ℤ
3 uzval 11523 . . 3 (1 ∈ ℤ → (ℤ‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
51, 4eqtr4i 2634 1 ℕ = (ℤ‘1)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  {crab 2899   class class class wbr 4577  cfv 5789  1c1 9793  cle 9931  cn 10869  cz 11212  cuz 11521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10870  df-z 11213  df-uz 11522
This theorem is referenced by:  elnnuz  11558  eluz2nn  11560  uznnssnn  11569  nnwo  11587  eluznn  11592  nninf  11603  fzssnn  12213  fseq1p1m1  12240  prednn  12288  elfzo1  12342  ltwenn  12580  nnnfi  12584  ser1const  12676  expp1  12686  digit1  12817  facnn  12881  fac0  12882  facp1  12884  faclbnd4lem1  12899  bcm1k  12921  bcval5  12924  bcpasc  12927  fz1isolem  13056  seqcoll  13059  seqcoll2  13060  climuni  14079  isercolllem2  14192  isercoll  14194  sumeq2ii  14219  summolem3  14240  summolem2a  14241  fsum  14246  sum0  14247  sumz  14248  fsumcl2lem  14257  fsumadd  14265  fsummulc2  14306  fsumrelem  14328  isumnn0nn  14361  climcndslem1  14368  climcndslem2  14369  climcnds  14370  divcnv  14372  divcnvshft  14374  supcvg  14375  trireciplem  14381  trirecip  14382  expcnv  14383  geo2lim  14393  geoisum1  14397  geoisum1c  14398  mertenslem2  14404  prodeq2ii  14430  prodmolem3  14450  prodmolem2a  14451  fprod  14458  prod0  14460  prod1  14461  fprodss  14465  fprodser  14466  fprodcl2lem  14467  fprodmul  14477  fproddiv  14478  fprodn0  14496  fallfacval4  14561  bpoly4  14577  ege2le3  14607  rpnnen2lem3  14732  rpnnen2lem5  14734  rpnnen2lem8  14737  rpnnen2lem12  14741  ruclem6  14751  pwp1fsum  14900  bezoutlem2  15043  bezoutlem3  15044  lcmcllem  15095  lcmledvds  15098  lcmfval  15120  lcmfcllem  15124  lcmfledvds  15131  isprm3  15182  phicl2  15259  phibndlem  15261  eulerthlem2  15273  odzcllem  15283  odzdvds  15286  iserodd  15326  pcmptcl  15381  pcmpt  15382  pockthlem  15395  pockthg  15396  unbenlem  15398  prmreclem3  15408  prmreclem5  15410  prmreclem6  15411  prmrec  15412  1arith  15417  4sqlem13  15447  4sqlem14  15448  4sqlem17  15451  4sqlem18  15452  vdwlem1  15471  vdwlem2  15472  vdwlem3  15473  vdwlem6  15476  vdwlem8  15478  vdwlem10  15480  vdw  15484  vdwnnlem1  15485  vdwnnlem3  15487  prmlem1a  15599  mulgnnp1  17320  mulgnnsubcl  17324  mulgnn0z  17338  mulgnndir  17340  mulgnndirOLD  17341  mulgpropd  17355  odlem1  17725  odlem2  17729  gexlem1  17765  gexlem2  17768  gexcl3  17773  sylow1lem1  17784  efgsdmi  17916  efgsrel  17918  efgs1b  17920  efgsp1  17921  mulgnn0di  18002  lt6abl  18067  gsumval3eu  18076  gsumval3  18079  gsumzcl2  18082  gsumzaddlem  18092  gsumconst  18105  gsumzmhm  18108  gsumzoppg  18115  zringlpirlem2  19600  zringlpirlem3  19601  lmcnp  20865  lmmo  20941  1stcelcls  21021  1stccnp  21022  1stckgenlem  21113  1stckgen  21114  imasdsf1olem  21935  cphipval  22794  lmnn  22813  cmetcaulem  22838  iscmet2  22844  causs  22848  nglmle  22852  caubl  22858  iscmet3i  22862  bcthlem5  22877  ovolsf  22992  ovollb2lem  23007  ovolctb  23009  ovolunlem1a  23015  ovolunlem1  23016  ovoliunlem1  23021  ovoliun  23024  ovoliun2  23025  ovoliunnul  23026  ovolscalem1  23032  ovolicc1  23035  ovolicc2lem2  23037  ovolicc2lem3  23038  ovolicc2lem4  23039  iundisj  23067  iundisj2  23068  voliunlem1  23069  voliunlem2  23070  voliunlem3  23071  volsup  23075  ioombl1lem4  23080  uniioovol  23097  uniioombllem2  23101  uniioombllem3  23103  uniioombllem4  23104  uniioombllem6  23106  vitalilem4  23130  vitalilem5  23131  itg1climres  23231  mbfi1fseqlem6  23237  mbfi1flimlem  23239  mbfmullem2  23241  itg2monolem1  23267  itg2i1fseqle  23271  itg2i1fseq  23272  itg2i1fseq2  23273  itg2addlem  23275  plyeq0lem  23714  vieta1lem2  23814  elqaalem1  23822  elqaalem3  23824  aaliou3lem4  23849  aaliou3lem7  23852  dvtaylp  23872  taylthlem2  23876  pserdvlem2  23930  pserdv2  23932  abelthlem6  23938  abelthlem9  23942  logtayl  24150  logtaylsum  24151  logtayl2  24152  atantayl  24408  leibpilem2  24412  leibpi  24413  birthdaylem2  24423  dfef2  24441  divsqrtsumlem  24450  emcllem2  24467  emcllem4  24469  emcllem5  24470  emcllem6  24471  emcllem7  24472  harmonicbnd4  24481  fsumharmonic  24482  zetacvg  24485  lgamgulmlem4  24502  lgamgulmlem6  24504  lgamgulm2  24506  lgamcvglem  24510  lgamcvg2  24525  gamcvg  24526  gamcvg2lem  24529  regamcl  24531  relgamcl  24532  lgam1  24534  wilthlem3  24540  ftalem2  24544  ftalem4  24546  ftalem5  24547  basellem5  24555  basellem6  24556  basellem7  24557  basellem8  24558  basellem9  24559  ppiprm  24621  ppinprm  24622  chtprm  24623  chtnprm  24624  chpp1  24625  vma1  24636  ppiltx  24647  fsumvma2  24683  chpchtsum  24688  logfacbnd3  24692  logexprlim  24694  bposlem5  24757  lgscllem  24773  lgsval2lem  24776  lgsval4a  24788  lgsneg  24790  lgsdir  24801  lgsdilem2  24802  lgsdi  24803  lgsne0  24804  gausslemma2dlem3  24837  lgsquadlem2  24850  chebbnd1lem1  24902  chtppilimlem1  24906  rplogsumlem1  24917  rplogsumlem2  24918  rpvmasumlem  24920  dchrisumlema  24921  dchrisumlem2  24923  dchrisumlem3  24924  dchrmusum2  24927  dchrvmasum2lem  24929  dchrvmasumiflem1  24934  dchrvmaeq0  24937  dchrisum0flblem2  24942  dchrisum0flb  24943  dchrisum0re  24946  dchrisum0lem1b  24948  dchrisum0lem1  24949  dchrisum0lem2a  24950  dchrisum0lem2  24951  dchrisum0lem3  24952  mudivsum  24963  mulogsum  24965  logdivsum  24966  mulog2sumlem2  24968  log2sumbnd  24977  selberg2lem  24983  logdivbnd  24989  pntrsumo1  24998  pntrsumbnd2  25000  pntrlog2bndlem2  25011  pntrlog2bndlem4  25013  pntrlog2bndlem6a  25015  pntlemf  25038  eedimeq  25523  axlowdimlem6  25572  axlowdimlem16  25582  axlowdimlem17  25583  eupath2lem3  26299  ipval2  26739  minvecolem3  26909  minvecolem4b  26911  minvecolem4  26913  h2hcau  27013  h2hlm  27014  hlimadd  27227  hlim0  27269  hhsscms  27313  occllem  27339  nlelchi  28097  opsqrlem4  28179  hmopidmchi  28187  iundisjf  28577  iundisj2f  28578  ssnnssfz  28730  iundisjfi  28735  iundisj2fi  28736  1smat1  28991  submat1n  28992  submatres  28993  submateqlem2  28995  lmatfval  29001  madjusmdetlem1  29014  madjusmdetlem2  29015  madjusmdetlem3  29016  madjusmdetlem4  29017  lmlim  29114  rge0scvg  29116  lmxrge0  29119  lmdvg  29120  esumfzf  29251  esumfsup  29252  esumpcvgval  29260  esumpmono  29261  esumcvg  29268  esumcvgsum  29270  esumsup  29271  fiunelros  29357  eulerpartlemsv2  29540  eulerpartlems  29542  eulerpartlemsv3  29543  eulerpartlemv  29546  eulerpartlemb  29550  fiblem  29580  fibp1  29583  rrvsum  29636  dstfrvclim1  29659  ballotlem1ri  29716  signsvfn  29778  subfacp1lem1  30208  subfacp1lem5  30213  subfacp1lem6  30214  erdszelem7  30226  cvmliftlem5  30318  cvmliftlem7  30320  cvmliftlem10  30323  cvmliftlem13  30325  sinccvg  30614  circum  30615  divcnvlin  30664  iprodgam  30674  faclimlem1  30675  faclimlem2  30676  faclim  30678  iprodfac  30679  faclim2  30680  poimirlem3  32365  poimirlem4  32366  poimirlem6  32368  poimirlem7  32369  poimirlem8  32370  poimirlem12  32374  poimirlem15  32377  poimirlem16  32378  poimirlem17  32379  poimirlem18  32380  poimirlem19  32381  poimirlem20  32382  poimirlem22  32384  poimirlem23  32385  poimirlem24  32386  poimirlem25  32387  poimirlem27  32389  poimirlem28  32390  poimirlem29  32391  poimirlem30  32392  poimirlem31  32393  mblfinlem2  32400  ovoliunnfl  32404  voliunnfl  32406  volsupnfl  32407  lmclim2  32507  geomcau  32508  heibor1lem  32561  heibor1  32562  bfplem1  32574  bfplem2  32575  rrncmslem  32584  rrncms  32585  eldioph3b  36129  diophin  36137  diophun  36138  diophren  36178  jm3.1lem2  36386  dgraalem  36517  dgraaub  36520  dftrcl3  36814  trclfvdecomr  36822  hashnzfz2  37325  hashnzfzclim  37326  dvradcnv2  37351  binomcxplemnotnn0  37360  nnsplit  38298  clim1fr1  38451  sumnnodd  38480  fprodsubrecnncnvlem  38577  fprodaddrecnncnvlem  38579  stoweidlem7  38683  stoweidlem14  38690  stoweidlem20  38696  stoweidlem34  38710  wallispilem5  38745  wallispi  38746  stirlinglem1  38750  stirlinglem5  38754  stirlinglem7  38756  stirlinglem8  38757  stirlinglem10  38759  stirlinglem11  38760  stirlinglem12  38761  stirlinglem13  38762  stirlinglem14  38763  stirlinglem15  38764  stirlingr  38766  dirkertrigeqlem2  38775  dirkertrigeqlem3  38776  fourierdlem11  38794  fourierdlem31  38814  fourierdlem48  38830  fourierdlem49  38831  fourierdlem69  38851  fourierdlem73  38855  fourierdlem81  38863  fourierdlem93  38875  fourierdlem103  38885  fourierdlem104  38886  fourierdlem112  38894  fouriersw  38907  sge0ad2en  39107  voliunsge0lem  39148  caragenunicl  39197  caratheodorylem2  39200  hoidmvlelem3  39270  ovolval2lem  39316  ovolval2  39317  vonioolem2  39355  vonicclem2  39358  fmtno4prmfac  39806
  Copyright terms: Public domain W3C validator