Theorem nnuz 12825

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  {crab 3392   class class class wbr 5079  ‘cfv 6492  1c1 11037   ≤ cle 11178  ℕcn 12172  ℤcz 12522  ℤ_≥cuz 12786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-z 12523  df-uz 12787

This theorem is referenced by:  elnnuz  12826  eluz2nn  12836  uznnssnn  12843  nnwo  12861  eluznn  12866  nninf  12877  fzssnn  13520  fseq1p1m1  13550  prednn  13603  elfzo1  13665  ltwenn  13922  nnnfi  13926  ser1const  14018  expp1  14028  digit1  14197  facnn  14235  fac0  14236  facp1  14238  faclbnd4lem1  14253  bcm1k  14275  bcval5  14278  bcpasc  14281  fz1isolem  14421  seqcoll  14424  seqcoll2  14425  climuni  15512  isercolllem2  15626  isercoll  15628  sumeq2ii  15653  summolem3  15674  summolem2a  15675  fsum  15680  sum0  15681  sumz  15682  fsumcl2lem  15691  fsumadd  15700  fsummulc2  15744  fsumrelem  15768  isumnn0nn  15805  climcndslem1  15812  climcndslem2  15813  climcnds  15814  divcnv  15816  divcnvshft  15818  supcvg  15819  trireciplem  15825  trirecip  15826  expcnv  15827  geo2lim  15838  geoisum1  15842  geoisum1c  15843  mertenslem2  15848  prodeq2ii  15874  prodmolem3  15896  prodmolem2a  15897  fprod  15904  prod0  15906  prod1  15907  fprodss  15911  fprodser  15912  fprodcl2lem  15913  fprodmul  15923  fproddiv  15924  fprodn0  15942  fallfacval4  16006  bpoly4  16022  ege2le3  16053  rpnnen2lem3  16181  rpnnen2lem5  16183  rpnnen2lem8  16186  rpnnen2lem12  16190  ruclem6  16200  pwp1fsum  16358  bezoutlem2  16507  bezoutlem3  16508  lcmcllem  16563  lcmledvds  16566  lcmfval  16588  lcmfcllem  16592  lcmfledvds  16599  isprm3  16650  phicl2  16736  phibndlem  16738  eulerthlem2  16750  odzcllem  16761  odzdvds  16764  iserodd  16804  pcmptcl  16860  pcmpt  16861  pockthlem  16874  pockthg  16875  unbenlem  16877  prmreclem3  16887  prmreclem5  16889  prmreclem6  16890  prmrec  16891  1arith  16896  4sqlem13  16926  4sqlem14  16927  4sqlem17  16930  4sqlem18  16931  vdwlem1  16950  vdwlem2  16951  vdwlem3  16952  vdwlem6  16955  vdwlem8  16957  vdwlem10  16959  vdw  16963  vdwnnlem3  16966  prmlem1a  17075  chnub  18586  mulgnnp1  19056  mulgnnsubcl  19060  mulgnn0z  19075  mulgnndir  19077  mulgpropd  19090  odfval  19505  odlem1  19508  odlem2  19512  gexlem1  19552  gexlem2  19555  gexcl3  19560  sylow1lem1  19571  efgsdmi  19705  efgsrel  19707  efgs1b  19709  efgsp1  19710  mulgnn0di  19798  lt6abl  19868  gsumval3eu  19877  gsumval3  19880  gsumzcl2  19883  gsumzaddlem  19894  gsumconst  19907  gsumzmhm  19910  gsumzoppg  19917  zringlpirlem2  21445  zringlpirlem3  21446  lmcnp  23294  lmmo  23370  1stcelcls  23451  1stccnp  23452  1stckgenlem  23543  1stckgen  23544  imasdsf1olem  24363  cphipval  25235  lmnn  25255  cmetcaulem  25280  iscmet2  25286  causs  25290  nglmle  25294  caubl  25300  iscmet3i  25304  bcthlem5  25320  ovolsf  25464  ovollb2lem  25480  ovolctb  25482  ovolunlem1a  25488  ovolunlem1  25489  ovoliunlem1  25494  ovoliun  25497  ovoliun2  25498  ovoliunnul  25499  ovolscalem1  25505  ovolicc1  25508  ovolicc2lem2  25510  ovolicc2lem3  25511  ovolicc2lem4  25512  iundisj  25540  iundisj2  25541  voliunlem1  25542  voliunlem2  25543  voliunlem3  25544  volsup  25548  ioombl1lem4  25553  uniioovol  25571  uniioombllem2  25575  uniioombllem3  25577  uniioombllem4  25578  uniioombllem6  25580  vitalilem4  25603  vitalilem5  25604  itg1climres  25706  mbfi1fseqlem6  25712  mbfi1flimlem  25714  mbfmullem2  25716  itg2monolem1  25742  itg2i1fseqle  25746  itg2i1fseq  25747  itg2i1fseq2  25748  itg2addlem  25750  plyeq0lem  26200  vieta1lem2  26302  elqaalem1  26310  elqaalem3  26312  aaliou3lem4  26337  aaliou3lem7  26340  dvtaylp  26360  taylthlem2  26364  pserdvlem2  26418  pserdv2  26420  abelthlem6  26426  abelthlem9  26430  logtayl  26649  logtaylsum  26650  logtayl2  26651  atantayl  26926  leibpilem2  26930  leibpi  26931  birthdaylem2  26941  dfef2  26959  divsqrtsumlem  26968  emcllem2  26985  emcllem4  26987  emcllem5  26988  emcllem6  26989  emcllem7  26990  harmonicbnd4  26999  fsumharmonic  27000  zetacvg  27003  lgamgulmlem4  27020  lgamgulmlem6  27022  lgamgulm2  27024  lgamcvglem  27028  lgamcvg2  27043  gamcvg  27044  gamcvg2lem  27047  regamcl  27049  relgamcl  27050  lgam1  27052  wilthlem3  27058  ftalem2  27062  ftalem4  27064  ftalem5  27065  basellem5  27073  basellem6  27074  basellem7  27075  basellem8  27076  basellem9  27077  ppiprm  27139  ppinprm  27140  chtprm  27141  chtnprm  27142  chpp1  27143  vma1  27154  ppiltx  27165  fsumvma2  27202  chpchtsum  27207  logfacbnd3  27211  logexprlim  27213  bposlem5  27276  lgscllem  27292  lgsval2lem  27295  lgsval4a  27307  lgsneg  27309  lgsdir  27320  lgsdilem2  27321  lgsdi  27322  lgsne0  27323  gausslemma2dlem3  27356  lgsquadlem2  27369  chebbnd1lem1  27457  chtppilimlem1  27461  rplogsumlem1  27472  rplogsumlem2  27473  rpvmasumlem  27475  dchrisumlema  27476  dchrisumlem2  27478  dchrisumlem3  27479  dchrmusum2  27482  dchrvmasum2lem  27484  dchrvmasumiflem1  27489  dchrvmaeq0  27492  dchrisum0flblem2  27497  dchrisum0flb  27498  dchrisum0re  27501  dchrisum0lem1b  27503  dchrisum0lem1  27504  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0lem3  27507  mudivsum  27518  mulogsum  27520  logdivsum  27521  mulog2sumlem2  27523  log2sumbnd  27532  selberg2lem  27538  logdivbnd  27544  pntrsumo1  27553  pntrsumbnd2  27555  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem6a  27570  pntlemf  27593  eedimeq  28992  axlowdimlem6  29041  axlowdimlem16  29051  axlowdimlem17  29052  ipval2  30803  minvecolem3  30972  minvecolem4b  30974  minvecolem4  30976  h2hcau  31075  h2hlm  31076  hlimadd  31289  hlim0  31331  hhsscms  31374  occllem  31399  nlelchi  32157  opsqrlem4  32239  hmopidmchi  32247  iundisjf  32685  iundisj2f  32686  ssnnssfz  32886  iundisjfi  32895  iundisj2fi  32896  cycpmco2lem7  33220  cycpmrn  33231  1smat1  33995  submat1n  33996  submatres  33997  submateqlem2  33999  lmatfval  34005  madjusmdetlem1  34018  madjusmdetlem2  34019  madjusmdetlem3  34020  madjusmdetlem4  34021  lmlim  34138  rge0scvg  34140  lmxrge0  34143  lmdvg  34144  esumfzf  34260  esumfsup  34261  esumpcvgval  34269  esumpmono  34270  esumcvg  34277  esumcvgsum  34279  esumsup  34280  fiunelros  34365  eulerpartlemsv2  34549  eulerpartlems  34551  eulerpartlemsv3  34552  eulerpartlemv  34555  eulerpartlemb  34559  fiblem  34589  fibp1  34592  rrvsum  34645  dstfrvclim1  34669  ballotlem1ri  34726  signsvfn  34773  chtvalz  34820  circlemethhgt  34834  subfacp1lem1  35414  subfacp1lem5  35419  subfacp1lem6  35420  erdszelem7  35432  cvmliftlem5  35524  cvmliftlem7  35526  cvmliftlem10  35529  cvmliftlem13  35531  sinccvg  35908  circum  35909  divcnvlin  35968  iprodgam  35977  faclimlem1  35978  faclimlem2  35979  faclim  35981  iprodfac  35982  faclim2  35983  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem12  38006  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem27  38021  poimirlem28  38022  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  mblfinlem2  38032  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  lmclim2  38132  geomcau  38133  heibor1lem  38183  heibor1  38184  bfplem1  38196  bfplem2  38197  rrncmslem  38206  rrncms  38207  aks4d1p1p1  42555  sticksstones10  42647  sticksstones12a  42649  fz1sump1  42794  sumcubes  42797  nna4b4nsq  43117  eldioph3b  43221  diophin  43228  diophun  43229  diophren  43265  jm3.1lem2  43470  dgraalem  43597  dgraaub  43600  dftrcl3  44171  trclfvdecomr  44179  hashnzfz2  44772  hashnzfzclim  44773  dvradcnv2  44798  binomcxplemnotnn0  44807  nnsplit  45810  rexanuz2nf  45942  clim1fr1  46053  sumnnodd  46082  limsup10exlem  46222  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  stoweidlem7  46457  stoweidlem14  46464  stoweidlem20  46470  stoweidlem34  46484  wallispilem5  46519  wallispi  46520  stirlinglem1  46524  stirlinglem5  46528  stirlinglem7  46530  stirlinglem8  46531  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  stirlinglem13  46536  stirlinglem14  46537  stirlinglem15  46538  stirlingr  46540  dirkertrigeqlem2  46549  dirkertrigeqlem3  46550  fourierdlem11  46568  fourierdlem31  46588  fourierdlem48  46604  fourierdlem49  46605  fourierdlem69  46625  fourierdlem73  46629  fourierdlem81  46637  fourierdlem93  46649  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fouriersw  46681  sge0ad2en  46881  voliunsge0lem  46922  caragenunicl  46974  caratheodorylem2  46977  hoidmvlelem3  47047  ovolval2lem  47093  ovolval2  47094  vonioolem2  47131  vonicclem2  47134  nthrucw  47338  fmtno4prmfac  48057