Theorem nnuz 12796

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 12521	. 2 ⊢ ℕ = {𝑘 ∈ ℤ ∣ 1 ≤ 𝑘}
2		1z 12523	. . 3 ⊢ 1 ∈ ℤ
3		uzval 12755	. . 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 3396   class class class wbr 5095  ‘cfv 6486  1c1 11029   ≤ cle 11169  ℕcn 12146  ℤcz 12489  ℤ_≥cuz 12753

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 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

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 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  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 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11367  df-neg 11368  df-nn 12147  df-z 12490  df-uz 12754

This theorem is referenced by:  elnnuz  12797  eluz2nn  12807  uznnssnn  12814  nnwo  12832  eluznn  12837  nninf  12848  fzssnn  13489  fseq1p1m1  13519  prednn  13572  elfzo1  13633  ltwenn  13887  nnnfi  13891  ser1const  13983  expp1  13993  digit1  14162  facnn  14200  fac0  14201  facp1  14203  faclbnd4lem1  14218  bcm1k  14240  bcval5  14243  bcpasc  14246  fz1isolem  14386  seqcoll  14389  seqcoll2  14390  climuni  15477  isercolllem2  15591  isercoll  15593  sumeq2ii  15618  summolem3  15639  summolem2a  15640  fsum  15645  sum0  15646  sumz  15647  fsumcl2lem  15656  fsumadd  15665  fsummulc2  15709  fsumrelem  15732  isumnn0nn  15767  climcndslem1  15774  climcndslem2  15775  climcnds  15776  divcnv  15778  divcnvshft  15780  supcvg  15781  trireciplem  15787  trirecip  15788  expcnv  15789  geo2lim  15800  geoisum1  15804  geoisum1c  15805  mertenslem2  15810  prodeq2ii  15836  prodmolem3  15858  prodmolem2a  15859  fprod  15866  prod0  15868  prod1  15869  fprodss  15873  fprodser  15874  fprodcl2lem  15875  fprodmul  15885  fproddiv  15886  fprodn0  15904  fallfacval4  15968  bpoly4  15984  ege2le3  16015  rpnnen2lem3  16143  rpnnen2lem5  16145  rpnnen2lem8  16148  rpnnen2lem12  16152  ruclem6  16162  pwp1fsum  16320  bezoutlem2  16469  bezoutlem3  16470  lcmcllem  16525  lcmledvds  16528  lcmfval  16550  lcmfcllem  16554  lcmfledvds  16561  isprm3  16612  phicl2  16697  phibndlem  16699  eulerthlem2  16711  odzcllem  16722  odzdvds  16725  iserodd  16765  pcmptcl  16821  pcmpt  16822  pockthlem  16835  pockthg  16836  unbenlem  16838  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  prmrec  16852  1arith  16857  4sqlem13  16887  4sqlem14  16888  4sqlem17  16891  4sqlem18  16892  vdwlem1  16911  vdwlem2  16912  vdwlem3  16913  vdwlem6  16916  vdwlem8  16918  vdwlem10  16920  vdw  16924  vdwnnlem3  16927  prmlem1a  17036  mulgnnp1  18979  mulgnnsubcl  18983  mulgnn0z  18998  mulgnndir  19000  mulgpropd  19013  odfval  19429  odlem1  19432  odlem2  19436  gexlem1  19476  gexlem2  19479  gexcl3  19484  sylow1lem1  19495  efgsdmi  19629  efgsrel  19631  efgs1b  19633  efgsp1  19634  mulgnn0di  19722  lt6abl  19792  gsumval3eu  19801  gsumval3  19804  gsumzcl2  19807  gsumzaddlem  19818  gsumconst  19831  gsumzmhm  19834  gsumzoppg  19841  zringlpirlem2  21388  zringlpirlem3  21389  lmcnp  23207  lmmo  23283  1stcelcls  23364  1stccnp  23365  1stckgenlem  23456  1stckgen  23457  imasdsf1olem  24277  cphipval  25159  lmnn  25179  cmetcaulem  25204  iscmet2  25210  causs  25214  nglmle  25218  caubl  25224  iscmet3i  25228  bcthlem5  25244  ovolsf  25389  ovollb2lem  25405  ovolctb  25407  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliun  25422  ovoliun2  25423  ovoliunnul  25424  ovolscalem1  25430  ovolicc1  25433  ovolicc2lem2  25435  ovolicc2lem3  25436  ovolicc2lem4  25437  iundisj  25465  iundisj2  25466  voliunlem1  25467  voliunlem2  25468  voliunlem3  25469  volsup  25473  ioombl1lem4  25478  uniioovol  25496  uniioombllem2  25500  uniioombllem3  25502  uniioombllem4  25503  uniioombllem6  25505  vitalilem4  25528  vitalilem5  25529  itg1climres  25631  mbfi1fseqlem6  25637  mbfi1flimlem  25639  mbfmullem2  25641  itg2monolem1  25667  itg2i1fseqle  25671  itg2i1fseq  25672  itg2i1fseq2  25673  itg2addlem  25675  plyeq0lem  26131  vieta1lem2  26235  elqaalem1  26243  elqaalem3  26245  aaliou3lem4  26270  aaliou3lem7  26273  dvtaylp  26294  taylthlem2  26298  taylthlem2OLD  26299  pserdvlem2  26354  pserdv2  26356  abelthlem6  26362  abelthlem9  26366  logtayl  26585  logtaylsum  26586  logtayl2  26587  atantayl  26863  leibpilem2  26867  leibpi  26868  birthdaylem2  26878  dfef2  26897  divsqrtsumlem  26906  emcllem2  26923  emcllem4  26925  emcllem5  26926  emcllem6  26927  emcllem7  26928  harmonicbnd4  26937  fsumharmonic  26938  zetacvg  26941  lgamgulmlem4  26958  lgamgulmlem6  26960  lgamgulm2  26962  lgamcvglem  26966  lgamcvg2  26981  gamcvg  26982  gamcvg2lem  26985  regamcl  26987  relgamcl  26988  lgam1  26990  wilthlem3  26996  ftalem2  27000  ftalem4  27002  ftalem5  27003  basellem5  27011  basellem6  27012  basellem7  27013  basellem8  27014  basellem9  27015  ppiprm  27077  ppinprm  27078  chtprm  27079  chtnprm  27080  chpp1  27081  vma1  27092  ppiltx  27103  fsumvma2  27141  chpchtsum  27146  logfacbnd3  27150  logexprlim  27152  bposlem5  27215  lgscllem  27231  lgsval2lem  27234  lgsval4a  27246  lgsneg  27248  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  gausslemma2dlem3  27295  lgsquadlem2  27308  chebbnd1lem1  27396  chtppilimlem1  27400  rplogsumlem1  27411  rplogsumlem2  27412  rpvmasumlem  27414  dchrisumlema  27415  dchrisumlem2  27417  dchrisumlem3  27418  dchrmusum2  27421  dchrvmasum2lem  27423  dchrvmasumiflem1  27428  dchrvmaeq0  27431  dchrisum0flblem2  27436  dchrisum0flb  27437  dchrisum0re  27440  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  mudivsum  27457  mulogsum  27459  logdivsum  27460  mulog2sumlem2  27462  log2sumbnd  27471  selberg2lem  27477  logdivbnd  27483  pntrsumo1  27492  pntrsumbnd2  27494  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntrlog2bndlem6a  27509  pntlemf  27532  eedimeq  28861  axlowdimlem6  28910  axlowdimlem16  28920  axlowdimlem17  28921  ipval2  30669  minvecolem3  30838  minvecolem4b  30840  minvecolem4  30842  h2hcau  30941  h2hlm  30942  hlimadd  31155  hlim0  31197  hhsscms  31240  occllem  31265  nlelchi  32023  opsqrlem4  32105  hmopidmchi  32113  iundisjf  32551  iundisj2f  32552  ssnnssfz  32743  iundisjfi  32752  iundisj2fi  32753  chnub  32967  cycpmco2lem7  33087  cycpmrn  33098  1smat1  33773  submat1n  33774  submatres  33775  submateqlem2  33777  lmatfval  33783  madjusmdetlem1  33796  madjusmdetlem2  33797  madjusmdetlem3  33798  madjusmdetlem4  33799  lmlim  33916  rge0scvg  33918  lmxrge0  33921  lmdvg  33922  esumfzf  34038  esumfsup  34039  esumpcvgval  34047  esumpmono  34048  esumcvg  34055  esumcvgsum  34057  esumsup  34058  fiunelros  34143  eulerpartlemsv2  34328  eulerpartlems  34330  eulerpartlemsv3  34331  eulerpartlemv  34334  eulerpartlemb  34338  fiblem  34368  fibp1  34371  rrvsum  34424  dstfrvclim1  34448  ballotlem1ri  34505  signsvfn  34552  chtvalz  34599  circlemethhgt  34613  subfacp1lem1  35154  subfacp1lem5  35159  subfacp1lem6  35160  erdszelem7  35172  cvmliftlem5  35264  cvmliftlem7  35266  cvmliftlem10  35269  cvmliftlem13  35271  sinccvg  35648  circum  35649  divcnvlin  35708  iprodgam  35717  faclimlem1  35718  faclimlem2  35719  faclim  35721  iprodfac  35722  faclim2  35723  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem17  37619  poimirlem18  37620  poimirlem19  37621  poimirlem20  37622  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem27  37629  poimirlem28  37630  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  mblfinlem2  37640  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  lmclim2  37740  geomcau  37741  heibor1lem  37791  heibor1  37792  bfplem1  37804  bfplem2  37805  rrncmslem  37814  rrncms  37815  aks4d1p1p1  42039  sticksstones10  42131  sticksstones12a  42133  fz1sump1  42286  sumcubes  42289  nna4b4nsq  42636  eldioph3b  42741  diophin  42748  diophun  42749  diophren  42789  jm3.1lem2  42994  dgraalem  43121  dgraaub  43124  dftrcl3  43696  trclfvdecomr  43704  hashnzfz2  44297  hashnzfzclim  44298  dvradcnv2  44323  binomcxplemnotnn0  44332  nnsplit  45341  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