Theorem nnuz 12871

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  {crab 3413   class class class wbr 5097  ‘cfv 6515  1c1 11067   ≤ cle 11210  ℕcn 12203  ℤcz 12561  ℤ_≥cuz 12832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142  ax-pre-mulgt0 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  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 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7841  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-sub 11409  df-neg 11410  df-nn 12204  df-z 12562  df-uz 12833

This theorem is referenced by:  elnnuz  12872  eluz2nn  12882  uznnssnn  12889  nnwo  12907  eluznn  12912  nninf  12923  fzssnn  13566  fseq1p1m1  13596  prednn  13649  elfzo1  13711  ltwenn  13968  nnnfi  13972  ser1const  14064  expp1  14074  digit1  14243  facnn  14281  fac0  14282  facp1  14284  faclbnd4lem1  14299  bcm1k  14321  bcval5  14324  bcpasc  14327  fz1isolem  14467  seqcoll  14470  seqcoll2  14471  climuni  15569  isercolllem2  15683  isercoll  15685  sumeq2ii  15710  summolem3  15731  summolem2a  15732  fsum  15737  sum0  15738  sumz  15739  fsumcl2lem  15748  fsumadd  15757  fsummulc2  15801  fsumrelem  15825  isumnn0nn  15862  climcndslem1  15869  climcndslem2  15870  climcnds  15871  divcnv  15873  divcnvshft  15875  supcvg  15876  trireciplem  15882  trirecip  15883  expcnv  15884  geo2lim  15895  geoisum1  15899  geoisum1c  15900  mertenslem2  15905  prodeq2ii  15931  prodmolem3  15953  prodmolem2a  15954  fprod  15961  prod0  15963  prod1  15964  fprodss  15968  fprodser  15969  fprodcl2lem  15970  fprodmul  15980  fproddiv  15981  fprodn0  15999  fallfacval4  16063  bpoly4  16079  ege2le3  16110  rpnnen2lem3  16238  rpnnen2lem5  16240  rpnnen2lem8  16243  rpnnen2lem12  16247  ruclem6  16257  pwp1fsum  16415  bezoutlem2  16564  bezoutlem3  16565  lcmcllem  16620  lcmledvds  16623  lcmfval  16645  lcmfcllem  16649  lcmfledvds  16656  isprm3  16707  phicl2  16793  phibndlem  16795  eulerthlem2  16807  odzcllem  16818  odzdvds  16821  iserodd  16861  pcmptcl  16917  pcmpt  16918  pockthlem  16931  pockthg  16932  unbenlem  16934  prmreclem3  16944  prmreclem5  16946  prmreclem6  16947  prmrec  16948  1arith  16953  4sqlem13  16983  4sqlem14  16984  4sqlem17  16987  4sqlem18  16988  vdwlem1  17007  vdwlem2  17008  vdwlem3  17009  vdwlem6  17012  vdwlem8  17014  vdwlem10  17016  vdw  17020  vdwnnlem3  17023  prmlem1a  17132  chnub  18644  mulgnnp1  19114  mulgnnsubcl  19118  mulgnn0z  19133  mulgnndir  19135  mulgpropd  19148  odfval  19562  odlem1  19565  odlem2  19569  gexlem1  19609  gexlem2  19612  gexcl3  19617  sylow1lem1  19628  efgsdmi  19762  efgsrel  19764  efgs1b  19766  efgsp1  19767  mulgnn0di  19855  lt6abl  19925  gsumval3eu  19934  gsumval3  19937  gsumzcl2  19940  gsumzaddlem  19951  gsumconst  19964  gsumzmhm  19967  gsumzoppg  19974  zringlpirlem2  21502  zringlpirlem3  21503  lmcnp  23351  lmmo  23427  1stcelcls  23508  1stccnp  23509  1stckgenlem  23600  1stckgen  23601  imasdsf1olem  24420  cphipval  25292  lmnn  25312  cmetcaulem  25337  iscmet2  25343  causs  25347  nglmle  25351  caubl  25357  iscmet3i  25361  bcthlem5  25377  ovolsf  25521  ovollb2lem  25537  ovolctb  25539  ovolunlem1a  25545  ovolunlem1  25546  ovoliunlem1  25551  ovoliun  25554  ovoliun2  25555  ovoliunnul  25556  ovolscalem1  25562  ovolicc1  25565  ovolicc2lem2  25567  ovolicc2lem3  25568  ovolicc2lem4  25569  iundisj  25597  iundisj2  25598  voliunlem1  25599  voliunlem2  25600  voliunlem3  25601  volsup  25605  ioombl1lem4  25610  uniioovol  25628  uniioombllem2  25632  uniioombllem3  25634  uniioombllem4  25635  uniioombllem6  25637  vitalilem4  25660  vitalilem5  25661  itg1climres  25763  mbfi1fseqlem6  25769  mbfi1flimlem  25771  mbfmullem2  25773  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  plyeq0lem  26257  vieta1lem2  26362  elqaalem1  26370  elqaalem3  26372  aaliou3lem4  26397  aaliou3lem7  26400  dvtaylp  26420  taylthlem2  26424  pserdvlem2  26478  pserdv2  26480  abelthlem6  26486  abelthlem9  26490  logtayl  26712  logtaylsum  26713  logtayl2  26714  atantayl  26989  leibpilem2  26993  leibpi  26994  birthdaylem2  27004  dfef2  27022  divsqrtsumlem  27031  emcllem2  27048  emcllem4  27050  emcllem5  27051  emcllem6  27052  emcllem7  27053  harmonicbnd4  27062  fsumharmonic  27063  zetacvg  27066  lgamgulmlem4  27083  lgamgulmlem6  27085  lgamgulm2  27087  lgamcvglem  27091  lgamcvg2  27106  gamcvg  27107  gamcvg2lem  27110  regamcl  27112  relgamcl  27113  lgam1  27115  wilthlem3  27121  ftalem2  27125  ftalem4  27127  ftalem5  27128  basellem5  27136  basellem6  27137  basellem7  27138  basellem8  27139  basellem9  27140  ppiprm  27202  ppinprm  27203  chtprm  27204  chtnprm  27205  chpp1  27206  vma1  27217  ppiltx  27228  fsumvma2  27265  chpchtsum  27270  logfacbnd3  27274  logexprlim  27276  bposlem5  27339  lgscllem  27355  lgsval2lem  27358  lgsval4a  27370  lgsneg  27372  lgsdir  27383  lgsdilem2  27384  lgsdi  27385  lgsne0  27386  gausslemma2dlem3  27419  lgsquadlem2  27432  chebbnd1lem1  27520  chtppilimlem1  27524  rplogsumlem1  27535  rplogsumlem2  27536  rpvmasumlem  27538  dchrisumlema  27539  dchrisumlem2  27541  dchrisumlem3  27542  dchrmusum2  27545  dchrvmasum2lem  27547  dchrvmasumiflem1  27552  dchrvmaeq0  27555  dchrisum0flblem2  27560  dchrisum0flb  27561  dchrisum0re  27564  dchrisum0lem1b  27566  dchrisum0lem1  27567  dchrisum0lem2a  27568  dchrisum0lem2  27569  dchrisum0lem3  27570  mudivsum  27581  mulogsum  27583  logdivsum  27584  mulog2sumlem2  27586  log2sumbnd  27595  selberg2lem  27601  logdivbnd  27607  pntrsumo1  27616  pntrsumbnd2  27618  pntrlog2bndlem2  27629  pntrlog2bndlem4  27631  pntrlog2bndlem6a  27633  pntlemf  27656  eedimeq  29055  axlowdimlem6  29104  axlowdimlem16  29114  axlowdimlem17  29115  ipval2  30866  minvecolem3  31035  minvecolem4b  31037  minvecolem4  31039  h2hcau  31138  h2hlm  31139  hlimadd  31352  hlim0  31394  hhsscms  31437  occllem  31462  nlelchi  32220  opsqrlem4  32302  hmopidmchi  32310  iundisjf  32748  iundisj2f  32749  ssnnssfz  32949  iundisjfi  32958  iundisj2fi  32959  cycpmco2lem7  33272  cycpmrn  33283  1smat1  34061  submat1n  34062  submatres  34063  submateqlem2  34065  lmatfval  34071  madjusmdetlem1  34084  madjusmdetlem2  34085  madjusmdetlem3  34086  madjusmdetlem4  34087  lmlim  34204  rge0scvg  34206  lmxrge0  34209  lmdvg  34210  esumfzf  34326  esumfsup  34327  esumpcvgval  34335  esumpmono  34336  esumcvg  34343  esumcvgsum  34345  esumsup  34346  fiunelros  34431  eulerpartlemsv2  34615  eulerpartlems  34617  eulerpartlemsv3  34618  eulerpartlemv  34621  eulerpartlemb  34625  fiblem  34655  fibp1  34658  rrvsum  34711  dstfrvclim1  34735  ballotlem1ri  34792  signsvfn  34836  chtvalz  34883  circlemethhgt  34897  subfacp1lem1  35489  subfacp1lem5  35494  subfacp1lem6  35495  erdszelem7  35507  cvmliftlem5  35599  cvmliftlem7  35601  cvmliftlem10  35604  cvmliftlem13  35606  sinccvg  35983  circum  35984  divcnvlin  36043  iprodgam  36052  faclimlem1  36053  faclimlem2  36054  faclim  36056  iprodfac  36057  faclim2  36058  poimirlem3  38082  poimirlem4  38083  poimirlem6  38085  poimirlem7  38086  poimirlem8  38087  poimirlem12  38091  poimirlem15  38094  poimirlem16  38095  poimirlem17  38096  poimirlem18  38097  poimirlem19  38098  poimirlem20  38099  poimirlem22  38101  poimirlem23  38102  poimirlem24  38103  poimirlem25  38104  poimirlem27  38106  poimirlem28  38107  poimirlem29  38108  poimirlem30  38109  poimirlem31  38110  mblfinlem2  38117  ovoliunnfl  38121  voliunnfl  38123  volsupnfl  38124  lmclim2  38217  geomcau  38218  heibor1lem  38268  heibor1  38269  bfplem1  38281  bfplem2  38282  rrncmslem  38291  rrncms  38292  aks4d1p1p1  42640  sticksstones10  42732  sticksstones12a  42734  fz1sump1  42879  sumcubes  42882  nna4b4nsq  43202  eldioph3b  43306  diophin  43313  diophun  43314  diophren  43350  jm3.1lem2  43555  dgraalem  43682  dgraaub  43685  dftrcl3  44256  trclfvdecomr  44264  hashnzfz2  44857  hashnzfzclim  44858  dvradcnv2  44883  binomcxplemnotnn0  44892  nnsplit  45894  rexanuz2nf  46026  clim1fr1  46137  sumnnodd  46166  limsup10exlem  46306  fprodsubrecnncnvlem  46441  fprodaddrecnncnvlem  46443  stoweidlem7  46541  stoweidlem14  46548  stoweidlem20  46554  stoweidlem34  46568  wallispilem5  46603  wallispi  46604  stirlinglem1  46608  stirlinglem5  46612  stirlinglem7  46614  stirlinglem8  46615  stirlinglem10  46617  stirlinglem11  46618  stirlinglem12  46619  stirlinglem13  46620  stirlinglem14  46621  stirlinglem15  46622  stirlingr  46624  dirkertrigeqlem2  46633  dirkertrigeqlem3  46634  fourierdlem11  46652  fourierdlem31  46672  fourierdlem48  46688  fourierdlem49  46689  fourierdlem69  46709  fourierdlem73  46713  fourierdlem81  46721  fourierdlem93  46733  fourierdlem103  46743  fourierdlem104  46744  fourierdlem112  46752  fouriersw  46765  sge0ad2en  46965  voliunsge0lem  47006  caragenunicl  47058  caratheodorylem2  47061  hoidmvlelem3  47131  ovolval2lem  47177  ovolval2  47178  vonioolem2  47215  vonicclem2  47218  nthrucw  47422  fmtno4prmfac  48141