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

Theorem nnuz 11145
Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
nnuz

Proof of Theorem nnuz
StepHypRef Expression
1 nnzrab 10917 . 2
2 1z 10919 . . 3
3 uzval 11112 . . 3
42, 3ax-mp 5 . 2
51, 4eqtr4i 2489 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  {crab 2811   class class class wbr 4452  `cfv 5593  1c1 9514   cle 9650   cn 10561   cz 10889   cuz 11110
This theorem is referenced by:  elnnuz  11146  eluz2nn  11148  uznnssnn  11157  nnwo  11176  eluznn  11181  nninfm  11191  fseq1p1m1  11781  elfzo1  11871  ltwenn  12073  ser1const  12163  expp1  12173  digit1  12300  facnn  12355  fac0  12356  facp1  12358  faclbnd4lem1  12371  bcm1k  12393  bcval5  12396  bcpasc  12399  fz1isolem  12510  seqcoll  12512  seqcoll2  12513  climuni  13375  isercolllem2  13488  isercoll  13490  sumeq2ii  13515  summolem3  13536  summolem2a  13537  fsum  13542  sum0  13543  sumz  13544  fsumcl2lem  13553  fsumadd  13561  fsummulc2  13599  fsumrelem  13621  isumnn0nn  13654  climcndslem1  13661  climcndslem2  13662  climcnds  13663  divcnv  13665  supcvg  13667  trireciplem  13673  trirecip  13674  expcnv  13675  geo2lim  13684  geoisum1  13688  geoisum1c  13689  mertenslem2  13694  prodeq2ii  13720  prodmolem3  13740  prodmolem2a  13741  fprod  13748  prod0  13750  prod1  13751  fprodss  13755  fprodser  13756  fprodcl2lem  13757  fprodmul  13765  fproddiv  13766  fprodn0  13783  ege2le3  13825  rpnnen2lem3  13950  rpnnen2lem5  13952  rpnnen2lem8  13955  rpnnen2  13959  ruclem6  13968  bezoutlem2  14177  bezoutlem3  14178  isprm3  14226  phicl2  14298  phibndlem  14300  eulerthlem2  14312  odzcllem  14319  odzdvds  14322  iserodd  14359  pcmptcl  14410  pcmpt  14411  pockthlem  14423  pockthg  14424  unbenlem  14426  prmreclem3  14436  prmreclem5  14438  prmreclem6  14439  prmrec  14440  1arith  14445  4sqlem13  14475  4sqlem14  14476  4sqlem17  14479  4sqlem18  14480  vdwlem1  14499  vdwlem2  14500  vdwlem3  14501  vdwlem6  14504  vdwlem8  14506  vdwlem10  14508  vdw  14512  vdwnnlem1  14513  vdwnnlem3  14515  prmlem1a  14592  mulgnnp1  16150  mulgnnsubcl  16154  mulgnn0z  16162  mulgnndir  16164  mulgpropd  16175  odlem1  16559  odlem2  16563  gexlem1  16599  gexlem2  16602  gexcl3  16607  sylow1lem1  16618  efgsdmi  16750  efgsrel  16752  efgs1b  16754  efgsp1  16755  mulgnn0di  16834  lt6abl  16897  gsumval3eu  16907  gsumval3OLD  16908  gsumval3  16911  gsumzcl2  16915  gsumzclOLD  16919  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  zringlpirlem2  18510  zringlpirlem3  18511  zlpirlem2  18515  zlpirlem3  18516  lmcnp  19805  lmmo  19881  1stcelcls  19962  1stccnp  19963  1stckgenlem  20054  1stckgen  20055  imasdsf1olem  20876  lmnn  21702  cmetcaulem  21727  iscmet2  21733  causs  21737  caubl  21746  iscmet3i  21750  bcthlem5  21767  ovolsf  21884  ovollb2lem  21899  ovolctb  21901  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliun  21916  ovoliun2  21917  ovoliunnul  21918  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem2  21929  ovolicc2lem3  21930  ovolicc2lem4  21931  iundisj  21958  iundisj2  21959  voliunlem1  21960  voliunlem2  21961  voliunlem3  21962  volsup  21966  ioombl1lem4  21971  uniioovol  21988  uniioombllem2  21992  uniioombllem3  21994  uniioombllem4  21995  uniioombllem6  21997  vitalilem4  22020  vitalilem5  22021  itg1climres  22121  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfmullem2  22131  itg2monolem1  22157  itg2i1fseqle  22161  itg2i1fseq  22162  itg2i1fseq2  22163  itg2addlem  22165  plyeq0lem  22607  vieta1lem2  22707  elqaalem1  22715  elqaalem3  22717  aaliou3lem4  22742  aaliou3lem7  22745  dvtaylp  22765  taylthlem2  22769  pserdvlem2  22823  pserdv2  22825  abelthlem6  22831  abelthlem9  22835  logtayl  23041  logtaylsum  23042  logtayl2  23043  atantayl  23268  leibpilem2  23272  leibpi  23273  birthdaylem2  23282  dfef2  23300  divsqrtsumlem  23309  emcllem2  23326  emcllem4  23328  emcllem5  23329  emcllem6  23330  emcllem7  23331  harmonicbnd4  23340  fsumharmonic  23341  wilthlem3  23344  ftalem2  23347  ftalem4  23349  ftalem5  23350  basellem5  23358  basellem6  23359  basellem7  23360  basellem8  23361  basellem9  23362  ppiprm  23425  ppinprm  23426  chtprm  23427  chtnprm  23428  chpp1  23429  vma1  23440  ppiltx  23451  fsumvma2  23489  chpchtsum  23494  logfacbnd3  23498  logexprlim  23500  bposlem5  23563  lgscllem  23578  lgsval2lem  23581  lgsval4a  23593  lgsneg  23594  lgsdir  23605  lgsdilem2  23606  lgsdi  23607  lgsne0  23608  lgsquadlem2  23630  chebbnd1lem1  23654  chtppilimlem1  23658  rplogsumlem1  23669  rplogsumlem2  23670  rpvmasumlem  23672  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  dchrmusum2  23679  dchrvmasum2lem  23681  dchrvmasumiflem1  23686  dchrvmaeq0  23689  dchrisum0flblem2  23694  dchrisum0flb  23695  dchrisum0re  23698  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  mudivsum  23715  mulogsum  23717  logdivsum  23718  mulog2sumlem2  23720  log2sumbnd  23729  selberg2lem  23735  logdivbnd  23741  pntrsumo1  23750  pntrsumbnd2  23752  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  pntrlog2bndlem6a  23767  pntlemf  23790  eedimeq  24201  axlowdimlem6  24250  axlowdimlem16  24260  axlowdimlem17  24261  eupath2lem3  24979  gxnn0suc  25266  nvlmle  25602  ipval2  25617  minvecolem3  25792  minvecolem4b  25794  minvecolem4  25796  h2hcau  25896  h2hlm  25897  hlimadd  26110  hlim0  26153  hhsscms  26195  occllem  26221  nlelchi  26980  opsqrlem4  27062  hmopidmchi  27070  iundisjf  27448  iundisj2f  27449  fzssnn  27595  ssnnssfz  27597  iundisjfi  27601  iundisj2fi  27602  lmlim  27929  rge0scvg  27931  lmxrge0  27934  lmdvg  27935  esumfzf  28075  esumfsup  28076  esumpcvgval  28084  esumpmono  28085  esumcvg  28092  eulerpartlemsv2  28297  eulerpartlems  28299  eulerpartlemsv3  28300  eulerpartlemv  28303  eulerpartlemb  28307  fiblem  28337  fibp1  28340  rrvsum  28393  dstfrvclim1  28416  ballotlemsup  28443  ballotlem1ri  28473  signsvfn  28539  zetacvg  28557  lgamgulmlem4  28574  lgamgulmlem6  28576  lgamgulm2  28578  lgamcvglem  28582  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  regamcl  28603  relgamcl  28604  lgam1  28606  subfacp1lem1  28623  subfacp1lem5  28628  subfacp1lem6  28629  erdszelem7  28641  cvmliftlem5  28734  cvmliftlem7  28736  cvmliftlem10  28739  cvmliftlem13  28741  sinccvg  29039  circum  29040  divcnvshft  29117  divcnvlin  29118  iprodgam  29125  fallfacval4  29165  faclimlem1  29168  faclimlem2  29169  faclim  29171  iprodfac  29172  faclim2  29173  prednn  29281  bpoly4  29821  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  lmclim2  30251  geomcau  30252  heibor1lem  30305  heibor1  30306  bfplem1  30318  bfplem2  30319  rrncmslem  30328  rrncms  30329  eldioph3b  30698  diophin  30706  diophun  30707  diophren  30747  jm3.1lem2  30960  dgraalem  31094  dgraaub  31097  lcmcllem  31202  lcmledvds  31205  hashnzfz2  31226  hashnzfzclim  31227  dvradcnv2  31252  binomcxplemnotnn0  31261  clim1fr1  31607  sumnnodd  31636  stoweidlem7  31789  stoweidlem14  31796  stoweidlem20  31802  stoweidlem34  31816  wallispilem5  31851  wallispi  31852  stirlinglem1  31856  stirlinglem5  31860  stirlinglem7  31862  stirlinglem8  31863  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  stirlingr  31872  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  fourierdlem11  31900  fourierdlem31  31920  fourierdlem48  31937  fourierdlem49  31938  fourierdlem69  31958  fourierdlem73  31962  fourierdlem81  31970  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fouriersw  32014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-nn 10562  df-z 10890  df-uz 11111
  Copyright terms: Public domain W3C validator