Theorem nnuz 12919

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {crab 3419   class class class wbr 5114  ‘cfv 6543  1c1 11119   ≤ cle 11262  ℕcn 12251  ℤcz 12609  ℤ_≥cuz 12880

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-z 12610  df-uz 12881

This theorem is used by:  elnnuz  12920  eluz2nn  12930  uznnssnn  12937  nnwo  12955  eluznn  12960  nninf  12971  fzssnn  13615  fseq1p1m1  13645  prednn  13698  elfzo1  13760  ltwenn  14018  nnnfi  14022  ser1const  14114  expp1  14124  digit1  14293  facnn  14331  fac0  14332  facp1  14334  faclbnd4lem1  14349  bcm1k  14371  bcval5  14374  bcpasc  14377  fz1isolem  14518  seqcoll  14521  seqcoll2  14522  climuni  15629  isercolllem2  15743  isercoll  15745  sumeq2ii  15770  summolem3  15791  summolem2a  15792  fsum  15797  sum0  15798  sumz  15799  fsumcl2lem  15808  fsumadd  15817  fsummulc2  15861  fsumrelem  15885  isumnn0nn  15922  climcndslem1  15929  climcndslem2  15930  climcnds  15931  divcnv  15933  divcnvshft  15935  supcvg  15936  trireciplem  15942  trirecip  15943  expcnv  15944  geo2lim  15955  geoisum1  15959  geoisum1c  15960  mertenslem2  15965  prodeq2ii  15991  prodmolem3  16013  prodmolem2a  16014  fprod  16021  prod0  16023  prod1  16024  fprodss  16028  fprodser  16029  fprodcl2lem  16030  fprodmul  16040  fproddiv  16041  fprodn0  16059  fallfacval4  16122  bpoly4  16138  ege2le3  16169  rpnnen2lem3  16297  rpnnen2lem5  16299  rpnnen2lem8  16302  rpnnen2lem12  16306  ruclem6  16316  pwp1fsum  16474  bezoutlem2  16623  bezoutlem3  16624  lcmcllem  16679  lcmledvds  16682  lcmfval  16704  lcmfcllem  16708  lcmfledvds  16715  isprm3  16766  phicl2  16852  phibndlem  16854  eulerthlem2  16866  odzcllem  16877  odzdvds  16880  iserodd  16920  pcmptcl  16976  pcmpt  16977  pockthlem  16990  pockthg  16991  unbenlem  16993  prmreclem3  17003  prmreclem5  17005  prmreclem6  17006  prmrec  17007  1arith  17012  4sqlem13  17042  4sqlem14  17043  4sqlem17  17046  4sqlem18  17047  vdwlem1  17066  vdwlem2  17067  vdwlem3  17068  vdwlem6  17071  vdwlem8  17073  vdwlem10  17075  vdw  17079  vdwnnlem3  17082  prmlem1a  17191  chnub  18703  mulgnnp1  19179  mulgnnsubcl  19183  mulgnn0z  19198  mulgnndir  19200  mulgpropd  19213  odfval  19633  odlem1  19636  odlem2  19640  gexlem1  19680  gexlem2  19683  gexcl3  19688  sylow1lem1  19699  efgsdmi  19833  efgsrel  19835  efgs1b  19837  efgsp1  19838  mulgnn0di  19926  lt6abl  19996  gsumval3eu  20005  gsumval3  20008  gsumzcl2  20011  gsumzaddlem  20022  gsumconst  20035  gsumzmhm  20038  gsumzoppg  20045  zringlpirlem2  21650  zringlpirlem3  21651  lmcnp  23498  lmmo  23574  1stcelcls  23655  1stccnp  23656  1stckgenlem  23747  1stckgen  23748  imasdsf1olem  24567  cphipval  25439  lmnn  25459  cmetcaulem  25484  iscmet2  25490  causs  25494  nglmle  25498  caubl  25504  iscmet3i  25508  bcthlem5  25524  ovolsf  25668  ovollb2lem  25684  ovolctb  25686  ovolunlem1a  25692  ovolunlem1  25693  ovoliunlem1  25698  ovoliun  25701  ovoliun2  25702  ovoliunnul  25703  ovolscalem1  25709  ovolicc1  25712  ovolicc2lem2  25714  ovolicc2lem3  25715  ovolicc2lem4  25716  iundisj  25744  iundisj2  25745  voliunlem1  25746  voliunlem2  25747  voliunlem3  25748  volsup  25752  ioombl1lem4  25757  uniioovol  25775  uniioombllem2  25779  uniioombllem3  25781  uniioombllem4  25782  uniioombllem6  25784  vitalilem4  25807  vitalilem5  25808  itg1climres  25910  mbfi1fseqlem6  25916  mbfi1flimlem  25918  mbfmullem2  25920  itg2monolem1  25946  itg2i1fseqle  25950  itg2i1fseq  25951  itg2i1fseq2  25952  itg2addlem  25954  plyeq0lem  26404  vieta1lem2  26509  elqaalem1  26517  elqaalem3  26519  aaliou3lem4  26546  aaliou3lem7  26549  dvtaylp  26570  taylthlem2  26574  pserdvlem2  26628  pserdv2  26630  abelthlem6  26636  abelthlem9  26640  logtayl  26862  logtaylsum  26863  logtayl2  26864  atantayl  27139  leibpilem2  27143  leibpi  27144  birthdaylem2  27154  dfef2  27172  divsqrtsumlem  27181  emcllem2  27198  emcllem4  27200  emcllem5  27201  emcllem6  27202  emcllem7  27203  harmonicbnd4  27212  fsumharmonic  27213  zetacvg  27216  lgamgulmlem4  27233  lgamgulmlem6  27235  lgamgulm2  27237  lgamcvglem  27241  lgamcvg2  27256  gamcvg  27257  gamcvg2lem  27260  regamcl  27262  relgamcl  27263  lgam1  27265  wilthlem3  27271  ftalem2  27275  ftalem4  27277  ftalem5  27278  basellem5  27286  basellem6  27287  basellem7  27288  basellem8  27289  basellem9  27290  ppiprm  27352  ppinprm  27353  chtprm  27354  chtnprm  27355  chpp1  27356  vma1  27367  ppiltx  27378  fsumvma2  27415  chpchtsum  27420  logfacbnd3  27424  logexprlim  27426  bposlem5  27489  lgscllem  27505  lgsval2lem  27508  lgsval4a  27520  lgsneg  27522  lgsdir  27533  lgsdilem2  27534  lgsdi  27535  lgsne0  27536  gausslemma2dlem3  27569  lgsquadlem2  27582  chebbnd1lem1  27670  chtppilimlem1  27674  rplogsumlem1  27685  rplogsumlem2  27686  rpvmasumlem  27688  dchrisumlema  27689  dchrisumlem2  27691  dchrisumlem3  27692  dchrmusum2  27695  dchrvmasum2lem  27697  dchrvmasumiflem1  27702  dchrvmaeq0  27705  dchrisum0flblem2  27710  dchrisum0flb  27711  dchrisum0re  27714  dchrisum0lem1b  27716  dchrisum0lem1  27717  dchrisum0lem2a  27718  dchrisum0lem2  27719  dchrisum0lem3  27720  mudivsum  27731  mulogsum  27733  logdivsum  27734  mulog2sumlem2  27736  log2sumbnd  27745  selberg2lem  27751  logdivbnd  27757  pntrsumo1  27766  pntrsumbnd2  27768  pntrlog2bndlem2  27779  pntrlog2bndlem4  27781  pntrlog2bndlem6a  27783  pntlemf  27806  eedimeq  29285  axlowdimlem6  29334  axlowdimlem16  29344  axlowdimlem17  29345  ipval2  31096  minvecolem3  31265  minvecolem4b  31267  minvecolem4  31269  h2hcau  31368  h2hlm  31369  hlimadd  31582  hlim0  31624  hhsscms  31667  occllem  31692  nlelchi  32450  opsqrlem4  32532  hmopidmchi  32540  iundisjf  32971  iundisj2f  32972  ssnnssfz  33169  iundisjfi  33178  iundisj2fi  33179  cycpmco2lem7  33483  cycpmrn  33494  1smat1  34225  submat1n  34226  submatres  34227  submateqlem2  34229  lmatfval  34235  madjusmdetlem1  34248  madjusmdetlem2  34249  madjusmdetlem3  34250  madjusmdetlem4  34251  lmlim  34368  rge0scvg  34370  lmxrge0  34373  lmdvg  34374  esumfzf  34490  esumfsup  34491  esumpcvgval  34499  esumpmono  34500  esumcvg  34507  esumcvgsum  34509  esumsup  34510  fiunelros  34596  eulerpartlemsv2  34780  eulerpartlems  34782  eulerpartlemsv3  34783  eulerpartlemv  34786  eulerpartlemb  34790  fiblem  34820  fibp1  34823  rrvsum  34876  dstfrvclim1  34900  ballotlem1ri  34957  signsvfn  35001  chtvalz  35048  circlemethhgt  35062  subfacp1lem1  35692  subfacp1lem5  35697  subfacp1lem6  35698  erdszelem7  35710  cvmliftlem5  35802  cvmliftlem7  35804  cvmliftlem10  35807  cvmliftlem13  35809  sinccvg  36186  circum  36187  divcnvlin  36246  iprodgam  36255  faclimlem1  36256  faclimlem2  36257  faclim  36259  iprodfac  36260  faclim2  36261  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem12  38324  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem18  38330  poimirlem19  38331  poimirlem20  38332  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem25  38337  poimirlem27  38339  poimirlem28  38340  poimirlem29  38341  poimirlem30  38342  poimirlem31  38343  mblfinlem2  38350  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  lmclim2  38450  geomcau  38451  heibor1lem  38501  heibor1  38502  bfplem1  38514  bfplem2  38515  rrncmslem  38524  rrncms  38525  aks4d1p1p1  42871  sticksstones10  42963  sticksstones12a  42965  fz1sump1  43112  sumcubes  43115  nna4b4nsq  43433  eldioph3b  43537  diophin  43544  diophun  43545  diophren  43581  jm3.1lem2  43786  dgraalem  43913  dgraaub  43916  dftrcl3  44487  trclfvdecomr  44495  hashnzfz2  45072  hashnzfzclim  45073  dvradcnv2  45098  binomcxplemnotnn0  45107  nnsplit  46115  rexanuz2nf  46247  clim1fr1  46358  sumnnodd  46387  limsup10exlem  46527  fprodsubrecnncnvlem  46662  fprodaddrecnncnvlem  46664  stoweidlem7  46762  stoweidlem14  46769  stoweidlem20  46775  stoweidlem34  46789  wallispilem5  46824  wallispi  46825  stirlinglem1  46829  stirlinglem5  46833  stirlinglem7  46835  stirlinglem8  46836  stirlinglem10  46838  stirlinglem11  46839  stirlinglem12  46840  stirlinglem13  46841  stirlinglem14  46842  stirlinglem15  46843  stirlingr  46845  dirkertrigeqlem2  46854  dirkertrigeqlem3  46855  fourierdlem11  46873  fourierdlem31  46893  fourierdlem48  46909  fourierdlem49  46910  fourierdlem69  46930  fourierdlem73  46934  fourierdlem81  46942  fourierdlem93  46954  fourierdlem103  46964  fourierdlem104  46965  fourierdlem112  46973  fouriersw  46986  sge0ad2en  47186  voliunsge0lem  47227  caragenunicl  47279  caratheodorylem2  47282  hoidmvlelem3  47352  ovolval2lem  47398  ovolval2  47399  vonioolem2  47436  vonicclem2  47439  fmtno4prmfac  48365