Theorem nnuz 12777

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3396   class class class wbr 5093  ‘cfv 6486  1c1 11014   ≤ cle 11154  ℕcn 12132  ℤcz 12475  ℤ_≥cuz 12738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-nn 12133  df-z 12476  df-uz 12739

This theorem is referenced by:  elnnuz  12778  eluz2nn  12788  uznnssnn  12795  nnwo  12813  eluznn  12818  nninf  12829  fzssnn  13470  fseq1p1m1  13500  prednn  13553  elfzo1  13614  ltwenn  13871  nnnfi  13875  ser1const  13967  expp1  13977  digit1  14146  facnn  14184  fac0  14185  facp1  14187  faclbnd4lem1  14202  bcm1k  14224  bcval5  14227  bcpasc  14230  fz1isolem  14370  seqcoll  14373  seqcoll2  14374  climuni  15461  isercolllem2  15575  isercoll  15577  sumeq2ii  15602  summolem3  15623  summolem2a  15624  fsum  15629  sum0  15630  sumz  15631  fsumcl2lem  15640  fsumadd  15649  fsummulc2  15693  fsumrelem  15716  isumnn0nn  15751  climcndslem1  15758  climcndslem2  15759  climcnds  15760  divcnv  15762  divcnvshft  15764  supcvg  15765  trireciplem  15771  trirecip  15772  expcnv  15773  geo2lim  15784  geoisum1  15788  geoisum1c  15789  mertenslem2  15794  prodeq2ii  15820  prodmolem3  15842  prodmolem2a  15843  fprod  15850  prod0  15852  prod1  15853  fprodss  15857  fprodser  15858  fprodcl2lem  15859  fprodmul  15869  fproddiv  15870  fprodn0  15888  fallfacval4  15952  bpoly4  15968  ege2le3  15999  rpnnen2lem3  16127  rpnnen2lem5  16129  rpnnen2lem8  16132  rpnnen2lem12  16136  ruclem6  16146  pwp1fsum  16304  bezoutlem2  16453  bezoutlem3  16454  lcmcllem  16509  lcmledvds  16512  lcmfval  16534  lcmfcllem  16538  lcmfledvds  16545  isprm3  16596  phicl2  16681  phibndlem  16683  eulerthlem2  16695  odzcllem  16706  odzdvds  16709  iserodd  16749  pcmptcl  16805  pcmpt  16806  pockthlem  16819  pockthg  16820  unbenlem  16822  prmreclem3  16832  prmreclem5  16834  prmreclem6  16835  prmrec  16836  1arith  16841  4sqlem13  16871  4sqlem14  16872  4sqlem17  16875  4sqlem18  16876  vdwlem1  16895  vdwlem2  16896  vdwlem3  16897  vdwlem6  16900  vdwlem8  16902  vdwlem10  16904  vdw  16908  vdwnnlem3  16911  prmlem1a  17020  chnub  18530  mulgnnp1  18997  mulgnnsubcl  19001  mulgnn0z  19016  mulgnndir  19018  mulgpropd  19031  odfval  19446  odlem1  19449  odlem2  19453  gexlem1  19493  gexlem2  19496  gexcl3  19501  sylow1lem1  19512  efgsdmi  19646  efgsrel  19648  efgs1b  19650  efgsp1  19651  mulgnn0di  19739  lt6abl  19809  gsumval3eu  19818  gsumval3  19821  gsumzcl2  19824  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  zringlpirlem2  21402  zringlpirlem3  21403  lmcnp  23220  lmmo  23296  1stcelcls  23377  1stccnp  23378  1stckgenlem  23469  1stckgen  23470  imasdsf1olem  24289  cphipval  25171  lmnn  25191  cmetcaulem  25216  iscmet2  25222  causs  25226  nglmle  25230  caubl  25236  iscmet3i  25240  bcthlem5  25256  ovolsf  25401  ovollb2lem  25417  ovolctb  25419  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliun  25434  ovoliun2  25435  ovoliunnul  25436  ovolscalem1  25442  ovolicc1  25445  ovolicc2lem2  25447  ovolicc2lem3  25448  ovolicc2lem4  25449  iundisj  25477  iundisj2  25478  voliunlem1  25479  voliunlem2  25480  voliunlem3  25481  volsup  25485  ioombl1lem4  25490  uniioovol  25508  uniioombllem2  25512  uniioombllem3  25514  uniioombllem4  25515  uniioombllem6  25517  vitalilem4  25540  vitalilem5  25541  itg1climres  25643  mbfi1fseqlem6  25649  mbfi1flimlem  25651  mbfmullem2  25653  itg2monolem1  25679  itg2i1fseqle  25683  itg2i1fseq  25684  itg2i1fseq2  25685  itg2addlem  25687  plyeq0lem  26143  vieta1lem2  26247  elqaalem1  26255  elqaalem3  26257  aaliou3lem4  26282  aaliou3lem7  26285  dvtaylp  26306  taylthlem2  26310  taylthlem2OLD  26311  pserdvlem2  26366  pserdv2  26368  abelthlem6  26374  abelthlem9  26378  logtayl  26597  logtaylsum  26598  logtayl2  26599  atantayl  26875  leibpilem2  26879  leibpi  26880  birthdaylem2  26890  dfef2  26909  divsqrtsumlem  26918  emcllem2  26935  emcllem4  26937  emcllem5  26938  emcllem6  26939  emcllem7  26940  harmonicbnd4  26949  fsumharmonic  26950  zetacvg  26953  lgamgulmlem4  26970  lgamgulmlem6  26972  lgamgulm2  26974  lgamcvglem  26978  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  regamcl  26999  relgamcl  27000  lgam1  27002  wilthlem3  27008  ftalem2  27012  ftalem4  27014  ftalem5  27015  basellem5  27023  basellem6  27024  basellem7  27025  basellem8  27026  basellem9  27027  ppiprm  27089  ppinprm  27090  chtprm  27091  chtnprm  27092  chpp1  27093  vma1  27104  ppiltx  27115  fsumvma2  27153  chpchtsum  27158  logfacbnd3  27162  logexprlim  27164  bposlem5  27227  lgscllem  27243  lgsval2lem  27246  lgsval4a  27258  lgsneg  27260  lgsdir  27271  lgsdilem2  27272  lgsdi  27273  lgsne0  27274  gausslemma2dlem3  27307  lgsquadlem2  27320  chebbnd1lem1  27408  chtppilimlem1  27412  rplogsumlem1  27423  rplogsumlem2  27424  rpvmasumlem  27426  dchrisumlema  27427  dchrisumlem2  27429  dchrisumlem3  27430  dchrmusum2  27433  dchrvmasum2lem  27435  dchrvmasumiflem1  27440  dchrvmaeq0  27443  dchrisum0flblem2  27448  dchrisum0flb  27449  dchrisum0re  27452  dchrisum0lem1b  27454  dchrisum0lem1  27455  dchrisum0lem2a  27456  dchrisum0lem2  27457  dchrisum0lem3  27458  mudivsum  27469  mulogsum  27471  logdivsum  27472  mulog2sumlem2  27474  log2sumbnd  27483  selberg2lem  27489  logdivbnd  27495  pntrsumo1  27504  pntrsumbnd2  27506  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  pntrlog2bndlem6a  27521  pntlemf  27544  eedimeq  28878  axlowdimlem6  28927  axlowdimlem16  28937  axlowdimlem17  28938  ipval2  30689  minvecolem3  30858  minvecolem4b  30860  minvecolem4  30862  h2hcau  30961  h2hlm  30962  hlimadd  31175  hlim0  31217  hhsscms  31260  occllem  31285  nlelchi  32043  opsqrlem4  32125  hmopidmchi  32133  iundisjf  32571  iundisj2f  32572  ssnnssfz  32774  iundisjfi  32783  iundisj2fi  32784  cycpmco2lem7  33108  cycpmrn  33119  1smat1  33838  submat1n  33839  submatres  33840  submateqlem2  33842  lmatfval  33848  madjusmdetlem1  33861  madjusmdetlem2  33862  madjusmdetlem3  33863  madjusmdetlem4  33864  lmlim  33981  rge0scvg  33983  lmxrge0  33986  lmdvg  33987  esumfzf  34103  esumfsup  34104  esumpcvgval  34112  esumpmono  34113  esumcvg  34120  esumcvgsum  34122  esumsup  34123  fiunelros  34208  eulerpartlemsv2  34392  eulerpartlems  34394  eulerpartlemsv3  34395  eulerpartlemv  34398  eulerpartlemb  34402  fiblem  34432  fibp1  34435  rrvsum  34488  dstfrvclim1  34512  ballotlem1ri  34569  signsvfn  34616  chtvalz  34663  circlemethhgt  34677  subfacp1lem1  35244  subfacp1lem5  35249  subfacp1lem6  35250  erdszelem7  35262  cvmliftlem5  35354  cvmliftlem7  35356  cvmliftlem10  35359  cvmliftlem13  35361  sinccvg  35738  circum  35739  divcnvlin  35798  iprodgam  35807  faclimlem1  35808  faclimlem2  35809  faclim  35811  iprodfac  35812  faclim2  35813  poimirlem3  37684  poimirlem4  37685  poimirlem6  37687  poimirlem7  37688  poimirlem8  37689  poimirlem12  37693  poimirlem15  37696  poimirlem16  37697  poimirlem17  37698  poimirlem18  37699  poimirlem19  37700  poimirlem20  37701  poimirlem22  37703  poimirlem23  37704  poimirlem24  37705  poimirlem25  37706  poimirlem27  37708  poimirlem28  37709  poimirlem29  37710  poimirlem30  37711  poimirlem31  37712  mblfinlem2  37719  ovoliunnfl  37723  voliunnfl  37725  volsupnfl  37726  lmclim2  37819  geomcau  37820  heibor1lem  37870  heibor1  37871  bfplem1  37883  bfplem2  37884  rrncmslem  37893  rrncms  37894  aks4d1p1p1  42177  sticksstones10  42269  sticksstones12a  42271  fz1sump1  42429  sumcubes  42432  nna4b4nsq  42779  eldioph3b  42883  diophin  42890  diophun  42891  diophren  42931  jm3.1lem2  43136  dgraalem  43263  dgraaub  43266  dftrcl3  43838  trclfvdecomr  43846  hashnzfz2  44439  hashnzfzclim  44440  dvradcnv2  44465  binomcxplemnotnn0  44474  nnsplit  45482  rexanuz2nf  45615  clim1fr1  45726  sumnnodd  45755  limsup10exlem  45895  fprodsubrecnncnvlem  46030  fprodaddrecnncnvlem  46032  stoweidlem7  46130  stoweidlem14  46137  stoweidlem20  46143  stoweidlem34  46157  wallispilem5  46192  wallispi  46193  stirlinglem1  46197  stirlinglem5  46201  stirlinglem7  46203  stirlinglem8  46204  stirlinglem10  46206  stirlinglem11  46207  stirlinglem12  46208  stirlinglem13  46209  stirlinglem14  46210  stirlinglem15  46211  stirlingr  46213  dirkertrigeqlem2  46222  dirkertrigeqlem3  46223  fourierdlem11  46241  fourierdlem31  46261  fourierdlem48  46277  fourierdlem49  46278  fourierdlem69  46298  fourierdlem73  46302  fourierdlem81  46310  fourierdlem93  46322  fourierdlem103  46332  fourierdlem104  46333  fourierdlem112  46341  fouriersw  46354  sge0ad2en  46554  voliunsge0lem  46595  caragenunicl  46647  caratheodorylem2  46650  hoidmvlelem3  46720  ovolval2lem  46766  ovolval2  46767  vonioolem2  46804  vonicclem2  46807  nthrucw  47009  fmtno4prmfac  47697