Theorem nnuz 12861

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  {crab 3432   class class class wbr 5147  ‘cfv 6540  1c1 11107   ≤ cle 11245  ℕcn 12208  ℤcz 12554  ℤ_≥cuz 12818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-z 12555  df-uz 12819

This theorem is referenced by:  elnnuz  12862  eluz2nn  12864  uznnssnn  12875  nnwo  12893  eluznn  12898  nninf  12909  fzssnn  13541  fseq1p1m1  13571  prednn  13620  elfzo1  13678  ltwenn  13923  nnnfi  13927  ser1const  14020  expp1  14030  digit1  14196  facnn  14231  fac0  14232  facp1  14234  faclbnd4lem1  14249  bcm1k  14271  bcval5  14274  bcpasc  14277  fz1isolem  14418  seqcoll  14421  seqcoll2  14422  climuni  15492  isercolllem2  15608  isercoll  15610  sumeq2ii  15635  summolem3  15656  summolem2a  15657  fsum  15662  sum0  15663  sumz  15664  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumrelem  15749  isumnn0nn  15784  climcndslem1  15791  climcndslem2  15792  climcnds  15793  divcnv  15795  divcnvshft  15797  supcvg  15798  trireciplem  15804  trirecip  15805  expcnv  15806  geo2lim  15817  geoisum1  15821  geoisum1c  15822  mertenslem2  15827  prodeq2ii  15853  prodmolem3  15873  prodmolem2a  15874  fprod  15881  prod0  15883  prod1  15884  fprodss  15888  fprodser  15889  fprodcl2lem  15890  fprodmul  15900  fproddiv  15901  fprodn0  15919  fallfacval4  15983  bpoly4  15999  ege2le3  16029  rpnnen2lem3  16155  rpnnen2lem5  16157  rpnnen2lem8  16160  rpnnen2lem12  16164  ruclem6  16174  pwp1fsum  16330  bezoutlem2  16478  bezoutlem3  16479  lcmcllem  16529  lcmledvds  16532  lcmfval  16554  lcmfcllem  16558  lcmfledvds  16565  isprm3  16616  phicl2  16697  phibndlem  16699  eulerthlem2  16711  odzcllem  16721  odzdvds  16724  iserodd  16764  pcmptcl  16820  pcmpt  16821  pockthlem  16834  pockthg  16835  unbenlem  16837  prmreclem3  16847  prmreclem5  16849  prmreclem6  16850  prmrec  16851  1arith  16856  4sqlem13  16886  4sqlem14  16887  4sqlem17  16890  4sqlem18  16891  vdwlem1  16910  vdwlem2  16911  vdwlem3  16912  vdwlem6  16915  vdwlem8  16917  vdwlem10  16919  vdw  16923  vdwnnlem3  16926  prmlem1a  17036  mulgnnp1  18956  mulgnnsubcl  18960  mulgnn0z  18975  mulgnndir  18977  mulgpropd  18990  odfval  19394  odlem1  19397  odlem2  19401  gexlem1  19441  gexlem2  19444  gexcl3  19449  sylow1lem1  19460  efgsdmi  19594  efgsrel  19596  efgs1b  19598  efgsp1  19599  mulgnn0di  19687  lt6abl  19757  gsumval3eu  19766  gsumval3  19769  gsumzcl2  19772  gsumzaddlem  19783  gsumconst  19796  gsumzmhm  19799  gsumzoppg  19806  zringlpirlem2  21024  zringlpirlem3  21025  lmcnp  22799  lmmo  22875  1stcelcls  22956  1stccnp  22957  1stckgenlem  23048  1stckgen  23049  imasdsf1olem  23870  cphipval  24751  lmnn  24771  cmetcaulem  24796  iscmet2  24802  causs  24806  nglmle  24810  caubl  24816  iscmet3i  24820  bcthlem5  24836  ovolsf  24980  ovollb2lem  24996  ovolctb  24998  ovolunlem1a  25004  ovolunlem1  25005  ovoliunlem1  25010  ovoliun  25013  ovoliun2  25014  ovoliunnul  25015  ovolscalem1  25021  ovolicc1  25024  ovolicc2lem2  25026  ovolicc2lem3  25027  ovolicc2lem4  25028  iundisj  25056  iundisj2  25057  voliunlem1  25058  voliunlem2  25059  voliunlem3  25060  volsup  25064  ioombl1lem4  25069  uniioovol  25087  uniioombllem2  25091  uniioombllem3  25093  uniioombllem4  25094  uniioombllem6  25096  vitalilem4  25119  vitalilem5  25120  itg1climres  25223  mbfi1fseqlem6  25229  mbfi1flimlem  25231  mbfmullem2  25233  itg2monolem1  25259  itg2i1fseqle  25263  itg2i1fseq  25264  itg2i1fseq2  25265  itg2addlem  25267  plyeq0lem  25715  vieta1lem2  25815  elqaalem1  25823  elqaalem3  25825  aaliou3lem4  25850  aaliou3lem7  25853  dvtaylp  25873  taylthlem2  25877  pserdvlem2  25931  pserdv2  25933  abelthlem6  25939  abelthlem9  25943  logtayl  26159  logtaylsum  26160  logtayl2  26161  atantayl  26431  leibpilem2  26435  leibpi  26436  birthdaylem2  26446  dfef2  26464  divsqrtsumlem  26473  emcllem2  26490  emcllem4  26492  emcllem5  26493  emcllem6  26494  emcllem7  26495  harmonicbnd4  26504  fsumharmonic  26505  zetacvg  26508  lgamgulmlem4  26525  lgamgulmlem6  26527  lgamgulm2  26529  lgamcvglem  26533  lgamcvg2  26548  gamcvg  26549  gamcvg2lem  26552  regamcl  26554  relgamcl  26555  lgam1  26557  wilthlem3  26563  ftalem2  26567  ftalem4  26569  ftalem5  26570  basellem5  26578  basellem6  26579  basellem7  26580  basellem8  26581  basellem9  26582  ppiprm  26644  ppinprm  26645  chtprm  26646  chtnprm  26647  chpp1  26648  vma1  26659  ppiltx  26670  fsumvma2  26706  chpchtsum  26711  logfacbnd3  26715  logexprlim  26717  bposlem5  26780  lgscllem  26796  lgsval2lem  26799  lgsval4a  26811  lgsneg  26813  lgsdir  26824  lgsdilem2  26825  lgsdi  26826  lgsne0  26827  gausslemma2dlem3  26860  lgsquadlem2  26873  chebbnd1lem1  26961  chtppilimlem1  26965  rplogsumlem1  26976  rplogsumlem2  26977  rpvmasumlem  26979  dchrisumlema  26980  dchrisumlem2  26982  dchrisumlem3  26983  dchrmusum2  26986  dchrvmasum2lem  26988  dchrvmasumiflem1  26993  dchrvmaeq0  26996  dchrisum0flblem2  27001  dchrisum0flb  27002  dchrisum0re  27005  dchrisum0lem1b  27007  dchrisum0lem1  27008  dchrisum0lem2a  27009  dchrisum0lem2  27010  dchrisum0lem3  27011  mudivsum  27022  mulogsum  27024  logdivsum  27025  mulog2sumlem2  27027  log2sumbnd  27036  selberg2lem  27042  logdivbnd  27048  pntrsumo1  27057  pntrsumbnd2  27059  pntrlog2bndlem2  27070  pntrlog2bndlem4  27072  pntrlog2bndlem6a  27074  pntlemf  27097  eedimeq  28145  axlowdimlem6  28194  axlowdimlem16  28204  axlowdimlem17  28205  ipval2  29947  minvecolem3  30116  minvecolem4b  30118  minvecolem4  30120  h2hcau  30219  h2hlm  30220  hlimadd  30433  hlim0  30475  hhsscms  30518  occllem  30543  nlelchi  31301  opsqrlem4  31383  hmopidmchi  31391  iundisjf  31807  iundisj2f  31808  ssnnssfz  31985  iundisjfi  31994  iundisj2fi  31995  cycpmco2lem7  32278  cycpmrn  32289  1smat1  32772  submat1n  32773  submatres  32774  submateqlem2  32776  lmatfval  32782  madjusmdetlem1  32795  madjusmdetlem2  32796  madjusmdetlem3  32797  madjusmdetlem4  32798  lmlim  32915  rge0scvg  32917  lmxrge0  32920  lmdvg  32921  esumfzf  33055  esumfsup  33056  esumpcvgval  33064  esumpmono  33065  esumcvg  33072  esumcvgsum  33074  esumsup  33075  fiunelros  33160  eulerpartlemsv2  33345  eulerpartlems  33347  eulerpartlemsv3  33348  eulerpartlemv  33351  eulerpartlemb  33355  fiblem  33385  fibp1  33388  rrvsum  33441  dstfrvclim1  33464  ballotlem1ri  33521  signsvfn  33581  chtvalz  33629  circlemethhgt  33643  subfacp1lem1  34158  subfacp1lem5  34163  subfacp1lem6  34164  erdszelem7  34176  cvmliftlem5  34268  cvmliftlem7  34270  cvmliftlem10  34273  cvmliftlem13  34275  sinccvg  34646  circum  34647  divcnvlin  34690  iprodgam  34700  faclimlem1  34701  faclimlem2  34702  faclim  34704  iprodfac  34705  faclim2  34706  poimirlem3  36479  poimirlem4  36480  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem12  36488  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem19  36495  poimirlem20  36496  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem27  36503  poimirlem28  36504  poimirlem29  36505  poimirlem30  36506  poimirlem31  36507  mblfinlem2  36514  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  lmclim2  36614  geomcau  36615  heibor1lem  36665  heibor1  36666  bfplem1  36678  bfplem2  36679  rrncmslem  36688  rrncms  36689  aks4d1p1p1  40916  sticksstones10  40959  sticksstones12a  40961  metakunt20  40992  fz1sump1  41203  sumcubes  41206  nna4b4nsq  41398  eldioph3b  41488  diophin  41495  diophun  41496  diophren  41536  jm3.1lem2  41742  dgraalem  41872  dgraaub  41875  dftrcl3  42456  trclfvdecomr  42464  hashnzfz2  43065  hashnzfzclim  43066  dvradcnv2  43091  binomcxplemnotnn0  43100  nnsplit  44054  rexanuz2nf  44189  clim1fr1  44303  sumnnodd  44332  limsup10exlem  44474  fprodsubrecnncnvlem  44609  fprodaddrecnncnvlem  44611  stoweidlem7  44709  stoweidlem14  44716  stoweidlem20  44722  stoweidlem34  44736  wallispilem5  44771  wallispi  44772  stirlinglem1  44776  stirlinglem5  44780  stirlinglem7  44782  stirlinglem8  44783  stirlinglem10  44785  stirlinglem11  44786  stirlinglem12  44787  stirlinglem13  44788  stirlinglem14  44789  stirlinglem15  44790  stirlingr  44792  dirkertrigeqlem2  44801  dirkertrigeqlem3  44802  fourierdlem11  44820  fourierdlem31  44840  fourierdlem48  44856  fourierdlem49  44857  fourierdlem69  44877  fourierdlem73  44881  fourierdlem81  44889  fourierdlem93  44901  fourierdlem103  44911  fourierdlem104  44912  fourierdlem112  44920  fouriersw  44933  sge0ad2en  45133  voliunsge0lem  45174  caragenunicl  45226  caratheodorylem2  45229  hoidmvlelem3  45299  ovolval2lem  45345  ovolval2  45346  vonioolem2  45383  vonicclem2  45386  fmtno4prmfac  46226