Theorem nn0uz 12801

Description: Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)

Assertion

Ref	Expression
nn0uz	⊢ ℕ0 = (ℤ≥‘0)

Proof of Theorem nn0uz

Step	Hyp	Ref	Expression
1		nn0zrab 12532	. 2 ⊢ ℕ0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2		0z 12511	. . 3 ⊢ 0 ∈ ℤ
3		uzval 12765	. . 3 ⊢ (0 ∈ ℤ → (ℤ≥‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
5	1, 4	eqtr4i 2763	1 ⊢ ℕ0 = (ℤ≥‘0)

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3401   class class class wbr 5100  ‘cfv 6500  0cc0 11038   ≤ cle 11179  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501  df-uz 12764

This theorem is referenced by:  elnn0uz  12804  2eluzge0  12806  eluznn0  12842  nn0inf  12855  fseq1p1m1  13526  fznn0sub2  13563  nn0split  13571  prednn0  13580  fzossnn0  13618  fzennn  13903  hashgf1o  13906  exple1  14112  faclbnd4lem1  14228  bcval5  14253  bcpasc  14256  hashfzo0  14365  hashf1  14392  ccatval2  14513  ccatass  14524  ccatrn  14525  swrdccat2  14605  wrdeqs1cat  14655  cats1un  14656  splfv2a  14691  splval2  14692  revccat  14701  cats1fv  14794  binom1dif  15768  isumnn0nn  15777  climcndslem1  15784  climcnds  15786  harmonic  15794  arisum2  15796  explecnv  15800  geoser  15802  pwdif  15803  geolim  15805  geolim2  15806  geomulcvg  15811  geoisum  15812  geoisumr  15813  mertenslem1  15819  mertenslem2  15820  mertens  15821  fallfacfwd  15971  0fallfac  15972  binomfallfaclem2  15975  bpolylem  15983  bpolysum  15988  bpolydiflem  15989  fsumkthpow  15991  bpoly2  15992  bpoly3  15993  bpoly4  15994  efcllem  16012  ef0lem  16013  eff  16016  efcvg  16020  efcvgfsum  16021  reefcl  16022  ege2le3  16025  efcj  16027  eftlcvg  16043  eftlub  16046  effsumlt  16048  ef4p  16050  efgt1p2  16051  efgt1p  16052  eflegeo  16058  eirrlem  16141  ruclem6  16172  ruclem7  16173  divalglem2  16334  divalglem5  16336  bitsfzolem  16373  bitsfzo  16374  bitsfi  16376  bitsinv1lem  16380  bitsinv1  16381  bitsinvp1  16388  sadcf  16392  sadcp1  16394  sadadd  16406  sadass  16410  bitsres  16412  smupf  16417  smupp1  16419  smuval2  16421  smupval  16427  smueqlem  16429  smumul  16432  alginv  16514  algcvg  16515  algcvga  16518  algfx  16519  eucalgcvga  16525  eucalg  16526  phiprmpw  16715  prmdiv  16724  iserodd  16775  pcfac  16839  prmreclem2  16857  prmreclem4  16859  vdwapun  16914  vdwlem1  16921  ramcl2lem  16949  ramtcl  16950  ramtub  16952  chnccats1  18560  gsumwsubmcl  18774  gsumws1  18775  gsumsgrpccat  18777  gsumwmhm  18782  psgnunilem2  19436  psgnunilem4  19438  sylow1lem1  19539  efginvrel2  19668  efgredleme  19684  efgredlemc  19686  efgcpbllemb  19696  frgpuplem  19713  telgsumfz0s  19932  telgsums  19934  pgpfaclem1  20024  psrbaglefi  21894  ltbwe  22011  pmatcollpw3fi1lem1  22742  chfacfisf  22810  chfacfisfcpmat  22811  iscmet3lem3  25258  dyadmax  25567  mbfi1fseqlem3  25686  itgcnlem  25759  dvnff  25893  dvnp1  25895  dvn2bss  25900  cpncn  25906  dveflem  25951  ig1peu  26148  ig1pdvds  26153  ply1termlem  26176  plyeq0lem  26183  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  dgrcl  26206  dgrub  26207  dgrlb  26209  coeid3  26213  plyco  26214  coeeq2  26215  coefv0  26221  coemulhi  26227  coemulc  26228  dvply1  26259  vieta1lem2  26287  vieta1  26288  elqaalem2  26296  elqaalem3  26297  geolim3  26315  dvntaylp  26347  taylthlem1  26349  radcnvlem1  26390  radcnvlem2  26391  radcnvlem3  26392  radcnv0  26393  radcnvlt2  26396  dvradcnv  26398  pserulm  26399  psercn2  26400  psercn2OLD  26401  pserdvlem2  26406  pserdv2  26408  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  advlogexp  26632  logtayllem  26636  logtayl  26637  cxpeq  26735  leibpi  26920  leibpisum  26921  log2cnv  26922  log2tlbnd  26923  log2ublem2  26925  birthdaylem3  26931  wilthlem2  27047  ftalem1  27051  ftalem5  27055  basellem2  27060  basellem3  27061  basellem5  27063  musum  27169  0sgmppw  27177  1sgmprm  27178  chtublem  27190  logexprlim  27204  lgseisenlem1  27354  lgsquadlem2  27360  dchrisumlem1  27468  dchrisumlem2  27469  dchrisum0flblem1  27487  ostth2lem3  27614  tgcgr4  28615  clwwlknonex2lem1  30194  eupth2lems  30325  fz2ssnn0  32876  nn0diffz0  32885  nn0split01  32909  ccatws1f1o  33044  gsummulsubdishift1  33162  gsumwrd2dccat  33172  cycpmco2rn  33219  cycpmco2lem6  33225  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  ig1pmindeg  33695  vietalem  33756  exsslsb  33774  oddpwdc  34532  eulerpartlemb  34546  sseqfn  34568  sseqf  34570  signsplypnf  34728  signstcl  34743  signstf  34744  signstfvn  34747  signstfvneq0  34750  fsum2dsub  34785  reprsuc  34793  breprexplema  34808  breprexplemc  34810  subfacval2  35403  subfaclim  35404  cvmliftlem7  35507  fwddifnp1  36381  knoppcnlem6  36720  knoppcnlem8  36722  knoppcnlem9  36723  knoppcnlem11  36725  knoppcn  36726  knoppndvlem4  36737  knoppndvlem6  36739  knoppf  36757  poimirlem3  37874  poimirlem4  37875  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  heiborlem4  38065  heiborlem6  38067  lcmfunnnd  42382  mapfzcons  43073  irrapxlem1  43179  ltrmynn0  43305  ltrmxnn0  43306  acongeq  43340  jm2.23  43353  jm2.26lem3  43358  dfrtrcl3  44089  radcnvrat  44670  bcc0  44696  dvradcnv2  44703  binomcxplemnn0  44705  binomcxplemrat  44706  binomcxplemradcnv  44708  binomcxplemnotnn0  44712  fzssnn0  45678  rexanuz2nf  45850  expfac  46015  dvnmptdivc  46296  dvnmul  46301  dvnprodlem3  46306  stoweidlem17  46375  stoweidlem34  46392  stirlinglem5  46436  stirlinglem7  46438  fourierdlem15  46480  fourierdlem25  46490  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem52  46516  fourierdlem54  46518  fourierdlem64  46528  fourierdlem65  46529  fourierdlem81  46545  fourierdlem92  46556  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem113  46577  fourierdlem114  46578  elaa2lem  46591  etransclem4  46596  etransclem10  46602  etransclem14  46606  etransclem15  46607  etransclem23  46615  etransclem24  46616  etransclem31  46623  etransclem32  46624  etransclem35  46627  etransclem44  46636  etransclem46  46638  etransclem48  46640  chnerlem1  47240  chnerlem2  47241  ssnn0ssfz  48709  itcoval1  49023  itcoval2  49024  itcoval3  49025  itcovalsuc  49027  ackvalsuc1mpt  49038  aacllem  50160