Theorem nnuz 12778

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3394   class class class wbr 5092  ‘cfv 6482  1c1 11010   ≤ cle 11150  ℕcn 12128  ℤcz 12471  ℤ_≥cuz 12735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  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 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-z 12472  df-uz 12736

This theorem is referenced by:  elnnuz  12779  eluz2nn  12789  uznnssnn  12796  nnwo  12814  eluznn  12819  nninf  12830  fzssnn  13471  fseq1p1m1  13501  prednn  13554  elfzo1  13615  ltwenn  13869  nnnfi  13873  ser1const  13965  expp1  13975  digit1  14144  facnn  14182  fac0  14183  facp1  14185  faclbnd4lem1  14200  bcm1k  14222  bcval5  14225  bcpasc  14228  fz1isolem  14368  seqcoll  14371  seqcoll2  14372  climuni  15459  isercolllem2  15573  isercoll  15575  sumeq2ii  15600  summolem3  15621  summolem2a  15622  fsum  15627  sum0  15628  sumz  15629  fsumcl2lem  15638  fsumadd  15647  fsummulc2  15691  fsumrelem  15714  isumnn0nn  15749  climcndslem1  15756  climcndslem2  15757  climcnds  15758  divcnv  15760  divcnvshft  15762  supcvg  15763  trireciplem  15769  trirecip  15770  expcnv  15771  geo2lim  15782  geoisum1  15786  geoisum1c  15787  mertenslem2  15792  prodeq2ii  15818  prodmolem3  15840  prodmolem2a  15841  fprod  15848  prod0  15850  prod1  15851  fprodss  15855  fprodser  15856  fprodcl2lem  15857  fprodmul  15867  fproddiv  15868  fprodn0  15886  fallfacval4  15950  bpoly4  15966  ege2le3  15997  rpnnen2lem3  16125  rpnnen2lem5  16127  rpnnen2lem8  16130  rpnnen2lem12  16134  ruclem6  16144  pwp1fsum  16302  bezoutlem2  16451  bezoutlem3  16452  lcmcllem  16507  lcmledvds  16510  lcmfval  16532  lcmfcllem  16536  lcmfledvds  16543  isprm3  16594  phicl2  16679  phibndlem  16681  eulerthlem2  16693  odzcllem  16704  odzdvds  16707  iserodd  16747  pcmptcl  16803  pcmpt  16804  pockthlem  16817  pockthg  16818  unbenlem  16820  prmreclem3  16830  prmreclem5  16832  prmreclem6  16833  prmrec  16834  1arith  16839  4sqlem13  16869  4sqlem14  16870  4sqlem17  16873  4sqlem18  16874  vdwlem1  16893  vdwlem2  16894  vdwlem3  16895  vdwlem6  16898  vdwlem8  16900  vdwlem10  16902  vdw  16906  vdwnnlem3  16909  prmlem1a  17018  mulgnnp1  18961  mulgnnsubcl  18965  mulgnn0z  18980  mulgnndir  18982  mulgpropd  18995  odfval  19411  odlem1  19414  odlem2  19418  gexlem1  19458  gexlem2  19461  gexcl3  19466  sylow1lem1  19477  efgsdmi  19611  efgsrel  19613  efgs1b  19615  efgsp1  19616  mulgnn0di  19704  lt6abl  19774  gsumval3eu  19783  gsumval3  19786  gsumzcl2  19789  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  zringlpirlem2  21370  zringlpirlem3  21371  lmcnp  23189  lmmo  23265  1stcelcls  23346  1stccnp  23347  1stckgenlem  23438  1stckgen  23439  imasdsf1olem  24259  cphipval  25141  lmnn  25161  cmetcaulem  25186  iscmet2  25192  causs  25196  nglmle  25200  caubl  25206  iscmet3i  25210  bcthlem5  25226  ovolsf  25371  ovollb2lem  25387  ovolctb  25389  ovolunlem1a  25395  ovolunlem1  25396  ovoliunlem1  25401  ovoliun  25404  ovoliun2  25405  ovoliunnul  25406  ovolscalem1  25412  ovolicc1  25415  ovolicc2lem2  25417  ovolicc2lem3  25418  ovolicc2lem4  25419  iundisj  25447  iundisj2  25448  voliunlem1  25449  voliunlem2  25450  voliunlem3  25451  volsup  25455  ioombl1lem4  25460  uniioovol  25478  uniioombllem2  25482  uniioombllem3  25484  uniioombllem4  25485  uniioombllem6  25487  vitalilem4  25510  vitalilem5  25511  itg1climres  25613  mbfi1fseqlem6  25619  mbfi1flimlem  25621  mbfmullem2  25623  itg2monolem1  25649  itg2i1fseqle  25653  itg2i1fseq  25654  itg2i1fseq2  25655  itg2addlem  25657  plyeq0lem  26113  vieta1lem2  26217  elqaalem1  26225  elqaalem3  26227  aaliou3lem4  26252  aaliou3lem7  26255  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  pserdvlem2  26336  pserdv2  26338  abelthlem6  26344  abelthlem9  26348  logtayl  26567  logtaylsum  26568  logtayl2  26569  atantayl  26845  leibpilem2  26849  leibpi  26850  birthdaylem2  26860  dfef2  26879  divsqrtsumlem  26888  emcllem2  26905  emcllem4  26907  emcllem5  26908  emcllem6  26909  emcllem7  26910  harmonicbnd4  26919  fsumharmonic  26920  zetacvg  26923  lgamgulmlem4  26940  lgamgulmlem6  26942  lgamgulm2  26944  lgamcvglem  26948  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  regamcl  26969  relgamcl  26970  lgam1  26972  wilthlem3  26978  ftalem2  26982  ftalem4  26984  ftalem5  26985  basellem5  26993  basellem6  26994  basellem7  26995  basellem8  26996  basellem9  26997  ppiprm  27059  ppinprm  27060  chtprm  27061  chtnprm  27062  chpp1  27063  vma1  27074  ppiltx  27085  fsumvma2  27123  chpchtsum  27128  logfacbnd3  27132  logexprlim  27134  bposlem5  27197  lgscllem  27213  lgsval2lem  27216  lgsval4a  27228  lgsneg  27230  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  gausslemma2dlem3  27277  lgsquadlem2  27290  chebbnd1lem1  27378  chtppilimlem1  27382  rplogsumlem1  27393  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  dchrmusum2  27403  dchrvmasum2lem  27405  dchrvmasumiflem1  27410  dchrvmaeq0  27413  dchrisum0flblem2  27418  dchrisum0flb  27419  dchrisum0re  27422  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0lem3  27428  mudivsum  27439  mulogsum  27441  logdivsum  27442  mulog2sumlem2  27444  log2sumbnd  27453  selberg2lem  27459  logdivbnd  27465  pntrsumo1  27474  pntrsumbnd2  27476  pntrlog2bndlem2  27487  pntrlog2bndlem4  27489  pntrlog2bndlem6a  27491  pntlemf  27514  eedimeq  28843  axlowdimlem6  28892  axlowdimlem16  28902  axlowdimlem17  28903  ipval2  30651  minvecolem3  30820  minvecolem4b  30822  minvecolem4  30824  h2hcau  30923  h2hlm  30924  hlimadd  31137  hlim0  31179  hhsscms  31222  occllem  31247  nlelchi  32005  opsqrlem4  32087  hmopidmchi  32095  iundisjf  32533  iundisj2f  32534  ssnnssfz  32730  iundisjfi  32739  iundisj2fi  32740  chnub  32954  cycpmco2lem7  33074  cycpmrn  33085  1smat1  33771  submat1n  33772  submatres  33773  submateqlem2  33775  lmatfval  33781  madjusmdetlem1  33794  madjusmdetlem2  33795  madjusmdetlem3  33796  madjusmdetlem4  33797  lmlim  33914  rge0scvg  33916  lmxrge0  33919  lmdvg  33920  esumfzf  34036  esumfsup  34037  esumpcvgval  34045  esumpmono  34046  esumcvg  34053  esumcvgsum  34055  esumsup  34056  fiunelros  34141  eulerpartlemsv2  34326  eulerpartlems  34328  eulerpartlemsv3  34329  eulerpartlemv  34332  eulerpartlemb  34336  fiblem  34366  fibp1  34369  rrvsum  34422  dstfrvclim1  34446  ballotlem1ri  34503  signsvfn  34550  chtvalz  34597  circlemethhgt  34611  subfacp1lem1  35156  subfacp1lem5  35161  subfacp1lem6  35162  erdszelem7  35174  cvmliftlem5  35266  cvmliftlem7  35268  cvmliftlem10  35271  cvmliftlem13  35273  sinccvg  35650  circum  35651  divcnvlin  35710  iprodgam  35719  faclimlem1  35720  faclimlem2  35721  faclim  35723  iprodfac  35724  faclim2  35725  poimirlem3  37607  poimirlem4  37608  poimirlem6  37610  poimirlem7  37611  poimirlem8  37612  poimirlem12  37616  poimirlem15  37619  poimirlem16  37620  poimirlem17  37621  poimirlem18  37622  poimirlem19  37623  poimirlem20  37624  poimirlem22  37626  poimirlem23  37627  poimirlem24  37628  poimirlem25  37629  poimirlem27  37631  poimirlem28  37632  poimirlem29  37633  poimirlem30  37634  poimirlem31  37635  mblfinlem2  37642  ovoliunnfl  37646  voliunnfl  37648  volsupnfl  37649  lmclim2  37742  geomcau  37743  heibor1lem  37793  heibor1  37794  bfplem1  37806  bfplem2  37807  rrncmslem  37816  rrncms  37817  aks4d1p1p1  42040  sticksstones10  42132  sticksstones12a  42134  fz1sump1  42287  sumcubes  42290  nna4b4nsq  42637  eldioph3b  42742  diophin  42749  diophun  42750  diophren  42790  jm3.1lem2  42995  dgraalem  43122  dgraaub  43125  dftrcl3  43697  trclfvdecomr  43705  hashnzfz2  44298  hashnzfzclim  44299  dvradcnv2  44324  binomcxplemnotnn0  44333  nnsplit  45342  rexanuz2nf  45475  clim1fr1  45586  sumnnodd  45615  limsup10exlem  45757  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  stoweidlem7  45992  stoweidlem14  45999  stoweidlem20  46005  stoweidlem34  46019  wallispilem5  46054  wallispi  46055  stirlinglem1  46059  stirlinglem5  46063  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  stirlinglem11  46069  stirlinglem12  46070  stirlinglem13  46071  stirlinglem14  46072  stirlinglem15  46073  stirlingr  46075  dirkertrigeqlem2  46084  dirkertrigeqlem3  46085  fourierdlem11  46103  fourierdlem31  46123  fourierdlem48  46139  fourierdlem49  46140  fourierdlem69  46160  fourierdlem73  46164  fourierdlem81  46172  fourierdlem93  46184  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  fouriersw  46216  sge0ad2en  46416  voliunsge0lem  46457  caragenunicl  46509  caratheodorylem2  46512  hoidmvlelem3  46582  ovolval2lem  46628  ovolval2  46629  vonioolem2  46666  vonicclem2  46669  fmtno4prmfac  47560