Theorem nnuz 11944

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

Syntax hints:   = wceq 1637   ∈ wcel 2157  {crab 3107   class class class wbr 4851  ‘cfv 6104  1c1 10225   ≤ cle 10363  ℕcn 11308  ℤcz 11646  ℤ_≥cuz 11907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-nn 11309  df-z 11647  df-uz 11908

This theorem is referenced by:  elnnuz  11945  eluz2nn  11947  uznnssnn  11956  nnwo  11975  eluznn  11980  nninf  11991  fzssnn  12611  fseq1p1m1  12640  prednn  12689  elfzo1  12745  ltwenn  12988  nnnfi  12992  ser1const  13083  expp1  13093  digit1  13224  facnn  13285  fac0  13286  facp1  13288  faclbnd4lem1  13303  bcm1k  13325  bcval5  13328  bcpasc  13331  fz1isolem  13465  seqcoll  13468  seqcoll2  13469  climuni  14509  isercolllem2  14622  isercoll  14624  sumeq2ii  14649  summolem3  14671  summolem2a  14672  fsum  14677  sum0  14678  sumz  14679  fsumcl2lem  14688  fsumadd  14696  fsummulc2  14741  fsumrelem  14764  isumnn0nn  14799  climcndslem1  14806  climcndslem2  14807  climcnds  14808  divcnv  14810  divcnvshft  14812  supcvg  14813  trireciplem  14819  trirecip  14820  expcnv  14821  geo2lim  14831  geoisum1  14835  geoisum1c  14836  mertenslem2  14841  prodeq2ii  14867  prodmolem3  14887  prodmolem2a  14888  fprod  14895  prod0  14897  prod1  14898  fprodss  14902  fprodser  14903  fprodcl2lem  14904  fprodmul  14914  fproddiv  14915  fprodn0  14933  fallfacval4  14997  bpoly4  15013  ege2le3  15043  rpnnen2lem3  15168  rpnnen2lem5  15170  rpnnen2lem8  15173  rpnnen2lem12  15177  ruclem6  15187  pwp1fsum  15337  bezoutlem2  15479  bezoutlem3  15480  lcmcllem  15531  lcmledvds  15534  lcmfval  15556  lcmfcllem  15560  lcmfledvds  15567  isprm3  15617  phicl2  15693  phibndlem  15695  eulerthlem2  15707  odzcllem  15717  odzdvds  15720  iserodd  15760  pcmptcl  15815  pcmpt  15816  pockthlem  15829  pockthg  15830  unbenlem  15832  prmreclem3  15842  prmreclem5  15844  prmreclem6  15845  prmrec  15846  1arith  15851  4sqlem13  15881  4sqlem14  15882  4sqlem17  15885  4sqlem18  15886  vdwlem1  15905  vdwlem2  15906  vdwlem3  15907  vdwlem6  15910  vdwlem8  15912  vdwlem10  15914  vdw  15918  vdwnnlem1  15919  vdwnnlem3  15921  prmlem1a  16028  mulgnnp1  17757  mulgnnsubcl  17761  mulgnn0z  17774  mulgnndir  17776  mulgpropd  17789  odlem1  18158  odlem2  18162  gexlem1  18198  gexlem2  18201  gexcl3  18206  sylow1lem1  18217  efgsdmi  18349  efgsrel  18351  efgs1b  18353  efgsp1  18354  mulgnn0di  18435  lt6abl  18500  gsumval3eu  18509  gsumval3  18512  gsumzcl2  18515  gsumzaddlem  18525  gsumconst  18538  gsumzmhm  18541  gsumzoppg  18548  zringlpirlem2  20044  zringlpirlem3  20045  lmcnp  21326  lmmo  21402  1stcelcls  21482  1stccnp  21483  1stckgenlem  21574  1stckgen  21575  imasdsf1olem  22395  cphipval  23258  lmnn  23278  cmetcaulem  23303  iscmet2  23309  causs  23313  nglmle  23317  caubl  23323  iscmet3i  23327  bcthlem5  23342  ovolsf  23459  ovollb2lem  23475  ovolctb  23477  ovolunlem1a  23483  ovolunlem1  23484  ovoliunlem1  23489  ovoliun  23492  ovoliun2  23493  ovoliunnul  23494  ovolscalem1  23500  ovolicc1  23503  ovolicc2lem2  23505  ovolicc2lem3  23506  ovolicc2lem4  23507  iundisj  23535  iundisj2  23536  voliunlem1  23537  voliunlem2  23538  voliunlem3  23539  volsup  23543  ioombl1lem4  23548  uniioovol  23566  uniioombllem2  23570  uniioombllem3  23572  uniioombllem4  23573  uniioombllem6  23575  vitalilem4  23598  vitalilem5  23599  itg1climres  23701  mbfi1fseqlem6  23707  mbfi1flimlem  23709  mbfmullem2  23711  itg2monolem1  23737  itg2i1fseqle  23741  itg2i1fseq  23742  itg2i1fseq2  23743  itg2addlem  23745  plyeq0lem  24186  vieta1lem2  24286  elqaalem1  24294  elqaalem3  24296  aaliou3lem4  24321  aaliou3lem7  24324  dvtaylp  24344  taylthlem2  24348  pserdvlem2  24402  pserdv2  24404  abelthlem6  24410  abelthlem9  24414  logtayl  24626  logtaylsum  24627  logtayl2  24628  atantayl  24884  leibpilem2  24888  leibpi  24889  birthdaylem2  24899  dfef2  24917  divsqrtsumlem  24926  emcllem2  24943  emcllem4  24945  emcllem5  24946  emcllem6  24947  emcllem7  24948  harmonicbnd4  24957  fsumharmonic  24958  zetacvg  24961  lgamgulmlem4  24978  lgamgulmlem6  24980  lgamgulm2  24982  lgamcvglem  24986  lgamcvg2  25001  gamcvg  25002  gamcvg2lem  25005  regamcl  25007  relgamcl  25008  lgam1  25010  wilthlem3  25016  ftalem2  25020  ftalem4  25022  ftalem5  25023  basellem5  25031  basellem6  25032  basellem7  25033  basellem8  25034  basellem9  25035  ppiprm  25097  ppinprm  25098  chtprm  25099  chtnprm  25100  chpp1  25101  vma1  25112  ppiltx  25123  fsumvma2  25159  chpchtsum  25164  logfacbnd3  25168  logexprlim  25170  bposlem5  25233  lgscllem  25249  lgsval2lem  25252  lgsval4a  25264  lgsneg  25266  lgsdir  25277  lgsdilem2  25278  lgsdi  25279  lgsne0  25280  gausslemma2dlem3  25313  lgsquadlem2  25326  chebbnd1lem1  25378  chtppilimlem1  25382  rplogsumlem1  25393  rplogsumlem2  25394  rpvmasumlem  25396  dchrisumlema  25397  dchrisumlem2  25399  dchrisumlem3  25400  dchrmusum2  25403  dchrvmasum2lem  25405  dchrvmasumiflem1  25410  dchrvmaeq0  25413  dchrisum0flblem2  25418  dchrisum0flb  25419  dchrisum0re  25422  dchrisum0lem1b  25424  dchrisum0lem1  25425  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0lem3  25428  mudivsum  25439  mulogsum  25441  logdivsum  25442  mulog2sumlem2  25444  log2sumbnd  25453  selberg2lem  25459  logdivbnd  25465  pntrsumo1  25474  pntrsumbnd2  25476  pntrlog2bndlem2  25487  pntrlog2bndlem4  25489  pntrlog2bndlem6a  25491  pntlemf  25514  eedimeq  25998  axlowdimlem6  26047  axlowdimlem16  26057  axlowdimlem17  26058  ipval2  27896  minvecolem3  28066  minvecolem4b  28068  minvecolem4  28070  h2hcau  28170  h2hlm  28171  hlimadd  28384  hlim0  28426  hhsscms  28470  occllem  28496  nlelchi  29254  opsqrlem4  29336  hmopidmchi  29344  iundisjf  29733  iundisj2f  29734  ssnnssfz  29882  iundisjfi  29888  iundisj2fi  29889  1smat1  30201  submat1n  30202  submatres  30203  submateqlem2  30205  lmatfval  30211  madjusmdetlem1  30224  madjusmdetlem2  30225  madjusmdetlem3  30226  madjusmdetlem4  30227  lmlim  30324  rge0scvg  30326  lmxrge0  30329  lmdvg  30330  esumfzf  30462  esumfsup  30463  esumpcvgval  30471  esumpmono  30472  esumcvg  30479  esumcvgsum  30481  esumsup  30482  fiunelros  30568  eulerpartlemsv2  30751  eulerpartlems  30753  eulerpartlemsv3  30754  eulerpartlemv  30757  eulerpartlemb  30761  fiblem  30791  fibp1  30794  rrvsum  30847  dstfrvclim1  30870  ballotlem1ri  30927  signsvfn  30990  chtvalz  31038  circlemethhgt  31052  subfacp1lem1  31489  subfacp1lem5  31494  subfacp1lem6  31495  erdszelem7  31507  cvmliftlem5  31599  cvmliftlem7  31601  cvmliftlem10  31604  cvmliftlem13  31606  sinccvg  31894  circum  31895  divcnvlin  31945  iprodgam  31955  faclimlem1  31956  faclimlem2  31957  faclim  31959  iprodfac  31960  faclim2  31961  poimirlem3  33727  poimirlem4  33728  poimirlem6  33730  poimirlem7  33731  poimirlem8  33732  poimirlem12  33736  poimirlem15  33739  poimirlem16  33740  poimirlem17  33741  poimirlem18  33742  poimirlem19  33743  poimirlem20  33744  poimirlem22  33746  poimirlem23  33747  poimirlem24  33748  poimirlem25  33749  poimirlem27  33751  poimirlem28  33752  poimirlem29  33753  poimirlem30  33754  poimirlem31  33755  mblfinlem2  33762  ovoliunnfl  33766  voliunnfl  33768  volsupnfl  33769  lmclim2  33867  geomcau  33868  heibor1lem  33921  heibor1  33922  bfplem1  33934  bfplem2  33935  rrncmslem  33944  rrncms  33945  eldioph3b  37831  diophin  37839  diophun  37840  diophren  37880  jm3.1lem2  38087  dgraalem  38217  dgraaub  38220  dftrcl3  38513  trclfvdecomr  38521  hashnzfz2  39021  hashnzfzclim  39022  dvradcnv2  39047  binomcxplemnotnn0  39056  nnsplit  40055  clim1fr1  40314  sumnnodd  40343  limsup10exlem  40485  fprodsubrecnncnvlem  40602  fprodaddrecnncnvlem  40604  stoweidlem7  40704  stoweidlem14  40711  stoweidlem20  40717  stoweidlem34  40731  wallispilem5  40766  wallispi  40767  stirlinglem1  40771  stirlinglem5  40775  stirlinglem7  40777  stirlinglem8  40778  stirlinglem10  40780  stirlinglem11  40781  stirlinglem12  40782  stirlinglem13  40783  stirlinglem14  40784  stirlinglem15  40785  stirlingr  40787  dirkertrigeqlem2  40796  dirkertrigeqlem3  40797  fourierdlem11  40815  fourierdlem31  40835  fourierdlem48  40851  fourierdlem49  40852  fourierdlem69  40872  fourierdlem73  40876  fourierdlem81  40884  fourierdlem93  40896  fourierdlem103  40906  fourierdlem104  40907  fourierdlem112  40915  fouriersw  40928  sge0ad2en  41128  voliunsge0lem  41169  caragenunicl  41221  caratheodorylem2  41224  hoidmvlelem3  41294  ovolval2lem  41340  ovolval2  41341  vonioolem2  41378  vonicclem2  41381  fmtno4prmfac  42060