Theorem nnuz 11599

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 11282	. 2 ⊢ ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2		1z 11284	. . 3 ⊢ 1 ∈ ℤ
3		uzval 11565	. . 3 ⊢ (1 ∈ ℤ → (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘1) = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
5	1, 4	eqtr4i 2635	1 ⊢ ℕ = (ℤ≥‘1)

Syntax hints:   = wceq 1475   ∈ wcel 1977  {crab 2900   class class class wbr 4583  ‘cfv 5804  1c1 9816   ≤ cle 9954  ℕcn 10897  ℤcz 11254  ℤ_≥cuz 11563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-z 11255  df-uz 11564

This theorem is referenced by:  elnnuz  11600  eluz2nn  11602  uznnssnn  11611  nnwo  11629  eluznn  11634  nninf  11645  fzssnn  12256  fseq1p1m1  12283  prednn  12331  elfzo1  12385  ltwenn  12623  nnnfi  12627  ser1const  12719  expp1  12729  digit1  12860  facnn  12924  fac0  12925  facp1  12927  faclbnd4lem1  12942  bcm1k  12964  bcval5  12967  bcpasc  12970  fz1isolem  13102  seqcoll  13105  seqcoll2  13106  climuni  14131  isercolllem2  14244  isercoll  14246  sumeq2ii  14271  summolem3  14292  summolem2a  14293  fsum  14298  sum0  14299  sumz  14300  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumrelem  14380  isumnn0nn  14413  climcndslem1  14420  climcndslem2  14421  climcnds  14422  divcnv  14424  divcnvshft  14426  supcvg  14427  trireciplem  14433  trirecip  14434  expcnv  14435  geo2lim  14445  geoisum1  14449  geoisum1c  14450  mertenslem2  14456  prodeq2ii  14482  prodmolem3  14502  prodmolem2a  14503  fprod  14510  prod0  14512  prod1  14513  fprodss  14517  fprodser  14518  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodn0  14548  fallfacval4  14613  bpoly4  14629  ege2le3  14659  rpnnen2lem3  14784  rpnnen2lem5  14786  rpnnen2lem8  14789  rpnnen2lem12  14793  ruclem6  14803  pwp1fsum  14952  bezoutlem2  15095  bezoutlem3  15096  lcmcllem  15147  lcmledvds  15150  lcmfval  15172  lcmfcllem  15176  lcmfledvds  15183  isprm3  15234  phicl2  15311  phibndlem  15313  eulerthlem2  15325  odzcllem  15335  odzdvds  15338  iserodd  15378  pcmptcl  15433  pcmpt  15434  pockthlem  15447  pockthg  15448  unbenlem  15450  prmreclem3  15460  prmreclem5  15462  prmreclem6  15463  prmrec  15464  1arith  15469  4sqlem13  15499  4sqlem14  15500  4sqlem17  15503  4sqlem18  15504  vdwlem1  15523  vdwlem2  15524  vdwlem3  15525  vdwlem6  15528  vdwlem8  15530  vdwlem10  15532  vdw  15536  vdwnnlem1  15537  vdwnnlem3  15539  prmlem1a  15651  mulgnnp1  17372  mulgnnsubcl  17376  mulgnn0z  17390  mulgnndir  17392  mulgnndirOLD  17393  mulgpropd  17407  odlem1  17777  odlem2  17781  gexlem1  17817  gexlem2  17820  gexcl3  17825  sylow1lem1  17836  efgsdmi  17968  efgsrel  17970  efgs1b  17972  efgsp1  17973  mulgnn0di  18054  lt6abl  18119  gsumval3eu  18128  gsumval3  18131  gsumzcl2  18134  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  zringlpirlem2  19652  zringlpirlem3  19653  lmcnp  20918  lmmo  20994  1stcelcls  21074  1stccnp  21075  1stckgenlem  21166  1stckgen  21167  imasdsf1olem  21988  cphipval  22850  lmnn  22869  cmetcaulem  22894  iscmet2  22900  causs  22904  nglmle  22908  caubl  22914  iscmet3i  22918  bcthlem5  22933  ovolsf  23048  ovollb2lem  23063  ovolctb  23065  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliun  23080  ovoliun2  23081  ovoliunnul  23082  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem4  23095  iundisj  23123  iundisj2  23124  voliunlem1  23125  voliunlem2  23126  voliunlem3  23127  volsup  23131  ioombl1lem4  23136  uniioovol  23153  uniioombllem2  23157  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  vitalilem4  23186  vitalilem5  23187  itg1climres  23287  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfmullem2  23297  itg2monolem1  23323  itg2i1fseqle  23327  itg2i1fseq  23328  itg2i1fseq2  23329  itg2addlem  23331  plyeq0lem  23770  vieta1lem2  23870  elqaalem1  23878  elqaalem3  23880  aaliou3lem4  23905  aaliou3lem7  23908  dvtaylp  23928  taylthlem2  23932  pserdvlem2  23986  pserdv2  23988  abelthlem6  23994  abelthlem9  23998  logtayl  24206  logtaylsum  24207  logtayl2  24208  atantayl  24464  leibpilem2  24468  leibpi  24469  birthdaylem2  24479  dfef2  24497  divsqrtsumlem  24506  emcllem2  24523  emcllem4  24525  emcllem5  24526  emcllem6  24527  emcllem7  24528  harmonicbnd4  24537  fsumharmonic  24538  zetacvg  24541  lgamgulmlem4  24558  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvglem  24566  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  regamcl  24587  relgamcl  24588  lgam1  24590  wilthlem3  24596  ftalem2  24600  ftalem4  24602  ftalem5  24603  basellem5  24611  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  ppiprm  24677  ppinprm  24678  chtprm  24679  chtnprm  24680  chpp1  24681  vma1  24692  ppiltx  24703  fsumvma2  24739  chpchtsum  24744  logfacbnd3  24748  logexprlim  24750  bposlem5  24813  lgscllem  24829  lgsval2lem  24832  lgsval4a  24844  lgsneg  24846  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  gausslemma2dlem3  24893  lgsquadlem2  24906  chebbnd1lem1  24958  chtppilimlem1  24962  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasum2lem  24985  dchrvmasumiflem1  24990  dchrvmaeq0  24993  dchrisum0flblem2  24998  dchrisum0flb  24999  dchrisum0re  25002  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  mudivsum  25019  mulogsum  25021  logdivsum  25022  mulog2sumlem2  25024  log2sumbnd  25033  selberg2lem  25039  logdivbnd  25045  pntrsumo1  25054  pntrsumbnd2  25056  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem6a  25071  pntlemf  25094  eedimeq  25578  axlowdimlem6  25627  axlowdimlem16  25637  axlowdimlem17  25638  eupath2lem3  26506  ipval2  26946  minvecolem3  27116  minvecolem4b  27118  minvecolem4  27120  h2hcau  27220  h2hlm  27221  hlimadd  27434  hlim0  27476  hhsscms  27520  occllem  27546  nlelchi  28304  opsqrlem4  28386  hmopidmchi  28394  iundisjf  28784  iundisj2f  28785  ssnnssfz  28937  iundisjfi  28942  iundisj2fi  28943  1smat1  29198  submat1n  29199  submatres  29200  submateqlem2  29202  lmatfval  29208  madjusmdetlem1  29221  madjusmdetlem2  29222  madjusmdetlem3  29223  madjusmdetlem4  29224  lmlim  29321  rge0scvg  29323  lmxrge0  29326  lmdvg  29327  esumfzf  29458  esumfsup  29459  esumpcvgval  29467  esumpmono  29468  esumcvg  29475  esumcvgsum  29477  esumsup  29478  fiunelros  29564  eulerpartlemsv2  29747  eulerpartlems  29749  eulerpartlemsv3  29750  eulerpartlemv  29753  eulerpartlemb  29757  fiblem  29787  fibp1  29790  rrvsum  29843  dstfrvclim1  29866  ballotlem1ri  29923  signsvfn  29985  subfacp1lem1  30415  subfacp1lem5  30420  subfacp1lem6  30421  erdszelem7  30433  cvmliftlem5  30525  cvmliftlem7  30527  cvmliftlem10  30530  cvmliftlem13  30532  sinccvg  30821  circum  30822  divcnvlin  30871  iprodgam  30881  faclimlem1  30882  faclimlem2  30883  faclim  30885  iprodfac  30886  faclim2  30887  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  lmclim2  32724  geomcau  32725  heibor1lem  32778  heibor1  32779  bfplem1  32791  bfplem2  32792  rrncmslem  32801  rrncms  32802  eldioph3b  36346  diophin  36354  diophun  36355  diophren  36395  jm3.1lem2  36603  dgraalem  36734  dgraaub  36737  dftrcl3  37031  trclfvdecomr  37039  hashnzfz2  37542  hashnzfzclim  37543  dvradcnv2  37568  binomcxplemnotnn0  37577  nnsplit  38515  clim1fr1  38668  sumnnodd  38697  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  stoweidlem7  38900  stoweidlem14  38907  stoweidlem20  38913  stoweidlem34  38927  wallispilem5  38962  wallispi  38963  stirlinglem1  38967  stirlinglem5  38971  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  fourierdlem11  39011  fourierdlem31  39031  fourierdlem48  39047  fourierdlem49  39048  fourierdlem69  39068  fourierdlem73  39072  fourierdlem81  39080  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fouriersw  39124  sge0ad2en  39324  voliunsge0lem  39365  caragenunicl  39414  caratheodorylem2  39417  hoidmvlelem3  39487  ovolval2lem  39533  ovolval2  39534  vonioolem2  39572  vonicclem2  39575  fmtno4prmfac  40022