Theorem nnuz 13034

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  {crab 3416   class class class wbr 5106  ‘cfv 6561  1c1 11231   ≤ cle 11374  ℕcn 12365  ℤcz 12723  ℤ_≥cuz 12995

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-nn 12366  df-z 12724  df-uz 12996

This theorem is used by:  elnnuz  13035  eluz2nn  13045  uznnssnn  13052  nnwo  13070  eluznn  13075  nninf  13086  fzssnn  13732  fseq1p1m1  13762  prednn  13815  elfzo1  13877  ltwenn  14135  nnnfi  14139  ser1const  14231  expp1  14241  digit1  14411  facnn  14449  fac0  14450  facp1  14452  faclbnd4lem1  14467  bcm1k  14489  bcval5  14492  bcpasc  14495  fz1isolem  14636  seqcoll  14639  seqcoll2  14640  climuni  15751  isercolllem2  15865  isercoll  15867  sumeq2ii  15892  summolem3  15912  summolem2a  15913  fsum  15918  sum0  15919  sumz  15920  fsumcl2lem  15929  fsumadd  15938  fsummulc2  15982  fsumrelem  16006  isumnn0nn  16043  climcndslem1  16050  climcndslem2  16051  climcnds  16052  divcnv  16054  divcnvshft  16056  supcvg  16057  trireciplem  16063  trirecip  16064  expcnv  16065  geo2lim  16076  geoisum1  16080  geoisum1c  16081  mertenslem2  16086  prodeq2ii  16112  prodmolem3  16132  prodmolem2a  16133  fprod  16140  prod0  16142  prod1  16143  fprodss  16147  fprodser  16148  fprodcl2lem  16149  fprodmul  16159  fproddiv  16160  fprodn0  16178  fallfacval4  16241  bpoly4  16257  ege2le3  16288  rpnnen2lem3  16416  rpnnen2lem5  16418  rpnnen2lem8  16421  rpnnen2lem12  16425  ruclem6  16435  pwp1fsum  16593  bezoutlem2  16745  bezoutlem3  16746  lcmcllem  16803  lcmledvds  16806  lcmfval  16828  lcmfcllem  16832  lcmfledvds  16839  isprm3  16890  phicl2  16977  phibndlem  16979  eulerthlem2  16991  odzcllem  17002  odzdvds  17005  iserodd  17045  pcmptcl  17101  pcmpt  17102  pockthlem  17115  pockthg  17116  unbenlem  17118  prmreclem3  17128  prmreclem5  17130  prmreclem6  17131  prmrec  17132  1arith  17137  4sqlem13  17167  4sqlem14  17168  4sqlem17  17171  4sqlem18  17172  vdwlem1  17191  vdwlem2  17192  vdwlem3  17193  vdwlem6  17196  vdwlem8  17198  vdwlem10  17200  vdw  17204  vdwnnlem3  17207  prmlem1a  17316  chnub  18828  mulgnnp1  19324  mulgnnsubcl  19328  mulgnn0z  19343  mulgnndir  19345  mulgpropd  19358  odfval  19779  odlem1  19782  odlem2  19786  gexlem1  19826  gexlem2  19829  gexcl3  19834  sylow1lem1  19845  efgsdmi  19979  efgsrel  19981  efgs1b  19983  efgsp1  19984  mulgnn0di  20072  lt6abl  20142  gsumval3eu  20151  gsumval3  20154  gsumzcl2  20157  gsumzaddlem  20168  gsumconst  20181  gsumzmhm  20184  gsumzoppg  20191  zringlpirlem2  21802  zringlpirlem3  21803  lmcnp  23655  lmmo  23731  1stcelcls  23813  1stccnp  23814  1stckgenlem  23905  1stckgen  23906  imasdsf1olem  24725  cphipval  25597  lmnn  25617  cmetcaulem  25642  iscmet2  25648  causs  25652  nglmle  25656  caubl  25662  iscmet3i  25666  bcthlem5  25682  ovolsf  25826  ovollb2lem  25842  ovolctb  25844  ovolunlem1a  25850  ovolunlem1  25851  ovoliunlem1  25856  ovoliun  25859  ovoliun2  25860  ovoliunnul  25861  ovolscalem1  25867  ovolicc1  25870  ovolicc2lem2  25872  ovolicc2lem3  25873  ovolicc2lem4  25874  iundisj  25902  iundisj2  25903  voliunlem1  25904  voliunlem2  25905  voliunlem3  25906  volsup  25910  ioombl1lem4  25915  uniioovol  25933  uniioombllem2  25937  uniioombllem3  25939  uniioombllem4  25940  uniioombllem6  25942  vitalilem4  25965  vitalilem5  25966  itg1climres  26068  mbfi1fseqlem6  26074  mbfi1flimlem  26076  mbfmullem2  26078  itg2monolem1  26104  itg2i1fseqle  26108  itg2i1fseq  26109  itg2i1fseq2  26110  itg2addlem  26112  plyeq0lem  26562  vieta1lem2  26667  elqaalem1  26675  elqaalem3  26677  aaliou3lem4  26706  aaliou3lem7  26709  dvtaylp  26730  taylthlem2  26734  pserdvlem2  26788  pserdv2  26790  abelthlem6  26796  abelthlem9  26800  logtayl  27021  logtaylsum  27022  logtayl2  27023  atantayl  27298  leibpilem2  27302  leibpi  27303  birthdaylem2  27313  dfef2  27331  divsqrtsumlem  27340  emcllem2  27357  emcllem4  27359  emcllem5  27360  emcllem6  27361  emcllem7  27362  harmonicbnd4  27371  fsumharmonic  27372  zetacvg  27375  lgamgulmlem4  27392  lgamgulmlem6  27394  lgamgulm2  27396  lgamcvglem  27400  lgamcvg2  27415  gamcvg  27416  gamcvg2lem  27419  regamcl  27421  relgamcl  27422  lgam1  27424  wilthlem3  27430  ftalem2  27434  ftalem4  27436  ftalem5  27437  basellem5  27445  basellem6  27446  basellem7  27447  basellem8  27448  basellem9  27449  ppiprm  27511  ppinprm  27512  chtprm  27513  chtnprm  27514  chpp1  27515  vma1  27526  ppiltx  27537  fsumvma2  27574  chpchtsum  27579  logfacbnd3  27583  logexprlim  27585  bposlem5  27648  lgscllem  27664  lgsval2lem  27667  lgsval4a  27679  lgsneg  27681  lgsdir  27692  lgsdilem2  27693  lgsdi  27694  lgsne0  27695  gausslemma2dlem3  27728  lgsquadlem2  27741  chebbnd1lem1  27829  chtppilimlem1  27833  rplogsumlem1  27844  rplogsumlem2  27845  rpvmasumlem  27847  dchrisumlema  27848  dchrisumlem2  27850  dchrisumlem3  27851  dchrmusum2  27854  dchrvmasum2lem  27856  dchrvmasumiflem1  27861  dchrvmaeq0  27864  dchrisum0flblem2  27869  dchrisum0flb  27870  dchrisum0re  27873  dchrisum0lem1b  27875  dchrisum0lem1  27876  dchrisum0lem2a  27877  dchrisum0lem2  27878  dchrisum0lem3  27879  mudivsum  27890  mulogsum  27892  logdivsum  27893  mulog2sumlem2  27895  log2sumbnd  27904  selberg2lem  27910  logdivbnd  27916  pntrsumo1  27925  pntrsumbnd2  27927  pntrlog2bndlem2  27938  pntrlog2bndlem4  27940  pntrlog2bndlem6a  27942  pntlemf  27965  nna4b4nsq  28023  eedimeq  29509  axlowdimlem6  29558  axlowdimlem16  29568  axlowdimlem17  29569  ipval2  31342  minvecolem3  31511  minvecolem4b  31513  minvecolem4  31515  h2hcau  31614  h2hlm  31615  hlimadd  31828  hlim0  31870  hhsscms  31913  occllem  31938  nlelchi  32696  opsqrlem4  32778  hmopidmchi  32786  iundisjf  33258  iundisj2f  33259  ssnnssfz  33452  iundisjfi  33461  iundisj2fi  33462  cycpmco2lem7  33769  cycpmrn  33780  1smat1  34519  submat1n  34520  submatres  34521  submateqlem2  34523  lmatfval  34529  madjusmdetlem1  34542  madjusmdetlem2  34543  madjusmdetlem3  34544  madjusmdetlem4  34545  lmlim  34662  rge0scvg  34664  lmxrge0  34667  lmdvg  34668  esumfzf  34784  esumfsup  34785  esumpcvgval  34793  esumpmono  34794  esumcvg  34801  esumcvgsum  34803  esumsup  34804  fiunelros  34890  eulerpartlemsv2  35073  eulerpartlems  35075  eulerpartlemsv3  35076  eulerpartlemv  35079  eulerpartlemb  35083  fiblem  35113  fibp1  35116  rrvsum  35169  dstfrvclim1  35193  ballotlem1ri  35250  signsvfn  35294  chtvalz  35341  circlemethhgt  35355  subfacp1lem1  36124  subfacp1lem5  36129  subfacp1lem6  36130  erdszelem7  36142  cvmliftlem5  36234  cvmliftlem7  36236  cvmliftlem10  36239  cvmliftlem13  36241  sinccvg  36618  circum  36619  divcnvlin  36689  iprodgam  36698  faclimlem1  36699  faclimlem2  36700  faclim  36702  iprodfac  36703  faclim2  36704  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem12  38755  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem18  38761  poimirlem19  38762  poimirlem20  38763  poimirlem22  38765  poimirlem23  38766  poimirlem24  38767  poimirlem25  38768  poimirlem27  38770  poimirlem28  38771  poimirlem29  38772  poimirlem30  38773  poimirlem31  38774  mblfinlem2  38781  ovoliunnfl  38785  voliunnfl  38787  volsupnfl  38788  lmclim2  38895  geomcau  38896  heibor1lem  38946  heibor1  38947  bfplem1  38959  bfplem2  38960  rrncmslem  38969  rrncms  38970  aks4d1p1p1  43316  sticksstones10  43408  sticksstones12a  43410  fz1sump1  43571  sumcubes  43574  eldioph3b  43980  diophin  43987  diophun  43988  diophren  44024  jm3.1lem2  44229  dgraalem  44350  dgraaub  44353  dftrcl3  44923  trclfvdecomr  44931  hashnzfz2  45508  hashnzfzclim  45509  dvradcnv2  45534  binomcxplemnotnn0  45543  nnsplit  46585  rexanuz2nf  46717  clim1fr1  46828  sumnnodd  46857  limsup10exlem  46997  fprodsubrecnncnvlem  47132  fprodaddrecnncnvlem  47134  stoweidlem7  47232  stoweidlem14  47239  stoweidlem20  47245  stoweidlem34  47259  wallispilem5  47294  wallispi  47295  stirlinglem1  47299  stirlinglem5  47303  stirlinglem7  47305  stirlinglem8  47306  stirlinglem10  47308  stirlinglem11  47309  stirlinglem12  47310  stirlinglem13  47311  stirlinglem14  47312  stirlinglem15  47313  stirlingr  47315  dirkertrigeqlem2  47324  dirkertrigeqlem3  47325  fourierdlem11  47343  fourierdlem31  47363  fourierdlem48  47379  fourierdlem49  47380  fourierdlem69  47400  fourierdlem73  47404  fourierdlem81  47412  fourierdlem93  47424  fourierdlem103  47434  fourierdlem104  47435  fourierdlem112  47443  fouriersw  47456  sge0ad2en  47656  voliunsge0lem  47697  caragenunicl  47749  caratheodorylem2  47752  hoidmvlelem3  47822  ovolval2lem  47868  ovolval2  47869  vonioolem2  47906  vonicclem2  47909  fmtno4prmfac  48872  veroquadgsumlem  51295