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

Theorem nnuz 12813
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 12538 . 2 ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2 1z 12540 . . 3 1 ∈ ℤ
3 uzval 12772 . . 3 (1 ∈ ℤ → (ℤ‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
51, 4eqtr4i 2768 1 ℕ = (ℤ‘1)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {crab 3410   class class class wbr 5110  cfv 6501  1c1 11059  cle 11197  cn 12160  cz 12506  cuz 12770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-z 12507  df-uz 12771
This theorem is referenced by:  elnnuz  12814  eluz2nn  12816  uznnssnn  12827  nnwo  12845  eluznn  12850  nninf  12861  fzssnn  13492  fseq1p1m1  13522  prednn  13571  elfzo1  13629  ltwenn  13874  nnnfi  13878  ser1const  13971  expp1  13981  digit1  14147  facnn  14182  fac0  14183  facp1  14185  faclbnd4lem1  14200  bcm1k  14222  bcval5  14225  bcpasc  14228  fz1isolem  14367  seqcoll  14370  seqcoll2  14371  climuni  15441  isercolllem2  15557  isercoll  15559  sumeq2ii  15585  summolem3  15606  summolem2a  15607  fsum  15612  sum0  15613  sumz  15614  fsumcl2lem  15623  fsumadd  15632  fsummulc2  15676  fsumrelem  15699  isumnn0nn  15734  climcndslem1  15741  climcndslem2  15742  climcnds  15743  divcnv  15745  divcnvshft  15747  supcvg  15748  trireciplem  15754  trirecip  15755  expcnv  15756  geo2lim  15767  geoisum1  15771  geoisum1c  15772  mertenslem2  15777  prodeq2ii  15803  prodmolem3  15823  prodmolem2a  15824  fprod  15831  prod0  15833  prod1  15834  fprodss  15838  fprodser  15839  fprodcl2lem  15840  fprodmul  15850  fproddiv  15851  fprodn0  15869  fallfacval4  15933  bpoly4  15949  ege2le3  15979  rpnnen2lem3  16105  rpnnen2lem5  16107  rpnnen2lem8  16110  rpnnen2lem12  16114  ruclem6  16124  pwp1fsum  16280  bezoutlem2  16428  bezoutlem3  16429  lcmcllem  16479  lcmledvds  16482  lcmfval  16504  lcmfcllem  16508  lcmfledvds  16515  isprm3  16566  phicl2  16647  phibndlem  16649  eulerthlem2  16661  odzcllem  16671  odzdvds  16674  iserodd  16714  pcmptcl  16770  pcmpt  16771  pockthlem  16784  pockthg  16785  unbenlem  16787  prmreclem3  16797  prmreclem5  16799  prmreclem6  16800  prmrec  16801  1arith  16806  4sqlem13  16836  4sqlem14  16837  4sqlem17  16840  4sqlem18  16841  vdwlem1  16860  vdwlem2  16861  vdwlem3  16862  vdwlem6  16865  vdwlem8  16867  vdwlem10  16869  vdw  16873  vdwnnlem3  16876  prmlem1a  16986  mulgnnp1  18891  mulgnnsubcl  18895  mulgnn0z  18910  mulgnndir  18912  mulgpropd  18925  odfval  19321  odlem1  19324  odlem2  19328  gexlem1  19368  gexlem2  19371  gexcl3  19376  sylow1lem1  19387  efgsdmi  19521  efgsrel  19523  efgs1b  19525  efgsp1  19526  mulgnn0di  19611  lt6abl  19679  gsumval3eu  19688  gsumval3  19691  gsumzcl2  19694  gsumzaddlem  19705  gsumconst  19718  gsumzmhm  19721  gsumzoppg  19728  zringlpirlem2  20900  zringlpirlem3  20901  lmcnp  22671  lmmo  22747  1stcelcls  22828  1stccnp  22829  1stckgenlem  22920  1stckgen  22921  imasdsf1olem  23742  cphipval  24623  lmnn  24643  cmetcaulem  24668  iscmet2  24674  causs  24678  nglmle  24682  caubl  24688  iscmet3i  24692  bcthlem5  24708  ovolsf  24852  ovollb2lem  24868  ovolctb  24870  ovolunlem1a  24876  ovolunlem1  24877  ovoliunlem1  24882  ovoliun  24885  ovoliun2  24886  ovoliunnul  24887  ovolscalem1  24893  ovolicc1  24896  ovolicc2lem2  24898  ovolicc2lem3  24899  ovolicc2lem4  24900  iundisj  24928  iundisj2  24929  voliunlem1  24930  voliunlem2  24931  voliunlem3  24932  volsup  24936  ioombl1lem4  24941  uniioovol  24959  uniioombllem2  24963  uniioombllem3  24965  uniioombllem4  24966  uniioombllem6  24968  vitalilem4  24991  vitalilem5  24992  itg1climres  25095  mbfi1fseqlem6  25101  mbfi1flimlem  25103  mbfmullem2  25105  itg2monolem1  25131  itg2i1fseqle  25135  itg2i1fseq  25136  itg2i1fseq2  25137  itg2addlem  25139  plyeq0lem  25587  vieta1lem2  25687  elqaalem1  25695  elqaalem3  25697  aaliou3lem4  25722  aaliou3lem7  25725  dvtaylp  25745  taylthlem2  25749  pserdvlem2  25803  pserdv2  25805  abelthlem6  25811  abelthlem9  25815  logtayl  26031  logtaylsum  26032  logtayl2  26033  atantayl  26303  leibpilem2  26307  leibpi  26308  birthdaylem2  26318  dfef2  26336  divsqrtsumlem  26345  emcllem2  26362  emcllem4  26364  emcllem5  26365  emcllem6  26366  emcllem7  26367  harmonicbnd4  26376  fsumharmonic  26377  zetacvg  26380  lgamgulmlem4  26397  lgamgulmlem6  26399  lgamgulm2  26401  lgamcvglem  26405  lgamcvg2  26420  gamcvg  26421  gamcvg2lem  26424  regamcl  26426  relgamcl  26427  lgam1  26429  wilthlem3  26435  ftalem2  26439  ftalem4  26441  ftalem5  26442  basellem5  26450  basellem6  26451  basellem7  26452  basellem8  26453  basellem9  26454  ppiprm  26516  ppinprm  26517  chtprm  26518  chtnprm  26519  chpp1  26520  vma1  26531  ppiltx  26542  fsumvma2  26578  chpchtsum  26583  logfacbnd3  26587  logexprlim  26589  bposlem5  26652  lgscllem  26668  lgsval2lem  26671  lgsval4a  26683  lgsneg  26685  lgsdir  26696  lgsdilem2  26697  lgsdi  26698  lgsne0  26699  gausslemma2dlem3  26732  lgsquadlem2  26745  chebbnd1lem1  26833  chtppilimlem1  26837  rplogsumlem1  26848  rplogsumlem2  26849  rpvmasumlem  26851  dchrisumlema  26852  dchrisumlem2  26854  dchrisumlem3  26855  dchrmusum2  26858  dchrvmasum2lem  26860  dchrvmasumiflem1  26865  dchrvmaeq0  26868  dchrisum0flblem2  26873  dchrisum0flb  26874  dchrisum0re  26877  dchrisum0lem1b  26879  dchrisum0lem1  26880  dchrisum0lem2a  26881  dchrisum0lem2  26882  dchrisum0lem3  26883  mudivsum  26894  mulogsum  26896  logdivsum  26897  mulog2sumlem2  26899  log2sumbnd  26908  selberg2lem  26914  logdivbnd  26920  pntrsumo1  26929  pntrsumbnd2  26931  pntrlog2bndlem2  26942  pntrlog2bndlem4  26944  pntrlog2bndlem6a  26946  pntlemf  26969  eedimeq  27889  axlowdimlem6  27938  axlowdimlem16  27948  axlowdimlem17  27949  ipval2  29691  minvecolem3  29860  minvecolem4b  29862  minvecolem4  29864  h2hcau  29963  h2hlm  29964  hlimadd  30177  hlim0  30219  hhsscms  30262  occllem  30287  nlelchi  31045  opsqrlem4  31127  hmopidmchi  31135  iundisjf  31549  iundisj2f  31550  ssnnssfz  31732  iundisjfi  31741  iundisj2fi  31742  cycpmco2lem7  32023  cycpmrn  32034  1smat1  32425  submat1n  32426  submatres  32427  submateqlem2  32429  lmatfval  32435  madjusmdetlem1  32448  madjusmdetlem2  32449  madjusmdetlem3  32450  madjusmdetlem4  32451  lmlim  32568  rge0scvg  32570  lmxrge0  32573  lmdvg  32574  esumfzf  32708  esumfsup  32709  esumpcvgval  32717  esumpmono  32718  esumcvg  32725  esumcvgsum  32727  esumsup  32728  fiunelros  32813  eulerpartlemsv2  32998  eulerpartlems  33000  eulerpartlemsv3  33001  eulerpartlemv  33004  eulerpartlemb  33008  fiblem  33038  fibp1  33041  rrvsum  33094  dstfrvclim1  33117  ballotlem1ri  33174  signsvfn  33234  chtvalz  33282  circlemethhgt  33296  subfacp1lem1  33813  subfacp1lem5  33818  subfacp1lem6  33819  erdszelem7  33831  cvmliftlem5  33923  cvmliftlem7  33925  cvmliftlem10  33928  cvmliftlem13  33930  sinccvg  34301  circum  34302  divcnvlin  34344  iprodgam  34354  faclimlem1  34355  faclimlem2  34356  faclim  34358  iprodfac  34359  faclim2  34360  poimirlem3  36110  poimirlem4  36111  poimirlem6  36113  poimirlem7  36114  poimirlem8  36115  poimirlem12  36119  poimirlem15  36122  poimirlem16  36123  poimirlem17  36124  poimirlem18  36125  poimirlem19  36126  poimirlem20  36127  poimirlem22  36129  poimirlem23  36130  poimirlem24  36131  poimirlem25  36132  poimirlem27  36134  poimirlem28  36135  poimirlem29  36136  poimirlem30  36137  poimirlem31  36138  mblfinlem2  36145  ovoliunnfl  36149  voliunnfl  36151  volsupnfl  36152  lmclim2  36246  geomcau  36247  heibor1lem  36297  heibor1  36298  bfplem1  36310  bfplem2  36311  rrncmslem  36320  rrncms  36321  aks4d1p1p1  40549  sticksstones10  40592  sticksstones12a  40594  metakunt20  40625  nna4b4nsq  41027  eldioph3b  41117  diophin  41124  diophun  41125  diophren  41165  jm3.1lem2  41371  dgraalem  41501  dgraaub  41504  dftrcl3  42066  trclfvdecomr  42074  hashnzfz2  42675  hashnzfzclim  42676  dvradcnv2  42701  binomcxplemnotnn0  42710  nnsplit  43666  rexanuz2nf  43802  clim1fr1  43916  sumnnodd  43945  limsup10exlem  44087  fprodsubrecnncnvlem  44222  fprodaddrecnncnvlem  44224  stoweidlem7  44322  stoweidlem14  44329  stoweidlem20  44335  stoweidlem34  44349  wallispilem5  44384  wallispi  44385  stirlinglem1  44389  stirlinglem5  44393  stirlinglem7  44395  stirlinglem8  44396  stirlinglem10  44398  stirlinglem11  44399  stirlinglem12  44400  stirlinglem13  44401  stirlinglem14  44402  stirlinglem15  44403  stirlingr  44405  dirkertrigeqlem2  44414  dirkertrigeqlem3  44415  fourierdlem11  44433  fourierdlem31  44453  fourierdlem48  44469  fourierdlem49  44470  fourierdlem69  44490  fourierdlem73  44494  fourierdlem81  44502  fourierdlem93  44514  fourierdlem103  44524  fourierdlem104  44525  fourierdlem112  44533  fouriersw  44546  sge0ad2en  44746  voliunsge0lem  44787  caragenunicl  44839  caratheodorylem2  44842  hoidmvlelem3  44912  ovolval2lem  44958  ovolval2  44959  vonioolem2  44996  vonicclem2  44999  fmtno4prmfac  45838
  Copyright terms: Public domain W3C validator