Theorem nnuz 12790

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3399   class class class wbr 5098  ‘cfv 6492  1c1 11027   ≤ cle 11167  ℕcn 12145  ℤcz 12488  ℤ_≥cuz 12751

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-z 12489  df-uz 12752

This theorem is referenced by:  elnnuz  12791  eluz2nn  12801  uznnssnn  12808  nnwo  12826  eluznn  12831  nninf  12842  fzssnn  13484  fseq1p1m1  13514  prednn  13567  elfzo1  13628  ltwenn  13885  nnnfi  13889  ser1const  13981  expp1  13991  digit1  14160  facnn  14198  fac0  14199  facp1  14201  faclbnd4lem1  14216  bcm1k  14238  bcval5  14241  bcpasc  14244  fz1isolem  14384  seqcoll  14387  seqcoll2  14388  climuni  15475  isercolllem2  15589  isercoll  15591  sumeq2ii  15616  summolem3  15637  summolem2a  15638  fsum  15643  sum0  15644  sumz  15645  fsumcl2lem  15654  fsumadd  15663  fsummulc2  15707  fsumrelem  15730  isumnn0nn  15765  climcndslem1  15772  climcndslem2  15773  climcnds  15774  divcnv  15776  divcnvshft  15778  supcvg  15779  trireciplem  15785  trirecip  15786  expcnv  15787  geo2lim  15798  geoisum1  15802  geoisum1c  15803  mertenslem2  15808  prodeq2ii  15834  prodmolem3  15856  prodmolem2a  15857  fprod  15864  prod0  15866  prod1  15867  fprodss  15871  fprodser  15872  fprodcl2lem  15873  fprodmul  15883  fproddiv  15884  fprodn0  15902  fallfacval4  15966  bpoly4  15982  ege2le3  16013  rpnnen2lem3  16141  rpnnen2lem5  16143  rpnnen2lem8  16146  rpnnen2lem12  16150  ruclem6  16160  pwp1fsum  16318  bezoutlem2  16467  bezoutlem3  16468  lcmcllem  16523  lcmledvds  16526  lcmfval  16548  lcmfcllem  16552  lcmfledvds  16559  isprm3  16610  phicl2  16695  phibndlem  16697  eulerthlem2  16709  odzcllem  16720  odzdvds  16723  iserodd  16763  pcmptcl  16819  pcmpt  16820  pockthlem  16833  pockthg  16834  unbenlem  16836  prmreclem3  16846  prmreclem5  16848  prmreclem6  16849  prmrec  16850  1arith  16855  4sqlem13  16885  4sqlem14  16886  4sqlem17  16889  4sqlem18  16890  vdwlem1  16909  vdwlem2  16910  vdwlem3  16911  vdwlem6  16914  vdwlem8  16916  vdwlem10  16918  vdw  16922  vdwnnlem3  16925  prmlem1a  17034  chnub  18545  mulgnnp1  19012  mulgnnsubcl  19016  mulgnn0z  19031  mulgnndir  19033  mulgpropd  19046  odfval  19461  odlem1  19464  odlem2  19468  gexlem1  19508  gexlem2  19511  gexcl3  19516  sylow1lem1  19527  efgsdmi  19661  efgsrel  19663  efgs1b  19665  efgsp1  19666  mulgnn0di  19754  lt6abl  19824  gsumval3eu  19833  gsumval3  19836  gsumzcl2  19839  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsumzoppg  19873  zringlpirlem2  21418  zringlpirlem3  21419  lmcnp  23248  lmmo  23324  1stcelcls  23405  1stccnp  23406  1stckgenlem  23497  1stckgen  23498  imasdsf1olem  24317  cphipval  25199  lmnn  25219  cmetcaulem  25244  iscmet2  25250  causs  25254  nglmle  25258  caubl  25264  iscmet3i  25268  bcthlem5  25284  ovolsf  25429  ovollb2lem  25445  ovolctb  25447  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliun  25462  ovoliun2  25463  ovoliunnul  25464  ovolscalem1  25470  ovolicc1  25473  ovolicc2lem2  25475  ovolicc2lem3  25476  ovolicc2lem4  25477  iundisj  25505  iundisj2  25506  voliunlem1  25507  voliunlem2  25508  voliunlem3  25509  volsup  25513  ioombl1lem4  25518  uniioovol  25536  uniioombllem2  25540  uniioombllem3  25542  uniioombllem4  25543  uniioombllem6  25545  vitalilem4  25568  vitalilem5  25569  itg1climres  25671  mbfi1fseqlem6  25677  mbfi1flimlem  25679  mbfmullem2  25681  itg2monolem1  25707  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  plyeq0lem  26171  vieta1lem2  26275  elqaalem1  26283  elqaalem3  26285  aaliou3lem4  26310  aaliou3lem7  26313  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  pserdvlem2  26394  pserdv2  26396  abelthlem6  26402  abelthlem9  26406  logtayl  26625  logtaylsum  26626  logtayl2  26627  atantayl  26903  leibpilem2  26907  leibpi  26908  birthdaylem2  26918  dfef2  26937  divsqrtsumlem  26946  emcllem2  26963  emcllem4  26965  emcllem5  26966  emcllem6  26967  emcllem7  26968  harmonicbnd4  26977  fsumharmonic  26978  zetacvg  26981  lgamgulmlem4  26998  lgamgulmlem6  27000  lgamgulm2  27002  lgamcvglem  27006  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  regamcl  27027  relgamcl  27028  lgam1  27030  wilthlem3  27036  ftalem2  27040  ftalem4  27042  ftalem5  27043  basellem5  27051  basellem6  27052  basellem7  27053  basellem8  27054  basellem9  27055  ppiprm  27117  ppinprm  27118  chtprm  27119  chtnprm  27120  chpp1  27121  vma1  27132  ppiltx  27143  fsumvma2  27181  chpchtsum  27186  logfacbnd3  27190  logexprlim  27192  bposlem5  27255  lgscllem  27271  lgsval2lem  27274  lgsval4a  27286  lgsneg  27288  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  gausslemma2dlem3  27335  lgsquadlem2  27348  chebbnd1lem1  27436  chtppilimlem1  27440  rplogsumlem1  27451  rplogsumlem2  27452  rpvmasumlem  27454  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasum2lem  27463  dchrvmasumiflem1  27468  dchrvmaeq0  27471  dchrisum0flblem2  27476  dchrisum0flb  27477  dchrisum0re  27480  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  mudivsum  27497  mulogsum  27499  logdivsum  27500  mulog2sumlem2  27502  log2sumbnd  27511  selberg2lem  27517  logdivbnd  27523  pntrsumo1  27532  pntrsumbnd2  27534  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntrlog2bndlem6a  27549  pntlemf  27572  eedimeq  28971  axlowdimlem6  29020  axlowdimlem16  29030  axlowdimlem17  29031  ipval2  30782  minvecolem3  30951  minvecolem4b  30953  minvecolem4  30955  h2hcau  31054  h2hlm  31055  hlimadd  31268  hlim0  31310  hhsscms  31353  occllem  31378  nlelchi  32136  opsqrlem4  32218  hmopidmchi  32226  iundisjf  32664  iundisj2f  32665  ssnnssfz  32867  iundisjfi  32876  iundisj2fi  32877  cycpmco2lem7  33214  cycpmrn  33225  1smat1  33961  submat1n  33962  submatres  33963  submateqlem2  33965  lmatfval  33971  madjusmdetlem1  33984  madjusmdetlem2  33985  madjusmdetlem3  33986  madjusmdetlem4  33987  lmlim  34104  rge0scvg  34106  lmxrge0  34109  lmdvg  34110  esumfzf  34226  esumfsup  34227  esumpcvgval  34235  esumpmono  34236  esumcvg  34243  esumcvgsum  34245  esumsup  34246  fiunelros  34331  eulerpartlemsv2  34515  eulerpartlems  34517  eulerpartlemsv3  34518  eulerpartlemv  34521  eulerpartlemb  34525  fiblem  34555  fibp1  34558  rrvsum  34611  dstfrvclim1  34635  ballotlem1ri  34692  signsvfn  34739  chtvalz  34786  circlemethhgt  34800  subfacp1lem1  35373  subfacp1lem5  35378  subfacp1lem6  35379  erdszelem7  35391  cvmliftlem5  35483  cvmliftlem7  35485  cvmliftlem10  35488  cvmliftlem13  35490  sinccvg  35867  circum  35868  divcnvlin  35927  iprodgam  35936  faclimlem1  35937  faclimlem2  35938  faclim  35940  iprodfac  35941  faclim2  35942  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem27  37848  poimirlem28  37849  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  mblfinlem2  37859  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  lmclim2  37959  geomcau  37960  heibor1lem  38010  heibor1  38011  bfplem1  38023  bfplem2  38024  rrncmslem  38033  rrncms  38034  aks4d1p1p1  42317  sticksstones10  42409  sticksstones12a  42411  fz1sump1  42565  sumcubes  42568  nna4b4nsq  42903  eldioph3b  43007  diophin  43014  diophun  43015  diophren  43055  jm3.1lem2  43260  dgraalem  43387  dgraaub  43390  dftrcl3  43961  trclfvdecomr  43969  hashnzfz2  44562  hashnzfzclim  44563  dvradcnv2  44588  binomcxplemnotnn0  44597  nnsplit  45603  rexanuz2nf  45736  clim1fr1  45847  sumnnodd  45876  limsup10exlem  46016  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  stoweidlem7  46251  stoweidlem14  46258  stoweidlem20  46264  stoweidlem34  46278  wallispilem5  46313  wallispi  46314  stirlinglem1  46318  stirlinglem5  46322  stirlinglem7  46324  stirlinglem8  46325  stirlinglem10  46327  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  stirlingr  46334  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  fourierdlem11  46362  fourierdlem31  46382  fourierdlem48  46398  fourierdlem49  46399  fourierdlem69  46419  fourierdlem73  46423  fourierdlem81  46431  fourierdlem93  46443  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fouriersw  46475  sge0ad2en  46675  voliunsge0lem  46716  caragenunicl  46768  caratheodorylem2  46771  hoidmvlelem3  46841  ovolval2lem  46887  ovolval2  46888  vonioolem2  46925  vonicclem2  46928  nthrucw  47130  fmtno4prmfac  47818