Theorem nnuz 12893

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3415   class class class wbr 5119  ‘cfv 6530  1c1 11128   ≤ cle 11268  ℕcn 12238  ℤcz 12586  ℤ_≥cuz 12850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-z 12587  df-uz 12851

This theorem is referenced by:  elnnuz  12894  eluz2nn  12896  uznnssnn  12909  nnwo  12927  eluznn  12932  nninf  12943  fzssnn  13583  fseq1p1m1  13613  prednn  13666  elfzo1  13727  ltwenn  13978  nnnfi  13982  ser1const  14074  expp1  14084  digit1  14253  facnn  14291  fac0  14292  facp1  14294  faclbnd4lem1  14309  bcm1k  14331  bcval5  14334  bcpasc  14337  fz1isolem  14477  seqcoll  14480  seqcoll2  14481  climuni  15566  isercolllem2  15680  isercoll  15682  sumeq2ii  15707  summolem3  15728  summolem2a  15729  fsum  15734  sum0  15735  sumz  15736  fsumcl2lem  15745  fsumadd  15754  fsummulc2  15798  fsumrelem  15821  isumnn0nn  15856  climcndslem1  15863  climcndslem2  15864  climcnds  15865  divcnv  15867  divcnvshft  15869  supcvg  15870  trireciplem  15876  trirecip  15877  expcnv  15878  geo2lim  15889  geoisum1  15893  geoisum1c  15894  mertenslem2  15899  prodeq2ii  15925  prodmolem3  15947  prodmolem2a  15948  fprod  15955  prod0  15957  prod1  15958  fprodss  15962  fprodser  15963  fprodcl2lem  15964  fprodmul  15974  fproddiv  15975  fprodn0  15993  fallfacval4  16057  bpoly4  16073  ege2le3  16104  rpnnen2lem3  16232  rpnnen2lem5  16234  rpnnen2lem8  16237  rpnnen2lem12  16241  ruclem6  16251  pwp1fsum  16408  bezoutlem2  16557  bezoutlem3  16558  lcmcllem  16613  lcmledvds  16616  lcmfval  16638  lcmfcllem  16642  lcmfledvds  16649  isprm3  16700  phicl2  16785  phibndlem  16787  eulerthlem2  16799  odzcllem  16810  odzdvds  16813  iserodd  16853  pcmptcl  16909  pcmpt  16910  pockthlem  16923  pockthg  16924  unbenlem  16926  prmreclem3  16936  prmreclem5  16938  prmreclem6  16939  prmrec  16940  1arith  16945  4sqlem13  16975  4sqlem14  16976  4sqlem17  16979  4sqlem18  16980  vdwlem1  16999  vdwlem2  17000  vdwlem3  17001  vdwlem6  17004  vdwlem8  17006  vdwlem10  17008  vdw  17012  vdwnnlem3  17015  prmlem1a  17124  mulgnnp1  19063  mulgnnsubcl  19067  mulgnn0z  19082  mulgnndir  19084  mulgpropd  19097  odfval  19511  odlem1  19514  odlem2  19518  gexlem1  19558  gexlem2  19561  gexcl3  19566  sylow1lem1  19577  efgsdmi  19711  efgsrel  19713  efgs1b  19715  efgsp1  19716  mulgnn0di  19804  lt6abl  19874  gsumval3eu  19883  gsumval3  19886  gsumzcl2  19889  gsumzaddlem  19900  gsumconst  19913  gsumzmhm  19916  gsumzoppg  19923  zringlpirlem2  21422  zringlpirlem3  21423  lmcnp  23240  lmmo  23316  1stcelcls  23397  1stccnp  23398  1stckgenlem  23489  1stckgen  23490  imasdsf1olem  24310  cphipval  25193  lmnn  25213  cmetcaulem  25238  iscmet2  25244  causs  25248  nglmle  25252  caubl  25258  iscmet3i  25262  bcthlem5  25278  ovolsf  25423  ovollb2lem  25439  ovolctb  25441  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliun  25456  ovoliun2  25457  ovoliunnul  25458  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem2  25469  ovolicc2lem3  25470  ovolicc2lem4  25471  iundisj  25499  iundisj2  25500  voliunlem1  25501  voliunlem2  25502  voliunlem3  25503  volsup  25507  ioombl1lem4  25512  uniioovol  25530  uniioombllem2  25534  uniioombllem3  25536  uniioombllem4  25537  uniioombllem6  25539  vitalilem4  25562  vitalilem5  25563  itg1climres  25665  mbfi1fseqlem6  25671  mbfi1flimlem  25673  mbfmullem2  25675  itg2monolem1  25701  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  plyeq0lem  26165  vieta1lem2  26269  elqaalem1  26277  elqaalem3  26279  aaliou3lem4  26304  aaliou3lem7  26307  dvtaylp  26328  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  pserdv2  26390  abelthlem6  26396  abelthlem9  26400  logtayl  26619  logtaylsum  26620  logtayl2  26621  atantayl  26897  leibpilem2  26901  leibpi  26902  birthdaylem2  26912  dfef2  26931  divsqrtsumlem  26940  emcllem2  26957  emcllem4  26959  emcllem5  26960  emcllem6  26961  emcllem7  26962  harmonicbnd4  26971  fsumharmonic  26972  zetacvg  26975  lgamgulmlem4  26992  lgamgulmlem6  26994  lgamgulm2  26996  lgamcvglem  27000  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  regamcl  27021  relgamcl  27022  lgam1  27024  wilthlem3  27030  ftalem2  27034  ftalem4  27036  ftalem5  27037  basellem5  27045  basellem6  27046  basellem7  27047  basellem8  27048  basellem9  27049  ppiprm  27111  ppinprm  27112  chtprm  27113  chtnprm  27114  chpp1  27115  vma1  27126  ppiltx  27137  fsumvma2  27175  chpchtsum  27180  logfacbnd3  27184  logexprlim  27186  bposlem5  27249  lgscllem  27265  lgsval2lem  27268  lgsval4a  27280  lgsneg  27282  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  gausslemma2dlem3  27329  lgsquadlem2  27342  chebbnd1lem1  27430  chtppilimlem1  27434  rplogsumlem1  27445  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasum2lem  27457  dchrvmasumiflem1  27462  dchrvmaeq0  27465  dchrisum0flblem2  27470  dchrisum0flb  27471  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  mudivsum  27491  mulogsum  27493  logdivsum  27494  mulog2sumlem2  27496  log2sumbnd  27505  selberg2lem  27511  logdivbnd  27517  pntrsumo1  27526  pntrsumbnd2  27528  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem6a  27543  pntlemf  27566  eedimeq  28823  axlowdimlem6  28872  axlowdimlem16  28882  axlowdimlem17  28883  ipval2  30634  minvecolem3  30803  minvecolem4b  30805  minvecolem4  30807  h2hcau  30906  h2hlm  30907  hlimadd  31120  hlim0  31162  hhsscms  31205  occllem  31230  nlelchi  31988  opsqrlem4  32070  hmopidmchi  32078  iundisjf  32516  iundisj2f  32517  ssnnssfz  32710  iundisjfi  32719  iundisj2fi  32720  chnub  32938  cycpmco2lem7  33089  cycpmrn  33100  1smat1  33781  submat1n  33782  submatres  33783  submateqlem2  33785  lmatfval  33791  madjusmdetlem1  33804  madjusmdetlem2  33805  madjusmdetlem3  33806  madjusmdetlem4  33807  lmlim  33924  rge0scvg  33926  lmxrge0  33929  lmdvg  33930  esumfzf  34046  esumfsup  34047  esumpcvgval  34055  esumpmono  34056  esumcvg  34063  esumcvgsum  34065  esumsup  34066  fiunelros  34151  eulerpartlemsv2  34336  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemv  34342  eulerpartlemb  34346  fiblem  34376  fibp1  34379  rrvsum  34432  dstfrvclim1  34456  ballotlem1ri  34513  signsvfn  34560  chtvalz  34607  circlemethhgt  34621  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  erdszelem7  35165  cvmliftlem5  35257  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem13  35264  sinccvg  35641  circum  35642  divcnvlin  35696  iprodgam  35705  faclimlem1  35706  faclimlem2  35707  faclim  35709  iprodfac  35710  faclim2  35711  poimirlem3  37593  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  lmclim2  37728  geomcau  37729  heibor1lem  37779  heibor1  37780  bfplem1  37792  bfplem2  37793  rrncmslem  37802  rrncms  37803  aks4d1p1p1  42022  sticksstones10  42114  sticksstones12a  42116  metakunt20  42183  fz1sump1  42306  sumcubes  42309  nna4b4nsq  42630  eldioph3b  42735  diophin  42742  diophun  42743  diophren  42783  jm3.1lem2  42989  dgraalem  43116  dgraaub  43119  dftrcl3  43691  trclfvdecomr  43699  hashnzfz2  44293  hashnzfzclim  44294  dvradcnv2  44319  binomcxplemnotnn0  44328  nnsplit  45333  rexanuz2nf  45467  clim1fr1  45578  sumnnodd  45607  limsup10exlem  45749  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  stoweidlem7  45984  stoweidlem14  45991  stoweidlem20  45997  stoweidlem34  46011  wallispilem5  46046  wallispi  46047  stirlinglem1  46051  stirlinglem5  46055  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  stirlingr  46067  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  fourierdlem11  46095  fourierdlem31  46115  fourierdlem48  46131  fourierdlem49  46132  fourierdlem69  46152  fourierdlem73  46156  fourierdlem81  46164  fourierdlem93  46176  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fouriersw  46208  sge0ad2en  46408  voliunsge0lem  46449  caragenunicl  46501  caratheodorylem2  46504  hoidmvlelem3  46574  ovolval2lem  46620  ovolval2  46621  vonioolem2  46658  vonicclem2  46661  fmtno4prmfac  47534