Theorem nnuz 12898

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  {crab 3418   class class class wbr 5149  ‘cfv 6549  1c1 11141   ≤ cle 11281  ℕcn 12245  ℤcz 12591  ℤ_≥cuz 12855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-z 12592  df-uz 12856

This theorem is referenced by:  elnnuz  12899  eluz2nn  12901  uznnssnn  12912  nnwo  12930  eluznn  12935  nninf  12946  fzssnn  13580  fseq1p1m1  13610  prednn  13659  elfzo1  13717  ltwenn  13963  nnnfi  13967  ser1const  14059  expp1  14069  digit1  14235  facnn  14270  fac0  14271  facp1  14273  faclbnd4lem1  14288  bcm1k  14310  bcval5  14313  bcpasc  14316  fz1isolem  14458  seqcoll  14461  seqcoll2  14462  climuni  15532  isercolllem2  15648  isercoll  15650  sumeq2ii  15675  summolem3  15696  summolem2a  15697  fsum  15702  sum0  15703  sumz  15704  fsumcl2lem  15713  fsumadd  15722  fsummulc2  15766  fsumrelem  15789  isumnn0nn  15824  climcndslem1  15831  climcndslem2  15832  climcnds  15833  divcnv  15835  divcnvshft  15837  supcvg  15838  trireciplem  15844  trirecip  15845  expcnv  15846  geo2lim  15857  geoisum1  15861  geoisum1c  15862  mertenslem2  15867  prodeq2ii  15893  prodmolem3  15913  prodmolem2a  15914  fprod  15921  prod0  15923  prod1  15924  fprodss  15928  fprodser  15929  fprodcl2lem  15930  fprodmul  15940  fproddiv  15941  fprodn0  15959  fallfacval4  16023  bpoly4  16039  ege2le3  16070  rpnnen2lem3  16196  rpnnen2lem5  16198  rpnnen2lem8  16201  rpnnen2lem12  16205  ruclem6  16215  pwp1fsum  16371  bezoutlem2  16519  bezoutlem3  16520  lcmcllem  16570  lcmledvds  16573  lcmfval  16595  lcmfcllem  16599  lcmfledvds  16606  isprm3  16657  phicl2  16740  phibndlem  16742  eulerthlem2  16754  odzcllem  16764  odzdvds  16767  iserodd  16807  pcmptcl  16863  pcmpt  16864  pockthlem  16877  pockthg  16878  unbenlem  16880  prmreclem3  16890  prmreclem5  16892  prmreclem6  16893  prmrec  16894  1arith  16899  4sqlem13  16929  4sqlem14  16930  4sqlem17  16933  4sqlem18  16934  vdwlem1  16953  vdwlem2  16954  vdwlem3  16955  vdwlem6  16958  vdwlem8  16960  vdwlem10  16962  vdw  16966  vdwnnlem3  16969  prmlem1a  17079  mulgnnp1  19045  mulgnnsubcl  19049  mulgnn0z  19064  mulgnndir  19066  mulgpropd  19079  odfval  19499  odlem1  19502  odlem2  19506  gexlem1  19546  gexlem2  19549  gexcl3  19554  sylow1lem1  19565  efgsdmi  19699  efgsrel  19701  efgs1b  19703  efgsp1  19704  mulgnn0di  19792  lt6abl  19862  gsumval3eu  19871  gsumval3  19874  gsumzcl2  19877  gsumzaddlem  19888  gsumconst  19901  gsumzmhm  19904  gsumzoppg  19911  zringlpirlem2  21406  zringlpirlem3  21407  lmcnp  23252  lmmo  23328  1stcelcls  23409  1stccnp  23410  1stckgenlem  23501  1stckgen  23502  imasdsf1olem  24323  cphipval  25215  lmnn  25235  cmetcaulem  25260  iscmet2  25266  causs  25270  nglmle  25274  caubl  25280  iscmet3i  25284  bcthlem5  25300  ovolsf  25445  ovollb2lem  25461  ovolctb  25463  ovolunlem1a  25469  ovolunlem1  25470  ovoliunlem1  25475  ovoliun  25478  ovoliun2  25479  ovoliunnul  25480  ovolscalem1  25486  ovolicc1  25489  ovolicc2lem2  25491  ovolicc2lem3  25492  ovolicc2lem4  25493  iundisj  25521  iundisj2  25522  voliunlem1  25523  voliunlem2  25524  voliunlem3  25525  volsup  25529  ioombl1lem4  25534  uniioovol  25552  uniioombllem2  25556  uniioombllem3  25558  uniioombllem4  25559  uniioombllem6  25561  vitalilem4  25584  vitalilem5  25585  itg1climres  25688  mbfi1fseqlem6  25694  mbfi1flimlem  25696  mbfmullem2  25698  itg2monolem1  25724  itg2i1fseqle  25728  itg2i1fseq  25729  itg2i1fseq2  25730  itg2addlem  25732  plyeq0lem  26189  vieta1lem2  26291  elqaalem1  26299  elqaalem3  26301  aaliou3lem4  26326  aaliou3lem7  26329  dvtaylp  26350  taylthlem2  26354  taylthlem2OLD  26355  pserdvlem2  26410  pserdv2  26412  abelthlem6  26418  abelthlem9  26422  logtayl  26639  logtaylsum  26640  logtayl2  26641  atantayl  26914  leibpilem2  26918  leibpi  26919  birthdaylem2  26929  dfef2  26948  divsqrtsumlem  26957  emcllem2  26974  emcllem4  26976  emcllem5  26977  emcllem6  26978  emcllem7  26979  harmonicbnd4  26988  fsumharmonic  26989  zetacvg  26992  lgamgulmlem4  27009  lgamgulmlem6  27011  lgamgulm2  27013  lgamcvglem  27017  lgamcvg2  27032  gamcvg  27033  gamcvg2lem  27036  regamcl  27038  relgamcl  27039  lgam1  27041  wilthlem3  27047  ftalem2  27051  ftalem4  27053  ftalem5  27054  basellem5  27062  basellem6  27063  basellem7  27064  basellem8  27065  basellem9  27066  ppiprm  27128  ppinprm  27129  chtprm  27130  chtnprm  27131  chpp1  27132  vma1  27143  ppiltx  27154  fsumvma2  27192  chpchtsum  27197  logfacbnd3  27201  logexprlim  27203  bposlem5  27266  lgscllem  27282  lgsval2lem  27285  lgsval4a  27297  lgsneg  27299  lgsdir  27310  lgsdilem2  27311  lgsdi  27312  lgsne0  27313  gausslemma2dlem3  27346  lgsquadlem2  27359  chebbnd1lem1  27447  chtppilimlem1  27451  rplogsumlem1  27462  rplogsumlem2  27463  rpvmasumlem  27465  dchrisumlema  27466  dchrisumlem2  27468  dchrisumlem3  27469  dchrmusum2  27472  dchrvmasum2lem  27474  dchrvmasumiflem1  27479  dchrvmaeq0  27482  dchrisum0flblem2  27487  dchrisum0flb  27488  dchrisum0re  27491  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem2a  27495  dchrisum0lem2  27496  dchrisum0lem3  27497  mudivsum  27508  mulogsum  27510  logdivsum  27511  mulog2sumlem2  27513  log2sumbnd  27522  selberg2lem  27528  logdivbnd  27534  pntrsumo1  27543  pntrsumbnd2  27545  pntrlog2bndlem2  27556  pntrlog2bndlem4  27558  pntrlog2bndlem6a  27560  pntlemf  27583  eedimeq  28781  axlowdimlem6  28830  axlowdimlem16  28840  axlowdimlem17  28841  ipval2  30589  minvecolem3  30758  minvecolem4b  30760  minvecolem4  30762  h2hcau  30861  h2hlm  30862  hlimadd  31075  hlim0  31117  hhsscms  31160  occllem  31185  nlelchi  31943  opsqrlem4  32025  hmopidmchi  32033  iundisjf  32458  iundisj2f  32459  ssnnssfz  32637  iundisjfi  32646  iundisj2fi  32647  cycpmco2lem7  32945  cycpmrn  32956  1smat1  33536  submat1n  33537  submatres  33538  submateqlem2  33540  lmatfval  33546  madjusmdetlem1  33559  madjusmdetlem2  33560  madjusmdetlem3  33561  madjusmdetlem4  33562  lmlim  33679  rge0scvg  33681  lmxrge0  33684  lmdvg  33685  esumfzf  33819  esumfsup  33820  esumpcvgval  33828  esumpmono  33829  esumcvg  33836  esumcvgsum  33838  esumsup  33839  fiunelros  33924  eulerpartlemsv2  34109  eulerpartlems  34111  eulerpartlemsv3  34112  eulerpartlemv  34115  eulerpartlemb  34119  fiblem  34149  fibp1  34152  rrvsum  34205  dstfrvclim1  34228  ballotlem1ri  34285  signsvfn  34345  chtvalz  34392  circlemethhgt  34406  subfacp1lem1  34920  subfacp1lem5  34925  subfacp1lem6  34926  erdszelem7  34938  cvmliftlem5  35030  cvmliftlem7  35032  cvmliftlem10  35035  cvmliftlem13  35037  sinccvg  35408  circum  35409  divcnvlin  35458  iprodgam  35467  faclimlem1  35468  faclimlem2  35469  faclim  35471  iprodfac  35472  faclim2  35473  poimirlem3  37227  poimirlem4  37228  poimirlem6  37230  poimirlem7  37231  poimirlem8  37232  poimirlem12  37236  poimirlem15  37239  poimirlem16  37240  poimirlem17  37241  poimirlem18  37242  poimirlem19  37243  poimirlem20  37244  poimirlem22  37246  poimirlem23  37247  poimirlem24  37248  poimirlem25  37249  poimirlem27  37251  poimirlem28  37252  poimirlem29  37253  poimirlem30  37254  poimirlem31  37255  mblfinlem2  37262  ovoliunnfl  37266  voliunnfl  37268  volsupnfl  37269  lmclim2  37362  geomcau  37363  heibor1lem  37413  heibor1  37414  bfplem1  37426  bfplem2  37427  rrncmslem  37436  rrncms  37437  aks4d1p1p1  41666  sticksstones10  41758  sticksstones12a  41760  metakunt20  41810  fz1sump1  42005  sumcubes  42008  nna4b4nsq  42219  eldioph3b  42327  diophin  42334  diophun  42335  diophren  42375  jm3.1lem2  42581  dgraalem  42711  dgraaub  42714  dftrcl3  43292  trclfvdecomr  43300  hashnzfz2  43900  hashnzfzclim  43901  dvradcnv2  43926  binomcxplemnotnn0  43935  nnsplit  44878  rexanuz2nf  45013  clim1fr1  45127  sumnnodd  45156  limsup10exlem  45298  fprodsubrecnncnvlem  45433  fprodaddrecnncnvlem  45435  stoweidlem7  45533  stoweidlem14  45540  stoweidlem20  45546  stoweidlem34  45560  wallispilem5  45595  wallispi  45596  stirlinglem1  45600  stirlinglem5  45604  stirlinglem7  45606  stirlinglem8  45607  stirlinglem10  45609  stirlinglem11  45610  stirlinglem12  45611  stirlinglem13  45612  stirlinglem14  45613  stirlinglem15  45614  stirlingr  45616  dirkertrigeqlem2  45625  dirkertrigeqlem3  45626  fourierdlem11  45644  fourierdlem31  45664  fourierdlem48  45680  fourierdlem49  45681  fourierdlem69  45701  fourierdlem73  45705  fourierdlem81  45713  fourierdlem93  45725  fourierdlem103  45735  fourierdlem104  45736  fourierdlem112  45744  fouriersw  45757  sge0ad2en  45957  voliunsge0lem  45998  caragenunicl  46050  caratheodorylem2  46053  hoidmvlelem3  46123  ovolval2lem  46169  ovolval2  46170  vonioolem2  46207  vonicclem2  46210  fmtno4prmfac  47049