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

Theorem nnuz 10888
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 10666 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10668 . . 3  |-  1  e.  ZZ
3 uzval 10855 . . 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 2461 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   {crab 2714   class class class wbr 4287   ` cfv 5413   1c1 9275    <_ cle 9411   NNcn 10314   ZZcz 10638   ZZ>=cuz 10853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-z 10639  df-uz 10854
This theorem is referenced by:  elnnuz  10889  uznnssnn  10894  nnwo  10912  eluznn  10917  nninfm  10927  fseq1p1m1  11526  elfzo1  11587  ltwenn  11777  ser1const  11854  expp1  11864  digit1  11990  facnn  12045  fac0  12046  facp1  12048  faclbnd4lem1  12061  bcm1k  12083  bcval5  12086  bcpasc  12089  fz1isolem  12206  seqcoll  12208  seqcoll2  12209  climuni  13022  isercolllem2  13135  isercoll  13137  sumeq2ii  13162  summolem3  13183  summolem2a  13184  fsum  13189  sum0  13190  sumz  13191  fsumcl2lem  13200  fsumadd  13207  fsummulc2  13243  fsumrelem  13262  isumnn0nn  13297  climcndslem1  13304  climcndslem2  13305  climcnds  13306  divcnv  13308  supcvg  13310  trireciplem  13316  trirecip  13317  expcnv  13318  geo2lim  13327  geoisum1  13331  geoisum1c  13332  mertenslem2  13337  ege2le3  13367  rpnnen2lem3  13491  rpnnen2lem5  13493  rpnnen2lem8  13496  rpnnen2  13500  ruclem6  13509  bezoutlem2  13715  bezoutlem3  13716  isprm3  13764  phicl2  13835  phibndlem  13837  eulerthlem2  13849  odzcllem  13856  odzdvds  13859  iserodd  13894  pcmptcl  13945  pcmpt  13946  pockthlem  13958  pockthg  13959  unbenlem  13961  prmreclem3  13971  prmreclem5  13973  prmreclem6  13974  prmrec  13975  1arith  13980  4sqlem13  14010  4sqlem14  14011  4sqlem17  14014  4sqlem18  14015  vdwlem1  14034  vdwlem2  14035  vdwlem3  14036  vdwlem6  14039  vdwlem8  14041  vdwlem10  14043  vdw  14047  vdwnnlem1  14048  vdwnnlem3  14050  prmlem1a  14126  mulgnnp1  15626  mulgnnsubcl  15630  mulgnn0z  15638  mulgnndir  15640  mulgpropd  15651  odlem1  16029  odlem2  16033  gexlem1  16069  gexlem2  16072  gexcl3  16077  sylow1lem1  16088  efgsdmi  16220  efgsrel  16222  efgs1b  16224  efgsp1  16225  mulgnn0di  16304  lt6abl  16362  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzcl2  16380  gsumzclOLD  16384  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzoppg  16430  gsumzoppgOLD  16431  zringlpirlem2  17879  zringlpirlem3  17880  zlpirlem2  17884  zlpirlem3  17885  lmcnp  18883  lmmo  18959  1stcelcls  19040  1stccnp  19041  1stckgenlem  19101  1stckgen  19102  imasdsf1olem  19923  lmnn  20749  cmetcaulem  20774  iscmet2  20780  causs  20784  caubl  20793  iscmet3i  20797  bcthlem5  20814  ovolsf  20931  ovollb2lem  20946  ovolctb  20948  ovolunlem1a  20954  ovolunlem1  20955  ovoliunlem1  20960  ovoliun  20963  ovoliun2  20964  ovoliunnul  20965  ovolscalem1  20971  ovolicc1  20974  ovolicc2lem2  20976  ovolicc2lem3  20977  ovolicc2lem4  20978  iundisj  21004  iundisj2  21005  voliunlem1  21006  voliunlem2  21007  voliunlem3  21008  iunmbl  21009  volsup  21012  ioombl1lem4  21017  uniioovol  21034  uniioombllem2  21038  uniioombllem3  21040  uniioombllem4  21041  uniioombllem6  21043  vitalilem4  21066  vitalilem5  21067  itg1climres  21167  mbfi1fseqlem6  21173  mbfi1flimlem  21175  mbfmullem2  21177  itg2monolem1  21203  itg2i1fseqle  21207  itg2i1fseq  21208  itg2i1fseq2  21209  itg2addlem  21211  plyeq0lem  21653  vieta1lem2  21752  elqaalem1  21760  elqaalem3  21762  aaliou3lem4  21787  aaliou3lem7  21790  dvtaylp  21810  taylthlem2  21814  pserdvlem2  21868  pserdv2  21870  abelthlem6  21876  abelthlem9  21880  logtayl  22080  logtaylsum  22081  logtayl2  22082  atantayl  22307  leibpilem2  22311  leibpi  22312  birthdaylem2  22321  dfef2  22339  divsqrsumlem  22348  emcllem2  22365  emcllem4  22367  emcllem5  22368  emcllem6  22369  emcllem7  22370  harmonicbnd4  22379  fsumharmonic  22380  wilthlem3  22383  ftalem2  22386  ftalem4  22388  ftalem5  22389  basellem5  22397  basellem6  22398  basellem7  22399  basellem8  22400  basellem9  22401  ppiprm  22464  ppinprm  22465  chtprm  22466  chtnprm  22467  chpp1  22468  vma1  22479  ppiltx  22490  prmorcht  22491  chtlepsi  22520  fsumvma2  22528  chpchtsum  22533  chpub  22534  logfacbnd3  22537  logexprlim  22539  bposlem5  22602  lgscllem  22617  lgsval2lem  22620  lgsval4a  22632  lgsneg  22633  lgsdir  22644  lgsdilem2  22645  lgsdi  22646  lgsne0  22647  lgsquadlem2  22669  chebbnd1lem1  22693  chtppilimlem1  22697  rplogsumlem1  22708  rplogsumlem2  22709  rpvmasumlem  22711  dchrisumlema  22712  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasum2lem  22720  dchrvmasumiflem1  22725  dchrvmaeq0  22728  dchrisum0flblem2  22733  dchrisum0flb  22734  dchrisum0re  22737  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  dchrisum0lem2  22742  dchrisum0lem3  22743  mudivsum  22754  mulogsum  22756  logdivsum  22757  mulog2sumlem2  22759  log2sumbnd  22768  selberg2lem  22774  logdivbnd  22780  pntrsumo1  22789  pntrsumbnd2  22791  pntrlog2bndlem2  22802  pntrlog2bndlem4  22804  pntrlog2bndlem6a  22806  pntlemf  22829  eedimeq  23095  axlowdimlem6  23144  axlowdimlem16  23154  axlowdimlem17  23155  axlowdim  23158  eupath2lem3  23551  gxnn0suc  23702  nvlmle  24038  ipval2  24053  minvecolem3  24228  minvecolem4b  24230  minvecolem4  24232  h2hcau  24332  h2hlm  24333  hlimadd  24546  hlim0  24589  hhsscms  24631  occllem  24657  nlelchi  25416  opsqrlem4  25498  hmopidmchi  25506  iundisjf  25882  iundisj2f  25883  fzssnn  26025  ssnnssfz  26027  iundisjfi  26031  iundisj2fi  26032  lmlim  26329  rge0scvg  26331  lmxrge0  26334  lmdvg  26335  rnlogblem  26410  esumfzf  26470  esumfsup  26471  esumpcvgval  26479  esumpmono  26480  esumcvg  26487  eulerpartlemsv2  26693  eulerpartlems  26695  eulerpartlemsv3  26696  eulerpartlemv  26699  eulerpartlemb  26703  fiblem  26733  fibp1  26736  rrvsum  26789  dstfrvclim1  26812  ballotlemsup  26839  ballotlem1ri  26869  signsvfn  26935  zetacvg  26953  lgamgulmlem4  26970  lgamgulmlem6  26972  lgamgulm2  26974  lgamcvglem  26978  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  regamcl  26999  relgamcl  27000  lgam1  27002  subfacp1lem1  27019  subfacp1lem5  27024  subfacp1lem6  27025  erdszelem7  27037  cvmliftlem5  27130  cvmliftlem7  27132  cvmliftlem10  27135  cvmliftlem13  27137  sinccvglem  27268  sinccvg  27269  circum  27270  divcnvshft  27349  divcnvlin  27350  prodeq2ii  27377  prodmolem3  27397  prodmolem2a  27398  fprod  27405  prod0  27407  prod1  27408  fprodss  27412  fprodser  27413  fprodcl2lem  27414  fprodmul  27422  fproddiv  27423  fprodn0  27441  iprodgam  27457  fallfacval4  27497  faclimlem1  27500  faclimlem2  27501  faclim  27503  iprodfac  27504  faclim2  27505  prednn  27613  bpoly4  28153  mblfinlem2  28382  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  lmclim2  28607  geomcau  28608  heibor1lem  28661  heibor1  28662  bfplem1  28674  bfplem2  28675  rrncmslem  28684  rrncms  28685  eldioph3b  29056  diophin  29064  diophun  29065  diophren  29105  jm3.1lem2  29320  dgraalem  29455  dgraaub  29458  clim1fr1  29727  stoweidlem7  29755  stoweidlem14  29762  stoweidlem20  29768  stoweidlem34  29782  wallispilem5  29817  wallispi  29818  stirlinglem1  29822  stirlinglem5  29826  stirlinglem7  29828  stirlinglem8  29829  stirlinglem10  29831  stirlinglem11  29832  stirlinglem12  29833  stirlinglem13  29834  stirlinglem14  29835  stirlinglem15  29836  stirlingr  29838  uz2nn  30144
  Copyright terms: Public domain W3C validator