Theorem nnuz 12088

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

Syntax hints:   = wceq 1507   ∈ wcel 2048  {crab 3086   class class class wbr 4923  ‘cfv 6182  1c1 10328   ≤ cle 10467  ℕcn 11431  ℤcz 11786  ℤ_≥cuz 12051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-er 8081  df-en 8299  df-dom 8300  df-sdom 8301  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-nn 11432  df-z 11787  df-uz 12052

This theorem is referenced by:  elnnuz  12089  eluz2nn  12091  uznnssnn  12102  nnwo  12120  eluznn  12125  nninf  12136  fzssnn  12760  fseq1p1m1  12790  prednn  12839  elfzo1  12895  ltwenn  13138  nnnfi  13142  ser1const  13234  expp1  13244  digit1  13406  facnn  13443  fac0  13444  facp1  13446  faclbnd4lem1  13461  bcm1k  13483  bcval5  13486  bcpasc  13489  fz1isolem  13622  seqcoll  13625  seqcoll2  13626  climuni  14760  isercolllem2  14873  isercoll  14875  sumeq2ii  14900  summolem3  14921  summolem2a  14922  fsum  14927  sum0  14928  sumz  14929  fsumcl2lem  14938  fsumadd  14946  fsummulc2  14989  fsumrelem  15012  isumnn0nn  15047  climcndslem1  15054  climcndslem2  15055  climcnds  15056  divcnv  15058  divcnvshft  15060  supcvg  15061  trireciplem  15067  trirecip  15068  expcnv  15069  geo2lim  15081  geoisum1  15085  geoisum1c  15086  mertenslem2  15091  prodeq2ii  15117  prodmolem3  15137  prodmolem2a  15138  fprod  15145  prod0  15147  prod1  15148  fprodss  15152  fprodser  15153  fprodcl2lem  15154  fprodmul  15164  fproddiv  15165  fprodn0  15183  fallfacval4  15247  bpoly4  15263  ege2le3  15293  rpnnen2lem3  15419  rpnnen2lem5  15421  rpnnen2lem8  15424  rpnnen2lem12  15428  ruclem6  15438  pwp1fsum  15592  bezoutlem2  15734  bezoutlem3  15735  lcmcllem  15786  lcmledvds  15789  lcmfval  15811  lcmfcllem  15815  lcmfledvds  15822  isprm3  15873  phicl2  15951  phibndlem  15953  eulerthlem2  15965  odzcllem  15975  odzdvds  15978  iserodd  16018  pcmptcl  16073  pcmpt  16074  pockthlem  16087  pockthg  16088  unbenlem  16090  prmreclem3  16100  prmreclem5  16102  prmreclem6  16103  prmrec  16104  1arith  16109  4sqlem13  16139  4sqlem14  16140  4sqlem17  16143  4sqlem18  16144  vdwlem1  16163  vdwlem2  16164  vdwlem3  16165  vdwlem6  16168  vdwlem8  16170  vdwlem10  16172  vdw  16176  vdwnnlem3  16179  prmlem1a  16286  mulgnnp1  18011  mulgnnsubcl  18015  mulgnn0z  18028  mulgnndir  18030  mulgpropd  18043  odfval  18412  odlem1  18415  odlem2  18419  gexlem1  18455  gexlem2  18458  gexcl3  18463  sylow1lem1  18474  efgsdmi  18606  efgsrel  18608  efgs1b  18610  efgsp1  18611  mulgnn0di  18694  lt6abl  18759  gsumval3eu  18768  gsumval3  18771  gsumzcl2  18774  gsumzaddlem  18784  gsumconst  18797  gsumzmhm  18800  gsumzoppg  18807  zringlpirlem2  20324  zringlpirlem3  20325  lmcnp  21606  lmmo  21682  1stcelcls  21763  1stccnp  21764  1stckgenlem  21855  1stckgen  21856  imasdsf1olem  22676  cphipval  23539  lmnn  23559  cmetcaulem  23584  iscmet2  23590  causs  23594  nglmle  23598  caubl  23604  iscmet3i  23608  bcthlem5  23624  ovolsf  23766  ovollb2lem  23782  ovolctb  23784  ovolunlem1a  23790  ovolunlem1  23791  ovoliunlem1  23796  ovoliun  23799  ovoliun2  23800  ovoliunnul  23801  ovolscalem1  23807  ovolicc1  23810  ovolicc2lem2  23812  ovolicc2lem3  23813  ovolicc2lem4  23814  iundisj  23842  iundisj2  23843  voliunlem1  23844  voliunlem2  23845  voliunlem3  23846  volsup  23850  ioombl1lem4  23855  uniioovol  23873  uniioombllem2  23877  uniioombllem3  23879  uniioombllem4  23880  uniioombllem6  23882  vitalilem4  23905  vitalilem5  23906  itg1climres  24008  mbfi1fseqlem6  24014  mbfi1flimlem  24016  mbfmullem2  24018  itg2monolem1  24044  itg2i1fseqle  24048  itg2i1fseq  24049  itg2i1fseq2  24050  itg2addlem  24052  plyeq0lem  24493  vieta1lem2  24593  elqaalem1  24601  elqaalem3  24603  aaliou3lem4  24628  aaliou3lem7  24631  dvtaylp  24651  taylthlem2  24655  pserdvlem2  24709  pserdv2  24711  abelthlem6  24717  abelthlem9  24721  logtayl  24934  logtaylsum  24935  logtayl2  24936  atantayl  25206  leibpilem2  25211  leibpi  25212  birthdaylem2  25222  dfef2  25240  divsqrtsumlem  25249  emcllem2  25266  emcllem4  25268  emcllem5  25269  emcllem6  25270  emcllem7  25271  harmonicbnd4  25280  fsumharmonic  25281  zetacvg  25284  lgamgulmlem4  25301  lgamgulmlem6  25303  lgamgulm2  25305  lgamcvglem  25309  lgamcvg2  25324  gamcvg  25325  gamcvg2lem  25328  regamcl  25330  relgamcl  25331  lgam1  25333  wilthlem3  25339  ftalem2  25343  ftalem4  25345  ftalem5  25346  basellem5  25354  basellem6  25355  basellem7  25356  basellem8  25357  basellem9  25358  ppiprm  25420  ppinprm  25421  chtprm  25422  chtnprm  25423  chpp1  25424  vma1  25435  ppiltx  25446  fsumvma2  25482  chpchtsum  25487  logfacbnd3  25491  logexprlim  25493  bposlem5  25556  lgscllem  25572  lgsval2lem  25575  lgsval4a  25587  lgsneg  25589  lgsdir  25600  lgsdilem2  25601  lgsdi  25602  lgsne0  25603  gausslemma2dlem3  25636  lgsquadlem2  25649  chebbnd1lem1  25737  chtppilimlem1  25741  rplogsumlem1  25752  rplogsumlem2  25753  rpvmasumlem  25755  dchrisumlema  25756  dchrisumlem2  25758  dchrisumlem3  25759  dchrmusum2  25762  dchrvmasum2lem  25764  dchrvmasumiflem1  25769  dchrvmaeq0  25772  dchrisum0flblem2  25777  dchrisum0flb  25778  dchrisum0re  25781  dchrisum0lem1b  25783  dchrisum0lem1  25784  dchrisum0lem2a  25785  dchrisum0lem2  25786  dchrisum0lem3  25787  mudivsum  25798  mulogsum  25800  logdivsum  25801  mulog2sumlem2  25803  log2sumbnd  25812  selberg2lem  25818  logdivbnd  25824  pntrsumo1  25833  pntrsumbnd2  25835  pntrlog2bndlem2  25846  pntrlog2bndlem4  25848  pntrlog2bndlem6a  25850  pntlemf  25873  eedimeq  26377  axlowdimlem6  26426  axlowdimlem16  26436  axlowdimlem17  26437  ipval2  28251  minvecolem3  28421  minvecolem4b  28423  minvecolem4  28425  h2hcau  28525  h2hlm  28526  hlimadd  28739  hlim0  28781  hhsscms  28825  occllem  28851  nlelchi  29609  opsqrlem4  29691  hmopidmchi  29699  iundisjf  30095  iundisj2f  30096  ssnnssfz  30251  iundisjfi  30257  iundisj2fi  30258  1smat1  30668  submat1n  30669  submatres  30670  submateqlem2  30672  lmatfval  30678  madjusmdetlem1  30691  madjusmdetlem2  30692  madjusmdetlem3  30693  madjusmdetlem4  30694  lmlim  30791  rge0scvg  30793  lmxrge0  30796  lmdvg  30797  esumfzf  30929  esumfsup  30930  esumpcvgval  30938  esumpmono  30939  esumcvg  30946  esumcvgsum  30948  esumsup  30949  fiunelros  31035  eulerpartlemsv2  31218  eulerpartlems  31220  eulerpartlemsv3  31221  eulerpartlemv  31224  eulerpartlemb  31228  fiblem  31259  fibp1  31262  rrvsum  31315  dstfrvclim1  31338  ballotlem1ri  31395  signsvfn  31461  chtvalz  31509  circlemethhgt  31523  subfacp1lem1  31971  subfacp1lem5  31976  subfacp1lem6  31977  erdszelem7  31989  cvmliftlem5  32081  cvmliftlem7  32083  cvmliftlem10  32086  cvmliftlem13  32088  sinccvg  32376  circum  32377  divcnvlin  32424  iprodgam  32434  faclimlem1  32435  faclimlem2  32436  faclim  32438  iprodfac  32439  faclim2  32440  poimirlem3  34284  poimirlem4  34285  poimirlem6  34287  poimirlem7  34288  poimirlem8  34289  poimirlem12  34293  poimirlem15  34296  poimirlem16  34297  poimirlem17  34298  poimirlem18  34299  poimirlem19  34300  poimirlem20  34301  poimirlem22  34303  poimirlem23  34304  poimirlem24  34305  poimirlem25  34306  poimirlem27  34308  poimirlem28  34309  poimirlem29  34310  poimirlem30  34311  poimirlem31  34312  mblfinlem2  34319  ovoliunnfl  34323  voliunnfl  34325  volsupnfl  34326  lmclim2  34423  geomcau  34424  heibor1lem  34477  heibor1  34478  bfplem1  34490  bfplem2  34491  rrncmslem  34500  rrncms  34501  eldioph3b  38702  diophin  38710  diophun  38711  diophren  38751  jm3.1lem2  38956  dgraalem  39086  dgraaub  39089  dftrcl3  39373  trclfvdecomr  39381  hashnzfz2  40013  hashnzfzclim  40014  dvradcnv2  40039  binomcxplemnotnn0  40048  nnsplit  41001  clim1fr1  41259  sumnnodd  41288  limsup10exlem  41430  fprodsubrecnncnvlem  41567  fprodaddrecnncnvlem  41569  stoweidlem7  41669  stoweidlem14  41676  stoweidlem20  41682  stoweidlem34  41696  wallispilem5  41731  wallispi  41732  stirlinglem1  41736  stirlinglem5  41740  stirlinglem7  41742  stirlinglem8  41743  stirlinglem10  41745  stirlinglem11  41746  stirlinglem12  41747  stirlinglem13  41748  stirlinglem14  41749  stirlinglem15  41750  stirlingr  41752  dirkertrigeqlem2  41761  dirkertrigeqlem3  41762  fourierdlem11  41780  fourierdlem31  41800  fourierdlem48  41816  fourierdlem49  41817  fourierdlem69  41837  fourierdlem73  41841  fourierdlem81  41849  fourierdlem93  41861  fourierdlem103  41871  fourierdlem104  41872  fourierdlem112  41880  fouriersw  41893  sge0ad2en  42090  voliunsge0lem  42131  caragenunicl  42183  caratheodorylem2  42186  hoidmvlelem3  42256  ovolval2lem  42302  ovolval2  42303  vonioolem2  42340  vonicclem2  42343  fmtno4prmfac  43042