Theorem nn0uz 12817

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 12547	. 2 ⊢ ℕ0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2		0z 12526	. . 3 ⊢ 0 ∈ ℤ
3		uzval 12781	. . 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 3390   class class class wbr 5086  ‘cfv 6492  0cc0 11029   ≤ cle 11171  ℕ₀cn0 12428  ℤcz 12515  ℤ_≥cuz 12779

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 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

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 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780

This theorem is referenced by:  elnn0uz  12820  2eluzge0  12822  eluznn0  12858  nn0inf  12871  fseq1p1m1  13543  fznn0sub2  13580  nn0split  13588  prednn0  13597  fzossnn0  13636  fzennn  13921  hashgf1o  13924  exple1  14130  faclbnd4lem1  14246  bcval5  14271  bcpasc  14274  hashfzo0  14383  hashf1  14410  ccatval2  14531  ccatass  14542  ccatrn  14543  swrdccat2  14623  wrdeqs1cat  14673  cats1un  14674  splfv2a  14709  splval2  14710  revccat  14719  cats1fv  14812  binom1dif  15789  isumnn0nn  15798  climcndslem1  15805  climcnds  15807  harmonic  15815  arisum2  15817  explecnv  15821  geoser  15823  pwdif  15824  geolim  15826  geolim2  15827  geomulcvg  15832  geoisum  15833  geoisumr  15834  mertenslem1  15840  mertenslem2  15841  mertens  15842  fallfacfwd  15992  0fallfac  15993  binomfallfaclem2  15996  bpolylem  16004  bpolysum  16009  bpolydiflem  16010  fsumkthpow  16012  bpoly2  16013  bpoly3  16014  bpoly4  16015  efcllem  16033  ef0lem  16034  eff  16037  efcvg  16041  efcvgfsum  16042  reefcl  16043  ege2le3  16046  efcj  16048  eftlcvg  16064  eftlub  16067  effsumlt  16069  ef4p  16071  efgt1p2  16072  efgt1p  16073  eflegeo  16079  eirrlem  16162  ruclem6  16193  ruclem7  16194  divalglem2  16355  divalglem5  16357  bitsfzolem  16394  bitsfzo  16395  bitsfi  16397  bitsinv1lem  16401  bitsinv1  16402  bitsinvp1  16409  sadcf  16413  sadcp1  16415  sadadd  16427  sadass  16431  bitsres  16433  smupf  16438  smupp1  16440  smuval2  16442  smupval  16448  smueqlem  16450  smumul  16453  alginv  16535  algcvg  16536  algcvga  16539  algfx  16540  eucalgcvga  16546  eucalg  16547  phiprmpw  16737  prmdiv  16746  iserodd  16797  pcfac  16861  prmreclem2  16879  prmreclem4  16881  vdwapun  16936  vdwlem1  16943  ramcl2lem  16971  ramtcl  16972  ramtub  16974  chnccats1  18582  gsumwsubmcl  18796  gsumws1  18797  gsumsgrpccat  18799  gsumwmhm  18804  psgnunilem2  19461  psgnunilem4  19463  sylow1lem1  19564  efginvrel2  19693  efgredleme  19709  efgredlemc  19711  efgcpbllemb  19721  frgpuplem  19738  telgsumfz0s  19957  telgsums  19959  pgpfaclem1  20049  psrbaglefi  21916  ltbwe  22032  pmatcollpw3fi1lem1  22761  chfacfisf  22829  chfacfisfcpmat  22830  iscmet3lem3  25267  dyadmax  25575  mbfi1fseqlem3  25694  itgcnlem  25767  dvnff  25900  dvnp1  25902  dvn2bss  25907  cpncn  25913  dveflem  25956  ig1peu  26150  ig1pdvds  26155  ply1termlem  26178  plyeq0lem  26185  plyaddlem1  26188  plymullem1  26189  coeeulem  26199  dgrcl  26208  dgrub  26209  dgrlb  26211  coeid3  26215  plyco  26216  coeeq2  26217  coefv0  26223  coemulhi  26229  coemulc  26230  dvply1  26260  vieta1lem2  26288  vieta1  26289  elqaalem2  26297  elqaalem3  26298  geolim3  26316  dvntaylp  26348  taylthlem1  26350  radcnvlem1  26391  radcnvlem2  26392  radcnvlem3  26393  radcnv0  26394  radcnvlt2  26397  dvradcnv  26399  pserulm  26400  psercn2  26401  pserdvlem2  26406  pserdv2  26408  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  advlogexp  26632  logtayllem  26636  logtayl  26637  cxpeq  26734  leibpi  26919  leibpisum  26920  log2cnv  26921  log2tlbnd  26922  log2ublem2  26924  birthdaylem3  26930  wilthlem2  27046  ftalem1  27050  ftalem5  27054  basellem2  27059  basellem3  27060  basellem5  27062  musum  27168  0sgmppw  27175  1sgmprm  27176  chtublem  27188  logexprlim  27202  lgseisenlem1  27352  lgsquadlem2  27358  dchrisumlem1  27466  dchrisumlem2  27467  dchrisum0flblem1  27485  ostth2lem3  27612  tgcgr4  28613  clwwlknonex2lem1  30192  eupth2lems  30323  fz2ssnn0  32873  nn0diffz0  32882  nn0split01  32906  ccatws1f1o  33026  gsummulsubdishift1  33144  gsumwrd2dccat  33154  cycpmco2rn  33201  cycpmco2lem6  33207  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  ig1pmindeg  33677  vietalem  33738  exsslsb  33756  oddpwdc  34514  eulerpartlemb  34528  sseqfn  34550  sseqf  34552  signsplypnf  34710  signstcl  34725  signstf  34726  signstfvn  34729  signstfvneq0  34732  fsum2dsub  34767  reprsuc  34775  breprexplema  34790  breprexplemc  34792  subfacval2  35385  subfaclim  35386  cvmliftlem7  35489  fwddifnp1  36363  knoppcnlem6  36774  knoppcnlem8  36776  knoppcnlem9  36777  knoppcnlem11  36779  knoppcn  36780  knoppndvlem4  36791  knoppndvlem6  36793  knoppf  36811  poimirlem3  37958  poimirlem4  37959  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  heiborlem4  38149  heiborlem6  38151  lcmfunnnd  42465  mapfzcons  43162  irrapxlem1  43268  ltrmynn0  43394  ltrmxnn0  43395  acongeq  43429  jm2.23  43442  jm2.26lem3  43447  dfrtrcl3  44178  radcnvrat  44759  bcc0  44785  dvradcnv2  44792  binomcxplemnn0  44794  binomcxplemrat  44795  binomcxplemradcnv  44797  binomcxplemnotnn0  44801  fzssnn0  45767  rexanuz2nf  45938  expfac  46103  dvnmptdivc  46384  dvnmul  46389  dvnprodlem3  46394  stoweidlem17  46463  stoweidlem34  46480  stirlinglem5  46524  stirlinglem7  46526  fourierdlem15  46568  fourierdlem25  46578  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem52  46604  fourierdlem54  46606  fourierdlem64  46616  fourierdlem65  46617  fourierdlem81  46633  fourierdlem92  46644  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  fourierdlem114  46666  elaa2lem  46679  etransclem4  46684  etransclem10  46690  etransclem14  46694  etransclem15  46695  etransclem23  46703  etransclem24  46704  etransclem31  46711  etransclem32  46712  etransclem35  46715  etransclem44  46724  etransclem46  46726  etransclem48  46728  chnerlem1  47328  chnerlem2  47329  ssnn0ssfz  48837  itcoval1  49151  itcoval2  49152  itcoval3  49153  itcovalsuc  49155  ackvalsuc1mpt  49166  aacllem  50288