Theorem nnuz 12889

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

Step	Hyp	Ref	Expression
1		nnzrab 12610	. 2 ⊢ ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2		1z 12612	. . 3 ⊢ 1 ∈ ℤ
3		uzval 12852	. . 3 ⊢ (1 ∈ ℤ → (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
5	1, 4	eqtr4i 2791	1 ⊢ ℕ = (ℤ≥‘1)

Syntax hints:   = wceq 1563   ∈ wcel 2145  {crab 3417   class class class wbr 5104  ‘cfv 6525  1c1 11089   ≤ cle 11232  ℕcn 12221  ℤcz 12579  ℤ_≥cuz 12850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12222  df-z 12580  df-uz 12851

This theorem is referenced by:  elnnuz  12890  eluz2nn  12900  uznnssnn  12907  nnwo  12925  eluznn  12930  nninf  12941  fzssnn  13584  fseq1p1m1  13614  prednn  13667  elfzo1  13729  ltwenn  13986  nnnfi  13990  ser1const  14082  expp1  14092  digit1  14261  facnn  14299  fac0  14300  facp1  14302  faclbnd4lem1  14317  bcm1k  14339  bcval5  14342  bcpasc  14345  fz1isolem  14486  seqcoll  14489  seqcoll2  14490  climuni  15591  isercolllem2  15705  isercoll  15707  sumeq2ii  15732  summolem3  15753  summolem2a  15754  fsum  15759  sum0  15760  sumz  15761  fsumcl2lem  15770  fsumadd  15779  fsummulc2  15823  fsumrelem  15847  isumnn0nn  15884  climcndslem1  15891  climcndslem2  15892  climcnds  15893  divcnv  15895  divcnvshft  15897  supcvg  15898  trireciplem  15904  trirecip  15905  expcnv  15906  geo2lim  15917  geoisum1  15921  geoisum1c  15922  mertenslem2  15927  prodeq2ii  15953  prodmolem3  15975  prodmolem2a  15976  fprod  15983  prod0  15985  prod1  15986  fprodss  15990  fprodser  15991  fprodcl2lem  15992  fprodmul  16002  fproddiv  16003  fprodn0  16021  fallfacval4  16085  bpoly4  16101  ege2le3  16132  rpnnen2lem3  16260  rpnnen2lem5  16262  rpnnen2lem8  16265  rpnnen2lem12  16269  ruclem6  16279  pwp1fsum  16437  bezoutlem2  16586  bezoutlem3  16587  lcmcllem  16642  lcmledvds  16645  lcmfval  16667  lcmfcllem  16671  lcmfledvds  16678  isprm3  16729  phicl2  16815  phibndlem  16817  eulerthlem2  16829  odzcllem  16840  odzdvds  16843  iserodd  16883  pcmptcl  16939  pcmpt  16940  pockthlem  16953  pockthg  16954  unbenlem  16956  prmreclem3  16966  prmreclem5  16968  prmreclem6  16969  prmrec  16970  1arith  16975  4sqlem13  17005  4sqlem14  17006  4sqlem17  17009  4sqlem18  17010  vdwlem1  17029  vdwlem2  17030  vdwlem3  17031  vdwlem6  17034  vdwlem8  17036  vdwlem10  17038  vdw  17042  vdwnnlem3  17045  prmlem1a  17154  chnub  18666  mulgnnp1  19136  mulgnnsubcl  19140  mulgnn0z  19155  mulgnndir  19157  mulgpropd  19170  odfval  19590  odlem1  19593  odlem2  19597  gexlem1  19637  gexlem2  19640  gexcl3  19645  sylow1lem1  19656  efgsdmi  19790  efgsrel  19792  efgs1b  19794  efgsp1  19795  mulgnn0di  19883  lt6abl  19953  gsumval3eu  19962  gsumval3  19965  gsumzcl2  19968  gsumzaddlem  19979  gsumconst  19992  gsumzmhm  19995  gsumzoppg  20002  zringlpirlem2  21570  zringlpirlem3  21571  lmcnp  23418  lmmo  23494  1stcelcls  23575  1stccnp  23576  1stckgenlem  23667  1stckgen  23668  imasdsf1olem  24487  cphipval  25359  lmnn  25379  cmetcaulem  25404  iscmet2  25410  causs  25414  nglmle  25418  caubl  25424  iscmet3i  25428  bcthlem5  25444  ovolsf  25588  ovollb2lem  25604  ovolctb  25606  ovolunlem1a  25612  ovolunlem1  25613  ovoliunlem1  25618  ovoliun  25621  ovoliun2  25622  ovoliunnul  25623  ovolscalem1  25629  ovolicc1  25632  ovolicc2lem2  25634  ovolicc2lem3  25635  ovolicc2lem4  25636  iundisj  25664  iundisj2  25665  voliunlem1  25666  voliunlem2  25667  voliunlem3  25668  volsup  25672  ioombl1lem4  25677  uniioovol  25695  uniioombllem2  25699  uniioombllem3  25701  uniioombllem4  25702  uniioombllem6  25704  vitalilem4  25727  vitalilem5  25728  itg1climres  25830  mbfi1fseqlem6  25836  mbfi1flimlem  25838  mbfmullem2  25840  itg2monolem1  25866  itg2i1fseqle  25870  itg2i1fseq  25871  itg2i1fseq2  25872  itg2addlem  25874  plyeq0lem  26324  vieta1lem2  26429  elqaalem1  26437  elqaalem3  26439  aaliou3lem4  26464  aaliou3lem7  26467  dvtaylp  26487  taylthlem2  26491  pserdvlem2  26545  pserdv2  26547  abelthlem6  26553  abelthlem9  26557  logtayl  26779  logtaylsum  26780  logtayl2  26781  atantayl  27056  leibpilem2  27060  leibpi  27061  birthdaylem2  27071  dfef2  27089  divsqrtsumlem  27098  emcllem2  27115  emcllem4  27117  emcllem5  27118  emcllem6  27119  emcllem7  27120  harmonicbnd4  27129  fsumharmonic  27130  zetacvg  27133  lgamgulmlem4  27150  lgamgulmlem6  27152  lgamgulm2  27154  lgamcvglem  27158  lgamcvg2  27173  gamcvg  27174  gamcvg2lem  27177  regamcl  27179  relgamcl  27180  lgam1  27182  wilthlem3  27188  ftalem2  27192  ftalem4  27194  ftalem5  27195  basellem5  27203  basellem6  27204  basellem7  27205  basellem8  27206  basellem9  27207  ppiprm  27269  ppinprm  27270  chtprm  27271  chtnprm  27272  chpp1  27273  vma1  27284  ppiltx  27295  fsumvma2  27332  chpchtsum  27337  logfacbnd3  27341  logexprlim  27343  bposlem5  27406  lgscllem  27422  lgsval2lem  27425  lgsval4a  27437  lgsneg  27439  lgsdir  27450  lgsdilem2  27451  lgsdi  27452  lgsne0  27453  gausslemma2dlem3  27486  lgsquadlem2  27499  chebbnd1lem1  27587  chtppilimlem1  27591  rplogsumlem1  27602  rplogsumlem2  27603  rpvmasumlem  27605  dchrisumlema  27606  dchrisumlem2  27608  dchrisumlem3  27609  dchrmusum2  27612  dchrvmasum2lem  27614  dchrvmasumiflem1  27619  dchrvmaeq0  27622  dchrisum0flblem2  27627  dchrisum0flb  27628  dchrisum0re  27631  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  dchrisum0lem3  27637  mudivsum  27648  mulogsum  27650  logdivsum  27651  mulog2sumlem2  27653  log2sumbnd  27662  selberg2lem  27668  logdivbnd  27674  pntrsumo1  27683  pntrsumbnd2  27685  pntrlog2bndlem2  27696  pntrlog2bndlem4  27698  pntrlog2bndlem6a  27700  pntlemf  27723  eedimeq  29153  axlowdimlem6  29202  axlowdimlem16  29212  axlowdimlem17  29213  ipval2  30964  minvecolem3  31133  minvecolem4b  31135  minvecolem4  31137  h2hcau  31236  h2hlm  31237  hlimadd  31450  hlim0  31492  hhsscms  31535  occllem  31560  nlelchi  32318  opsqrlem4  32400  hmopidmchi  32408  iundisjf  32840  iundisj2f  32841  ssnnssfz  33040  iundisjfi  33049  iundisj2fi  33050  cycpmco2lem7  33360  cycpmrn  33371  1smat1  34106  submat1n  34107  submatres  34108  submateqlem2  34110  lmatfval  34116  madjusmdetlem1  34129  madjusmdetlem2  34130  madjusmdetlem3  34131  madjusmdetlem4  34132  lmlim  34249  rge0scvg  34251  lmxrge0  34254  lmdvg  34255  esumfzf  34371  esumfsup  34372  esumpcvgval  34380  esumpmono  34381  esumcvg  34388  esumcvgsum  34390  esumsup  34391  fiunelros  34476  eulerpartlemsv2  34660  eulerpartlems  34662  eulerpartlemsv3  34663  eulerpartlemv  34666  eulerpartlemb  34670  fiblem  34700  fibp1  34703  rrvsum  34756  dstfrvclim1  34780  ballotlem1ri  34837  signsvfn  34881  chtvalz  34928  circlemethhgt  34942  subfacp1lem1  35537  subfacp1lem5  35542  subfacp1lem6  35543  erdszelem7  35555  cvmliftlem5  35647  cvmliftlem7  35649  cvmliftlem10  35652  cvmliftlem13  35654  sinccvg  36031  circum  36032  divcnvlin  36091  iprodgam  36100  faclimlem1  36101  faclimlem2  36102  faclim  36104  iprodfac  36105  faclim2  36106  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem12  38138  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem18  38144  poimirlem19  38145  poimirlem20  38146  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem25  38151  poimirlem27  38153  poimirlem28  38154  poimirlem29  38155  poimirlem30  38156  poimirlem31  38157  mblfinlem2  38164  ovoliunnfl  38168  voliunnfl  38170  volsupnfl  38171  lmclim2  38264  geomcau  38265  heibor1lem  38315  heibor1  38316  bfplem1  38328  bfplem2  38329  rrncmslem  38338  rrncms  38339  aks4d1p1p1  42687  sticksstones10  42779  sticksstones12a  42781  fz1sump1  42926  sumcubes  42929  nna4b4nsq  43249  eldioph3b  43353  diophin  43360  diophun  43361  diophren  43397  jm3.1lem2  43602  dgraalem  43729  dgraaub  43732  dftrcl3  44303  trclfvdecomr  44311  hashnzfz2  44890  hashnzfzclim  44891  dvradcnv2  44916  binomcxplemnotnn0  44925  nnsplit  45933  rexanuz2nf  46065  clim1fr1  46176  sumnnodd  46205  limsup10exlem  46345  fprodsubrecnncnvlem  46480  fprodaddrecnncnvlem  46482  stoweidlem7  46580  stoweidlem14  46587  stoweidlem20  46593  stoweidlem34  46607  wallispilem5  46642  wallispi  46643  stirlinglem1  46647  stirlinglem5  46651  stirlinglem7  46653  stirlinglem8  46654  stirlinglem10  46656  stirlinglem11  46657  stirlinglem12  46658  stirlinglem13  46659  stirlinglem14  46660  stirlinglem15  46661  stirlingr  46663  dirkertrigeqlem2  46672  dirkertrigeqlem3  46673  fourierdlem11  46691  fourierdlem31  46711  fourierdlem48  46727  fourierdlem49  46728  fourierdlem69  46748  fourierdlem73  46752  fourierdlem81  46760  fourierdlem93  46772  fourierdlem103  46782  fourierdlem104  46783  fourierdlem112  46791  fouriersw  46804  sge0ad2en  47004  voliunsge0lem  47045  caragenunicl  47097  caratheodorylem2  47100  hoidmvlelem3  47170  ovolval2lem  47216  ovolval2  47217  vonioolem2  47254  vonicclem2  47257  nthrucw  47461  fmtno4prmfac  48180