Theorem nnuz 12442

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

Syntax hints:   = wceq 1543   ∈ wcel 2112  {crab 3055   class class class wbr 5039  ‘cfv 6358  1c1 10695   ≤ cle 10833  ℕcn 11795  ℤcz 12141  ℤ_≥cuz 12403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-cnex 10750  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-nn 11796  df-z 12142  df-uz 12404

This theorem is referenced by:  elnnuz  12443  eluz2nn  12445  uznnssnn  12456  nnwo  12474  eluznn  12479  nninf  12490  fzssnn  13121  fseq1p1m1  13151  prednn  13200  elfzo1  13257  ltwenn  13500  nnnfi  13504  ser1const  13597  expp1  13607  digit1  13769  facnn  13806  fac0  13807  facp1  13809  faclbnd4lem1  13824  bcm1k  13846  bcval5  13849  bcpasc  13852  fz1isolem  13992  seqcoll  13995  seqcoll2  13996  climuni  15078  isercolllem2  15194  isercoll  15196  sumeq2ii  15222  summolem3  15243  summolem2a  15244  fsum  15249  sum0  15250  sumz  15251  fsumcl2lem  15260  fsumadd  15268  fsummulc2  15311  fsumrelem  15334  isumnn0nn  15369  climcndslem1  15376  climcndslem2  15377  climcnds  15378  divcnv  15380  divcnvshft  15382  supcvg  15383  trireciplem  15389  trirecip  15390  expcnv  15391  geo2lim  15402  geoisum1  15406  geoisum1c  15407  mertenslem2  15412  prodeq2ii  15438  prodmolem3  15458  prodmolem2a  15459  fprod  15466  prod0  15468  prod1  15469  fprodss  15473  fprodser  15474  fprodcl2lem  15475  fprodmul  15485  fproddiv  15486  fprodn0  15504  fallfacval4  15568  bpoly4  15584  ege2le3  15614  rpnnen2lem3  15740  rpnnen2lem5  15742  rpnnen2lem8  15745  rpnnen2lem12  15749  ruclem6  15759  pwp1fsum  15915  bezoutlem2  16063  bezoutlem3  16064  lcmcllem  16116  lcmledvds  16119  lcmfval  16141  lcmfcllem  16145  lcmfledvds  16152  isprm3  16203  phicl2  16284  phibndlem  16286  eulerthlem2  16298  odzcllem  16308  odzdvds  16311  iserodd  16351  pcmptcl  16407  pcmpt  16408  pockthlem  16421  pockthg  16422  unbenlem  16424  prmreclem3  16434  prmreclem5  16436  prmreclem6  16437  prmrec  16438  1arith  16443  4sqlem13  16473  4sqlem14  16474  4sqlem17  16477  4sqlem18  16478  vdwlem1  16497  vdwlem2  16498  vdwlem3  16499  vdwlem6  16502  vdwlem8  16504  vdwlem10  16506  vdw  16510  vdwnnlem3  16513  prmlem1a  16623  mulgnnp1  18454  mulgnnsubcl  18458  mulgnn0z  18472  mulgnndir  18474  mulgpropd  18487  odfval  18878  odlem1  18881  odlem2  18885  gexlem1  18922  gexlem2  18925  gexcl3  18930  sylow1lem1  18941  efgsdmi  19076  efgsrel  19078  efgs1b  19080  efgsp1  19081  mulgnn0di  19165  lt6abl  19234  gsumval3eu  19243  gsumval3  19246  gsumzcl2  19249  gsumzaddlem  19260  gsumconst  19273  gsumzmhm  19276  gsumzoppg  19283  zringlpirlem2  20404  zringlpirlem3  20405  lmcnp  22155  lmmo  22231  1stcelcls  22312  1stccnp  22313  1stckgenlem  22404  1stckgen  22405  imasdsf1olem  23225  cphipval  24094  lmnn  24114  cmetcaulem  24139  iscmet2  24145  causs  24149  nglmle  24153  caubl  24159  iscmet3i  24163  bcthlem5  24179  ovolsf  24323  ovollb2lem  24339  ovolctb  24341  ovolunlem1a  24347  ovolunlem1  24348  ovoliunlem1  24353  ovoliun  24356  ovoliun2  24357  ovoliunnul  24358  ovolscalem1  24364  ovolicc1  24367  ovolicc2lem2  24369  ovolicc2lem3  24370  ovolicc2lem4  24371  iundisj  24399  iundisj2  24400  voliunlem1  24401  voliunlem2  24402  voliunlem3  24403  volsup  24407  ioombl1lem4  24412  uniioovol  24430  uniioombllem2  24434  uniioombllem3  24436  uniioombllem4  24437  uniioombllem6  24439  vitalilem4  24462  vitalilem5  24463  itg1climres  24566  mbfi1fseqlem6  24572  mbfi1flimlem  24574  mbfmullem2  24576  itg2monolem1  24602  itg2i1fseqle  24606  itg2i1fseq  24607  itg2i1fseq2  24608  itg2addlem  24610  plyeq0lem  25058  vieta1lem2  25158  elqaalem1  25166  elqaalem3  25168  aaliou3lem4  25193  aaliou3lem7  25196  dvtaylp  25216  taylthlem2  25220  pserdvlem2  25274  pserdv2  25276  abelthlem6  25282  abelthlem9  25286  logtayl  25502  logtaylsum  25503  logtayl2  25504  atantayl  25774  leibpilem2  25778  leibpi  25779  birthdaylem2  25789  dfef2  25807  divsqrtsumlem  25816  emcllem2  25833  emcllem4  25835  emcllem5  25836  emcllem6  25837  emcllem7  25838  harmonicbnd4  25847  fsumharmonic  25848  zetacvg  25851  lgamgulmlem4  25868  lgamgulmlem6  25870  lgamgulm2  25872  lgamcvglem  25876  lgamcvg2  25891  gamcvg  25892  gamcvg2lem  25895  regamcl  25897  relgamcl  25898  lgam1  25900  wilthlem3  25906  ftalem2  25910  ftalem4  25912  ftalem5  25913  basellem5  25921  basellem6  25922  basellem7  25923  basellem8  25924  basellem9  25925  ppiprm  25987  ppinprm  25988  chtprm  25989  chtnprm  25990  chpp1  25991  vma1  26002  ppiltx  26013  fsumvma2  26049  chpchtsum  26054  logfacbnd3  26058  logexprlim  26060  bposlem5  26123  lgscllem  26139  lgsval2lem  26142  lgsval4a  26154  lgsneg  26156  lgsdir  26167  lgsdilem2  26168  lgsdi  26169  lgsne0  26170  gausslemma2dlem3  26203  lgsquadlem2  26216  chebbnd1lem1  26304  chtppilimlem1  26308  rplogsumlem1  26319  rplogsumlem2  26320  rpvmasumlem  26322  dchrisumlema  26323  dchrisumlem2  26325  dchrisumlem3  26326  dchrmusum2  26329  dchrvmasum2lem  26331  dchrvmasumiflem1  26336  dchrvmaeq0  26339  dchrisum0flblem2  26344  dchrisum0flb  26345  dchrisum0re  26348  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0lem2  26353  dchrisum0lem3  26354  mudivsum  26365  mulogsum  26367  logdivsum  26368  mulog2sumlem2  26370  log2sumbnd  26379  selberg2lem  26385  logdivbnd  26391  pntrsumo1  26400  pntrsumbnd2  26402  pntrlog2bndlem2  26413  pntrlog2bndlem4  26415  pntrlog2bndlem6a  26417  pntlemf  26440  eedimeq  26943  axlowdimlem6  26992  axlowdimlem16  27002  axlowdimlem17  27003  ipval2  28742  minvecolem3  28911  minvecolem4b  28913  minvecolem4  28915  h2hcau  29014  h2hlm  29015  hlimadd  29228  hlim0  29270  hhsscms  29313  occllem  29338  nlelchi  30096  opsqrlem4  30178  hmopidmchi  30186  iundisjf  30601  iundisj2f  30602  ssnnssfz  30782  iundisjfi  30791  iundisj2fi  30792  cycpmco2lem7  31072  cycpmrn  31083  1smat1  31422  submat1n  31423  submatres  31424  submateqlem2  31426  lmatfval  31432  madjusmdetlem1  31445  madjusmdetlem2  31446  madjusmdetlem3  31447  madjusmdetlem4  31448  lmlim  31565  rge0scvg  31567  lmxrge0  31570  lmdvg  31571  esumfzf  31703  esumfsup  31704  esumpcvgval  31712  esumpmono  31713  esumcvg  31720  esumcvgsum  31722  esumsup  31723  fiunelros  31808  eulerpartlemsv2  31991  eulerpartlems  31993  eulerpartlemsv3  31994  eulerpartlemv  31997  eulerpartlemb  32001  fiblem  32031  fibp1  32034  rrvsum  32087  dstfrvclim1  32110  ballotlem1ri  32167  signsvfn  32227  chtvalz  32275  circlemethhgt  32289  subfacp1lem1  32808  subfacp1lem5  32813  subfacp1lem6  32814  erdszelem7  32826  cvmliftlem5  32918  cvmliftlem7  32920  cvmliftlem10  32923  cvmliftlem13  32925  sinccvg  33298  circum  33299  divcnvlin  33367  iprodgam  33377  faclimlem1  33378  faclimlem2  33379  faclim  33381  iprodfac  33382  faclim2  33383  poimirlem3  35466  poimirlem4  35467  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem12  35475  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  poimirlem22  35485  poimirlem23  35486  poimirlem24  35487  poimirlem25  35488  poimirlem27  35490  poimirlem28  35491  poimirlem29  35492  poimirlem30  35493  poimirlem31  35494  mblfinlem2  35501  ovoliunnfl  35505  voliunnfl  35507  volsupnfl  35508  lmclim2  35602  geomcau  35603  heibor1lem  35653  heibor1  35654  bfplem1  35666  bfplem2  35667  rrncmslem  35676  rrncms  35677  aks4d1p1p1  39753  sticksstones10  39780  sticksstones12a  39782  metakunt20  39807  nna4b4nsq  40141  eldioph3b  40231  diophin  40238  diophun  40239  diophren  40279  jm3.1lem2  40484  dgraalem  40614  dgraaub  40617  dftrcl3  40946  trclfvdecomr  40954  hashnzfz2  41553  hashnzfzclim  41554  dvradcnv2  41579  binomcxplemnotnn0  41588  nnsplit  42511  clim1fr1  42760  sumnnodd  42789  limsup10exlem  42931  fprodsubrecnncnvlem  43066  fprodaddrecnncnvlem  43068  stoweidlem7  43166  stoweidlem14  43173  stoweidlem20  43179  stoweidlem34  43193  wallispilem5  43228  wallispi  43229  stirlinglem1  43233  stirlinglem5  43237  stirlinglem7  43239  stirlinglem8  43240  stirlinglem10  43242  stirlinglem11  43243  stirlinglem12  43244  stirlinglem13  43245  stirlinglem14  43246  stirlinglem15  43247  stirlingr  43249  dirkertrigeqlem2  43258  dirkertrigeqlem3  43259  fourierdlem11  43277  fourierdlem31  43297  fourierdlem48  43313  fourierdlem49  43314  fourierdlem69  43334  fourierdlem73  43338  fourierdlem81  43346  fourierdlem93  43358  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  fouriersw  43390  sge0ad2en  43587  voliunsge0lem  43628  caragenunicl  43680  caratheodorylem2  43683  hoidmvlelem3  43753  ovolval2lem  43799  ovolval2  43800  vonioolem2  43837  vonicclem2  43840  fmtno4prmfac  44640