Theorem nnuz 12921

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3436   class class class wbr 5143  ‘cfv 6561  1c1 11156   ≤ cle 11296  ℕcn 12266  ℤcz 12613  ℤ_≥cuz 12878

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 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-z 12614  df-uz 12879

This theorem is referenced by:  elnnuz  12922  eluz2nn  12924  uznnssnn  12937  nnwo  12955  eluznn  12960  nninf  12971  fzssnn  13608  fseq1p1m1  13638  prednn  13691  elfzo1  13752  ltwenn  14003  nnnfi  14007  ser1const  14099  expp1  14109  digit1  14276  facnn  14314  fac0  14315  facp1  14317  faclbnd4lem1  14332  bcm1k  14354  bcval5  14357  bcpasc  14360  fz1isolem  14500  seqcoll  14503  seqcoll2  14504  climuni  15588  isercolllem2  15702  isercoll  15704  sumeq2ii  15729  summolem3  15750  summolem2a  15751  fsum  15756  sum0  15757  sumz  15758  fsumcl2lem  15767  fsumadd  15776  fsummulc2  15820  fsumrelem  15843  isumnn0nn  15878  climcndslem1  15885  climcndslem2  15886  climcnds  15887  divcnv  15889  divcnvshft  15891  supcvg  15892  trireciplem  15898  trirecip  15899  expcnv  15900  geo2lim  15911  geoisum1  15915  geoisum1c  15916  mertenslem2  15921  prodeq2ii  15947  prodmolem3  15969  prodmolem2a  15970  fprod  15977  prod0  15979  prod1  15980  fprodss  15984  fprodser  15985  fprodcl2lem  15986  fprodmul  15996  fproddiv  15997  fprodn0  16015  fallfacval4  16079  bpoly4  16095  ege2le3  16126  rpnnen2lem3  16252  rpnnen2lem5  16254  rpnnen2lem8  16257  rpnnen2lem12  16261  ruclem6  16271  pwp1fsum  16428  bezoutlem2  16577  bezoutlem3  16578  lcmcllem  16633  lcmledvds  16636  lcmfval  16658  lcmfcllem  16662  lcmfledvds  16669  isprm3  16720  phicl2  16805  phibndlem  16807  eulerthlem2  16819  odzcllem  16830  odzdvds  16833  iserodd  16873  pcmptcl  16929  pcmpt  16930  pockthlem  16943  pockthg  16944  unbenlem  16946  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  prmrec  16960  1arith  16965  4sqlem13  16995  4sqlem14  16996  4sqlem17  16999  4sqlem18  17000  vdwlem1  17019  vdwlem2  17020  vdwlem3  17021  vdwlem6  17024  vdwlem8  17026  vdwlem10  17028  vdw  17032  vdwnnlem3  17035  prmlem1a  17144  mulgnnp1  19100  mulgnnsubcl  19104  mulgnn0z  19119  mulgnndir  19121  mulgpropd  19134  odfval  19550  odlem1  19553  odlem2  19557  gexlem1  19597  gexlem2  19600  gexcl3  19605  sylow1lem1  19616  efgsdmi  19750  efgsrel  19752  efgs1b  19754  efgsp1  19755  mulgnn0di  19843  lt6abl  19913  gsumval3eu  19922  gsumval3  19925  gsumzcl2  19928  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsumzoppg  19962  zringlpirlem2  21474  zringlpirlem3  21475  lmcnp  23312  lmmo  23388  1stcelcls  23469  1stccnp  23470  1stckgenlem  23561  1stckgen  23562  imasdsf1olem  24383  cphipval  25277  lmnn  25297  cmetcaulem  25322  iscmet2  25328  causs  25332  nglmle  25336  caubl  25342  iscmet3i  25346  bcthlem5  25362  ovolsf  25507  ovollb2lem  25523  ovolctb  25525  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun  25540  ovoliun2  25541  ovoliunnul  25542  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem2  25553  ovolicc2lem3  25554  ovolicc2lem4  25555  iundisj  25583  iundisj2  25584  voliunlem1  25585  voliunlem2  25586  voliunlem3  25587  volsup  25591  ioombl1lem4  25596  uniioovol  25614  uniioombllem2  25618  uniioombllem3  25620  uniioombllem4  25621  uniioombllem6  25623  vitalilem4  25646  vitalilem5  25647  itg1climres  25749  mbfi1fseqlem6  25755  mbfi1flimlem  25757  mbfmullem2  25759  itg2monolem1  25785  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  plyeq0lem  26249  vieta1lem2  26353  elqaalem1  26361  elqaalem3  26363  aaliou3lem4  26388  aaliou3lem7  26391  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  pserdv2  26474  abelthlem6  26480  abelthlem9  26484  logtayl  26702  logtaylsum  26703  logtayl2  26704  atantayl  26980  leibpilem2  26984  leibpi  26985  birthdaylem2  26995  dfef2  27014  divsqrtsumlem  27023  emcllem2  27040  emcllem4  27042  emcllem5  27043  emcllem6  27044  emcllem7  27045  harmonicbnd4  27054  fsumharmonic  27055  zetacvg  27058  lgamgulmlem4  27075  lgamgulmlem6  27077  lgamgulm2  27079  lgamcvglem  27083  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  regamcl  27104  relgamcl  27105  lgam1  27107  wilthlem3  27113  ftalem2  27117  ftalem4  27119  ftalem5  27120  basellem5  27128  basellem6  27129  basellem7  27130  basellem8  27131  basellem9  27132  ppiprm  27194  ppinprm  27195  chtprm  27196  chtnprm  27197  chpp1  27198  vma1  27209  ppiltx  27220  fsumvma2  27258  chpchtsum  27263  logfacbnd3  27267  logexprlim  27269  bposlem5  27332  lgscllem  27348  lgsval2lem  27351  lgsval4a  27363  lgsneg  27365  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  gausslemma2dlem3  27412  lgsquadlem2  27425  chebbnd1lem1  27513  chtppilimlem1  27517  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasum2lem  27540  dchrvmasumiflem1  27545  dchrvmaeq0  27548  dchrisum0flblem2  27553  dchrisum0flb  27554  dchrisum0re  27557  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  mudivsum  27574  mulogsum  27576  logdivsum  27577  mulog2sumlem2  27579  log2sumbnd  27588  selberg2lem  27594  logdivbnd  27600  pntrsumo1  27609  pntrsumbnd2  27611  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem6a  27626  pntlemf  27649  eedimeq  28913  axlowdimlem6  28962  axlowdimlem16  28972  axlowdimlem17  28973  ipval2  30726  minvecolem3  30895  minvecolem4b  30897  minvecolem4  30899  h2hcau  30998  h2hlm  30999  hlimadd  31212  hlim0  31254  hhsscms  31297  occllem  31322  nlelchi  32080  opsqrlem4  32162  hmopidmchi  32170  iundisjf  32602  iundisj2f  32603  ssnnssfz  32789  iundisjfi  32798  iundisj2fi  32799  chnub  33002  cycpmco2lem7  33152  cycpmrn  33163  1smat1  33803  submat1n  33804  submatres  33805  submateqlem2  33807  lmatfval  33813  madjusmdetlem1  33826  madjusmdetlem2  33827  madjusmdetlem3  33828  madjusmdetlem4  33829  lmlim  33946  rge0scvg  33948  lmxrge0  33951  lmdvg  33952  esumfzf  34070  esumfsup  34071  esumpcvgval  34079  esumpmono  34080  esumcvg  34087  esumcvgsum  34089  esumsup  34090  fiunelros  34175  eulerpartlemsv2  34360  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemv  34366  eulerpartlemb  34370  fiblem  34400  fibp1  34403  rrvsum  34456  dstfrvclim1  34480  ballotlem1ri  34537  signsvfn  34597  chtvalz  34644  circlemethhgt  34658  subfacp1lem1  35184  subfacp1lem5  35189  subfacp1lem6  35190  erdszelem7  35202  cvmliftlem5  35294  cvmliftlem7  35296  cvmliftlem10  35299  cvmliftlem13  35301  sinccvg  35678  circum  35679  divcnvlin  35733  iprodgam  35742  faclimlem1  35743  faclimlem2  35744  faclim  35746  iprodfac  35747  faclim2  35748  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem27  37654  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  lmclim2  37765  geomcau  37766  heibor1lem  37816  heibor1  37817  bfplem1  37829  bfplem2  37830  rrncmslem  37839  rrncms  37840  aks4d1p1p1  42064  sticksstones10  42156  sticksstones12a  42158  metakunt20  42225  fz1sump1  42344  sumcubes  42347  nna4b4nsq  42670  eldioph3b  42776  diophin  42783  diophun  42784  diophren  42824  jm3.1lem2  43030  dgraalem  43157  dgraaub  43160  dftrcl3  43733  trclfvdecomr  43741  hashnzfz2  44340  hashnzfzclim  44341  dvradcnv2  44366  binomcxplemnotnn0  44375  nnsplit  45369  rexanuz2nf  45503  clim1fr1  45616  sumnnodd  45645  limsup10exlem  45787  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  stoweidlem7  46022  stoweidlem14  46029  stoweidlem20  46035  stoweidlem34  46049  wallispilem5  46084  wallispi  46085  stirlinglem1  46089  stirlinglem5  46093  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  fourierdlem11  46133  fourierdlem31  46153  fourierdlem48  46169  fourierdlem49  46170  fourierdlem69  46190  fourierdlem73  46194  fourierdlem81  46202  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fouriersw  46246  sge0ad2en  46446  voliunsge0lem  46487  caragenunicl  46539  caratheodorylem2  46542  hoidmvlelem3  46612  ovolval2lem  46658  ovolval2  46659  vonioolem2  46696  vonicclem2  46699  fmtno4prmfac  47559