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

Theorem nnuz 11036
Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
nnuz  |-  NN  =  ( ZZ>= `  1 )

Proof of Theorem nnuz
StepHypRef Expression
1 nnzrab 10809 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10811 . . 3  |-  1  e.  ZZ
3 uzval 11003 . . 3  |-  ( 1  e.  ZZ  ->  ( ZZ>=
`  1 )  =  { k  e.  ZZ  |  1  <_  k } )
42, 3ax-mp 5 . 2  |-  ( ZZ>= ` 
1 )  =  {
k  e.  ZZ  | 
1  <_  k }
51, 4eqtr4i 2414 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399    e. wcel 1826   {crab 2736   class class class wbr 4367   ` cfv 5496   1c1 9404    <_ cle 9540   NNcn 10452   ZZcz 10781   ZZ>=cuz 11001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-recs 6960  df-rdg 6994  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-nn 10453  df-z 10782  df-uz 11002
This theorem is referenced by:  elnnuz  11037  eluz2nn  11039  uznnssnn  11048  nnwo  11066  eluznn  11071  nninfm  11081  fseq1p1m1  11674  elfzo1  11766  ltwenn  11976  ser1const  12066  expp1  12076  digit1  12202  facnn  12257  fac0  12258  facp1  12260  faclbnd4lem1  12273  bcm1k  12295  bcval5  12298  bcpasc  12301  fz1isolem  12414  seqcoll  12416  seqcoll2  12417  climuni  13377  isercolllem2  13490  isercoll  13492  sumeq2ii  13517  summolem3  13538  summolem2a  13539  fsum  13544  sum0  13545  sumz  13546  fsumcl2lem  13555  fsumadd  13563  fsummulc2  13601  fsumrelem  13623  isumnn0nn  13656  climcndslem1  13663  climcndslem2  13664  climcnds  13665  divcnv  13667  supcvg  13669  trireciplem  13675  trirecip  13676  expcnv  13677  geo2lim  13686  geoisum1  13690  geoisum1c  13691  mertenslem2  13696  prodeq2ii  13722  prodmolem3  13742  prodmolem2a  13743  fprod  13750  prod0  13752  prod1  13753  fprodss  13757  fprodser  13758  fprodcl2lem  13759  fprodmul  13767  fproddiv  13768  fprodn0  13785  ege2le3  13827  rpnnen2lem3  13952  rpnnen2lem5  13954  rpnnen2lem8  13957  rpnnen2  13961  ruclem6  13970  bezoutlem2  14179  bezoutlem3  14180  isprm3  14228  phicl2  14300  phibndlem  14302  eulerthlem2  14314  odzcllem  14321  odzdvds  14324  iserodd  14361  pcmptcl  14412  pcmpt  14413  pockthlem  14425  pockthg  14426  unbenlem  14428  prmreclem3  14438  prmreclem5  14440  prmreclem6  14441  prmrec  14442  1arith  14447  4sqlem13  14477  4sqlem14  14478  4sqlem17  14481  4sqlem18  14482  vdwlem1  14501  vdwlem2  14502  vdwlem3  14503  vdwlem6  14506  vdwlem8  14508  vdwlem10  14510  vdw  14514  vdwnnlem1  14515  vdwnnlem3  14517  prmlem1a  14594  mulgnnp1  16267  mulgnnsubcl  16271  mulgnn0z  16279  mulgnndir  16281  mulgpropd  16292  odlem1  16676  odlem2  16680  gexlem1  16716  gexlem2  16719  gexcl3  16724  sylow1lem1  16735  efgsdmi  16867  efgsrel  16869  efgs1b  16871  efgsp1  16872  mulgnn0di  16951  lt6abl  17014  gsumval3eu  17024  gsumval3OLD  17025  gsumval3  17028  gsumzcl2  17032  gsumzclOLD  17036  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumconst  17070  gsumzmhm  17073  gsumzmhmOLD  17074  gsumzoppg  17083  gsumzoppgOLD  17084  zringlpirlem2  18616  zringlpirlem3  18617  lmcnp  19891  lmmo  19967  1stcelcls  20047  1stccnp  20048  1stckgenlem  20139  1stckgen  20140  imasdsf1olem  20961  lmnn  21787  cmetcaulem  21812  iscmet2  21818  causs  21822  caubl  21831  iscmet3i  21835  bcthlem5  21852  ovolsf  21969  ovollb2lem  21984  ovolctb  21986  ovolunlem1a  21992  ovolunlem1  21993  ovoliunlem1  21998  ovoliun  22001  ovoliun2  22002  ovoliunnul  22003  ovolscalem1  22009  ovolicc1  22012  ovolicc2lem2  22014  ovolicc2lem3  22015  ovolicc2lem4  22016  iundisj  22043  iundisj2  22044  voliunlem1  22045  voliunlem2  22046  voliunlem3  22047  volsup  22051  ioombl1lem4  22056  uniioovol  22073  uniioombllem2  22077  uniioombllem3  22079  uniioombllem4  22080  uniioombllem6  22082  vitalilem4  22105  vitalilem5  22106  itg1climres  22206  mbfi1fseqlem6  22212  mbfi1flimlem  22214  mbfmullem2  22216  itg2monolem1  22242  itg2i1fseqle  22246  itg2i1fseq  22247  itg2i1fseq2  22248  itg2addlem  22250  plyeq0lem  22692  vieta1lem2  22792  elqaalem1  22800  elqaalem3  22802  aaliou3lem4  22827  aaliou3lem7  22830  dvtaylp  22850  taylthlem2  22854  pserdvlem2  22908  pserdv2  22910  abelthlem6  22916  abelthlem9  22920  logtayl  23128  logtaylsum  23129  logtayl2  23130  atantayl  23384  leibpilem2  23388  leibpi  23389  birthdaylem2  23399  dfef2  23417  divsqrtsumlem  23426  emcllem2  23443  emcllem4  23445  emcllem5  23446  emcllem6  23447  emcllem7  23448  harmonicbnd4  23457  fsumharmonic  23458  wilthlem3  23461  ftalem2  23464  ftalem4  23466  ftalem5  23467  basellem5  23475  basellem6  23476  basellem7  23477  basellem8  23478  basellem9  23479  ppiprm  23542  ppinprm  23543  chtprm  23544  chtnprm  23545  chpp1  23546  vma1  23557  ppiltx  23568  fsumvma2  23606  chpchtsum  23611  logfacbnd3  23615  logexprlim  23617  bposlem5  23680  lgscllem  23695  lgsval2lem  23698  lgsval4a  23710  lgsneg  23711  lgsdir  23722  lgsdilem2  23723  lgsdi  23724  lgsne0  23725  lgsquadlem2  23747  chebbnd1lem1  23771  chtppilimlem1  23775  rplogsumlem1  23786  rplogsumlem2  23787  rpvmasumlem  23789  dchrisumlema  23790  dchrisumlem2  23792  dchrisumlem3  23793  dchrmusum2  23796  dchrvmasum2lem  23798  dchrvmasumiflem1  23803  dchrvmaeq0  23806  dchrisum0flblem2  23811  dchrisum0flb  23812  dchrisum0re  23815  dchrisum0lem1b  23817  dchrisum0lem1  23818  dchrisum0lem2a  23819  dchrisum0lem2  23820  dchrisum0lem3  23821  mudivsum  23832  mulogsum  23834  logdivsum  23835  mulog2sumlem2  23837  log2sumbnd  23846  selberg2lem  23852  logdivbnd  23858  pntrsumo1  23867  pntrsumbnd2  23869  pntrlog2bndlem2  23880  pntrlog2bndlem4  23882  pntrlog2bndlem6a  23884  pntlemf  23907  eedimeq  24322  axlowdimlem6  24371  axlowdimlem16  24381  axlowdimlem17  24382  eupath2lem3  25100  gxnn0suc  25383  nvlmle  25719  ipval2  25734  minvecolem3  25909  minvecolem4b  25911  minvecolem4  25913  h2hcau  26013  h2hlm  26014  hlimadd  26227  hlim0  26270  hhsscms  26312  occllem  26338  nlelchi  27096  opsqrlem4  27178  hmopidmchi  27186  iundisjf  27578  iundisj2f  27579  fzssnn  27748  ssnnssfz  27750  iundisjfi  27754  iundisj2fi  27755  lmlim  28083  rge0scvg  28085  lmxrge0  28088  lmdvg  28089  esumfzf  28217  esumfsup  28218  esumpcvgval  28226  esumpmono  28227  esumcvg  28234  esumcvgsum  28236  esumsup  28237  eulerpartlemsv2  28480  eulerpartlems  28482  eulerpartlemsv3  28483  eulerpartlemv  28486  eulerpartlemb  28490  fiblem  28520  fibp1  28523  rrvsum  28576  dstfrvclim1  28599  ballotlemsup  28626  ballotlem1ri  28656  signsvfn  28722  zetacvg  28746  lgamgulmlem4  28763  lgamgulmlem6  28765  lgamgulm2  28767  lgamcvglem  28771  lgamcvg2  28786  gamcvg  28787  gamcvg2lem  28790  regamcl  28792  relgamcl  28793  lgam1  28795  subfacp1lem1  28812  subfacp1lem5  28817  subfacp1lem6  28818  erdszelem7  28830  cvmliftlem5  28923  cvmliftlem7  28925  cvmliftlem10  28928  cvmliftlem13  28930  sinccvg  29228  circum  29229  divcnvshft  29283  divcnvlin  29284  iprodgam  29291  fallfacval4  29331  faclimlem1  29334  faclimlem2  29335  faclim  29337  iprodfac  29338  faclim2  29339  prednn  29446  bpoly4  29974  mblfinlem2  30217  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  lmclim2  30417  geomcau  30418  heibor1lem  30471  heibor1  30472  bfplem1  30484  bfplem2  30485  rrncmslem  30494  rrncms  30495  eldioph3b  30863  diophin  30871  diophun  30872  diophren  30912  jm3.1lem2  31126  dgraalem  31262  dgraaub  31265  lcmcllem  31370  lcmledvds  31373  hashnzfz2  31394  hashnzfzclim  31395  dvradcnv2  31420  binomcxplemnotnn0  31429  clim1fr1  31773  sumnnodd  31802  stoweidlem7  31955  stoweidlem14  31962  stoweidlem20  31968  stoweidlem34  31982  wallispilem5  32017  wallispi  32018  stirlinglem1  32022  stirlinglem5  32026  stirlinglem7  32028  stirlinglem8  32029  stirlinglem10  32031  stirlinglem11  32032  stirlinglem12  32033  stirlinglem13  32034  stirlinglem14  32035  stirlinglem15  32036  stirlingr  32038  dirkertrigeqlem2  32047  dirkertrigeqlem3  32048  fourierdlem11  32066  fourierdlem31  32086  fourierdlem48  32103  fourierdlem49  32104  fourierdlem69  32124  fourierdlem73  32128  fourierdlem81  32136  fourierdlem93  32148  fourierdlem103  32158  fourierdlem104  32159  fourierdlem112  32167  fouriersw  32180  dftrcl3  38231
  Copyright terms: Public domain W3C validator