Theorem nnuz 12930

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {crab 3414   class class class wbr 5107  ‘cfv 6537  1c1 11129   ≤ cle 11272  ℕcn 12261  ℤcz 12619  ℤ_≥cuz 12891

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-nn 12262  df-z 12620  df-uz 12892

This theorem is used by:  elnnuz  12931  eluz2nn  12941  uznnssnn  12948  nnwo  12966  eluznn  12971  nninf  12982  fzssnn  13627  fseq1p1m1  13657  prednn  13710  elfzo1  13772  ltwenn  14030  nnnfi  14034  ser1const  14126  expp1  14136  digit1  14305  facnn  14343  fac0  14344  facp1  14346  faclbnd4lem1  14361  bcm1k  14383  bcval5  14386  bcpasc  14389  fz1isolem  14530  seqcoll  14533  seqcoll2  14534  climuni  15643  isercolllem2  15757  isercoll  15759  sumeq2ii  15784  summolem3  15804  summolem2a  15805  fsum  15810  sum0  15811  sumz  15812  fsumcl2lem  15821  fsumadd  15830  fsummulc2  15874  fsumrelem  15898  isumnn0nn  15935  climcndslem1  15942  climcndslem2  15943  climcnds  15944  divcnv  15946  divcnvshft  15948  supcvg  15949  trireciplem  15955  trirecip  15956  expcnv  15957  geo2lim  15968  geoisum1  15972  geoisum1c  15973  mertenslem2  15978  prodeq2ii  16004  prodmolem3  16026  prodmolem2a  16027  fprod  16034  prod0  16036  prod1  16037  fprodss  16041  fprodser  16042  fprodcl2lem  16043  fprodmul  16053  fproddiv  16054  fprodn0  16072  fallfacval4  16135  bpoly4  16151  ege2le3  16182  rpnnen2lem3  16310  rpnnen2lem5  16312  rpnnen2lem8  16315  rpnnen2lem12  16319  ruclem6  16329  pwp1fsum  16487  bezoutlem2  16636  bezoutlem3  16637  lcmcllem  16692  lcmledvds  16695  lcmfval  16717  lcmfcllem  16721  lcmfledvds  16728  isprm3  16779  phicl2  16865  phibndlem  16867  eulerthlem2  16879  odzcllem  16890  odzdvds  16893  iserodd  16933  pcmptcl  16989  pcmpt  16990  pockthlem  17003  pockthg  17004  unbenlem  17006  prmreclem3  17016  prmreclem5  17018  prmreclem6  17019  prmrec  17020  1arith  17025  4sqlem13  17055  4sqlem14  17056  4sqlem17  17059  4sqlem18  17060  vdwlem1  17079  vdwlem2  17080  vdwlem3  17081  vdwlem6  17084  vdwlem8  17086  vdwlem10  17088  vdw  17092  vdwnnlem3  17095  prmlem1a  17204  chnub  18716  mulgnnp1  19211  mulgnnsubcl  19215  mulgnn0z  19230  mulgnndir  19232  mulgpropd  19245  odfval  19665  odlem1  19668  odlem2  19672  gexlem1  19712  gexlem2  19715  gexcl3  19720  sylow1lem1  19731  efgsdmi  19865  efgsrel  19867  efgs1b  19869  efgsp1  19870  mulgnn0di  19958  lt6abl  20028  gsumval3eu  20037  gsumval3  20040  gsumzcl2  20043  gsumzaddlem  20054  gsumconst  20067  gsumzmhm  20070  gsumzoppg  20077  zringlpirlem2  21682  zringlpirlem3  21683  lmcnp  23535  lmmo  23611  1stcelcls  23693  1stccnp  23694  1stckgenlem  23785  1stckgen  23786  imasdsf1olem  24605  cphipval  25477  lmnn  25497  cmetcaulem  25522  iscmet2  25528  causs  25532  nglmle  25536  caubl  25542  iscmet3i  25546  bcthlem5  25562  ovolsf  25706  ovollb2lem  25722  ovolctb  25724  ovolunlem1a  25730  ovolunlem1  25731  ovoliunlem1  25736  ovoliun  25739  ovoliun2  25740  ovoliunnul  25741  ovolscalem1  25747  ovolicc1  25750  ovolicc2lem2  25752  ovolicc2lem3  25753  ovolicc2lem4  25754  iundisj  25782  iundisj2  25783  voliunlem1  25784  voliunlem2  25785  voliunlem3  25786  volsup  25790  ioombl1lem4  25795  uniioovol  25813  uniioombllem2  25817  uniioombllem3  25819  uniioombllem4  25820  uniioombllem6  25822  vitalilem4  25845  vitalilem5  25846  itg1climres  25948  mbfi1fseqlem6  25954  mbfi1flimlem  25956  mbfmullem2  25958  itg2monolem1  25984  itg2i1fseqle  25988  itg2i1fseq  25989  itg2i1fseq2  25990  itg2addlem  25992  plyeq0lem  26443  vieta1lem2  26550  elqaalem1  26558  elqaalem3  26560  aaliou3lem4  26589  aaliou3lem7  26592  dvtaylp  26613  taylthlem2  26617  pserdvlem2  26671  pserdv2  26673  abelthlem6  26679  abelthlem9  26683  logtayl  26905  logtaylsum  26906  logtayl2  26907  atantayl  27182  leibpilem2  27186  leibpi  27187  birthdaylem2  27197  dfef2  27215  divsqrtsumlem  27224  emcllem2  27241  emcllem4  27243  emcllem5  27244  emcllem6  27245  emcllem7  27246  harmonicbnd4  27255  fsumharmonic  27256  zetacvg  27259  lgamgulmlem4  27276  lgamgulmlem6  27278  lgamgulm2  27280  lgamcvglem  27284  lgamcvg2  27299  gamcvg  27300  gamcvg2lem  27303  regamcl  27305  relgamcl  27306  lgam1  27308  wilthlem3  27314  ftalem2  27318  ftalem4  27320  ftalem5  27321  basellem5  27329  basellem6  27330  basellem7  27331  basellem8  27332  basellem9  27333  ppiprm  27395  ppinprm  27396  chtprm  27397  chtnprm  27398  chpp1  27399  vma1  27410  ppiltx  27421  fsumvma2  27458  chpchtsum  27463  logfacbnd3  27467  logexprlim  27469  bposlem5  27532  lgscllem  27548  lgsval2lem  27551  lgsval4a  27563  lgsneg  27565  lgsdir  27576  lgsdilem2  27577  lgsdi  27578  lgsne0  27579  gausslemma2dlem3  27612  lgsquadlem2  27625  chebbnd1lem1  27713  chtppilimlem1  27717  rplogsumlem1  27728  rplogsumlem2  27729  rpvmasumlem  27731  dchrisumlema  27732  dchrisumlem2  27734  dchrisumlem3  27735  dchrmusum2  27738  dchrvmasum2lem  27740  dchrvmasumiflem1  27745  dchrvmaeq0  27748  dchrisum0flblem2  27753  dchrisum0flb  27754  dchrisum0re  27757  dchrisum0lem1b  27759  dchrisum0lem1  27760  dchrisum0lem2a  27761  dchrisum0lem2  27762  dchrisum0lem3  27763  mudivsum  27774  mulogsum  27776  logdivsum  27777  mulog2sumlem2  27779  log2sumbnd  27788  selberg2lem  27794  logdivbnd  27800  pntrsumo1  27809  pntrsumbnd2  27811  pntrlog2bndlem2  27822  pntrlog2bndlem4  27824  pntrlog2bndlem6a  27826  pntlemf  27849  eedimeq  29363  axlowdimlem6  29412  axlowdimlem16  29422  axlowdimlem17  29423  ipval2  31196  minvecolem3  31365  minvecolem4b  31367  minvecolem4  31369  h2hcau  31468  h2hlm  31469  hlimadd  31682  hlim0  31724  hhsscms  31767  occllem  31792  nlelchi  32550  opsqrlem4  32632  hmopidmchi  32640  iundisjf  33070  iundisj2f  33071  ssnnssfz  33266  iundisjfi  33275  iundisj2fi  33276  cycpmco2lem7  33580  cycpmrn  33591  1smat1  34322  submat1n  34323  submatres  34324  submateqlem2  34326  lmatfval  34332  madjusmdetlem1  34345  madjusmdetlem2  34346  madjusmdetlem3  34347  madjusmdetlem4  34348  lmlim  34465  rge0scvg  34467  lmxrge0  34470  lmdvg  34471  esumfzf  34587  esumfsup  34588  esumpcvgval  34596  esumpmono  34597  esumcvg  34604  esumcvgsum  34606  esumsup  34607  fiunelros  34693  eulerpartlemsv2  34877  eulerpartlems  34879  eulerpartlemsv3  34880  eulerpartlemv  34883  eulerpartlemb  34887  fiblem  34917  fibp1  34920  rrvsum  34973  dstfrvclim1  34997  ballotlem1ri  35054  signsvfn  35098  chtvalz  35145  circlemethhgt  35159  subfacp1lem1  35766  subfacp1lem5  35771  subfacp1lem6  35772  erdszelem7  35784  cvmliftlem5  35876  cvmliftlem7  35878  cvmliftlem10  35881  cvmliftlem13  35883  sinccvg  36260  circum  36261  divcnvlin  36320  iprodgam  36329  faclimlem1  36330  faclimlem2  36331  faclim  36333  iprodfac  36334  faclim2  36335  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem12  38389  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem27  38404  poimirlem28  38405  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  mblfinlem2  38415  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  lmclim2  38516  geomcau  38517  heibor1lem  38567  heibor1  38568  bfplem1  38580  bfplem2  38581  rrncmslem  38590  rrncms  38591  aks4d1p1p1  42937  sticksstones10  43029  sticksstones12a  43031  fz1sump1  43193  sumcubes  43196  nna4b4nsq  43514  eldioph3b  43618  diophin  43625  diophun  43626  diophren  43662  jm3.1lem2  43867  dgraalem  43994  dgraaub  43997  dftrcl3  44568  trclfvdecomr  44576  hashnzfz2  45153  hashnzfzclim  45154  dvradcnv2  45179  binomcxplemnotnn0  45188  nnsplit  46196  rexanuz2nf  46328  clim1fr1  46439  sumnnodd  46468  limsup10exlem  46608  fprodsubrecnncnvlem  46743  fprodaddrecnncnvlem  46745  stoweidlem7  46843  stoweidlem14  46850  stoweidlem20  46856  stoweidlem34  46870  wallispilem5  46905  wallispi  46906  stirlinglem1  46910  stirlinglem5  46914  stirlinglem7  46916  stirlinglem8  46917  stirlinglem10  46919  stirlinglem11  46920  stirlinglem12  46921  stirlinglem13  46922  stirlinglem14  46923  stirlinglem15  46924  stirlingr  46926  dirkertrigeqlem2  46935  dirkertrigeqlem3  46936  fourierdlem11  46954  fourierdlem31  46974  fourierdlem48  46990  fourierdlem49  46991  fourierdlem69  47011  fourierdlem73  47015  fourierdlem81  47023  fourierdlem93  47035  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  fouriersw  47067  sge0ad2en  47267  voliunsge0lem  47308  caragenunicl  47360  caratheodorylem2  47363  hoidmvlelem3  47433  ovolval2lem  47479  ovolval2  47480  vonioolem2  47517  vonicclem2  47520  fmtno4prmfac  48483  veroquadgsumlem  50824