Theorem nn0uz 12892

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3415   class class class wbr 5119  ‘cfv 6530  0cc0 11127   ≤ cle 11268  ℕ₀cn0 12499  ℤcz 12586  ℤ_≥cuz 12850

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-n0 12500  df-z 12587  df-uz 12851

This theorem is referenced by:  elnn0uz  12895  2eluzge0  12907  eluznn0  12931  nn0inf  12944  fseq1p1m1  13613  fznn0sub2  13650  nn0split  13658  prednn0  13667  fzossnn0  13705  fzennn  13984  hashgf1o  13987  exple1  14193  faclbnd4lem1  14309  bcval5  14334  bcpasc  14337  hashfzo0  14446  hashf1  14473  ccatval2  14594  ccatass  14604  ccatrn  14605  swrdccat2  14685  wrdeqs1cat  14736  cats1un  14737  splfv2a  14772  splval2  14773  revccat  14782  cats1fv  14876  binom1dif  15847  isumnn0nn  15856  climcndslem1  15863  climcnds  15865  harmonic  15873  arisum2  15875  explecnv  15879  geoser  15881  pwdif  15882  geolim  15884  geolim2  15885  geomulcvg  15890  geoisum  15891  geoisumr  15892  mertenslem1  15898  mertenslem2  15899  mertens  15900  fallfacfwd  16050  0fallfac  16051  binomfallfaclem2  16054  bpolylem  16062  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  bpoly2  16071  bpoly3  16072  bpoly4  16073  efcllem  16091  ef0lem  16092  eff  16095  efcvg  16099  efcvgfsum  16100  reefcl  16101  ege2le3  16104  efcj  16106  eftlcvg  16122  eftlub  16125  effsumlt  16127  ef4p  16129  efgt1p2  16130  efgt1p  16131  eflegeo  16137  eirrlem  16220  ruclem6  16251  ruclem7  16252  divalglem2  16412  divalglem5  16414  bitsfzolem  16451  bitsfzo  16452  bitsfi  16454  bitsinv1lem  16458  bitsinv1  16459  bitsinvp1  16466  sadcf  16470  sadcp1  16472  sadadd  16484  sadass  16488  bitsres  16490  smupf  16495  smupp1  16497  smuval2  16499  smupval  16505  smueqlem  16507  smumul  16510  alginv  16592  algcvg  16593  algcvga  16596  algfx  16597  eucalgcvga  16603  eucalg  16604  phiprmpw  16793  prmdiv  16802  iserodd  16853  pcfac  16917  prmreclem2  16935  prmreclem4  16937  vdwapun  16992  vdwlem1  16999  ramcl2lem  17027  ramtcl  17028  ramtub  17030  gsumwsubmcl  18813  gsumws1  18814  gsumsgrpccat  18816  gsumwmhm  18821  psgnunilem2  19474  psgnunilem4  19476  sylow1lem1  19577  efginvrel2  19706  efgredleme  19722  efgredlemc  19724  efgcpbllemb  19734  frgpuplem  19751  telgsumfz0s  19970  telgsums  19972  pgpfaclem1  20062  psrbaglefi  21884  ltbwe  22000  pmatcollpw3fi1lem1  22722  chfacfisf  22790  chfacfisfcpmat  22791  iscmet3lem3  25240  dyadmax  25549  mbfi1fseqlem3  25668  itgcnlem  25741  dvnff  25875  dvnp1  25877  dvn2bss  25882  cpncn  25888  dveflem  25933  ig1peu  26130  ig1pdvds  26135  ply1termlem  26158  plyeq0lem  26165  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  dgrcl  26188  dgrub  26189  dgrlb  26191  coeid3  26195  plyco  26196  coeeq2  26197  coefv0  26203  coemulhi  26209  coemulc  26210  dvply1  26241  vieta1lem2  26269  vieta1  26270  elqaalem2  26278  elqaalem3  26279  geolim3  26297  dvntaylp  26329  taylthlem1  26331  radcnvlem1  26372  radcnvlem2  26373  radcnvlem3  26374  radcnv0  26375  radcnvlt2  26378  dvradcnv  26380  pserulm  26381  psercn2  26382  psercn2OLD  26383  pserdvlem2  26388  pserdv2  26390  abelthlem4  26394  abelthlem5  26395  abelthlem6  26396  abelthlem7  26398  abelthlem8  26399  abelthlem9  26400  advlogexp  26614  logtayllem  26618  logtayl  26619  cxpeq  26717  leibpi  26902  leibpisum  26903  log2cnv  26904  log2tlbnd  26905  log2ublem2  26907  birthdaylem3  26913  wilthlem2  27029  ftalem1  27033  ftalem5  27037  basellem2  27042  basellem3  27043  basellem5  27045  musum  27151  0sgmppw  27159  1sgmprm  27160  chtublem  27172  logexprlim  27186  lgseisenlem1  27336  lgsquadlem2  27342  dchrisumlem1  27450  dchrisumlem2  27451  dchrisum0flblem1  27469  ostth2lem3  27596  tgcgr4  28456  clwwlknonex2lem1  30034  eupth2lems  30165  fz2ssnn0  32708  nn0split01  32742  ccatws1f1o  32873  chnccats1  32941  gsumwrd2dccat  33007  cycpmco2rn  33082  cycpmco2lem6  33088  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  ig1pmindeg  33557  exsslsb  33582  oddpwdc  34332  eulerpartlemb  34346  sseqfn  34368  sseqf  34370  signsplypnf  34528  signstcl  34543  signstf  34544  signstfvn  34547  signstfvneq0  34550  fsum2dsub  34585  reprsuc  34593  breprexplema  34608  breprexplemc  34610  subfacval2  35155  subfaclim  35156  cvmliftlem7  35259  fwddifnp1  36129  knoppcnlem6  36462  knoppcnlem8  36464  knoppcnlem9  36465  knoppcnlem11  36467  knoppcn  36468  knoppndvlem4  36479  knoppndvlem6  36481  knoppf  36499  poimirlem3  37593  poimirlem4  37594  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  heiborlem4  37784  heiborlem6  37786  lcmfunnnd  41971  mapfzcons  42686  irrapxlem1  42792  ltrmynn0  42919  ltrmxnn0  42920  acongeq  42954  jm2.23  42967  jm2.26lem3  42972  dfrtrcl3  43704  radcnvrat  44286  bcc0  44312  dvradcnv2  44319  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemradcnv  44324  binomcxplemnotnn0  44328  fzssnn0  45293  rexanuz2nf  45467  expfac  45634  dvnmptdivc  45915  dvnmul  45920  dvnprodlem3  45925  stoweidlem17  45994  stoweidlem34  46011  stirlinglem5  46055  stirlinglem7  46057  fourierdlem15  46099  fourierdlem25  46109  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem52  46135  fourierdlem54  46137  fourierdlem64  46147  fourierdlem65  46148  fourierdlem81  46164  fourierdlem92  46175  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem113  46196  fourierdlem114  46197  elaa2lem  46210  etransclem4  46215  etransclem10  46221  etransclem14  46225  etransclem15  46226  etransclem23  46234  etransclem24  46235  etransclem31  46242  etransclem32  46243  etransclem35  46246  etransclem44  46255  etransclem46  46257  etransclem48  46259  ssnn0ssfz  48272  itcoval1  48591  itcoval2  48592  itcoval3  48593  itcovalsuc  48595  ackvalsuc1mpt  48606  aacllem  49613