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

Syntax hints:   = wceq 1534   ∈ wcel 2099  {crab 3428   class class class wbr 5142  ‘cfv 6542  1c1 11133   ≤ cle 11273  ℕcn 12236  ℤcz 12582  ℤ_≥cuz 12846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-nn 12237  df-z 12583  df-uz 12847

This theorem is referenced by:  elnnuz  12890  eluz2nn  12892  uznnssnn  12903  nnwo  12921  eluznn  12926  nninf  12937  fzssnn  13571  fseq1p1m1  13601  prednn  13650  elfzo1  13708  ltwenn  13953  nnnfi  13957  ser1const  14049  expp1  14059  digit1  14225  facnn  14260  fac0  14261  facp1  14263  faclbnd4lem1  14278  bcm1k  14300  bcval5  14303  bcpasc  14306  fz1isolem  14448  seqcoll  14451  seqcoll2  14452  climuni  15522  isercolllem2  15638  isercoll  15640  sumeq2ii  15665  summolem3  15686  summolem2a  15687  fsum  15692  sum0  15693  sumz  15694  fsumcl2lem  15703  fsumadd  15712  fsummulc2  15756  fsumrelem  15779  isumnn0nn  15814  climcndslem1  15821  climcndslem2  15822  climcnds  15823  divcnv  15825  divcnvshft  15827  supcvg  15828  trireciplem  15834  trirecip  15835  expcnv  15836  geo2lim  15847  geoisum1  15851  geoisum1c  15852  mertenslem2  15857  prodeq2ii  15883  prodmolem3  15903  prodmolem2a  15904  fprod  15911  prod0  15913  prod1  15914  fprodss  15918  fprodser  15919  fprodcl2lem  15920  fprodmul  15930  fproddiv  15931  fprodn0  15949  fallfacval4  16013  bpoly4  16029  ege2le3  16060  rpnnen2lem3  16186  rpnnen2lem5  16188  rpnnen2lem8  16191  rpnnen2lem12  16195  ruclem6  16205  pwp1fsum  16361  bezoutlem2  16509  bezoutlem3  16510  lcmcllem  16560  lcmledvds  16563  lcmfval  16585  lcmfcllem  16589  lcmfledvds  16596  isprm3  16647  phicl2  16730  phibndlem  16732  eulerthlem2  16744  odzcllem  16754  odzdvds  16757  iserodd  16797  pcmptcl  16853  pcmpt  16854  pockthlem  16867  pockthg  16868  unbenlem  16870  prmreclem3  16880  prmreclem5  16882  prmreclem6  16883  prmrec  16884  1arith  16889  4sqlem13  16919  4sqlem14  16920  4sqlem17  16923  4sqlem18  16924  vdwlem1  16943  vdwlem2  16944  vdwlem3  16945  vdwlem6  16948  vdwlem8  16950  vdwlem10  16952  vdw  16956  vdwnnlem3  16959  prmlem1a  17069  mulgnnp1  19030  mulgnnsubcl  19034  mulgnn0z  19049  mulgnndir  19051  mulgpropd  19064  odfval  19480  odlem1  19483  odlem2  19487  gexlem1  19527  gexlem2  19530  gexcl3  19535  sylow1lem1  19546  efgsdmi  19680  efgsrel  19682  efgs1b  19684  efgsp1  19685  mulgnn0di  19773  lt6abl  19843  gsumval3eu  19852  gsumval3  19855  gsumzcl2  19858  gsumzaddlem  19869  gsumconst  19882  gsumzmhm  19885  gsumzoppg  19892  zringlpirlem2  21382  zringlpirlem3  21383  lmcnp  23201  lmmo  23277  1stcelcls  23358  1stccnp  23359  1stckgenlem  23450  1stckgen  23451  imasdsf1olem  24272  cphipval  25164  lmnn  25184  cmetcaulem  25209  iscmet2  25215  causs  25219  nglmle  25223  caubl  25229  iscmet3i  25233  bcthlem5  25249  ovolsf  25394  ovollb2lem  25410  ovolctb  25412  ovolunlem1a  25418  ovolunlem1  25419  ovoliunlem1  25424  ovoliun  25427  ovoliun2  25428  ovoliunnul  25429  ovolscalem1  25435  ovolicc1  25438  ovolicc2lem2  25440  ovolicc2lem3  25441  ovolicc2lem4  25442  iundisj  25470  iundisj2  25471  voliunlem1  25472  voliunlem2  25473  voliunlem3  25474  volsup  25478  ioombl1lem4  25483  uniioovol  25501  uniioombllem2  25505  uniioombllem3  25507  uniioombllem4  25508  uniioombllem6  25510  vitalilem4  25533  vitalilem5  25534  itg1climres  25637  mbfi1fseqlem6  25643  mbfi1flimlem  25645  mbfmullem2  25647  itg2monolem1  25673  itg2i1fseqle  25677  itg2i1fseq  25678  itg2i1fseq2  25679  itg2addlem  25681  plyeq0lem  26137  vieta1lem2  26239  elqaalem1  26247  elqaalem3  26249  aaliou3lem4  26274  aaliou3lem7  26277  dvtaylp  26298  taylthlem2  26302  taylthlem2OLD  26303  pserdvlem2  26358  pserdv2  26360  abelthlem6  26366  abelthlem9  26370  logtayl  26587  logtaylsum  26588  logtayl2  26589  atantayl  26862  leibpilem2  26866  leibpi  26867  birthdaylem2  26877  dfef2  26896  divsqrtsumlem  26905  emcllem2  26922  emcllem4  26924  emcllem5  26925  emcllem6  26926  emcllem7  26927  harmonicbnd4  26936  fsumharmonic  26937  zetacvg  26940  lgamgulmlem4  26957  lgamgulmlem6  26959  lgamgulm2  26961  lgamcvglem  26965  lgamcvg2  26980  gamcvg  26981  gamcvg2lem  26984  regamcl  26986  relgamcl  26987  lgam1  26989  wilthlem3  26995  ftalem2  26999  ftalem4  27001  ftalem5  27002  basellem5  27010  basellem6  27011  basellem7  27012  basellem8  27013  basellem9  27014  ppiprm  27076  ppinprm  27077  chtprm  27078  chtnprm  27079  chpp1  27080  vma1  27091  ppiltx  27102  fsumvma2  27140  chpchtsum  27145  logfacbnd3  27149  logexprlim  27151  bposlem5  27214  lgscllem  27230  lgsval2lem  27233  lgsval4a  27245  lgsneg  27247  lgsdir  27258  lgsdilem2  27259  lgsdi  27260  lgsne0  27261  gausslemma2dlem3  27294  lgsquadlem2  27307  chebbnd1lem1  27395  chtppilimlem1  27399  rplogsumlem1  27410  rplogsumlem2  27411  rpvmasumlem  27413  dchrisumlema  27414  dchrisumlem2  27416  dchrisumlem3  27417  dchrmusum2  27420  dchrvmasum2lem  27422  dchrvmasumiflem1  27427  dchrvmaeq0  27430  dchrisum0flblem2  27435  dchrisum0flb  27436  dchrisum0re  27439  dchrisum0lem1b  27441  dchrisum0lem1  27442  dchrisum0lem2a  27443  dchrisum0lem2  27444  dchrisum0lem3  27445  mudivsum  27456  mulogsum  27458  logdivsum  27459  mulog2sumlem2  27461  log2sumbnd  27470  selberg2lem  27476  logdivbnd  27482  pntrsumo1  27491  pntrsumbnd2  27493  pntrlog2bndlem2  27504  pntrlog2bndlem4  27506  pntrlog2bndlem6a  27508  pntlemf  27531  eedimeq  28702  axlowdimlem6  28751  axlowdimlem16  28761  axlowdimlem17  28762  ipval2  30510  minvecolem3  30679  minvecolem4b  30681  minvecolem4  30683  h2hcau  30782  h2hlm  30783  hlimadd  30996  hlim0  31038  hhsscms  31081  occllem  31106  nlelchi  31864  opsqrlem4  31946  hmopidmchi  31954  iundisjf  32372  iundisj2f  32373  ssnnssfz  32549  iundisjfi  32558  iundisj2fi  32559  cycpmco2lem7  32847  cycpmrn  32858  1smat1  33399  submat1n  33400  submatres  33401  submateqlem2  33403  lmatfval  33409  madjusmdetlem1  33422  madjusmdetlem2  33423  madjusmdetlem3  33424  madjusmdetlem4  33425  lmlim  33542  rge0scvg  33544  lmxrge0  33547  lmdvg  33548  esumfzf  33682  esumfsup  33683  esumpcvgval  33691  esumpmono  33692  esumcvg  33699  esumcvgsum  33701  esumsup  33702  fiunelros  33787  eulerpartlemsv2  33972  eulerpartlems  33974  eulerpartlemsv3  33975  eulerpartlemv  33978  eulerpartlemb  33982  fiblem  34012  fibp1  34015  rrvsum  34068  dstfrvclim1  34091  ballotlem1ri  34148  signsvfn  34208  chtvalz  34255  circlemethhgt  34269  subfacp1lem1  34783  subfacp1lem5  34788  subfacp1lem6  34789  erdszelem7  34801  cvmliftlem5  34893  cvmliftlem7  34895  cvmliftlem10  34898  cvmliftlem13  34900  sinccvg  35271  circum  35272  divcnvlin  35321  iprodgam  35330  faclimlem1  35331  faclimlem2  35332  faclim  35334  iprodfac  35335  faclim2  35336  poimirlem3  37090  poimirlem4  37091  poimirlem6  37093  poimirlem7  37094  poimirlem8  37095  poimirlem12  37099  poimirlem15  37102  poimirlem16  37103  poimirlem17  37104  poimirlem18  37105  poimirlem19  37106  poimirlem20  37107  poimirlem22  37109  poimirlem23  37110  poimirlem24  37111  poimirlem25  37112  poimirlem27  37114  poimirlem28  37115  poimirlem29  37116  poimirlem30  37117  poimirlem31  37118  mblfinlem2  37125  ovoliunnfl  37129  voliunnfl  37131  volsupnfl  37132  lmclim2  37225  geomcau  37226  heibor1lem  37276  heibor1  37277  bfplem1  37289  bfplem2  37290  rrncmslem  37299  rrncms  37300  aks4d1p1p1  41528  sticksstones10  41621  sticksstones12a  41623  metakunt20  41670  fz1sump1  41864  sumcubes  41867  nna4b4nsq  42078  eldioph3b  42179  diophin  42186  diophun  42187  diophren  42227  jm3.1lem2  42433  dgraalem  42563  dgraaub  42566  dftrcl3  43144  trclfvdecomr  43152  hashnzfz2  43752  hashnzfzclim  43753  dvradcnv2  43778  binomcxplemnotnn0  43787  nnsplit  44734  rexanuz2nf  44869  clim1fr1  44983  sumnnodd  45012  limsup10exlem  45154  fprodsubrecnncnvlem  45289  fprodaddrecnncnvlem  45291  stoweidlem7  45389  stoweidlem14  45396  stoweidlem20  45402  stoweidlem34  45416  wallispilem5  45451  wallispi  45452  stirlinglem1  45456  stirlinglem5  45460  stirlinglem7  45462  stirlinglem8  45463  stirlinglem10  45465  stirlinglem11  45466  stirlinglem12  45467  stirlinglem13  45468  stirlinglem14  45469  stirlinglem15  45470  stirlingr  45472  dirkertrigeqlem2  45481  dirkertrigeqlem3  45482  fourierdlem11  45500  fourierdlem31  45520  fourierdlem48  45536  fourierdlem49  45537  fourierdlem69  45557  fourierdlem73  45561  fourierdlem81  45569  fourierdlem93  45581  fourierdlem103  45591  fourierdlem104  45592  fourierdlem112  45600  fouriersw  45613  sge0ad2en  45813  voliunsge0lem  45854  caragenunicl  45906  caratheodorylem2  45909  hoidmvlelem3  45979  ovolval2lem  46025  ovolval2  46026  vonioolem2  46063  vonicclem2  46066  fmtno4prmfac  46906