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

Theorem nnuz 12270
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 11999 . 2 ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2 1z 12001 . . 3 1 ∈ ℤ
3 uzval 12234 . . 3 (1 ∈ ℤ → (ℤ‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
51, 4eqtr4i 2847 1 ℕ = (ℤ‘1)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  {crab 3142   class class class wbr 5058  cfv 6349  1c1 10527  cle 10665  cn 11627  cz 11970  cuz 12232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-z 11971  df-uz 12233
This theorem is referenced by:  elnnuz  12271  eluz2nn  12273  uznnssnn  12284  nnwo  12302  eluznn  12307  nninf  12318  fzssnn  12941  fseq1p1m1  12971  prednn  13020  elfzo1  13077  ltwenn  13320  nnnfi  13324  ser1const  13416  expp1  13426  digit1  13588  facnn  13625  fac0  13626  facp1  13628  faclbnd4lem1  13643  bcm1k  13665  bcval5  13668  bcpasc  13671  fz1isolem  13809  seqcoll  13812  seqcoll2  13813  climuni  14899  isercolllem2  15012  isercoll  15014  sumeq2ii  15040  summolem3  15061  summolem2a  15062  fsum  15067  sum0  15068  sumz  15069  fsumcl2lem  15078  fsumadd  15086  fsummulc2  15129  fsumrelem  15152  isumnn0nn  15187  climcndslem1  15194  climcndslem2  15195  climcnds  15196  divcnv  15198  divcnvshft  15200  supcvg  15201  trireciplem  15207  trirecip  15208  expcnv  15209  geo2lim  15221  geoisum1  15225  geoisum1c  15226  mertenslem2  15231  prodeq2ii  15257  prodmolem3  15277  prodmolem2a  15278  fprod  15285  prod0  15287  prod1  15288  fprodss  15292  fprodser  15293  fprodcl2lem  15294  fprodmul  15304  fproddiv  15305  fprodn0  15323  fallfacval4  15387  bpoly4  15403  ege2le3  15433  rpnnen2lem3  15559  rpnnen2lem5  15561  rpnnen2lem8  15564  rpnnen2lem12  15568  ruclem6  15578  pwp1fsum  15732  bezoutlem2  15878  bezoutlem3  15879  lcmcllem  15930  lcmledvds  15933  lcmfval  15955  lcmfcllem  15959  lcmfledvds  15966  isprm3  16017  phicl2  16095  phibndlem  16097  eulerthlem2  16109  odzcllem  16119  odzdvds  16122  iserodd  16162  pcmptcl  16217  pcmpt  16218  pockthlem  16231  pockthg  16232  unbenlem  16234  prmreclem3  16244  prmreclem5  16246  prmreclem6  16247  prmrec  16248  1arith  16253  4sqlem13  16283  4sqlem14  16284  4sqlem17  16287  4sqlem18  16288  vdwlem1  16307  vdwlem2  16308  vdwlem3  16309  vdwlem6  16312  vdwlem8  16314  vdwlem10  16316  vdw  16320  vdwnnlem3  16323  prmlem1a  16430  mulgnnp1  18176  mulgnnsubcl  18180  mulgnn0z  18194  mulgnndir  18196  mulgpropd  18209  odfval  18591  odlem1  18594  odlem2  18598  gexlem1  18635  gexlem2  18638  gexcl3  18643  sylow1lem1  18654  efgsdmi  18789  efgsrel  18791  efgs1b  18793  efgsp1  18794  mulgnn0di  18877  lt6abl  18946  gsumval3eu  18955  gsumval3  18958  gsumzcl2  18961  gsumzaddlem  18972  gsumconst  18985  gsumzmhm  18988  gsumzoppg  18995  zringlpirlem2  20562  zringlpirlem3  20563  lmcnp  21842  lmmo  21918  1stcelcls  21999  1stccnp  22000  1stckgenlem  22091  1stckgen  22092  imasdsf1olem  22912  cphipval  23775  lmnn  23795  cmetcaulem  23820  iscmet2  23826  causs  23830  nglmle  23834  caubl  23840  iscmet3i  23844  bcthlem5  23860  ovolsf  24002  ovollb2lem  24018  ovolctb  24020  ovolunlem1a  24026  ovolunlem1  24027  ovoliunlem1  24032  ovoliun  24035  ovoliun2  24036  ovoliunnul  24037  ovolscalem1  24043  ovolicc1  24046  ovolicc2lem2  24048  ovolicc2lem3  24049  ovolicc2lem4  24050  iundisj  24078  iundisj2  24079  voliunlem1  24080  voliunlem2  24081  voliunlem3  24082  volsup  24086  ioombl1lem4  24091  uniioovol  24109  uniioombllem2  24113  uniioombllem3  24115  uniioombllem4  24116  uniioombllem6  24118  vitalilem4  24141  vitalilem5  24142  itg1climres  24244  mbfi1fseqlem6  24250  mbfi1flimlem  24252  mbfmullem2  24254  itg2monolem1  24280  itg2i1fseqle  24284  itg2i1fseq  24285  itg2i1fseq2  24286  itg2addlem  24288  plyeq0lem  24729  vieta1lem2  24829  elqaalem1  24837  elqaalem3  24839  aaliou3lem4  24864  aaliou3lem7  24867  dvtaylp  24887  taylthlem2  24891  pserdvlem2  24945  pserdv2  24947  abelthlem6  24953  abelthlem9  24957  logtayl  25170  logtaylsum  25171  logtayl2  25172  atantayl  25442  leibpilem2  25447  leibpi  25448  birthdaylem2  25458  dfef2  25476  divsqrtsumlem  25485  emcllem2  25502  emcllem4  25504  emcllem5  25505  emcllem6  25506  emcllem7  25507  harmonicbnd4  25516  fsumharmonic  25517  zetacvg  25520  lgamgulmlem4  25537  lgamgulmlem6  25539  lgamgulm2  25541  lgamcvglem  25545  lgamcvg2  25560  gamcvg  25561  gamcvg2lem  25564  regamcl  25566  relgamcl  25567  lgam1  25569  wilthlem3  25575  ftalem2  25579  ftalem4  25581  ftalem5  25582  basellem5  25590  basellem6  25591  basellem7  25592  basellem8  25593  basellem9  25594  ppiprm  25656  ppinprm  25657  chtprm  25658  chtnprm  25659  chpp1  25660  vma1  25671  ppiltx  25682  fsumvma2  25718  chpchtsum  25723  logfacbnd3  25727  logexprlim  25729  bposlem5  25792  lgscllem  25808  lgsval2lem  25811  lgsval4a  25823  lgsneg  25825  lgsdir  25836  lgsdilem2  25837  lgsdi  25838  lgsne0  25839  gausslemma2dlem3  25872  lgsquadlem2  25885  chebbnd1lem1  25973  chtppilimlem1  25977  rplogsumlem1  25988  rplogsumlem2  25989  rpvmasumlem  25991  dchrisumlema  25992  dchrisumlem2  25994  dchrisumlem3  25995  dchrmusum2  25998  dchrvmasum2lem  26000  dchrvmasumiflem1  26005  dchrvmaeq0  26008  dchrisum0flblem2  26013  dchrisum0flb  26014  dchrisum0re  26017  dchrisum0lem1b  26019  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  mudivsum  26034  mulogsum  26036  logdivsum  26037  mulog2sumlem2  26039  log2sumbnd  26048  selberg2lem  26054  logdivbnd  26060  pntrsumo1  26069  pntrsumbnd2  26071  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  pntrlog2bndlem6a  26086  pntlemf  26109  eedimeq  26612  axlowdimlem6  26661  axlowdimlem16  26671  axlowdimlem17  26672  ipval2  28412  minvecolem3  28581  minvecolem4b  28583  minvecolem4  28585  h2hcau  28684  h2hlm  28685  hlimadd  28898  hlim0  28940  hhsscms  28983  occllem  29008  nlelchi  29766  opsqrlem4  29848  hmopidmchi  29856  iundisjf  30268  iundisj2f  30269  ssnnssfz  30437  iundisjfi  30446  iundisj2fi  30447  cycpmco2lem7  30702  cycpmrn  30713  1smat1  30969  submat1n  30970  submatres  30971  submateqlem2  30973  lmatfval  30979  madjusmdetlem1  30992  madjusmdetlem2  30993  madjusmdetlem3  30994  madjusmdetlem4  30995  lmlim  31090  rge0scvg  31092  lmxrge0  31095  lmdvg  31096  esumfzf  31228  esumfsup  31229  esumpcvgval  31237  esumpmono  31238  esumcvg  31245  esumcvgsum  31247  esumsup  31248  fiunelros  31333  eulerpartlemsv2  31516  eulerpartlems  31518  eulerpartlemsv3  31519  eulerpartlemv  31522  eulerpartlemb  31526  fiblem  31556  fibp1  31559  rrvsum  31612  dstfrvclim1  31635  ballotlem1ri  31692  signsvfn  31752  chtvalz  31800  circlemethhgt  31814  subfacp1lem1  32324  subfacp1lem5  32329  subfacp1lem6  32330  erdszelem7  32342  cvmliftlem5  32434  cvmliftlem7  32436  cvmliftlem10  32439  cvmliftlem13  32441  sinccvg  32814  circum  32815  divcnvlin  32862  iprodgam  32872  faclimlem1  32873  faclimlem2  32874  faclim  32876  iprodfac  32877  faclim2  32878  poimirlem3  34777  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem12  34786  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  poimirlem24  34798  poimirlem25  34799  poimirlem27  34801  poimirlem28  34802  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  mblfinlem2  34812  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  lmclim2  34916  geomcau  34917  heibor1lem  34970  heibor1  34971  bfplem1  34983  bfplem2  34984  rrncmslem  34993  rrncms  34994  eldioph3b  39242  diophin  39249  diophun  39250  diophren  39290  jm3.1lem2  39495  dgraalem  39625  dgraaub  39628  dftrcl3  39945  trclfvdecomr  39953  hashnzfz2  40533  hashnzfzclim  40534  dvradcnv2  40559  binomcxplemnotnn0  40568  nnsplit  41506  clim1fr1  41762  sumnnodd  41791  limsup10exlem  41933  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  stoweidlem7  42173  stoweidlem14  42180  stoweidlem20  42186  stoweidlem34  42200  wallispilem5  42235  wallispi  42236  stirlinglem1  42240  stirlinglem5  42244  stirlinglem7  42246  stirlinglem8  42247  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  stirlinglem14  42253  stirlinglem15  42254  stirlingr  42256  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  fourierdlem11  42284  fourierdlem31  42304  fourierdlem48  42320  fourierdlem49  42321  fourierdlem69  42341  fourierdlem73  42345  fourierdlem81  42353  fourierdlem93  42365  fourierdlem103  42375  fourierdlem104  42376  fourierdlem112  42384  fouriersw  42397  sge0ad2en  42594  voliunsge0lem  42635  caragenunicl  42687  caratheodorylem2  42690  hoidmvlelem3  42760  ovolval2lem  42806  ovolval2  42807  vonioolem2  42844  vonicclem2  42847  fmtno4prmfac  43581
  Copyright terms: Public domain W3C validator