Theorem nn0uz 12920

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 12646	. 2 ⊢ ℕ0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2		0z 12624	. . 3 ⊢ 0 ∈ ℤ
3		uzval 12880	. . 3 ⊢ (0 ∈ ℤ → (ℤ≥‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
4	2, 3	ax-mp 5	. 2 ⊢ (ℤ≥‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
5	1, 4	eqtr4i 2768	1 ⊢ ℕ0 = (ℤ≥‘0)

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3436   class class class wbr 5143  ‘cfv 6561  0cc0 11155   ≤ cle 11296  ℕ₀cn0 12526  ℤcz 12613  ℤ_≥cuz 12878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879

This theorem is referenced by:  elnn0uz  12923  2eluzge0  12935  eluznn0  12959  nn0inf  12972  fseq1p1m1  13638  fznn0sub2  13675  nn0split  13683  prednn0  13692  fzossnn0  13730  fzennn  14009  hashgf1o  14012  exple1  14216  faclbnd4lem1  14332  bcval5  14357  bcpasc  14360  hashfzo0  14469  hashf1  14496  ccatval2  14616  ccatass  14626  ccatrn  14627  swrdccat2  14707  wrdeqs1cat  14758  cats1un  14759  splfv2a  14794  splval2  14795  revccat  14804  cats1fv  14898  binom1dif  15869  isumnn0nn  15878  climcndslem1  15885  climcnds  15887  harmonic  15895  arisum2  15897  explecnv  15901  geoser  15903  pwdif  15904  geolim  15906  geolim2  15907  geomulcvg  15912  geoisum  15913  geoisumr  15914  mertenslem1  15920  mertenslem2  15921  mertens  15922  fallfacfwd  16072  0fallfac  16073  binomfallfaclem2  16076  bpolylem  16084  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  bpoly2  16093  bpoly3  16094  bpoly4  16095  efcllem  16113  ef0lem  16114  eff  16117  efcvg  16121  efcvgfsum  16122  reefcl  16123  ege2le3  16126  efcj  16128  eftlcvg  16142  eftlub  16145  effsumlt  16147  ef4p  16149  efgt1p2  16150  efgt1p  16151  eflegeo  16157  eirrlem  16240  ruclem6  16271  ruclem7  16272  divalglem2  16432  divalglem5  16434  bitsfzolem  16471  bitsfzo  16472  bitsfi  16474  bitsinv1lem  16478  bitsinv1  16479  bitsinvp1  16486  sadcf  16490  sadcp1  16492  sadadd  16504  sadass  16508  bitsres  16510  smupf  16515  smupp1  16517  smuval2  16519  smupval  16525  smueqlem  16527  smumul  16530  alginv  16612  algcvg  16613  algcvga  16616  algfx  16617  eucalgcvga  16623  eucalg  16624  phiprmpw  16813  prmdiv  16822  iserodd  16873  pcfac  16937  prmreclem2  16955  prmreclem4  16957  vdwapun  17012  vdwlem1  17019  ramcl2lem  17047  ramtcl  17048  ramtub  17050  gsumwsubmcl  18850  gsumws1  18851  gsumsgrpccat  18853  gsumwmhm  18858  psgnunilem2  19513  psgnunilem4  19515  sylow1lem1  19616  efginvrel2  19745  efgredleme  19761  efgredlemc  19763  efgcpbllemb  19773  frgpuplem  19790  telgsumfz0s  20009  telgsums  20011  pgpfaclem1  20101  psrbaglefi  21946  ltbwe  22062  pmatcollpw3fi1lem1  22792  chfacfisf  22860  chfacfisfcpmat  22861  iscmet3lem3  25324  dyadmax  25633  mbfi1fseqlem3  25752  itgcnlem  25825  dvnff  25959  dvnp1  25961  dvn2bss  25966  cpncn  25972  dveflem  26017  ig1peu  26214  ig1pdvds  26219  ply1termlem  26242  plyeq0lem  26249  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  dgrcl  26272  dgrub  26273  dgrlb  26275  coeid3  26279  plyco  26280  coeeq2  26281  coefv0  26287  coemulhi  26293  coemulc  26294  dvply1  26325  vieta1lem2  26353  vieta1  26354  elqaalem2  26362  elqaalem3  26363  geolim3  26381  dvntaylp  26413  taylthlem1  26415  radcnvlem1  26456  radcnvlem2  26457  radcnvlem3  26458  radcnv0  26459  radcnvlt2  26462  dvradcnv  26464  pserulm  26465  psercn2  26466  psercn2OLD  26467  pserdvlem2  26472  pserdv2  26474  abelthlem4  26478  abelthlem5  26479  abelthlem6  26480  abelthlem7  26482  abelthlem8  26483  abelthlem9  26484  advlogexp  26697  logtayllem  26701  logtayl  26702  cxpeq  26800  leibpi  26985  leibpisum  26986  log2cnv  26987  log2tlbnd  26988  log2ublem2  26990  birthdaylem3  26996  wilthlem2  27112  ftalem1  27116  ftalem5  27120  basellem2  27125  basellem3  27126  basellem5  27128  musum  27234  0sgmppw  27242  1sgmprm  27243  chtublem  27255  logexprlim  27269  lgseisenlem1  27419  lgsquadlem2  27425  dchrisumlem1  27533  dchrisumlem2  27534  dchrisum0flblem1  27552  ostth2lem3  27679  tgcgr4  28539  clwwlknonex2lem1  30126  eupth2lems  30257  fz2ssnn0  32787  nn0split01  32819  ccatws1f1o  32936  chnccats1  33005  gsumwrd2dccat  33070  cycpmco2rn  33145  cycpmco2lem6  33151  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  ig1pmindeg  33622  exsslsb  33647  oddpwdc  34356  eulerpartlemb  34370  sseqfn  34392  sseqf  34394  signsplypnf  34565  signstcl  34580  signstf  34581  signstfvn  34584  signstfvneq0  34587  fsum2dsub  34622  reprsuc  34630  breprexplema  34645  breprexplemc  34647  subfacval2  35192  subfaclim  35193  cvmliftlem7  35296  fwddifnp1  36166  knoppcnlem6  36499  knoppcnlem8  36501  knoppcnlem9  36502  knoppcnlem11  36504  knoppcn  36505  knoppndvlem4  36516  knoppndvlem6  36518  knoppf  36536  poimirlem3  37630  poimirlem4  37631  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  heiborlem4  37821  heiborlem6  37823  lcmfunnnd  42013  mapfzcons  42727  irrapxlem1  42833  ltrmynn0  42960  ltrmxnn0  42961  acongeq  42995  jm2.23  43008  jm2.26lem3  43013  dfrtrcl3  43746  radcnvrat  44333  bcc0  44359  dvradcnv2  44366  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemradcnv  44371  binomcxplemnotnn0  44375  fzssnn0  45329  rexanuz2nf  45503  expfac  45672  dvnmptdivc  45953  dvnmul  45958  dvnprodlem3  45963  stoweidlem17  46032  stoweidlem34  46049  stirlinglem5  46093  stirlinglem7  46095  fourierdlem15  46137  fourierdlem25  46147  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem52  46173  fourierdlem54  46175  fourierdlem64  46185  fourierdlem65  46186  fourierdlem81  46202  fourierdlem92  46213  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  fourierdlem114  46235  elaa2lem  46248  etransclem4  46253  etransclem10  46259  etransclem14  46263  etransclem15  46264  etransclem23  46272  etransclem24  46273  etransclem31  46280  etransclem32  46281  etransclem35  46284  etransclem44  46293  etransclem46  46295  etransclem48  46297  ssnn0ssfz  48265  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsuc  48588  ackvalsuc1mpt  48599  aacllem  49320