Theorem nnuz 12985

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {crab 3413   class class class wbr 5103  ‘cfv 6531  1c1 11182   ≤ cle 11325  ℕcn 12316  ℤcz 12674  ℤ_≥cuz 12946

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-nn 12317  df-z 12675  df-uz 12947

This theorem is used by:  elnnuz  12986  eluz2nn  12996  uznnssnn  13003  nnwo  13021  eluznn  13026  nninf  13037  fzssnn  13682  fseq1p1m1  13712  prednn  13765  elfzo1  13827  ltwenn  14085  nnnfi  14089  ser1const  14181  expp1  14191  digit1  14361  facnn  14399  fac0  14400  facp1  14402  faclbnd4lem1  14417  bcm1k  14439  bcval5  14442  bcpasc  14445  fz1isolem  14586  seqcoll  14589  seqcoll2  14590  climuni  15699  isercolllem2  15813  isercoll  15815  sumeq2ii  15840  summolem3  15860  summolem2a  15861  fsum  15866  sum0  15867  sumz  15868  fsumcl2lem  15877  fsumadd  15886  fsummulc2  15930  fsumrelem  15954  isumnn0nn  15991  climcndslem1  15998  climcndslem2  15999  climcnds  16000  divcnv  16002  divcnvshft  16004  supcvg  16005  trireciplem  16011  trirecip  16012  expcnv  16013  geo2lim  16024  geoisum1  16028  geoisum1c  16029  mertenslem2  16034  prodeq2ii  16060  prodmolem3  16080  prodmolem2a  16081  fprod  16088  prod0  16090  prod1  16091  fprodss  16095  fprodser  16096  fprodcl2lem  16097  fprodmul  16107  fproddiv  16108  fprodn0  16126  fallfacval4  16189  bpoly4  16205  ege2le3  16236  rpnnen2lem3  16364  rpnnen2lem5  16366  rpnnen2lem8  16369  rpnnen2lem12  16373  ruclem6  16383  pwp1fsum  16541  bezoutlem2  16693  bezoutlem3  16694  lcmcllem  16751  lcmledvds  16754  lcmfval  16776  lcmfcllem  16780  lcmfledvds  16787  isprm3  16838  phicl2  16925  phibndlem  16927  eulerthlem2  16939  odzcllem  16950  odzdvds  16953  iserodd  16993  pcmptcl  17049  pcmpt  17050  pockthlem  17063  pockthg  17064  unbenlem  17066  prmreclem3  17076  prmreclem5  17078  prmreclem6  17079  prmrec  17080  1arith  17085  4sqlem13  17115  4sqlem14  17116  4sqlem17  17119  4sqlem18  17120  vdwlem1  17139  vdwlem2  17140  vdwlem3  17141  vdwlem6  17144  vdwlem8  17146  vdwlem10  17148  vdw  17152  vdwnnlem3  17155  prmlem1a  17264  chnub  18776  mulgnnp1  19272  mulgnnsubcl  19276  mulgnn0z  19291  mulgnndir  19293  mulgpropd  19306  odfval  19726  odlem1  19729  odlem2  19733  gexlem1  19773  gexlem2  19776  gexcl3  19781  sylow1lem1  19792  efgsdmi  19926  efgsrel  19928  efgs1b  19930  efgsp1  19931  mulgnn0di  20019  lt6abl  20089  gsumval3eu  20098  gsumval3  20101  gsumzcl2  20104  gsumzaddlem  20115  gsumconst  20128  gsumzmhm  20131  gsumzoppg  20138  zringlpirlem2  21749  zringlpirlem3  21750  lmcnp  23602  lmmo  23678  1stcelcls  23760  1stccnp  23761  1stckgenlem  23852  1stckgen  23853  imasdsf1olem  24672  cphipval  25544  lmnn  25564  cmetcaulem  25589  iscmet2  25595  causs  25599  nglmle  25603  caubl  25609  iscmet3i  25613  bcthlem5  25629  ovolsf  25773  ovollb2lem  25789  ovolctb  25791  ovolunlem1a  25797  ovolunlem1  25798  ovoliunlem1  25803  ovoliun  25806  ovoliun2  25807  ovoliunnul  25808  ovolscalem1  25814  ovolicc1  25817  ovolicc2lem2  25819  ovolicc2lem3  25820  ovolicc2lem4  25821  iundisj  25849  iundisj2  25850  voliunlem1  25851  voliunlem2  25852  voliunlem3  25853  volsup  25857  ioombl1lem4  25862  uniioovol  25880  uniioombllem2  25884  uniioombllem3  25886  uniioombllem4  25887  uniioombllem6  25889  vitalilem4  25912  vitalilem5  25913  itg1climres  26015  mbfi1fseqlem6  26021  mbfi1flimlem  26023  mbfmullem2  26025  itg2monolem1  26051  itg2i1fseqle  26055  itg2i1fseq  26056  itg2i1fseq2  26057  itg2addlem  26059  plyeq0lem  26509  vieta1lem2  26616  elqaalem1  26624  elqaalem3  26626  aaliou3lem4  26655  aaliou3lem7  26658  dvtaylp  26679  taylthlem2  26683  pserdvlem2  26737  pserdv2  26739  abelthlem6  26745  abelthlem9  26749  logtayl  26970  logtaylsum  26971  logtayl2  26972  atantayl  27247  leibpilem2  27251  leibpi  27252  birthdaylem2  27262  dfef2  27280  divsqrtsumlem  27289  emcllem2  27306  emcllem4  27308  emcllem5  27309  emcllem6  27310  emcllem7  27311  harmonicbnd4  27320  fsumharmonic  27321  zetacvg  27324  lgamgulmlem4  27341  lgamgulmlem6  27343  lgamgulm2  27345  lgamcvglem  27349  lgamcvg2  27364  gamcvg  27365  gamcvg2lem  27368  regamcl  27370  relgamcl  27371  lgam1  27373  wilthlem3  27379  ftalem2  27383  ftalem4  27385  ftalem5  27386  basellem5  27394  basellem6  27395  basellem7  27396  basellem8  27397  basellem9  27398  ppiprm  27460  ppinprm  27461  chtprm  27462  chtnprm  27463  chpp1  27464  vma1  27475  ppiltx  27486  fsumvma2  27523  chpchtsum  27528  logfacbnd3  27532  logexprlim  27534  bposlem5  27597  lgscllem  27613  lgsval2lem  27616  lgsval4a  27628  lgsneg  27630  lgsdir  27641  lgsdilem2  27642  lgsdi  27643  lgsne0  27644  gausslemma2dlem3  27677  lgsquadlem2  27690  chebbnd1lem1  27778  chtppilimlem1  27782  rplogsumlem1  27793  rplogsumlem2  27794  rpvmasumlem  27796  dchrisumlema  27797  dchrisumlem2  27799  dchrisumlem3  27800  dchrmusum2  27803  dchrvmasum2lem  27805  dchrvmasumiflem1  27810  dchrvmaeq0  27813  dchrisum0flblem2  27818  dchrisum0flb  27819  dchrisum0re  27822  dchrisum0lem1b  27824  dchrisum0lem1  27825  dchrisum0lem2a  27826  dchrisum0lem2  27827  dchrisum0lem3  27828  mudivsum  27839  mulogsum  27841  logdivsum  27842  mulog2sumlem2  27844  log2sumbnd  27853  selberg2lem  27859  logdivbnd  27865  pntrsumo1  27874  pntrsumbnd2  27876  pntrlog2bndlem2  27887  pntrlog2bndlem4  27889  pntrlog2bndlem6a  27891  pntlemf  27914  nna4b4nsq  27972  eedimeq  29458  axlowdimlem6  29507  axlowdimlem16  29517  axlowdimlem17  29518  ipval2  31291  minvecolem3  31460  minvecolem4b  31462  minvecolem4  31464  h2hcau  31563  h2hlm  31564  hlimadd  31777  hlim0  31819  hhsscms  31862  occllem  31887  nlelchi  32645  opsqrlem4  32727  hmopidmchi  32735  iundisjf  33165  iundisj2f  33166  ssnnssfz  33361  iundisjfi  33370  iundisj2fi  33371  cycpmco2lem7  33675  cycpmrn  33686  1smat1  34418  submat1n  34419  submatres  34420  submateqlem2  34422  lmatfval  34428  madjusmdetlem1  34441  madjusmdetlem2  34442  madjusmdetlem3  34443  madjusmdetlem4  34444  lmlim  34561  rge0scvg  34563  lmxrge0  34566  lmdvg  34567  esumfzf  34683  esumfsup  34684  esumpcvgval  34692  esumpmono  34693  esumcvg  34700  esumcvgsum  34702  esumsup  34703  fiunelros  34789  eulerpartlemsv2  34973  eulerpartlems  34975  eulerpartlemsv3  34976  eulerpartlemv  34979  eulerpartlemb  34983  fiblem  35013  fibp1  35016  rrvsum  35069  dstfrvclim1  35093  ballotlem1ri  35150  signsvfn  35194  chtvalz  35241  circlemethhgt  35255  subfacp1lem1  35913  subfacp1lem5  35918  subfacp1lem6  35919  erdszelem7  35931  cvmliftlem5  36023  cvmliftlem7  36025  cvmliftlem10  36028  cvmliftlem13  36030  sinccvg  36407  circum  36408  divcnvlin  36467  iprodgam  36476  faclimlem1  36477  faclimlem2  36478  faclim  36480  iprodfac  36481  faclim2  36482  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem12  38518  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem27  38533  poimirlem28  38534  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  mblfinlem2  38544  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  lmclim2  38660  geomcau  38661  heibor1lem  38711  heibor1  38712  bfplem1  38724  bfplem2  38725  rrncmslem  38734  rrncms  38735  aks4d1p1p1  43081  sticksstones10  43173  sticksstones12a  43175  fz1sump1  43335  sumcubes  43338  eldioph3b  43729  diophin  43736  diophun  43737  diophren  43773  jm3.1lem2  43978  dgraalem  44105  dgraaub  44108  dftrcl3  44679  trclfvdecomr  44687  hashnzfz2  45264  hashnzfzclim  45265  dvradcnv2  45290  binomcxplemnotnn0  45299  nnsplit  46314  rexanuz2nf  46446  clim1fr1  46557  sumnnodd  46586  limsup10exlem  46726  fprodsubrecnncnvlem  46861  fprodaddrecnncnvlem  46863  stoweidlem7  46961  stoweidlem14  46968  stoweidlem20  46974  stoweidlem34  46988  wallispilem5  47023  wallispi  47024  stirlinglem1  47028  stirlinglem5  47032  stirlinglem7  47034  stirlinglem8  47035  stirlinglem10  47037  stirlinglem11  47038  stirlinglem12  47039  stirlinglem13  47040  stirlinglem14  47041  stirlinglem15  47042  stirlingr  47044  dirkertrigeqlem2  47053  dirkertrigeqlem3  47054  fourierdlem11  47072  fourierdlem31  47092  fourierdlem48  47108  fourierdlem49  47109  fourierdlem69  47129  fourierdlem73  47133  fourierdlem81  47141  fourierdlem93  47153  fourierdlem103  47163  fourierdlem104  47164  fourierdlem112  47172  fouriersw  47185  sge0ad2en  47385  voliunsge0lem  47426  caragenunicl  47478  caratheodorylem2  47481  hoidmvlelem3  47551  ovolval2lem  47597  ovolval2  47598  vonioolem2  47635  vonicclem2  47638  fmtno4prmfac  48601  veroquadgsumlem  50927