Theorem nnuz 12630

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  {crab 3069   class class class wbr 5075  ‘cfv 6437  1c1 10881   ≤ cle 11019  ℕcn 11982  ℤcz 12328  ℤ_≥cuz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-z 12329  df-uz 12592

This theorem is referenced by:  elnnuz  12631  eluz2nn  12633  uznnssnn  12644  nnwo  12662  eluznn  12667  nninf  12678  fzssnn  13309  fseq1p1m1  13339  prednn  13388  elfzo1  13446  ltwenn  13691  nnnfi  13695  ser1const  13788  expp1  13798  digit1  13961  facnn  13998  fac0  13999  facp1  14001  faclbnd4lem1  14016  bcm1k  14038  bcval5  14041  bcpasc  14044  fz1isolem  14184  seqcoll  14187  seqcoll2  14188  climuni  15270  isercolllem2  15386  isercoll  15388  sumeq2ii  15414  summolem3  15435  summolem2a  15436  fsum  15441  sum0  15442  sumz  15443  fsumcl2lem  15452  fsumadd  15461  fsummulc2  15505  fsumrelem  15528  isumnn0nn  15563  climcndslem1  15570  climcndslem2  15571  climcnds  15572  divcnv  15574  divcnvshft  15576  supcvg  15577  trireciplem  15583  trirecip  15584  expcnv  15585  geo2lim  15596  geoisum1  15600  geoisum1c  15601  mertenslem2  15606  prodeq2ii  15632  prodmolem3  15652  prodmolem2a  15653  fprod  15660  prod0  15662  prod1  15663  fprodss  15667  fprodser  15668  fprodcl2lem  15669  fprodmul  15679  fproddiv  15680  fprodn0  15698  fallfacval4  15762  bpoly4  15778  ege2le3  15808  rpnnen2lem3  15934  rpnnen2lem5  15936  rpnnen2lem8  15939  rpnnen2lem12  15943  ruclem6  15953  pwp1fsum  16109  bezoutlem2  16257  bezoutlem3  16258  lcmcllem  16310  lcmledvds  16313  lcmfval  16335  lcmfcllem  16339  lcmfledvds  16346  isprm3  16397  phicl2  16478  phibndlem  16480  eulerthlem2  16492  odzcllem  16502  odzdvds  16505  iserodd  16545  pcmptcl  16601  pcmpt  16602  pockthlem  16615  pockthg  16616  unbenlem  16618  prmreclem3  16628  prmreclem5  16630  prmreclem6  16631  prmrec  16632  1arith  16637  4sqlem13  16667  4sqlem14  16668  4sqlem17  16671  4sqlem18  16672  vdwlem1  16691  vdwlem2  16692  vdwlem3  16693  vdwlem6  16696  vdwlem8  16698  vdwlem10  16700  vdw  16704  vdwnnlem3  16707  prmlem1a  16817  mulgnnp1  18721  mulgnnsubcl  18725  mulgnn0z  18739  mulgnndir  18741  mulgpropd  18754  odfval  19149  odlem1  19152  odlem2  19156  gexlem1  19193  gexlem2  19196  gexcl3  19201  sylow1lem1  19212  efgsdmi  19347  efgsrel  19349  efgs1b  19351  efgsp1  19352  mulgnn0di  19436  lt6abl  19505  gsumval3eu  19514  gsumval3  19517  gsumzcl2  19520  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  zringlpirlem2  20694  zringlpirlem3  20695  lmcnp  22464  lmmo  22540  1stcelcls  22621  1stccnp  22622  1stckgenlem  22713  1stckgen  22714  imasdsf1olem  23535  cphipval  24416  lmnn  24436  cmetcaulem  24461  iscmet2  24467  causs  24471  nglmle  24475  caubl  24481  iscmet3i  24485  bcthlem5  24501  ovolsf  24645  ovollb2lem  24661  ovolctb  24663  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliun  24678  ovoliun2  24679  ovoliunnul  24680  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem2  24691  ovolicc2lem3  24692  ovolicc2lem4  24693  iundisj  24721  iundisj2  24722  voliunlem1  24723  voliunlem2  24724  voliunlem3  24725  volsup  24729  ioombl1lem4  24734  uniioovol  24752  uniioombllem2  24756  uniioombllem3  24758  uniioombllem4  24759  uniioombllem6  24761  vitalilem4  24784  vitalilem5  24785  itg1climres  24888  mbfi1fseqlem6  24894  mbfi1flimlem  24896  mbfmullem2  24898  itg2monolem1  24924  itg2i1fseqle  24928  itg2i1fseq  24929  itg2i1fseq2  24930  itg2addlem  24932  plyeq0lem  25380  vieta1lem2  25480  elqaalem1  25488  elqaalem3  25490  aaliou3lem4  25515  aaliou3lem7  25518  dvtaylp  25538  taylthlem2  25542  pserdvlem2  25596  pserdv2  25598  abelthlem6  25604  abelthlem9  25608  logtayl  25824  logtaylsum  25825  logtayl2  25826  atantayl  26096  leibpilem2  26100  leibpi  26101  birthdaylem2  26111  dfef2  26129  divsqrtsumlem  26138  emcllem2  26155  emcllem4  26157  emcllem5  26158  emcllem6  26159  emcllem7  26160  harmonicbnd4  26169  fsumharmonic  26170  zetacvg  26173  lgamgulmlem4  26190  lgamgulmlem6  26192  lgamgulm2  26194  lgamcvglem  26198  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  regamcl  26219  relgamcl  26220  lgam1  26222  wilthlem3  26228  ftalem2  26232  ftalem4  26234  ftalem5  26235  basellem5  26243  basellem6  26244  basellem7  26245  basellem8  26246  basellem9  26247  ppiprm  26309  ppinprm  26310  chtprm  26311  chtnprm  26312  chpp1  26313  vma1  26324  ppiltx  26335  fsumvma2  26371  chpchtsum  26376  logfacbnd3  26380  logexprlim  26382  bposlem5  26445  lgscllem  26461  lgsval2lem  26464  lgsval4a  26476  lgsneg  26478  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  gausslemma2dlem3  26525  lgsquadlem2  26538  chebbnd1lem1  26626  chtppilimlem1  26630  rplogsumlem1  26641  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasum2lem  26653  dchrvmasumiflem1  26658  dchrvmaeq0  26661  dchrisum0flblem2  26666  dchrisum0flb  26667  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  mudivsum  26687  mulogsum  26689  logdivsum  26690  mulog2sumlem2  26692  log2sumbnd  26701  selberg2lem  26707  logdivbnd  26713  pntrsumo1  26722  pntrsumbnd2  26724  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  pntrlog2bndlem6a  26739  pntlemf  26762  eedimeq  27275  axlowdimlem6  27324  axlowdimlem16  27334  axlowdimlem17  27335  ipval2  29078  minvecolem3  29247  minvecolem4b  29249  minvecolem4  29251  h2hcau  29350  h2hlm  29351  hlimadd  29564  hlim0  29606  hhsscms  29649  occllem  29674  nlelchi  30432  opsqrlem4  30514  hmopidmchi  30522  iundisjf  30937  iundisj2f  30938  ssnnssfz  31117  iundisjfi  31126  iundisj2fi  31127  cycpmco2lem7  31408  cycpmrn  31419  1smat1  31763  submat1n  31764  submatres  31765  submateqlem2  31767  lmatfval  31773  madjusmdetlem1  31786  madjusmdetlem2  31787  madjusmdetlem3  31788  madjusmdetlem4  31789  lmlim  31906  rge0scvg  31908  lmxrge0  31911  lmdvg  31912  esumfzf  32046  esumfsup  32047  esumpcvgval  32055  esumpmono  32056  esumcvg  32063  esumcvgsum  32065  esumsup  32066  fiunelros  32151  eulerpartlemsv2  32334  eulerpartlems  32336  eulerpartlemsv3  32337  eulerpartlemv  32340  eulerpartlemb  32344  fiblem  32374  fibp1  32377  rrvsum  32430  dstfrvclim1  32453  ballotlem1ri  32510  signsvfn  32570  chtvalz  32618  circlemethhgt  32632  subfacp1lem1  33150  subfacp1lem5  33155  subfacp1lem6  33156  erdszelem7  33168  cvmliftlem5  33260  cvmliftlem7  33262  cvmliftlem10  33265  cvmliftlem13  33267  sinccvg  33640  circum  33641  divcnvlin  33707  iprodgam  33717  faclimlem1  33718  faclimlem2  33719  faclim  33721  iprodfac  33722  faclim2  33723  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem12  35798  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  mblfinlem2  35824  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  lmclim2  35925  geomcau  35926  heibor1lem  35976  heibor1  35977  bfplem1  35989  bfplem2  35990  rrncmslem  35999  rrncms  36000  aks4d1p1p1  40078  sticksstones10  40118  sticksstones12a  40120  metakunt20  40151  nna4b4nsq  40504  eldioph3b  40594  diophin  40601  diophun  40602  diophren  40642  jm3.1lem2  40847  dgraalem  40977  dgraaub  40980  dftrcl3  41335  trclfvdecomr  41343  hashnzfz2  41946  hashnzfzclim  41947  dvradcnv2  41972  binomcxplemnotnn0  41981  nnsplit  42904  clim1fr1  43149  sumnnodd  43178  limsup10exlem  43320  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  stoweidlem7  43555  stoweidlem14  43562  stoweidlem20  43568  stoweidlem34  43582  wallispilem5  43617  wallispi  43618  stirlinglem1  43622  stirlinglem5  43626  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  stirlingr  43638  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  fourierdlem11  43666  fourierdlem31  43686  fourierdlem48  43702  fourierdlem49  43703  fourierdlem69  43723  fourierdlem73  43727  fourierdlem81  43735  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fouriersw  43779  sge0ad2en  43976  voliunsge0lem  44017  caragenunicl  44069  caratheodorylem2  44072  hoidmvlelem3  44142  ovolval2lem  44188  ovolval2  44189  vonioolem2  44226  vonicclem2  44229  fmtno4prmfac  45035