Theorem nnuz 12282

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  {crab 3142   class class class wbr 5066  ‘cfv 6355  1c1 10538   ≤ cle 10676  ℕcn 11638  ℤcz 11982  ℤ_≥cuz 12244

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-z 11983  df-uz 12245

This theorem is referenced by:  elnnuz  12283  eluz2nn  12285  uznnssnn  12296  nnwo  12314  eluznn  12319  nninf  12330  fzssnn  12952  fseq1p1m1  12982  prednn  13031  elfzo1  13088  ltwenn  13331  nnnfi  13335  ser1const  13427  expp1  13437  digit1  13599  facnn  13636  fac0  13637  facp1  13639  faclbnd4lem1  13654  bcm1k  13676  bcval5  13679  bcpasc  13682  fz1isolem  13820  seqcoll  13823  seqcoll2  13824  climuni  14909  isercolllem2  15022  isercoll  15024  sumeq2ii  15050  summolem3  15071  summolem2a  15072  fsum  15077  sum0  15078  sumz  15079  fsumcl2lem  15088  fsumadd  15096  fsummulc2  15139  fsumrelem  15162  isumnn0nn  15197  climcndslem1  15204  climcndslem2  15205  climcnds  15206  divcnv  15208  divcnvshft  15210  supcvg  15211  trireciplem  15217  trirecip  15218  expcnv  15219  geo2lim  15231  geoisum1  15235  geoisum1c  15236  mertenslem2  15241  prodeq2ii  15267  prodmolem3  15287  prodmolem2a  15288  fprod  15295  prod0  15297  prod1  15298  fprodss  15302  fprodser  15303  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodn0  15333  fallfacval4  15397  bpoly4  15413  ege2le3  15443  rpnnen2lem3  15569  rpnnen2lem5  15571  rpnnen2lem8  15574  rpnnen2lem12  15578  ruclem6  15588  pwp1fsum  15742  bezoutlem2  15888  bezoutlem3  15889  lcmcllem  15940  lcmledvds  15943  lcmfval  15965  lcmfcllem  15969  lcmfledvds  15976  isprm3  16027  phicl2  16105  phibndlem  16107  eulerthlem2  16119  odzcllem  16129  odzdvds  16132  iserodd  16172  pcmptcl  16227  pcmpt  16228  pockthlem  16241  pockthg  16242  unbenlem  16244  prmreclem3  16254  prmreclem5  16256  prmreclem6  16257  prmrec  16258  1arith  16263  4sqlem13  16293  4sqlem14  16294  4sqlem17  16297  4sqlem18  16298  vdwlem1  16317  vdwlem2  16318  vdwlem3  16319  vdwlem6  16322  vdwlem8  16324  vdwlem10  16326  vdw  16330  vdwnnlem3  16333  prmlem1a  16440  mulgnnp1  18236  mulgnnsubcl  18240  mulgnn0z  18254  mulgnndir  18256  mulgpropd  18269  odfval  18660  odlem1  18663  odlem2  18667  gexlem1  18704  gexlem2  18707  gexcl3  18712  sylow1lem1  18723  efgsdmi  18858  efgsrel  18860  efgs1b  18862  efgsp1  18863  mulgnn0di  18946  lt6abl  19015  gsumval3eu  19024  gsumval3  19027  gsumzcl2  19030  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsumzoppg  19064  zringlpirlem2  20632  zringlpirlem3  20633  lmcnp  21912  lmmo  21988  1stcelcls  22069  1stccnp  22070  1stckgenlem  22161  1stckgen  22162  imasdsf1olem  22983  cphipval  23846  lmnn  23866  cmetcaulem  23891  iscmet2  23897  causs  23901  nglmle  23905  caubl  23911  iscmet3i  23915  bcthlem5  23931  ovolsf  24073  ovollb2lem  24089  ovolctb  24091  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliun  24106  ovoliun2  24107  ovoliunnul  24108  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem2  24119  ovolicc2lem3  24120  ovolicc2lem4  24121  iundisj  24149  iundisj2  24150  voliunlem1  24151  voliunlem2  24152  voliunlem3  24153  volsup  24157  ioombl1lem4  24162  uniioovol  24180  uniioombllem2  24184  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  vitalilem4  24212  vitalilem5  24213  itg1climres  24315  mbfi1fseqlem6  24321  mbfi1flimlem  24323  mbfmullem2  24325  itg2monolem1  24351  itg2i1fseqle  24355  itg2i1fseq  24356  itg2i1fseq2  24357  itg2addlem  24359  plyeq0lem  24800  vieta1lem2  24900  elqaalem1  24908  elqaalem3  24910  aaliou3lem4  24935  aaliou3lem7  24938  dvtaylp  24958  taylthlem2  24962  pserdvlem2  25016  pserdv2  25018  abelthlem6  25024  abelthlem9  25028  logtayl  25243  logtaylsum  25244  logtayl2  25245  atantayl  25515  leibpilem2  25519  leibpi  25520  birthdaylem2  25530  dfef2  25548  divsqrtsumlem  25557  emcllem2  25574  emcllem4  25576  emcllem5  25577  emcllem6  25578  emcllem7  25579  harmonicbnd4  25588  fsumharmonic  25589  zetacvg  25592  lgamgulmlem4  25609  lgamgulmlem6  25611  lgamgulm2  25613  lgamcvglem  25617  lgamcvg2  25632  gamcvg  25633  gamcvg2lem  25636  regamcl  25638  relgamcl  25639  lgam1  25641  wilthlem3  25647  ftalem2  25651  ftalem4  25653  ftalem5  25654  basellem5  25662  basellem6  25663  basellem7  25664  basellem8  25665  basellem9  25666  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  chpp1  25732  vma1  25743  ppiltx  25754  fsumvma2  25790  chpchtsum  25795  logfacbnd3  25799  logexprlim  25801  bposlem5  25864  lgscllem  25880  lgsval2lem  25883  lgsval4a  25895  lgsneg  25897  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  gausslemma2dlem3  25944  lgsquadlem2  25957  chebbnd1lem1  26045  chtppilimlem1  26049  rplogsumlem1  26060  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasum2lem  26072  dchrvmasumiflem1  26077  dchrvmaeq0  26080  dchrisum0flblem2  26085  dchrisum0flb  26086  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  mudivsum  26106  mulogsum  26108  logdivsum  26109  mulog2sumlem2  26111  log2sumbnd  26120  selberg2lem  26126  logdivbnd  26132  pntrsumo1  26141  pntrsumbnd2  26143  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntrlog2bndlem6a  26158  pntlemf  26181  eedimeq  26684  axlowdimlem6  26733  axlowdimlem16  26743  axlowdimlem17  26744  ipval2  28484  minvecolem3  28653  minvecolem4b  28655  minvecolem4  28657  h2hcau  28756  h2hlm  28757  hlimadd  28970  hlim0  29012  hhsscms  29055  occllem  29080  nlelchi  29838  opsqrlem4  29920  hmopidmchi  29928  iundisjf  30339  iundisj2f  30340  ssnnssfz  30510  iundisjfi  30519  iundisj2fi  30520  cycpmco2lem7  30774  cycpmrn  30785  1smat1  31069  submat1n  31070  submatres  31071  submateqlem2  31073  lmatfval  31079  madjusmdetlem1  31092  madjusmdetlem2  31093  madjusmdetlem3  31094  madjusmdetlem4  31095  lmlim  31190  rge0scvg  31192  lmxrge0  31195  lmdvg  31196  esumfzf  31328  esumfsup  31329  esumpcvgval  31337  esumpmono  31338  esumcvg  31345  esumcvgsum  31347  esumsup  31348  fiunelros  31433  eulerpartlemsv2  31616  eulerpartlems  31618  eulerpartlemsv3  31619  eulerpartlemv  31622  eulerpartlemb  31626  fiblem  31656  fibp1  31659  rrvsum  31712  dstfrvclim1  31735  ballotlem1ri  31792  signsvfn  31852  chtvalz  31900  circlemethhgt  31914  subfacp1lem1  32426  subfacp1lem5  32431  subfacp1lem6  32432  erdszelem7  32444  cvmliftlem5  32536  cvmliftlem7  32538  cvmliftlem10  32541  cvmliftlem13  32543  sinccvg  32916  circum  32917  divcnvlin  32964  iprodgam  32974  faclimlem1  32975  faclimlem2  32976  faclim  32978  iprodfac  32979  faclim2  32980  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem12  34919  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  mblfinlem2  34945  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  lmclim2  35048  geomcau  35049  heibor1lem  35102  heibor1  35103  bfplem1  35115  bfplem2  35116  rrncmslem  35125  rrncms  35126  eldioph3b  39382  diophin  39389  diophun  39390  diophren  39430  jm3.1lem2  39635  dgraalem  39765  dgraaub  39768  dftrcl3  40085  trclfvdecomr  40093  hashnzfz2  40673  hashnzfzclim  40674  dvradcnv2  40699  binomcxplemnotnn0  40708  nnsplit  41646  clim1fr1  41902  sumnnodd  41931  limsup10exlem  42073  fprodsubrecnncnvlem  42211  fprodaddrecnncnvlem  42213  stoweidlem7  42312  stoweidlem14  42319  stoweidlem20  42325  stoweidlem34  42339  wallispilem5  42374  wallispi  42375  stirlinglem1  42379  stirlinglem5  42383  stirlinglem7  42385  stirlinglem8  42386  stirlinglem10  42388  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  stirlingr  42395  dirkertrigeqlem2  42404  dirkertrigeqlem3  42405  fourierdlem11  42423  fourierdlem31  42443  fourierdlem48  42459  fourierdlem49  42460  fourierdlem69  42480  fourierdlem73  42484  fourierdlem81  42492  fourierdlem93  42504  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  fouriersw  42536  sge0ad2en  42733  voliunsge0lem  42774  caragenunicl  42826  caratheodorylem2  42829  hoidmvlelem3  42899  ovolval2lem  42945  ovolval2  42946  vonioolem2  42983  vonicclem2  42986  fmtno4prmfac  43754