Theorem nn0uz 12896

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  {crab 3423   class class class wbr 5110  ‘cfv 6533  0cc0 11096   ≤ cle 11240  ℕ₀cn0 12500  ℤcz 12587  ℤ_≥cuz 12858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-nn 12230  df-n0 12501  df-z 12588  df-uz 12859

This theorem is referenced by:  elnn0uz  12899  2eluzge0  12901  eluznn0  12937  nn0inf  12950  fseq1p1m1  13622  fznn0sub2  13659  nn0split  13667  prednn0  13676  fzossnn0  13715  fzennn  14000  hashgf1o  14003  exple1  14209  faclbnd4lem1  14325  bcval5  14350  bcpasc  14353  hashfzo0  14463  hashf1  14490  ccatval2  14611  ccatass  14622  ccatrn  14623  swrdccat2  14703  wrdeqs1cat  14753  cats1un  14754  splfv2a  14789  splval2  14790  revccat  14799  cats1fv  14892  binom1dif  15883  isumnn0nn  15892  climcndslem1  15899  climcnds  15901  harmonic  15909  arisum2  15911  explecnv  15915  geoser  15917  pwdif  15918  geolim  15920  geolim2  15921  geomulcvg  15926  geoisum  15927  geoisumr  15928  mertenslem1  15934  mertenslem2  15935  mertens  15936  fallfacfwd  16086  0fallfac  16087  binomfallfaclem2  16090  bpolylem  16098  bpolysum  16103  bpolydiflem  16104  fsumkthpow  16106  bpoly2  16107  bpoly3  16108  bpoly4  16109  efcllem  16127  ef0lem  16128  eff  16131  efcvg  16135  efcvgfsum  16136  reefcl  16137  ege2le3  16140  efcj  16142  eftlcvg  16158  eftlub  16161  effsumlt  16163  ef4p  16165  efgt1p2  16166  efgt1p  16167  eflegeo  16173  eirrlem  16256  ruclem6  16287  ruclem7  16288  divalglem2  16449  divalglem5  16451  bitsfzolem  16488  bitsfzo  16489  bitsfi  16491  bitsinv1lem  16495  bitsinv1  16496  bitsinvp1  16503  sadcf  16507  sadcp1  16509  sadadd  16521  sadass  16525  bitsres  16527  smupf  16532  smupp1  16534  smuval2  16536  smupval  16542  smueqlem  16544  smumul  16547  alginv  16629  algcvg  16630  algcvga  16633  algfx  16634  eucalgcvga  16640  eucalg  16641  phiprmpw  16831  prmdiv  16840  iserodd  16891  pcfac  16955  prmreclem2  16973  prmreclem4  16975  vdwapun  17030  vdwlem1  17037  ramcl2lem  17065  ramtcl  17066  ramtub  17068  chnccats1  18677  gsumwsubmcl  18892  gsumws1  18893  gsumsgrpccat  18895  gsumwmhm  18900  psgnunilem2  19561  psgnunilem4  19563  sylow1lem1  19664  efginvrel2  19793  efgredleme  19809  efgredlemc  19811  efgcpbllemb  19821  frgpuplem  19838  telgsumfz0s  20057  telgsums  20059  pgpfaclem1  20149  psrbaglefi  22041  ltbwe  22160  pmatcollpw3fi1lem1  22908  chfacfisf  22976  chfacfisfcpmat  22977  iscmet3lem3  25414  dyadmax  25722  mbfi1fseqlem3  25841  itgcnlem  25914  dvnff  26047  dvnp1  26049  dvn2bss  26054  cpncn  26060  dveflem  26103  ig1peu  26297  ig1pdvds  26302  ply1termlem  26325  plyeq0lem  26332  plyaddlem1  26335  plymullem1  26336  coeeulem  26346  dgrcl  26355  dgrub  26356  dgrlb  26358  coeid3  26362  plyco  26363  coeeq2  26364  coefv0  26370  coemulhi  26376  coemulc  26377  dvply1  26410  vieta1lem2  26437  vieta1  26438  elqaalem2  26446  elqaalem3  26447  geolim3  26465  dvntaylp  26496  taylthlem1  26498  radcnvlem1  26538  radcnvlem2  26539  radcnvlem3  26540  radcnv0  26541  radcnvlt2  26544  dvradcnv  26546  pserulm  26547  psercn2  26548  pserdvlem2  26553  pserdv2  26555  abelthlem4  26559  abelthlem5  26560  abelthlem6  26561  abelthlem7  26563  abelthlem8  26564  abelthlem9  26565  advlogexp  26782  logtayllem  26786  logtayl  26787  cxpeq  26884  leibpi  27069  leibpisum  27070  log2cnv  27071  log2tlbnd  27072  log2ublem2  27074  birthdaylem3  27080  wilthlem2  27195  ftalem1  27199  ftalem5  27203  basellem2  27208  basellem3  27209  basellem5  27211  musum  27317  0sgmppw  27324  1sgmprm  27325  chtublem  27337  logexprlim  27351  lgseisenlem1  27501  lgsquadlem2  27507  dchrisumlem1  27615  dchrisumlem2  27616  dchrisum0flblem1  27634  ostth2lem3  27761  tgcgr4  28762  clwwlknonex2lem1  30395  eupth2lems  30526  fz2ssnn0  33067  nn0diffz0  33076  nn0split01  33099  ccatws1f1o  33208  gsummulsubdishift1  33325  gsumwrd2dccat  33335  cycpmco2rn  33382  cycpmco2lem6  33388  evl1deg1  33807  evl1deg2  33808  evl1deg3  33809  ig1pmindeg  33833  vietalem  33910  exsslsb  33928  oddpwdc  34685  eulerpartlemb  34699  sseqfn  34721  sseqf  34723  signsplypnf  34878  signstcl  34893  signstf  34894  signstfvn  34897  signstfvneq0  34900  fsum2dsub  34935  reprsuc  34943  breprexplema  34958  breprexplemc  34960  subfacval2  35574  subfaclim  35575  cvmliftlem7  35678  fwddifnp1  36552  knoppcnlem6  36972  knoppcnlem8  36974  knoppcnlem9  36975  knoppcnlem11  36977  knoppcn  36978  knoppndvlem4  36989  knoppndvlem6  36991  knoppf  37009  poimirlem3  38157  poimirlem4  38158  poimirlem18  38172  poimirlem21  38175  poimirlem22  38176  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  heiborlem4  38348  heiborlem6  38350  lcmfunnnd  42664  mapfzcons  43332  irrapxlem1  43434  ltrmynn0  43560  ltrmxnn0  43561  acongeq  43595  jm2.23  43608  jm2.26lem3  43613  dfrtrcl3  44344  radcnvrat  44909  bcc0  44935  dvradcnv2  44942  binomcxplemnn0  44944  binomcxplemrat  44945  binomcxplemradcnv  44947  binomcxplemnotnn0  44951  fzssnn0  45920  rexanuz2nf  46091  expfac  46256  dvnmptdivc  46537  dvnmul  46542  dvnprodlem3  46547  stoweidlem17  46616  stoweidlem34  46633  stirlinglem5  46677  stirlinglem7  46679  fourierdlem15  46721  fourierdlem25  46731  fourierdlem48  46753  fourierdlem49  46754  fourierdlem50  46755  fourierdlem52  46757  fourierdlem54  46759  fourierdlem64  46769  fourierdlem65  46770  fourierdlem81  46786  fourierdlem92  46797  fourierdlem102  46807  fourierdlem103  46808  fourierdlem104  46809  fourierdlem113  46818  fourierdlem114  46819  elaa2lem  46832  etransclem4  46837  etransclem10  46843  etransclem14  46847  etransclem15  46848  etransclem23  46856  etransclem24  46857  etransclem31  46864  etransclem32  46865  etransclem35  46868  etransclem44  46877  etransclem46  46879  etransclem48  46881  chnerlem1  47483  chnerlem2  47484  ssnn0ssfz  49007  itcoval1  49321  itcoval2  49322  itcoval3  49323  itcovalsuc  49325  ackvalsuc1mpt  49336  aacllem  50457