Theorem nnuz 12714

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  {crab 3403   class class class wbr 5089  ‘cfv 6473  1c1 10965   ≤ cle 11103  ℕcn 12066  ℤcz 12412  ℤ_≥cuz 12675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-er 8561  df-en 8797  df-dom 8798  df-sdom 8799  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-nn 12067  df-z 12413  df-uz 12676

This theorem is referenced by:  elnnuz  12715  eluz2nn  12717  uznnssnn  12728  nnwo  12746  eluznn  12751  nninf  12762  fzssnn  13393  fseq1p1m1  13423  prednn  13472  elfzo1  13530  ltwenn  13775  nnnfi  13779  ser1const  13872  expp1  13882  digit1  14045  facnn  14082  fac0  14083  facp1  14085  faclbnd4lem1  14100  bcm1k  14122  bcval5  14125  bcpasc  14128  fz1isolem  14267  seqcoll  14270  seqcoll2  14271  climuni  15352  isercolllem2  15468  isercoll  15470  sumeq2ii  15496  summolem3  15517  summolem2a  15518  fsum  15523  sum0  15524  sumz  15525  fsumcl2lem  15534  fsumadd  15543  fsummulc2  15587  fsumrelem  15610  isumnn0nn  15645  climcndslem1  15652  climcndslem2  15653  climcnds  15654  divcnv  15656  divcnvshft  15658  supcvg  15659  trireciplem  15665  trirecip  15666  expcnv  15667  geo2lim  15678  geoisum1  15682  geoisum1c  15683  mertenslem2  15688  prodeq2ii  15714  prodmolem3  15734  prodmolem2a  15735  fprod  15742  prod0  15744  prod1  15745  fprodss  15749  fprodser  15750  fprodcl2lem  15751  fprodmul  15761  fproddiv  15762  fprodn0  15780  fallfacval4  15844  bpoly4  15860  ege2le3  15890  rpnnen2lem3  16016  rpnnen2lem5  16018  rpnnen2lem8  16021  rpnnen2lem12  16025  ruclem6  16035  pwp1fsum  16191  bezoutlem2  16339  bezoutlem3  16340  lcmcllem  16390  lcmledvds  16393  lcmfval  16415  lcmfcllem  16419  lcmfledvds  16426  isprm3  16477  phicl2  16558  phibndlem  16560  eulerthlem2  16572  odzcllem  16582  odzdvds  16585  iserodd  16625  pcmptcl  16681  pcmpt  16682  pockthlem  16695  pockthg  16696  unbenlem  16698  prmreclem3  16708  prmreclem5  16710  prmreclem6  16711  prmrec  16712  1arith  16717  4sqlem13  16747  4sqlem14  16748  4sqlem17  16751  4sqlem18  16752  vdwlem1  16771  vdwlem2  16772  vdwlem3  16773  vdwlem6  16776  vdwlem8  16778  vdwlem10  16780  vdw  16784  vdwnnlem3  16787  prmlem1a  16897  mulgnnp1  18800  mulgnnsubcl  18804  mulgnn0z  18818  mulgnndir  18820  mulgpropd  18833  odfval  19228  odlem1  19231  odlem2  19235  gexlem1  19272  gexlem2  19275  gexcl3  19280  sylow1lem1  19291  efgsdmi  19425  efgsrel  19427  efgs1b  19429  efgsp1  19430  mulgnn0di  19514  lt6abl  19583  gsumval3eu  19592  gsumval3  19595  gsumzcl2  19598  gsumzaddlem  19609  gsumconst  19622  gsumzmhm  19625  gsumzoppg  19632  zringlpirlem2  20783  zringlpirlem3  20784  lmcnp  22553  lmmo  22629  1stcelcls  22710  1stccnp  22711  1stckgenlem  22802  1stckgen  22803  imasdsf1olem  23624  cphipval  24505  lmnn  24525  cmetcaulem  24550  iscmet2  24556  causs  24560  nglmle  24564  caubl  24570  iscmet3i  24574  bcthlem5  24590  ovolsf  24734  ovollb2lem  24750  ovolctb  24752  ovolunlem1a  24758  ovolunlem1  24759  ovoliunlem1  24764  ovoliun  24767  ovoliun2  24768  ovoliunnul  24769  ovolscalem1  24775  ovolicc1  24778  ovolicc2lem2  24780  ovolicc2lem3  24781  ovolicc2lem4  24782  iundisj  24810  iundisj2  24811  voliunlem1  24812  voliunlem2  24813  voliunlem3  24814  volsup  24818  ioombl1lem4  24823  uniioovol  24841  uniioombllem2  24845  uniioombllem3  24847  uniioombllem4  24848  uniioombllem6  24850  vitalilem4  24873  vitalilem5  24874  itg1climres  24977  mbfi1fseqlem6  24983  mbfi1flimlem  24985  mbfmullem2  24987  itg2monolem1  25013  itg2i1fseqle  25017  itg2i1fseq  25018  itg2i1fseq2  25019  itg2addlem  25021  plyeq0lem  25469  vieta1lem2  25569  elqaalem1  25577  elqaalem3  25579  aaliou3lem4  25604  aaliou3lem7  25607  dvtaylp  25627  taylthlem2  25631  pserdvlem2  25685  pserdv2  25687  abelthlem6  25693  abelthlem9  25697  logtayl  25913  logtaylsum  25914  logtayl2  25915  atantayl  26185  leibpilem2  26189  leibpi  26190  birthdaylem2  26200  dfef2  26218  divsqrtsumlem  26227  emcllem2  26244  emcllem4  26246  emcllem5  26247  emcllem6  26248  emcllem7  26249  harmonicbnd4  26258  fsumharmonic  26259  zetacvg  26262  lgamgulmlem4  26279  lgamgulmlem6  26281  lgamgulm2  26283  lgamcvglem  26287  lgamcvg2  26302  gamcvg  26303  gamcvg2lem  26306  regamcl  26308  relgamcl  26309  lgam1  26311  wilthlem3  26317  ftalem2  26321  ftalem4  26323  ftalem5  26324  basellem5  26332  basellem6  26333  basellem7  26334  basellem8  26335  basellem9  26336  ppiprm  26398  ppinprm  26399  chtprm  26400  chtnprm  26401  chpp1  26402  vma1  26413  ppiltx  26424  fsumvma2  26460  chpchtsum  26465  logfacbnd3  26469  logexprlim  26471  bposlem5  26534  lgscllem  26550  lgsval2lem  26553  lgsval4a  26565  lgsneg  26567  lgsdir  26578  lgsdilem2  26579  lgsdi  26580  lgsne0  26581  gausslemma2dlem3  26614  lgsquadlem2  26627  chebbnd1lem1  26715  chtppilimlem1  26719  rplogsumlem1  26730  rplogsumlem2  26731  rpvmasumlem  26733  dchrisumlema  26734  dchrisumlem2  26736  dchrisumlem3  26737  dchrmusum2  26740  dchrvmasum2lem  26742  dchrvmasumiflem1  26747  dchrvmaeq0  26750  dchrisum0flblem2  26755  dchrisum0flb  26756  dchrisum0re  26759  dchrisum0lem1b  26761  dchrisum0lem1  26762  dchrisum0lem2a  26763  dchrisum0lem2  26764  dchrisum0lem3  26765  mudivsum  26776  mulogsum  26778  logdivsum  26779  mulog2sumlem2  26781  log2sumbnd  26790  selberg2lem  26796  logdivbnd  26802  pntrsumo1  26811  pntrsumbnd2  26813  pntrlog2bndlem2  26824  pntrlog2bndlem4  26826  pntrlog2bndlem6a  26828  pntlemf  26851  eedimeq  27496  axlowdimlem6  27545  axlowdimlem16  27555  axlowdimlem17  27556  ipval2  29298  minvecolem3  29467  minvecolem4b  29469  minvecolem4  29471  h2hcau  29570  h2hlm  29571  hlimadd  29784  hlim0  29826  hhsscms  29869  occllem  29894  nlelchi  30652  opsqrlem4  30734  hmopidmchi  30742  iundisjf  31156  iundisj2f  31157  ssnnssfz  31336  iundisjfi  31345  iundisj2fi  31346  cycpmco2lem7  31627  cycpmrn  31638  1smat1  31993  submat1n  31994  submatres  31995  submateqlem2  31997  lmatfval  32003  madjusmdetlem1  32016  madjusmdetlem2  32017  madjusmdetlem3  32018  madjusmdetlem4  32019  lmlim  32136  rge0scvg  32138  lmxrge0  32141  lmdvg  32142  esumfzf  32276  esumfsup  32277  esumpcvgval  32285  esumpmono  32286  esumcvg  32293  esumcvgsum  32295  esumsup  32296  fiunelros  32381  eulerpartlemsv2  32566  eulerpartlems  32568  eulerpartlemsv3  32569  eulerpartlemv  32572  eulerpartlemb  32576  fiblem  32606  fibp1  32609  rrvsum  32662  dstfrvclim1  32685  ballotlem1ri  32742  signsvfn  32802  chtvalz  32850  circlemethhgt  32864  subfacp1lem1  33381  subfacp1lem5  33386  subfacp1lem6  33387  erdszelem7  33399  cvmliftlem5  33491  cvmliftlem7  33493  cvmliftlem10  33496  cvmliftlem13  33498  sinccvg  33871  circum  33872  divcnvlin  33932  iprodgam  33942  faclimlem1  33943  faclimlem2  33944  faclim  33946  iprodfac  33947  faclim2  33948  poimirlem3  35878  poimirlem4  35879  poimirlem6  35881  poimirlem7  35882  poimirlem8  35883  poimirlem12  35887  poimirlem15  35890  poimirlem16  35891  poimirlem17  35892  poimirlem18  35893  poimirlem19  35894  poimirlem20  35895  poimirlem22  35897  poimirlem23  35898  poimirlem24  35899  poimirlem25  35900  poimirlem27  35902  poimirlem28  35903  poimirlem29  35904  poimirlem30  35905  poimirlem31  35906  mblfinlem2  35913  ovoliunnfl  35917  voliunnfl  35919  volsupnfl  35920  lmclim2  36014  geomcau  36015  heibor1lem  36065  heibor1  36066  bfplem1  36078  bfplem2  36079  rrncmslem  36088  rrncms  36089  aks4d1p1p1  40318  sticksstones10  40361  sticksstones12a  40363  metakunt20  40394  nna4b4nsq  40747  eldioph3b  40837  diophin  40844  diophun  40845  diophren  40885  jm3.1lem2  41091  dgraalem  41221  dgraaub  41224  dftrcl3  41638  trclfvdecomr  41646  hashnzfz2  42249  hashnzfzclim  42250  dvradcnv2  42275  binomcxplemnotnn0  42284  nnsplit  43221  clim1fr1  43467  sumnnodd  43496  limsup10exlem  43638  fprodsubrecnncnvlem  43773  fprodaddrecnncnvlem  43775  stoweidlem7  43873  stoweidlem14  43880  stoweidlem20  43886  stoweidlem34  43900  wallispilem5  43935  wallispi  43936  stirlinglem1  43940  stirlinglem5  43944  stirlinglem7  43946  stirlinglem8  43947  stirlinglem10  43949  stirlinglem11  43950  stirlinglem12  43951  stirlinglem13  43952  stirlinglem14  43953  stirlinglem15  43954  stirlingr  43956  dirkertrigeqlem2  43965  dirkertrigeqlem3  43966  fourierdlem11  43984  fourierdlem31  44004  fourierdlem48  44020  fourierdlem49  44021  fourierdlem69  44041  fourierdlem73  44045  fourierdlem81  44053  fourierdlem93  44065  fourierdlem103  44075  fourierdlem104  44076  fourierdlem112  44084  fouriersw  44097  sge0ad2en  44295  voliunsge0lem  44336  caragenunicl  44388  caratheodorylem2  44391  hoidmvlelem3  44461  ovolval2lem  44507  ovolval2  44508  vonioolem2  44545  vonicclem2  44548  fmtno4prmfac  45364