Theorem nnuz 12863

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  {crab 3424   class class class wbr 5139  ‘cfv 6534  1c1 11108   ≤ cle 11247  ℕcn 12210  ℤcz 12556  ℤ_≥cuz 12820

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 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-z 12557  df-uz 12821

This theorem is referenced by:  elnnuz  12864  eluz2nn  12866  uznnssnn  12877  nnwo  12895  eluznn  12900  nninf  12911  fzssnn  13543  fseq1p1m1  13573  prednn  13622  elfzo1  13680  ltwenn  13925  nnnfi  13929  ser1const  14022  expp1  14032  digit1  14198  facnn  14233  fac0  14234  facp1  14236  faclbnd4lem1  14251  bcm1k  14273  bcval5  14276  bcpasc  14279  fz1isolem  14420  seqcoll  14423  seqcoll2  14424  climuni  15494  isercolllem2  15610  isercoll  15612  sumeq2ii  15637  summolem3  15658  summolem2a  15659  fsum  15664  sum0  15665  sumz  15666  fsumcl2lem  15675  fsumadd  15684  fsummulc2  15728  fsumrelem  15751  isumnn0nn  15786  climcndslem1  15793  climcndslem2  15794  climcnds  15795  divcnv  15797  divcnvshft  15799  supcvg  15800  trireciplem  15806  trirecip  15807  expcnv  15808  geo2lim  15819  geoisum1  15823  geoisum1c  15824  mertenslem2  15829  prodeq2ii  15855  prodmolem3  15875  prodmolem2a  15876  fprod  15883  prod0  15885  prod1  15886  fprodss  15890  fprodser  15891  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodn0  15921  fallfacval4  15985  bpoly4  16001  ege2le3  16032  rpnnen2lem3  16158  rpnnen2lem5  16160  rpnnen2lem8  16163  rpnnen2lem12  16167  ruclem6  16177  pwp1fsum  16333  bezoutlem2  16481  bezoutlem3  16482  lcmcllem  16532  lcmledvds  16535  lcmfval  16557  lcmfcllem  16561  lcmfledvds  16568  isprm3  16619  phicl2  16702  phibndlem  16704  eulerthlem2  16716  odzcllem  16726  odzdvds  16729  iserodd  16769  pcmptcl  16825  pcmpt  16826  pockthlem  16839  pockthg  16840  unbenlem  16842  prmreclem3  16852  prmreclem5  16854  prmreclem6  16855  prmrec  16856  1arith  16861  4sqlem13  16891  4sqlem14  16892  4sqlem17  16895  4sqlem18  16896  vdwlem1  16915  vdwlem2  16916  vdwlem3  16917  vdwlem6  16920  vdwlem8  16922  vdwlem10  16924  vdw  16928  vdwnnlem3  16931  prmlem1a  17041  mulgnnp1  19001  mulgnnsubcl  19005  mulgnn0z  19020  mulgnndir  19022  mulgpropd  19035  odfval  19444  odlem1  19447  odlem2  19451  gexlem1  19491  gexlem2  19494  gexcl3  19499  sylow1lem1  19510  efgsdmi  19644  efgsrel  19646  efgs1b  19648  efgsp1  19649  mulgnn0di  19737  lt6abl  19807  gsumval3eu  19816  gsumval3  19819  gsumzcl2  19822  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  zringlpirlem2  21320  zringlpirlem3  21321  lmcnp  23132  lmmo  23208  1stcelcls  23289  1stccnp  23290  1stckgenlem  23381  1stckgen  23382  imasdsf1olem  24203  cphipval  25095  lmnn  25115  cmetcaulem  25140  iscmet2  25146  causs  25150  nglmle  25154  caubl  25160  iscmet3i  25164  bcthlem5  25180  ovolsf  25325  ovollb2lem  25341  ovolctb  25343  ovolunlem1a  25349  ovolunlem1  25350  ovoliunlem1  25355  ovoliun  25358  ovoliun2  25359  ovoliunnul  25360  ovolscalem1  25366  ovolicc1  25369  ovolicc2lem2  25371  ovolicc2lem3  25372  ovolicc2lem4  25373  iundisj  25401  iundisj2  25402  voliunlem1  25403  voliunlem2  25404  voliunlem3  25405  volsup  25409  ioombl1lem4  25414  uniioovol  25432  uniioombllem2  25436  uniioombllem3  25438  uniioombllem4  25439  uniioombllem6  25441  vitalilem4  25464  vitalilem5  25465  itg1climres  25568  mbfi1fseqlem6  25574  mbfi1flimlem  25576  mbfmullem2  25578  itg2monolem1  25604  itg2i1fseqle  25608  itg2i1fseq  25609  itg2i1fseq2  25610  itg2addlem  25612  plyeq0lem  26066  vieta1lem2  26167  elqaalem1  26175  elqaalem3  26177  aaliou3lem4  26202  aaliou3lem7  26205  dvtaylp  26225  taylthlem2  26229  pserdvlem2  26284  pserdv2  26286  abelthlem6  26292  abelthlem9  26296  logtayl  26513  logtaylsum  26514  logtayl2  26515  atantayl  26788  leibpilem2  26792  leibpi  26793  birthdaylem2  26803  dfef2  26822  divsqrtsumlem  26831  emcllem2  26848  emcllem4  26850  emcllem5  26851  emcllem6  26852  emcllem7  26853  harmonicbnd4  26862  fsumharmonic  26863  zetacvg  26866  lgamgulmlem4  26883  lgamgulmlem6  26885  lgamgulm2  26887  lgamcvglem  26891  lgamcvg2  26906  gamcvg  26907  gamcvg2lem  26910  regamcl  26912  relgamcl  26913  lgam1  26915  wilthlem3  26921  ftalem2  26925  ftalem4  26927  ftalem5  26928  basellem5  26936  basellem6  26937  basellem7  26938  basellem8  26939  basellem9  26940  ppiprm  27002  ppinprm  27003  chtprm  27004  chtnprm  27005  chpp1  27006  vma1  27017  ppiltx  27028  fsumvma2  27066  chpchtsum  27071  logfacbnd3  27075  logexprlim  27077  bposlem5  27140  lgscllem  27156  lgsval2lem  27159  lgsval4a  27171  lgsneg  27173  lgsdir  27184  lgsdilem2  27185  lgsdi  27186  lgsne0  27187  gausslemma2dlem3  27220  lgsquadlem2  27233  chebbnd1lem1  27321  chtppilimlem1  27325  rplogsumlem1  27336  rplogsumlem2  27337  rpvmasumlem  27339  dchrisumlema  27340  dchrisumlem2  27342  dchrisumlem3  27343  dchrmusum2  27346  dchrvmasum2lem  27348  dchrvmasumiflem1  27353  dchrvmaeq0  27356  dchrisum0flblem2  27361  dchrisum0flb  27362  dchrisum0re  27365  dchrisum0lem1b  27367  dchrisum0lem1  27368  dchrisum0lem2a  27369  dchrisum0lem2  27370  dchrisum0lem3  27371  mudivsum  27382  mulogsum  27384  logdivsum  27385  mulog2sumlem2  27387  log2sumbnd  27396  selberg2lem  27402  logdivbnd  27408  pntrsumo1  27417  pntrsumbnd2  27419  pntrlog2bndlem2  27430  pntrlog2bndlem4  27432  pntrlog2bndlem6a  27434  pntlemf  27457  eedimeq  28628  axlowdimlem6  28677  axlowdimlem16  28687  axlowdimlem17  28688  ipval2  30432  minvecolem3  30601  minvecolem4b  30603  minvecolem4  30605  h2hcau  30704  h2hlm  30705  hlimadd  30918  hlim0  30960  hhsscms  31003  occllem  31028  nlelchi  31786  opsqrlem4  31868  hmopidmchi  31876  iundisjf  32292  iundisj2f  32293  ssnnssfz  32470  iundisjfi  32479  iundisj2fi  32480  cycpmco2lem7  32762  cycpmrn  32773  1smat1  33276  submat1n  33277  submatres  33278  submateqlem2  33280  lmatfval  33286  madjusmdetlem1  33299  madjusmdetlem2  33300  madjusmdetlem3  33301  madjusmdetlem4  33302  lmlim  33419  rge0scvg  33421  lmxrge0  33424  lmdvg  33425  esumfzf  33559  esumfsup  33560  esumpcvgval  33568  esumpmono  33569  esumcvg  33576  esumcvgsum  33578  esumsup  33579  fiunelros  33664  eulerpartlemsv2  33849  eulerpartlems  33851  eulerpartlemsv3  33852  eulerpartlemv  33855  eulerpartlemb  33859  fiblem  33889  fibp1  33892  rrvsum  33945  dstfrvclim1  33968  ballotlem1ri  34025  signsvfn  34085  chtvalz  34132  circlemethhgt  34146  subfacp1lem1  34661  subfacp1lem5  34666  subfacp1lem6  34667  erdszelem7  34679  cvmliftlem5  34771  cvmliftlem7  34773  cvmliftlem10  34776  cvmliftlem13  34778  sinccvg  35149  circum  35150  divcnvlin  35199  iprodgam  35208  faclimlem1  35209  faclimlem2  35210  faclim  35212  iprodfac  35213  faclim2  35214  gg-taylthlem2  35658  poimirlem3  36985  poimirlem4  36986  poimirlem6  36988  poimirlem7  36989  poimirlem8  36990  poimirlem12  36994  poimirlem15  36997  poimirlem16  36998  poimirlem17  36999  poimirlem18  37000  poimirlem19  37001  poimirlem20  37002  poimirlem22  37004  poimirlem23  37005  poimirlem24  37006  poimirlem25  37007  poimirlem27  37009  poimirlem28  37010  poimirlem29  37011  poimirlem30  37012  poimirlem31  37013  mblfinlem2  37020  ovoliunnfl  37024  voliunnfl  37026  volsupnfl  37027  lmclim2  37120  geomcau  37121  heibor1lem  37171  heibor1  37172  bfplem1  37184  bfplem2  37185  rrncmslem  37194  rrncms  37195  aks4d1p1p1  41425  sticksstones10  41468  sticksstones12a  41470  metakunt20  41501  fz1sump1  41702  sumcubes  41705  nna4b4nsq  41916  eldioph3b  42017  diophin  42024  diophun  42025  diophren  42065  jm3.1lem2  42271  dgraalem  42401  dgraaub  42404  dftrcl3  42985  trclfvdecomr  42993  hashnzfz2  43594  hashnzfzclim  43595  dvradcnv2  43620  binomcxplemnotnn0  43629  nnsplit  44578  rexanuz2nf  44713  clim1fr1  44827  sumnnodd  44856  limsup10exlem  44998  fprodsubrecnncnvlem  45133  fprodaddrecnncnvlem  45135  stoweidlem7  45233  stoweidlem14  45240  stoweidlem20  45246  stoweidlem34  45260  wallispilem5  45295  wallispi  45296  stirlinglem1  45300  stirlinglem5  45304  stirlinglem7  45306  stirlinglem8  45307  stirlinglem10  45309  stirlinglem11  45310  stirlinglem12  45311  stirlinglem13  45312  stirlinglem14  45313  stirlinglem15  45314  stirlingr  45316  dirkertrigeqlem2  45325  dirkertrigeqlem3  45326  fourierdlem11  45344  fourierdlem31  45364  fourierdlem48  45380  fourierdlem49  45381  fourierdlem69  45401  fourierdlem73  45405  fourierdlem81  45413  fourierdlem93  45425  fourierdlem103  45435  fourierdlem104  45436  fourierdlem112  45444  fouriersw  45457  sge0ad2en  45657  voliunsge0lem  45698  caragenunicl  45750  caratheodorylem2  45753  hoidmvlelem3  45823  ovolval2lem  45869  ovolval2  45870  vonioolem2  45907  vonicclem2  45910  fmtno4prmfac  46750