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

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

Proof of Theorem nnuz
StepHypRef Expression
1 nnzrab 10098 . 2  |-  NN  =  { k  e.  ZZ  |  1  <_  k }
2 1z 10100 . . 3  |-  1  e.  ZZ
3 uzval 10279 . . 3  |-  ( 1  e.  ZZ  ->  ( ZZ>=
`  1 )  =  { k  e.  ZZ  |  1  <_  k } )
42, 3ax-mp 8 . 2  |-  ( ZZ>= ` 
1 )  =  {
k  e.  ZZ  | 
1  <_  k }
51, 4eqtr4i 2339 1  |-  NN  =  ( ZZ>= `  1 )
Colors of variables: wff set class
Syntax hints:    = wceq 1633    e. wcel 1701   {crab 2581   class class class wbr 4060   ` cfv 5292   1c1 8783    <_ cle 8913   NNcn 9791   ZZcz 10071   ZZ>=cuz 10277
This theorem is referenced by:  elnnuz  10311  uznnssnn  10313  nnwo  10331  nninfm  10345  fseq1p1m1  10904  ltwenn  11072  ser1const  11149  expp1  11157  expmulnbnd  11280  digit1  11282  facnn  11337  fac0  11338  facp1  11340  faclbnd4lem1  11353  bcm1k  11374  bcval5  11377  bcpasc  11380  fz1isolem  11446  seqcoll  11448  seqcoll2  11449  climuni  12073  isercolllem1  12185  isercolllem2  12186  isercoll  12188  sumeq2ii  12213  summolem3  12234  summolem2a  12235  fsum  12240  sum0  12241  sumz  12242  fsumcl2lem  12251  fsumadd  12258  fsummulc2  12293  fsumrelem  12312  o1fsum  12318  isumnn0nn  12348  climcndslem1  12355  climcndslem2  12356  climcnds  12357  divcnv  12359  supcvg  12361  trireciplem  12367  trirecip  12368  expcnv  12369  geo2lim  12378  geoisum1  12382  geoisum1c  12383  mertenslem2  12388  ege2le3  12418  rpnnen2lem3  12542  rpnnen2lem5  12544  rpnnen2lem6  12545  rpnnen2lem7  12546  rpnnen2lem8  12547  rpnnen2lem9  12548  rpnnen2lem11  12550  rpnnen2  12551  ruclem6  12560  bezoutlem2  12765  bezoutlem3  12766  isprm3  12814  phicl2  12883  phibndlem  12885  eulerthlem2  12897  odzcllem  12904  odzdvds  12907  iserodd  12935  pcmptcl  12986  pcmpt  12987  pcmpt2  12988  pcmptdvds  12989  pockthlem  12999  pockthg  13000  unbenlem  13002  prmreclem3  13012  prmreclem4  13013  prmreclem5  13014  prmreclem6  13015  prmrec  13016  1arith  13021  4sqlem13  13051  4sqlem14  13052  4sqlem17  13055  4sqlem18  13056  vdwlem1  13075  vdwlem2  13076  vdwlem3  13077  vdwlem6  13080  vdwlem8  13082  vdwlem10  13084  vdw  13088  vdwnnlem1  13089  vdwnnlem2  13090  vdwnnlem3  13091  2expltfac  13152  prmlem1a  13155  mulgnnp1  14624  mulgnnsubcl  14628  mulgnn0z  14636  mulgnndir  14638  mulgpropd  14649  odlem1  14899  odlem2  14903  gexlem1  14939  gexlem2  14942  gexcl3  14947  sylow1lem1  14958  efgsdmi  15090  efgsrel  15092  efgs1b  15094  efgsp1  15095  mulgnn0di  15174  lt6abl  15230  gsumval3eu  15239  gsumval3  15240  gsumzcl  15244  gsumzaddlem  15252  gsumconst  15258  gsumzmhm  15259  gsumzoppg  15265  zlpirlem2  16498  zlpirlem3  16499  lmcnp  17088  lmmo  17164  1stcelcls  17243  1stccnp  17244  1stckgenlem  17304  1stckgen  17305  imasdsf1olem  17989  lmnn  18742  cmetcaulem  18767  iscmet2  18773  causs  18777  caubl  18786  caublcls  18787  iscmet3i  18790  bcthlem5  18803  ovolsf  18885  ovollb2lem  18900  ovolctb  18902  ovolunlem1a  18908  ovolunlem1  18909  ovoliunlem1  18914  ovoliun  18917  ovoliun2  18918  ovoliunnul  18919  ovolscalem1  18925  ovolicc1  18928  ovolicc2lem2  18930  ovolicc2lem3  18931  ovolicc2lem4  18932  iundisj  18958  iundisj2  18959  voliunlem1  18960  voliunlem2  18961  voliunlem3  18962  iunmbl  18963  volsuplem  18965  volsup  18966  ioombl1lem4  18971  uniioovol  18987  uniioombllem2  18991  uniioombllem3  18993  uniioombllem4  18994  uniioombllem6  18996  vitalilem4  19019  vitalilem5  19020  itg1climres  19122  mbfi1fseqlem6  19128  mbfi1flimlem  19130  mbfmullem2  19132  itg2monolem1  19158  itg2i1fseqle  19162  itg2i1fseq  19163  itg2i1fseq2  19164  itg2addlem  19166  plyeq0lem  19645  vieta1lem2  19744  elqaalem1  19752  elqaalem3  19754  aaliou3lem4  19779  aaliou3lem7  19782  dvtaylp  19802  taylthlem2  19806  pserdvlem2  19857  pserdv2  19859  abelthlem6  19865  abelthlem9  19869  logtayl  20060  logtaylsum  20061  logtayl2  20062  atantayl  20286  leibpilem2  20290  leibpi  20291  birthdaylem2  20300  dfef2  20318  divsqrsumlem  20327  emcllem2  20343  emcllem4  20345  emcllem5  20346  emcllem6  20347  emcllem7  20348  harmonicbnd4  20357  fsumharmonic  20358  wilthlem3  20361  ftalem2  20364  ftalem4  20366  ftalem5  20367  basellem5  20375  basellem6  20376  basellem7  20377  basellem8  20378  basellem9  20379  ppiprm  20442  ppinprm  20443  chtprm  20444  chtnprm  20445  chpp1  20446  vma1  20457  ppiltx  20468  prmorcht  20469  chtlepsi  20498  chtub  20504  fsumvma2  20506  chpchtsum  20511  chpub  20512  logfacbnd3  20515  logexprlim  20517  bclbnd  20572  bposlem3  20578  bposlem4  20579  bposlem5  20580  bposlem6  20581  lgscllem  20595  lgsval2lem  20598  lgsval4a  20610  lgsneg  20611  lgsdir  20622  lgsdilem2  20623  lgsdi  20624  lgsne0  20625  lgsquadlem2  20647  chebbnd1lem1  20671  chebbnd1lem2  20672  chebbnd1lem3  20673  chtppilimlem1  20675  rplogsumlem1  20686  rplogsumlem2  20687  rpvmasumlem  20689  dchrisumlema  20690  dchrisumlem2  20692  dchrisumlem3  20693  dchrmusum2  20696  dchrvmasum2lem  20698  dchrvmasumiflem1  20703  dchrvmaeq0  20706  dchrisum0flblem2  20711  dchrisum0flb  20712  dchrisum0re  20715  dchrisum0lem1b  20717  dchrisum0lem1  20718  dchrisum0lem2a  20719  dchrisum0lem2  20720  dchrisum0lem3  20721  mudivsum  20732  mulogsum  20734  logdivsum  20735  mulog2sumlem2  20737  log2sumbnd  20746  selberg2lem  20752  logdivbnd  20758  pntrsumo1  20767  pntrsumbnd2  20769  pntrlog2bndlem2  20780  pntrlog2bndlem4  20782  pntrlog2bndlem6a  20784  pntpbnd1  20788  pntpbnd2  20789  pntlemh  20801  pntlemq  20803  pntlemr  20804  pntlemj  20805  pntlemf  20807  gxnn0suc  20984  nvlmle  21320  ipval2  21335  minvecolem3  21510  minvecolem4b  21512  minvecolem4  21514  h2hcau  21614  h2hlm  21615  hlimadd  21827  hlim0  21870  hhsscms  21911  occllem  21937  chscllem2  22272  nlelchi  22696  opsqrlem4  22778  hmopidmchi  22786  iundisjf  23171  iundisj2f  23172  fzssnn  23294  ssnnssfz  23295  elfzo1  23300  iundisjfi  23301  iundisj2fi  23302  lmlim  23402  rge0scvg  23404  lmxrge0  23406  lmdvg  23407  rnlogblem  23591  esumfzf  23635  esumfsup  23636  esumfsupre  23637  esumpcvgval  23644  esumpmono  23645  esumcvg  23652  rrvsum  23886  dstfrvclim1  23909  ballotlemsup  23936  ballotlem1ri  23966  zetacvg  23973  subfacp1lem1  23994  subfacp1lem5  23999  subfacp1lem6  24000  erdszelem7  24012  cvmliftlem5  24104  cvmliftlem7  24106  cvmliftlem10  24109  cvmliftlem13  24111  eupath2lem3  24187  sinccvglem  24289  sinccvg  24290  circum  24291  divcnvshft  24392  divcnvlin  24393  prodeq2ii  24416  prodmolem3  24436  prodmolem2a  24437  fprod  24444  prod0  24446  prod1  24447  fprodss  24451  fprodser  24452  fprodcl2lem  24453  fprodmul  24461  gamma1  24480  faclimlem1  24481  faclimlem2  24482  faclim  24484  iprodfac  24485  faclim2  24486  prednn  24586  eedimeq  24912  axlowdimlem6  24961  axlowdimlem16  24971  axlowdimlem17  24972  axlowdim  24975  bpoly4  25180  ovoliunnfl  25315  lmclim2  25623  geomcau  25624  heibor1lem  25681  heibor1  25682  bfplem1  25694  bfplem2  25695  rrncmslem  25704  rrncms  25705  eldioph3b  25992  diophin  26000  diophun  26001  diophren  26044  jm3.1lem2  26259  dgraalem  26498  dgraaub  26501  clim1fr1  26875  stoweidlem7  26904  stoweidlem14  26911  stoweidlem20  26917  stoweidlem34  26931  wallispilem5  26966  wallispi  26967  wallispi2lem1  26968  wallispi2lem2  26969  wallispi2  26970  stirlinglem1  26971  stirlinglem5  26975  stirlinglem7  26977  stirlinglem8  26978  stirlinglem10  26980  stirlinglem11  26981  stirlinglem12  26982  stirlinglem13  26983  stirlinglem14  26984  stirlinglem15  26985  stirlingr  26987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-riota 6346  df-recs 6430  df-rdg 6465  df-er 6702  df-en 6907  df-dom 6908  df-sdom 6909  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-z 10072  df-uz 10278
  Copyright terms: Public domain W3C validator