Theorem nnuz 12802

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3401   class class class wbr 5100  ‘cfv 6500  1c1 11039   ≤ cle 11179  ℕcn 12157  ℤcz 12500  ℤ_≥cuz 12763

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-z 12501  df-uz 12764

This theorem is referenced by:  elnnuz  12803  eluz2nn  12813  uznnssnn  12820  nnwo  12838  eluznn  12843  nninf  12854  fzssnn  13496  fseq1p1m1  13526  prednn  13579  elfzo1  13640  ltwenn  13897  nnnfi  13901  ser1const  13993  expp1  14003  digit1  14172  facnn  14210  fac0  14211  facp1  14213  faclbnd4lem1  14228  bcm1k  14250  bcval5  14253  bcpasc  14256  fz1isolem  14396  seqcoll  14399  seqcoll2  14400  climuni  15487  isercolllem2  15601  isercoll  15603  sumeq2ii  15628  summolem3  15649  summolem2a  15650  fsum  15655  sum0  15656  sumz  15657  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumrelem  15742  isumnn0nn  15777  climcndslem1  15784  climcndslem2  15785  climcnds  15786  divcnv  15788  divcnvshft  15790  supcvg  15791  trireciplem  15797  trirecip  15798  expcnv  15799  geo2lim  15810  geoisum1  15814  geoisum1c  15815  mertenslem2  15820  prodeq2ii  15846  prodmolem3  15868  prodmolem2a  15869  fprod  15876  prod0  15878  prod1  15879  fprodss  15883  fprodser  15884  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodn0  15914  fallfacval4  15978  bpoly4  15994  ege2le3  16025  rpnnen2lem3  16153  rpnnen2lem5  16155  rpnnen2lem8  16158  rpnnen2lem12  16162  ruclem6  16172  pwp1fsum  16330  bezoutlem2  16479  bezoutlem3  16480  lcmcllem  16535  lcmledvds  16538  lcmfval  16560  lcmfcllem  16564  lcmfledvds  16571  isprm3  16622  phicl2  16707  phibndlem  16709  eulerthlem2  16721  odzcllem  16732  odzdvds  16735  iserodd  16775  pcmptcl  16831  pcmpt  16832  pockthlem  16845  pockthg  16846  unbenlem  16848  prmreclem3  16858  prmreclem5  16860  prmreclem6  16861  prmrec  16862  1arith  16867  4sqlem13  16897  4sqlem14  16898  4sqlem17  16901  4sqlem18  16902  vdwlem1  16921  vdwlem2  16922  vdwlem3  16923  vdwlem6  16926  vdwlem8  16928  vdwlem10  16930  vdw  16934  vdwnnlem3  16937  prmlem1a  17046  chnub  18557  mulgnnp1  19024  mulgnnsubcl  19028  mulgnn0z  19043  mulgnndir  19045  mulgpropd  19058  odfval  19473  odlem1  19476  odlem2  19480  gexlem1  19520  gexlem2  19523  gexcl3  19528  sylow1lem1  19539  efgsdmi  19673  efgsrel  19675  efgs1b  19677  efgsp1  19678  mulgnn0di  19766  lt6abl  19836  gsumval3eu  19845  gsumval3  19848  gsumzcl2  19851  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsumzoppg  19885  zringlpirlem2  21430  zringlpirlem3  21431  lmcnp  23260  lmmo  23336  1stcelcls  23417  1stccnp  23418  1stckgenlem  23509  1stckgen  23510  imasdsf1olem  24329  cphipval  25211  lmnn  25231  cmetcaulem  25256  iscmet2  25262  causs  25266  nglmle  25270  caubl  25276  iscmet3i  25280  bcthlem5  25296  ovolsf  25441  ovollb2lem  25457  ovolctb  25459  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun  25474  ovoliun2  25475  ovoliunnul  25476  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem2  25487  ovolicc2lem3  25488  ovolicc2lem4  25489  iundisj  25517  iundisj2  25518  voliunlem1  25519  voliunlem2  25520  voliunlem3  25521  volsup  25525  ioombl1lem4  25530  uniioovol  25548  uniioombllem2  25552  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  vitalilem4  25580  vitalilem5  25581  itg1climres  25683  mbfi1fseqlem6  25689  mbfi1flimlem  25691  mbfmullem2  25693  itg2monolem1  25719  itg2i1fseqle  25723  itg2i1fseq  25724  itg2i1fseq2  25725  itg2addlem  25727  plyeq0lem  26183  vieta1lem2  26287  elqaalem1  26295  elqaalem3  26297  aaliou3lem4  26322  aaliou3lem7  26325  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  pserdvlem2  26406  pserdv2  26408  abelthlem6  26414  abelthlem9  26418  logtayl  26637  logtaylsum  26638  logtayl2  26639  atantayl  26915  leibpilem2  26919  leibpi  26920  birthdaylem2  26930  dfef2  26949  divsqrtsumlem  26958  emcllem2  26975  emcllem4  26977  emcllem5  26978  emcllem6  26979  emcllem7  26980  harmonicbnd4  26989  fsumharmonic  26990  zetacvg  26993  lgamgulmlem4  27010  lgamgulmlem6  27012  lgamgulm2  27014  lgamcvglem  27018  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  regamcl  27039  relgamcl  27040  lgam1  27042  wilthlem3  27048  ftalem2  27052  ftalem4  27054  ftalem5  27055  basellem5  27063  basellem6  27064  basellem7  27065  basellem8  27066  basellem9  27067  ppiprm  27129  ppinprm  27130  chtprm  27131  chtnprm  27132  chpp1  27133  vma1  27144  ppiltx  27155  fsumvma2  27193  chpchtsum  27198  logfacbnd3  27202  logexprlim  27204  bposlem5  27267  lgscllem  27283  lgsval2lem  27286  lgsval4a  27298  lgsneg  27300  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  gausslemma2dlem3  27347  lgsquadlem2  27360  chebbnd1lem1  27448  chtppilimlem1  27452  rplogsumlem1  27463  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasum2lem  27475  dchrvmasumiflem1  27480  dchrvmaeq0  27483  dchrisum0flblem2  27488  dchrisum0flb  27489  dchrisum0re  27492  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  mudivsum  27509  mulogsum  27511  logdivsum  27512  mulog2sumlem2  27514  log2sumbnd  27523  selberg2lem  27529  logdivbnd  27535  pntrsumo1  27544  pntrsumbnd2  27546  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntrlog2bndlem6a  27561  pntlemf  27584  eedimeq  28983  axlowdimlem6  29032  axlowdimlem16  29042  axlowdimlem17  29043  ipval2  30794  minvecolem3  30963  minvecolem4b  30965  minvecolem4  30967  h2hcau  31066  h2hlm  31067  hlimadd  31280  hlim0  31322  hhsscms  31365  occllem  31390  nlelchi  32148  opsqrlem4  32230  hmopidmchi  32238  iundisjf  32675  iundisj2f  32676  ssnnssfz  32877  iundisjfi  32886  iundisj2fi  32887  cycpmco2lem7  33225  cycpmrn  33236  1smat1  33981  submat1n  33982  submatres  33983  submateqlem2  33985  lmatfval  33991  madjusmdetlem1  34004  madjusmdetlem2  34005  madjusmdetlem3  34006  madjusmdetlem4  34007  lmlim  34124  rge0scvg  34126  lmxrge0  34129  lmdvg  34130  esumfzf  34246  esumfsup  34247  esumpcvgval  34255  esumpmono  34256  esumcvg  34263  esumcvgsum  34265  esumsup  34266  fiunelros  34351  eulerpartlemsv2  34535  eulerpartlems  34537  eulerpartlemsv3  34538  eulerpartlemv  34541  eulerpartlemb  34545  fiblem  34575  fibp1  34578  rrvsum  34631  dstfrvclim1  34655  ballotlem1ri  34712  signsvfn  34759  chtvalz  34806  circlemethhgt  34820  subfacp1lem1  35392  subfacp1lem5  35397  subfacp1lem6  35398  erdszelem7  35410  cvmliftlem5  35502  cvmliftlem7  35504  cvmliftlem10  35507  cvmliftlem13  35509  sinccvg  35886  circum  35887  divcnvlin  35946  iprodgam  35955  faclimlem1  35956  faclimlem2  35957  faclim  35959  iprodfac  35960  faclim2  35961  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem12  37880  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem18  37886  poimirlem19  37887  poimirlem20  37888  poimirlem22  37890  poimirlem23  37891  poimirlem24  37892  poimirlem25  37893  poimirlem27  37895  poimirlem28  37896  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  mblfinlem2  37906  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  lmclim2  38006  geomcau  38007  heibor1lem  38057  heibor1  38058  bfplem1  38070  bfplem2  38071  rrncmslem  38080  rrncms  38081  aks4d1p1p1  42430  sticksstones10  42522  sticksstones12a  42524  fz1sump1  42677  sumcubes  42680  nna4b4nsq  43015  eldioph3b  43119  diophin  43126  diophun  43127  diophren  43167  jm3.1lem2  43372  dgraalem  43499  dgraaub  43502  dftrcl3  44073  trclfvdecomr  44081  hashnzfz2  44674  hashnzfzclim  44675  dvradcnv2  44700  binomcxplemnotnn0  44709  nnsplit  45714  rexanuz2nf  45847  clim1fr1  45958  sumnnodd  45987  limsup10exlem  46127  fprodsubrecnncnvlem  46262  fprodaddrecnncnvlem  46264  stoweidlem7  46362  stoweidlem14  46369  stoweidlem20  46375  stoweidlem34  46389  wallispilem5  46424  wallispi  46425  stirlinglem1  46429  stirlinglem5  46433  stirlinglem7  46435  stirlinglem8  46436  stirlinglem10  46438  stirlinglem11  46439  stirlinglem12  46440  stirlinglem13  46441  stirlinglem14  46442  stirlinglem15  46443  stirlingr  46445  dirkertrigeqlem2  46454  dirkertrigeqlem3  46455  fourierdlem11  46473  fourierdlem31  46493  fourierdlem48  46509  fourierdlem49  46510  fourierdlem69  46530  fourierdlem73  46534  fourierdlem81  46542  fourierdlem93  46554  fourierdlem103  46564  fourierdlem104  46565  fourierdlem112  46573  fouriersw  46586  sge0ad2en  46786  voliunsge0lem  46827  caragenunicl  46879  caratheodorylem2  46882  hoidmvlelem3  46952  ovolval2lem  46998  ovolval2  46999  vonioolem2  47036  vonicclem2  47039  nthrucw  47241  fmtno4prmfac  47929