Theorem nnuz 12836

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3405   class class class wbr 5107  ‘cfv 6511  1c1 11069   ≤ cle 11209  ℕcn 12186  ℤcz 12529  ℤ_≥cuz 12793

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-z 12530  df-uz 12794

This theorem is referenced by:  elnnuz  12837  eluz2nn  12847  uznnssnn  12854  nnwo  12872  eluznn  12877  nninf  12888  fzssnn  13529  fseq1p1m1  13559  prednn  13612  elfzo1  13673  ltwenn  13927  nnnfi  13931  ser1const  14023  expp1  14033  digit1  14202  facnn  14240  fac0  14241  facp1  14243  faclbnd4lem1  14258  bcm1k  14280  bcval5  14283  bcpasc  14286  fz1isolem  14426  seqcoll  14429  seqcoll2  14430  climuni  15518  isercolllem2  15632  isercoll  15634  sumeq2ii  15659  summolem3  15680  summolem2a  15681  fsum  15686  sum0  15687  sumz  15688  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumrelem  15773  isumnn0nn  15808  climcndslem1  15815  climcndslem2  15816  climcnds  15817  divcnv  15819  divcnvshft  15821  supcvg  15822  trireciplem  15828  trirecip  15829  expcnv  15830  geo2lim  15841  geoisum1  15845  geoisum1c  15846  mertenslem2  15851  prodeq2ii  15877  prodmolem3  15899  prodmolem2a  15900  fprod  15907  prod0  15909  prod1  15910  fprodss  15914  fprodser  15915  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodn0  15945  fallfacval4  16009  bpoly4  16025  ege2le3  16056  rpnnen2lem3  16184  rpnnen2lem5  16186  rpnnen2lem8  16189  rpnnen2lem12  16193  ruclem6  16203  pwp1fsum  16361  bezoutlem2  16510  bezoutlem3  16511  lcmcllem  16566  lcmledvds  16569  lcmfval  16591  lcmfcllem  16595  lcmfledvds  16602  isprm3  16653  phicl2  16738  phibndlem  16740  eulerthlem2  16752  odzcllem  16763  odzdvds  16766  iserodd  16806  pcmptcl  16862  pcmpt  16863  pockthlem  16876  pockthg  16877  unbenlem  16879  prmreclem3  16889  prmreclem5  16891  prmreclem6  16892  prmrec  16893  1arith  16898  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  vdw  16965  vdwnnlem3  16968  prmlem1a  17077  mulgnnp1  19014  mulgnnsubcl  19018  mulgnn0z  19033  mulgnndir  19035  mulgpropd  19048  odfval  19462  odlem1  19465  odlem2  19469  gexlem1  19509  gexlem2  19512  gexcl3  19517  sylow1lem1  19528  efgsdmi  19662  efgsrel  19664  efgs1b  19666  efgsp1  19667  mulgnn0di  19755  lt6abl  19825  gsumval3eu  19834  gsumval3  19837  gsumzcl2  19840  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  zringlpirlem2  21373  zringlpirlem3  21374  lmcnp  23191  lmmo  23267  1stcelcls  23348  1stccnp  23349  1stckgenlem  23440  1stckgen  23441  imasdsf1olem  24261  cphipval  25143  lmnn  25163  cmetcaulem  25188  iscmet2  25194  causs  25198  nglmle  25202  caubl  25208  iscmet3i  25212  bcthlem5  25228  ovolsf  25373  ovollb2lem  25389  ovolctb  25391  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun  25406  ovoliun2  25407  ovoliunnul  25408  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem2  25419  ovolicc2lem3  25420  ovolicc2lem4  25421  iundisj  25449  iundisj2  25450  voliunlem1  25451  voliunlem2  25452  voliunlem3  25453  volsup  25457  ioombl1lem4  25462  uniioovol  25480  uniioombllem2  25484  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  vitalilem4  25512  vitalilem5  25513  itg1climres  25615  mbfi1fseqlem6  25621  mbfi1flimlem  25623  mbfmullem2  25625  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  plyeq0lem  26115  vieta1lem2  26219  elqaalem1  26227  elqaalem3  26229  aaliou3lem4  26254  aaliou3lem7  26257  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  pserdv2  26340  abelthlem6  26346  abelthlem9  26350  logtayl  26569  logtaylsum  26570  logtayl2  26571  atantayl  26847  leibpilem2  26851  leibpi  26852  birthdaylem2  26862  dfef2  26881  divsqrtsumlem  26890  emcllem2  26907  emcllem4  26909  emcllem5  26910  emcllem6  26911  emcllem7  26912  harmonicbnd4  26921  fsumharmonic  26922  zetacvg  26925  lgamgulmlem4  26942  lgamgulmlem6  26944  lgamgulm2  26946  lgamcvglem  26950  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  regamcl  26971  relgamcl  26972  lgam1  26974  wilthlem3  26980  ftalem2  26984  ftalem4  26986  ftalem5  26987  basellem5  26995  basellem6  26996  basellem7  26997  basellem8  26998  basellem9  26999  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  chpp1  27065  vma1  27076  ppiltx  27087  fsumvma2  27125  chpchtsum  27130  logfacbnd3  27134  logexprlim  27136  bposlem5  27199  lgscllem  27215  lgsval2lem  27218  lgsval4a  27230  lgsneg  27232  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  gausslemma2dlem3  27279  lgsquadlem2  27292  chebbnd1lem1  27380  chtppilimlem1  27384  rplogsumlem1  27395  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasum2lem  27407  dchrvmasumiflem1  27412  dchrvmaeq0  27415  dchrisum0flblem2  27420  dchrisum0flb  27421  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  mudivsum  27441  mulogsum  27443  logdivsum  27444  mulog2sumlem2  27446  log2sumbnd  27455  selberg2lem  27461  logdivbnd  27467  pntrsumo1  27476  pntrsumbnd2  27478  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem6a  27493  pntlemf  27516  eedimeq  28825  axlowdimlem6  28874  axlowdimlem16  28884  axlowdimlem17  28885  ipval2  30636  minvecolem3  30805  minvecolem4b  30807  minvecolem4  30809  h2hcau  30908  h2hlm  30909  hlimadd  31122  hlim0  31164  hhsscms  31207  occllem  31232  nlelchi  31990  opsqrlem4  32072  hmopidmchi  32080  iundisjf  32518  iundisj2f  32519  ssnnssfz  32710  iundisjfi  32719  iundisj2fi  32720  chnub  32938  cycpmco2lem7  33089  cycpmrn  33100  1smat1  33794  submat1n  33795  submatres  33796  submateqlem2  33798  lmatfval  33804  madjusmdetlem1  33817  madjusmdetlem2  33818  madjusmdetlem3  33819  madjusmdetlem4  33820  lmlim  33937  rge0scvg  33939  lmxrge0  33942  lmdvg  33943  esumfzf  34059  esumfsup  34060  esumpcvgval  34068  esumpmono  34069  esumcvg  34076  esumcvgsum  34078  esumsup  34079  fiunelros  34164  eulerpartlemsv2  34349  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemv  34355  eulerpartlemb  34359  fiblem  34389  fibp1  34392  rrvsum  34445  dstfrvclim1  34469  ballotlem1ri  34526  signsvfn  34573  chtvalz  34620  circlemethhgt  34634  subfacp1lem1  35166  subfacp1lem5  35171  subfacp1lem6  35172  erdszelem7  35184  cvmliftlem5  35276  cvmliftlem7  35278  cvmliftlem10  35281  cvmliftlem13  35283  sinccvg  35660  circum  35661  divcnvlin  35720  iprodgam  35729  faclimlem1  35730  faclimlem2  35731  faclim  35733  iprodfac  35734  faclim2  35735  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem27  37641  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  lmclim2  37752  geomcau  37753  heibor1lem  37803  heibor1  37804  bfplem1  37816  bfplem2  37817  rrncmslem  37826  rrncms  37827  aks4d1p1p1  42051  sticksstones10  42143  sticksstones12a  42145  fz1sump1  42298  sumcubes  42301  nna4b4nsq  42648  eldioph3b  42753  diophin  42760  diophun  42761  diophren  42801  jm3.1lem2  43007  dgraalem  43134  dgraaub  43137  dftrcl3  43709  trclfvdecomr  43717  hashnzfz2  44310  hashnzfzclim  44311  dvradcnv2  44336  binomcxplemnotnn0  44345  nnsplit  45354  rexanuz2nf  45488  clim1fr1  45599  sumnnodd  45628  limsup10exlem  45770  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  stoweidlem7  46005  stoweidlem14  46012  stoweidlem20  46018  stoweidlem34  46032  wallispilem5  46067  wallispi  46068  stirlinglem1  46072  stirlinglem5  46076  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  stirlingr  46088  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  fourierdlem11  46116  fourierdlem31  46136  fourierdlem48  46152  fourierdlem49  46153  fourierdlem69  46173  fourierdlem73  46177  fourierdlem81  46185  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fouriersw  46229  sge0ad2en  46429  voliunsge0lem  46470  caragenunicl  46522  caratheodorylem2  46525  hoidmvlelem3  46595  ovolval2lem  46641  ovolval2  46642  vonioolem2  46679  vonicclem2  46682  fmtno4prmfac  47573