Theorem nnuz 12550

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  {crab 3067   class class class wbr 5070  ‘cfv 6418  1c1 10803   ≤ cle 10941  ℕcn 11903  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-z 12250  df-uz 12512

This theorem is referenced by:  elnnuz  12551  eluz2nn  12553  uznnssnn  12564  nnwo  12582  eluznn  12587  nninf  12598  fzssnn  13229  fseq1p1m1  13259  prednn  13308  elfzo1  13365  ltwenn  13610  nnnfi  13614  ser1const  13707  expp1  13717  digit1  13880  facnn  13917  fac0  13918  facp1  13920  faclbnd4lem1  13935  bcm1k  13957  bcval5  13960  bcpasc  13963  fz1isolem  14103  seqcoll  14106  seqcoll2  14107  climuni  15189  isercolllem2  15305  isercoll  15307  sumeq2ii  15333  summolem3  15354  summolem2a  15355  fsum  15360  sum0  15361  sumz  15362  fsumcl2lem  15371  fsumadd  15380  fsummulc2  15424  fsumrelem  15447  isumnn0nn  15482  climcndslem1  15489  climcndslem2  15490  climcnds  15491  divcnv  15493  divcnvshft  15495  supcvg  15496  trireciplem  15502  trirecip  15503  expcnv  15504  geo2lim  15515  geoisum1  15519  geoisum1c  15520  mertenslem2  15525  prodeq2ii  15551  prodmolem3  15571  prodmolem2a  15572  fprod  15579  prod0  15581  prod1  15582  fprodss  15586  fprodser  15587  fprodcl2lem  15588  fprodmul  15598  fproddiv  15599  fprodn0  15617  fallfacval4  15681  bpoly4  15697  ege2le3  15727  rpnnen2lem3  15853  rpnnen2lem5  15855  rpnnen2lem8  15858  rpnnen2lem12  15862  ruclem6  15872  pwp1fsum  16028  bezoutlem2  16176  bezoutlem3  16177  lcmcllem  16229  lcmledvds  16232  lcmfval  16254  lcmfcllem  16258  lcmfledvds  16265  isprm3  16316  phicl2  16397  phibndlem  16399  eulerthlem2  16411  odzcllem  16421  odzdvds  16424  iserodd  16464  pcmptcl  16520  pcmpt  16521  pockthlem  16534  pockthg  16535  unbenlem  16537  prmreclem3  16547  prmreclem5  16549  prmreclem6  16550  prmrec  16551  1arith  16556  4sqlem13  16586  4sqlem14  16587  4sqlem17  16590  4sqlem18  16591  vdwlem1  16610  vdwlem2  16611  vdwlem3  16612  vdwlem6  16615  vdwlem8  16617  vdwlem10  16619  vdw  16623  vdwnnlem3  16626  prmlem1a  16736  mulgnnp1  18627  mulgnnsubcl  18631  mulgnn0z  18645  mulgnndir  18647  mulgpropd  18660  odfval  19055  odlem1  19058  odlem2  19062  gexlem1  19099  gexlem2  19102  gexcl3  19107  sylow1lem1  19118  efgsdmi  19253  efgsrel  19255  efgs1b  19257  efgsp1  19258  mulgnn0di  19342  lt6abl  19411  gsumval3eu  19420  gsumval3  19423  gsumzcl2  19426  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  zringlpirlem2  20597  zringlpirlem3  20598  lmcnp  22363  lmmo  22439  1stcelcls  22520  1stccnp  22521  1stckgenlem  22612  1stckgen  22613  imasdsf1olem  23434  cphipval  24312  lmnn  24332  cmetcaulem  24357  iscmet2  24363  causs  24367  nglmle  24371  caubl  24377  iscmet3i  24381  bcthlem5  24397  ovolsf  24541  ovollb2lem  24557  ovolctb  24559  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliun  24574  ovoliun2  24575  ovoliunnul  24576  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem2  24587  ovolicc2lem3  24588  ovolicc2lem4  24589  iundisj  24617  iundisj2  24618  voliunlem1  24619  voliunlem2  24620  voliunlem3  24621  volsup  24625  ioombl1lem4  24630  uniioovol  24648  uniioombllem2  24652  uniioombllem3  24654  uniioombllem4  24655  uniioombllem6  24657  vitalilem4  24680  vitalilem5  24681  itg1climres  24784  mbfi1fseqlem6  24790  mbfi1flimlem  24792  mbfmullem2  24794  itg2monolem1  24820  itg2i1fseqle  24824  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  plyeq0lem  25276  vieta1lem2  25376  elqaalem1  25384  elqaalem3  25386  aaliou3lem4  25411  aaliou3lem7  25414  dvtaylp  25434  taylthlem2  25438  pserdvlem2  25492  pserdv2  25494  abelthlem6  25500  abelthlem9  25504  logtayl  25720  logtaylsum  25721  logtayl2  25722  atantayl  25992  leibpilem2  25996  leibpi  25997  birthdaylem2  26007  dfef2  26025  divsqrtsumlem  26034  emcllem2  26051  emcllem4  26053  emcllem5  26054  emcllem6  26055  emcllem7  26056  harmonicbnd4  26065  fsumharmonic  26066  zetacvg  26069  lgamgulmlem4  26086  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvglem  26094  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  regamcl  26115  relgamcl  26116  lgam1  26118  wilthlem3  26124  ftalem2  26128  ftalem4  26130  ftalem5  26131  basellem5  26139  basellem6  26140  basellem7  26141  basellem8  26142  basellem9  26143  ppiprm  26205  ppinprm  26206  chtprm  26207  chtnprm  26208  chpp1  26209  vma1  26220  ppiltx  26231  fsumvma2  26267  chpchtsum  26272  logfacbnd3  26276  logexprlim  26278  bposlem5  26341  lgscllem  26357  lgsval2lem  26360  lgsval4a  26372  lgsneg  26374  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  gausslemma2dlem3  26421  lgsquadlem2  26434  chebbnd1lem1  26522  chtppilimlem1  26526  rplogsumlem1  26537  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasum2lem  26549  dchrvmasumiflem1  26554  dchrvmaeq0  26557  dchrisum0flblem2  26562  dchrisum0flb  26563  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  mudivsum  26583  mulogsum  26585  logdivsum  26586  mulog2sumlem2  26588  log2sumbnd  26597  selberg2lem  26603  logdivbnd  26609  pntrsumo1  26618  pntrsumbnd2  26620  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntrlog2bndlem6a  26635  pntlemf  26658  eedimeq  27169  axlowdimlem6  27218  axlowdimlem16  27228  axlowdimlem17  27229  ipval2  28970  minvecolem3  29139  minvecolem4b  29141  minvecolem4  29143  h2hcau  29242  h2hlm  29243  hlimadd  29456  hlim0  29498  hhsscms  29541  occllem  29566  nlelchi  30324  opsqrlem4  30406  hmopidmchi  30414  iundisjf  30829  iundisj2f  30830  ssnnssfz  31010  iundisjfi  31019  iundisj2fi  31020  cycpmco2lem7  31301  cycpmrn  31312  1smat1  31656  submat1n  31657  submatres  31658  submateqlem2  31660  lmatfval  31666  madjusmdetlem1  31679  madjusmdetlem2  31680  madjusmdetlem3  31681  madjusmdetlem4  31682  lmlim  31799  rge0scvg  31801  lmxrge0  31804  lmdvg  31805  esumfzf  31937  esumfsup  31938  esumpcvgval  31946  esumpmono  31947  esumcvg  31954  esumcvgsum  31956  esumsup  31957  fiunelros  32042  eulerpartlemsv2  32225  eulerpartlems  32227  eulerpartlemsv3  32228  eulerpartlemv  32231  eulerpartlemb  32235  fiblem  32265  fibp1  32268  rrvsum  32321  dstfrvclim1  32344  ballotlem1ri  32401  signsvfn  32461  chtvalz  32509  circlemethhgt  32523  subfacp1lem1  33041  subfacp1lem5  33046  subfacp1lem6  33047  erdszelem7  33059  cvmliftlem5  33151  cvmliftlem7  33153  cvmliftlem10  33156  cvmliftlem13  33158  sinccvg  33531  circum  33532  divcnvlin  33604  iprodgam  33614  faclimlem1  33615  faclimlem2  33616  faclim  33618  iprodfac  33619  faclim2  33620  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  lmclim2  35843  geomcau  35844  heibor1lem  35894  heibor1  35895  bfplem1  35907  bfplem2  35908  rrncmslem  35917  rrncms  35918  aks4d1p1p1  39999  sticksstones10  40039  sticksstones12a  40041  metakunt20  40072  nna4b4nsq  40413  eldioph3b  40503  diophin  40510  diophun  40511  diophren  40551  jm3.1lem2  40756  dgraalem  40886  dgraaub  40889  dftrcl3  41217  trclfvdecomr  41225  hashnzfz2  41828  hashnzfzclim  41829  dvradcnv2  41854  binomcxplemnotnn0  41863  nnsplit  42787  clim1fr1  43032  sumnnodd  43061  limsup10exlem  43203  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  stoweidlem7  43438  stoweidlem14  43445  stoweidlem20  43451  stoweidlem34  43465  wallispilem5  43500  wallispi  43501  stirlinglem1  43505  stirlinglem5  43509  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  fourierdlem11  43549  fourierdlem31  43569  fourierdlem48  43585  fourierdlem49  43586  fourierdlem69  43606  fourierdlem73  43610  fourierdlem81  43618  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fouriersw  43662  sge0ad2en  43859  voliunsge0lem  43900  caragenunicl  43952  caratheodorylem2  43955  hoidmvlelem3  44025  ovolval2lem  44071  ovolval2  44072  vonioolem2  44109  vonicclem2  44112  fmtno4prmfac  44912