Theorem nnuz 12918

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  {crab 3432   class class class wbr 5147  ‘cfv 6562  1c1 11153   ≤ cle 11293  ℕcn 12263  ℤcz 12610  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-z 12611  df-uz 12876

This theorem is referenced by:  elnnuz  12919  eluz2nn  12921  uznnssnn  12934  nnwo  12952  eluznn  12957  nninf  12968  fzssnn  13604  fseq1p1m1  13634  prednn  13687  elfzo1  13748  ltwenn  13999  nnnfi  14003  ser1const  14095  expp1  14105  digit1  14272  facnn  14310  fac0  14311  facp1  14313  faclbnd4lem1  14328  bcm1k  14350  bcval5  14353  bcpasc  14356  fz1isolem  14496  seqcoll  14499  seqcoll2  14500  climuni  15584  isercolllem2  15698  isercoll  15700  sumeq2ii  15725  summolem3  15746  summolem2a  15747  fsum  15752  sum0  15753  sumz  15754  fsumcl2lem  15763  fsumadd  15772  fsummulc2  15816  fsumrelem  15839  isumnn0nn  15874  climcndslem1  15881  climcndslem2  15882  climcnds  15883  divcnv  15885  divcnvshft  15887  supcvg  15888  trireciplem  15894  trirecip  15895  expcnv  15896  geo2lim  15907  geoisum1  15911  geoisum1c  15912  mertenslem2  15917  prodeq2ii  15943  prodmolem3  15965  prodmolem2a  15966  fprod  15973  prod0  15975  prod1  15976  fprodss  15980  fprodser  15981  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodn0  16011  fallfacval4  16075  bpoly4  16091  ege2le3  16122  rpnnen2lem3  16248  rpnnen2lem5  16250  rpnnen2lem8  16253  rpnnen2lem12  16257  ruclem6  16267  pwp1fsum  16424  bezoutlem2  16573  bezoutlem3  16574  lcmcllem  16629  lcmledvds  16632  lcmfval  16654  lcmfcllem  16658  lcmfledvds  16665  isprm3  16716  phicl2  16801  phibndlem  16803  eulerthlem2  16815  odzcllem  16825  odzdvds  16828  iserodd  16868  pcmptcl  16924  pcmpt  16925  pockthlem  16938  pockthg  16939  unbenlem  16941  prmreclem3  16951  prmreclem5  16953  prmreclem6  16954  prmrec  16955  1arith  16960  4sqlem13  16990  4sqlem14  16991  4sqlem17  16994  4sqlem18  16995  vdwlem1  17014  vdwlem2  17015  vdwlem3  17016  vdwlem6  17019  vdwlem8  17021  vdwlem10  17023  vdw  17027  vdwnnlem3  17030  prmlem1a  17140  mulgnnp1  19112  mulgnnsubcl  19116  mulgnn0z  19131  mulgnndir  19133  mulgpropd  19146  odfval  19564  odlem1  19567  odlem2  19571  gexlem1  19611  gexlem2  19614  gexcl3  19619  sylow1lem1  19630  efgsdmi  19764  efgsrel  19766  efgs1b  19768  efgsp1  19769  mulgnn0di  19857  lt6abl  19927  gsumval3eu  19936  gsumval3  19939  gsumzcl2  19942  gsumzaddlem  19953  gsumconst  19966  gsumzmhm  19969  gsumzoppg  19976  zringlpirlem2  21491  zringlpirlem3  21492  lmcnp  23327  lmmo  23403  1stcelcls  23484  1stccnp  23485  1stckgenlem  23576  1stckgen  23577  imasdsf1olem  24398  cphipval  25290  lmnn  25310  cmetcaulem  25335  iscmet2  25341  causs  25345  nglmle  25349  caubl  25355  iscmet3i  25359  bcthlem5  25375  ovolsf  25520  ovollb2lem  25536  ovolctb  25538  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun  25553  ovoliun2  25554  ovoliunnul  25555  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem2  25566  ovolicc2lem3  25567  ovolicc2lem4  25568  iundisj  25596  iundisj2  25597  voliunlem1  25598  voliunlem2  25599  voliunlem3  25600  volsup  25604  ioombl1lem4  25609  uniioovol  25627  uniioombllem2  25631  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  vitalilem4  25659  vitalilem5  25660  itg1climres  25763  mbfi1fseqlem6  25769  mbfi1flimlem  25771  mbfmullem2  25773  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  plyeq0lem  26263  vieta1lem2  26367  elqaalem1  26375  elqaalem3  26377  aaliou3lem4  26402  aaliou3lem7  26405  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  pserdv2  26488  abelthlem6  26494  abelthlem9  26498  logtayl  26716  logtaylsum  26717  logtayl2  26718  atantayl  26994  leibpilem2  26998  leibpi  26999  birthdaylem2  27009  dfef2  27028  divsqrtsumlem  27037  emcllem2  27054  emcllem4  27056  emcllem5  27057  emcllem6  27058  emcllem7  27059  harmonicbnd4  27068  fsumharmonic  27069  zetacvg  27072  lgamgulmlem4  27089  lgamgulmlem6  27091  lgamgulm2  27093  lgamcvglem  27097  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  regamcl  27118  relgamcl  27119  lgam1  27121  wilthlem3  27127  ftalem2  27131  ftalem4  27133  ftalem5  27134  basellem5  27142  basellem6  27143  basellem7  27144  basellem8  27145  basellem9  27146  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  chpp1  27212  vma1  27223  ppiltx  27234  fsumvma2  27272  chpchtsum  27277  logfacbnd3  27281  logexprlim  27283  bposlem5  27346  lgscllem  27362  lgsval2lem  27365  lgsval4a  27377  lgsneg  27379  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  gausslemma2dlem3  27426  lgsquadlem2  27439  chebbnd1lem1  27527  chtppilimlem1  27531  rplogsumlem1  27542  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasum2lem  27554  dchrvmasumiflem1  27559  dchrvmaeq0  27562  dchrisum0flblem2  27567  dchrisum0flb  27568  dchrisum0re  27571  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  mudivsum  27588  mulogsum  27590  logdivsum  27591  mulog2sumlem2  27593  log2sumbnd  27602  selberg2lem  27608  logdivbnd  27614  pntrsumo1  27623  pntrsumbnd2  27625  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem6a  27640  pntlemf  27663  eedimeq  28927  axlowdimlem6  28976  axlowdimlem16  28986  axlowdimlem17  28987  ipval2  30735  minvecolem3  30904  minvecolem4b  30906  minvecolem4  30908  h2hcau  31007  h2hlm  31008  hlimadd  31221  hlim0  31263  hhsscms  31306  occllem  31331  nlelchi  32089  opsqrlem4  32171  hmopidmchi  32179  iundisjf  32608  iundisj2f  32609  ssnnssfz  32795  iundisjfi  32803  iundisj2fi  32804  chnub  32985  cycpmco2lem7  33134  cycpmrn  33145  1smat1  33764  submat1n  33765  submatres  33766  submateqlem2  33768  lmatfval  33774  madjusmdetlem1  33787  madjusmdetlem2  33788  madjusmdetlem3  33789  madjusmdetlem4  33790  lmlim  33907  rge0scvg  33909  lmxrge0  33912  lmdvg  33913  esumfzf  34049  esumfsup  34050  esumpcvgval  34058  esumpmono  34059  esumcvg  34066  esumcvgsum  34068  esumsup  34069  fiunelros  34154  eulerpartlemsv2  34339  eulerpartlems  34341  eulerpartlemsv3  34342  eulerpartlemv  34345  eulerpartlemb  34349  fiblem  34379  fibp1  34382  rrvsum  34435  dstfrvclim1  34458  ballotlem1ri  34515  signsvfn  34575  chtvalz  34622  circlemethhgt  34636  subfacp1lem1  35163  subfacp1lem5  35168  subfacp1lem6  35169  erdszelem7  35181  cvmliftlem5  35273  cvmliftlem7  35275  cvmliftlem10  35278  cvmliftlem13  35280  sinccvg  35657  circum  35658  divcnvlin  35712  iprodgam  35721  faclimlem1  35722  faclimlem2  35723  faclim  35725  iprodfac  35726  faclim2  35727  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem27  37633  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  lmclim2  37744  geomcau  37745  heibor1lem  37795  heibor1  37796  bfplem1  37808  bfplem2  37809  rrncmslem  37818  rrncms  37819  aks4d1p1p1  42044  sticksstones10  42136  sticksstones12a  42138  metakunt20  42205  fz1sump1  42322  sumcubes  42325  nna4b4nsq  42646  eldioph3b  42752  diophin  42759  diophun  42760  diophren  42800  jm3.1lem2  43006  dgraalem  43133  dgraaub  43136  dftrcl3  43709  trclfvdecomr  43717  hashnzfz2  44316  hashnzfzclim  44317  dvradcnv2  44342  binomcxplemnotnn0  44351  nnsplit  45307  rexanuz2nf  45442  clim1fr1  45556  sumnnodd  45585  limsup10exlem  45727  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  stoweidlem7  45962  stoweidlem14  45969  stoweidlem20  45975  stoweidlem34  45989  wallispilem5  46024  wallispi  46025  stirlinglem1  46029  stirlinglem5  46033  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  stirlingr  46045  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  fourierdlem11  46073  fourierdlem31  46093  fourierdlem48  46109  fourierdlem49  46110  fourierdlem69  46130  fourierdlem73  46134  fourierdlem81  46142  fourierdlem93  46154  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fouriersw  46186  sge0ad2en  46386  voliunsge0lem  46427  caragenunicl  46479  caratheodorylem2  46482  hoidmvlelem3  46552  ovolval2lem  46598  ovolval2  46599  vonioolem2  46636  vonicclem2  46639  fmtno4prmfac  47496