Theorem nnuz 13008

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  {crab 3412   class class class wbr 5102  ‘cfv 6539  1c1 11205   ≤ cle 11348  ℕcn 12339  ℤcz 12697  ℤ_≥cuz 12969

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-z 12698  df-uz 12970

This theorem is used by:  elnnuz  13009  eluz2nn  13019  uznnssnn  13026  nnwo  13044  eluznn  13049  nninf  13060  fzssnn  13706  fseq1p1m1  13736  prednn  13789  elfzo1  13851  ltwenn  14109  nnnfi  14113  ser1const  14205  expp1  14215  digit1  14385  facnn  14423  fac0  14424  facp1  14426  faclbnd4lem1  14441  bcm1k  14463  bcval5  14466  bcpasc  14469  fz1isolem  14610  seqcoll  14613  seqcoll2  14614  climuni  15725  isercolllem2  15839  isercoll  15841  sumeq2ii  15866  summolem3  15886  summolem2a  15887  fsum  15892  sum0  15893  sumz  15894  fsumcl2lem  15903  fsumadd  15912  fsummulc2  15956  fsumrelem  15980  isumnn0nn  16017  climcndslem1  16024  climcndslem2  16025  climcnds  16026  divcnv  16028  divcnvshft  16030  supcvg  16031  trireciplem  16037  trirecip  16038  expcnv  16039  geo2lim  16050  geoisum1  16054  geoisum1c  16055  mertenslem2  16060  prodeq2ii  16086  prodmolem3  16106  prodmolem2a  16107  fprod  16114  prod0  16116  prod1  16117  fprodss  16121  fprodser  16122  fprodcl2lem  16123  fprodmul  16133  fproddiv  16134  fprodn0  16152  fallfacval4  16215  bpoly4  16231  ege2le3  16262  rpnnen2lem3  16390  rpnnen2lem5  16392  rpnnen2lem8  16395  rpnnen2lem12  16399  ruclem6  16409  pwp1fsum  16567  bezoutlem2  16719  bezoutlem3  16720  lcmcllem  16777  lcmledvds  16780  lcmfval  16802  lcmfcllem  16806  lcmfledvds  16813  isprm3  16864  phicl2  16951  phibndlem  16953  eulerthlem2  16965  odzcllem  16976  odzdvds  16979  iserodd  17019  pcmptcl  17075  pcmpt  17076  pockthlem  17089  pockthg  17090  unbenlem  17092  prmreclem3  17102  prmreclem5  17104  prmreclem6  17105  prmrec  17106  1arith  17111  4sqlem13  17141  4sqlem14  17142  4sqlem17  17145  4sqlem18  17146  vdwlem1  17165  vdwlem2  17166  vdwlem3  17167  vdwlem6  17170  vdwlem8  17172  vdwlem10  17174  vdw  17178  vdwnnlem3  17181  prmlem1a  17290  chnub  18802  mulgnnp1  19298  mulgnnsubcl  19302  mulgnn0z  19317  mulgnndir  19319  mulgpropd  19332  odfval  19752  odlem1  19755  odlem2  19759  gexlem1  19799  gexlem2  19802  gexcl3  19807  sylow1lem1  19818  efgsdmi  19952  efgsrel  19954  efgs1b  19956  efgsp1  19957  mulgnn0di  20045  lt6abl  20115  gsumval3eu  20124  gsumval3  20127  gsumzcl2  20130  gsumzaddlem  20141  gsumconst  20154  gsumzmhm  20157  gsumzoppg  20164  zringlpirlem2  21775  zringlpirlem3  21776  lmcnp  23628  lmmo  23704  1stcelcls  23786  1stccnp  23787  1stckgenlem  23878  1stckgen  23879  imasdsf1olem  24698  cphipval  25570  lmnn  25590  cmetcaulem  25615  iscmet2  25621  causs  25625  nglmle  25629  caubl  25635  iscmet3i  25639  bcthlem5  25655  ovolsf  25799  ovollb2lem  25815  ovolctb  25817  ovolunlem1a  25823  ovolunlem1  25824  ovoliunlem1  25829  ovoliun  25832  ovoliun2  25833  ovoliunnul  25834  ovolscalem1  25840  ovolicc1  25843  ovolicc2lem2  25845  ovolicc2lem3  25846  ovolicc2lem4  25847  iundisj  25875  iundisj2  25876  voliunlem1  25877  voliunlem2  25878  voliunlem3  25879  volsup  25883  ioombl1lem4  25888  uniioovol  25906  uniioombllem2  25910  uniioombllem3  25912  uniioombllem4  25913  uniioombllem6  25915  vitalilem4  25938  vitalilem5  25939  itg1climres  26041  mbfi1fseqlem6  26047  mbfi1flimlem  26049  mbfmullem2  26051  itg2monolem1  26077  itg2i1fseqle  26081  itg2i1fseq  26082  itg2i1fseq2  26083  itg2addlem  26085  plyeq0lem  26535  vieta1lem2  26640  elqaalem1  26648  elqaalem3  26650  aaliou3lem4  26679  aaliou3lem7  26682  dvtaylp  26703  taylthlem2  26707  pserdvlem2  26761  pserdv2  26763  abelthlem6  26769  abelthlem9  26773  logtayl  26994  logtaylsum  26995  logtayl2  26996  atantayl  27271  leibpilem2  27275  leibpi  27276  birthdaylem2  27286  dfef2  27304  divsqrtsumlem  27313  emcllem2  27330  emcllem4  27332  emcllem5  27333  emcllem6  27334  emcllem7  27335  harmonicbnd4  27344  fsumharmonic  27345  zetacvg  27348  lgamgulmlem4  27365  lgamgulmlem6  27367  lgamgulm2  27369  lgamcvglem  27373  lgamcvg2  27388  gamcvg  27389  gamcvg2lem  27392  regamcl  27394  relgamcl  27395  lgam1  27397  wilthlem3  27403  ftalem2  27407  ftalem4  27409  ftalem5  27410  basellem5  27418  basellem6  27419  basellem7  27420  basellem8  27421  basellem9  27422  ppiprm  27484  ppinprm  27485  chtprm  27486  chtnprm  27487  chpp1  27488  vma1  27499  ppiltx  27510  fsumvma2  27547  chpchtsum  27552  logfacbnd3  27556  logexprlim  27558  bposlem5  27621  lgscllem  27637  lgsval2lem  27640  lgsval4a  27652  lgsneg  27654  lgsdir  27665  lgsdilem2  27666  lgsdi  27667  lgsne0  27668  gausslemma2dlem3  27701  lgsquadlem2  27714  chebbnd1lem1  27802  chtppilimlem1  27806  rplogsumlem1  27817  rplogsumlem2  27818  rpvmasumlem  27820  dchrisumlema  27821  dchrisumlem2  27823  dchrisumlem3  27824  dchrmusum2  27827  dchrvmasum2lem  27829  dchrvmasumiflem1  27834  dchrvmaeq0  27837  dchrisum0flblem2  27842  dchrisum0flb  27843  dchrisum0re  27846  dchrisum0lem1b  27848  dchrisum0lem1  27849  dchrisum0lem2a  27850  dchrisum0lem2  27851  dchrisum0lem3  27852  mudivsum  27863  mulogsum  27865  logdivsum  27866  mulog2sumlem2  27868  log2sumbnd  27877  selberg2lem  27883  logdivbnd  27889  pntrsumo1  27898  pntrsumbnd2  27900  pntrlog2bndlem2  27911  pntrlog2bndlem4  27913  pntrlog2bndlem6a  27915  pntlemf  27938  nna4b4nsq  27996  eedimeq  29482  axlowdimlem6  29531  axlowdimlem16  29541  axlowdimlem17  29542  ipval2  31315  minvecolem3  31484  minvecolem4b  31486  minvecolem4  31488  h2hcau  31587  h2hlm  31588  hlimadd  31801  hlim0  31843  hhsscms  31886  occllem  31911  nlelchi  32669  opsqrlem4  32751  hmopidmchi  32759  iundisjf  33231  iundisj2f  33232  ssnnssfz  33426  iundisjfi  33435  iundisj2fi  33436  cycpmco2lem7  33740  cycpmrn  33751  1smat1  34483  submat1n  34484  submatres  34485  submateqlem2  34487  lmatfval  34493  madjusmdetlem1  34506  madjusmdetlem2  34507  madjusmdetlem3  34508  madjusmdetlem4  34509  lmlim  34626  rge0scvg  34628  lmxrge0  34631  lmdvg  34632  esumfzf  34748  esumfsup  34749  esumpcvgval  34757  esumpmono  34758  esumcvg  34765  esumcvgsum  34767  esumsup  34768  fiunelros  34854  eulerpartlemsv2  35037  eulerpartlems  35039  eulerpartlemsv3  35040  eulerpartlemv  35043  eulerpartlemb  35047  fiblem  35077  fibp1  35080  rrvsum  35133  dstfrvclim1  35157  ballotlem1ri  35214  signsvfn  35258  chtvalz  35305  circlemethhgt  35319  subfacp1lem1  36031  subfacp1lem5  36036  subfacp1lem6  36037  erdszelem7  36049  cvmliftlem5  36141  cvmliftlem7  36143  cvmliftlem10  36146  cvmliftlem13  36148  sinccvg  36525  circum  36526  divcnvlin  36591  iprodgam  36600  faclimlem1  36601  faclimlem2  36602  faclim  36604  iprodfac  36605  faclim2  36606  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem8  38640  poimirlem12  38644  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem18  38650  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem27  38659  poimirlem28  38660  poimirlem29  38661  poimirlem30  38662  poimirlem31  38663  mblfinlem2  38670  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  lmclim2  38786  geomcau  38787  heibor1lem  38837  heibor1  38838  bfplem1  38850  bfplem2  38851  rrncmslem  38860  rrncms  38861  aks4d1p1p1  43207  sticksstones10  43299  sticksstones12a  43301  fz1sump1  43461  sumcubes  43464  eldioph3b  43870  diophin  43877  diophun  43878  diophren  43914  jm3.1lem2  44119  dgraalem  44241  dgraaub  44244  dftrcl3  44814  trclfvdecomr  44822  hashnzfz2  45399  hashnzfzclim  45400  dvradcnv2  45425  binomcxplemnotnn0  45434  nnsplit  46464  rexanuz2nf  46596  clim1fr1  46707  sumnnodd  46736  limsup10exlem  46876  fprodsubrecnncnvlem  47011  fprodaddrecnncnvlem  47013  stoweidlem7  47111  stoweidlem14  47118  stoweidlem20  47124  stoweidlem34  47138  wallispilem5  47173  wallispi  47174  stirlinglem1  47178  stirlinglem5  47182  stirlinglem7  47184  stirlinglem8  47185  stirlinglem10  47187  stirlinglem11  47188  stirlinglem12  47189  stirlinglem13  47190  stirlinglem14  47191  stirlinglem15  47192  stirlingr  47194  dirkertrigeqlem2  47203  dirkertrigeqlem3  47204  fourierdlem11  47222  fourierdlem31  47242  fourierdlem48  47258  fourierdlem49  47259  fourierdlem69  47279  fourierdlem73  47283  fourierdlem81  47291  fourierdlem93  47303  fourierdlem103  47313  fourierdlem104  47314  fourierdlem112  47322  fouriersw  47335  sge0ad2en  47535  voliunsge0lem  47576  caragenunicl  47628  caratheodorylem2  47631  hoidmvlelem3  47701  ovolval2lem  47747  ovolval2  47748  vonioolem2  47785  vonicclem2  47788  fmtno4prmfac  48751  veroquadgsumlem  51152