Theorem nn0uz 12355

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

Syntax hints:   = wceq 1542   ∈ wcel 2113  {crab 3057   class class class wbr 5027  ‘cfv 6333  0cc0 10608   ≤ cle 10747  ℕ₀cn0 11969  ℤcz 12055  ℤ_≥cuz 12317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-n0 11970  df-z 12056  df-uz 12318

This theorem is referenced by:  elnn0uz  12358  2eluzge0  12368  eluznn0  12392  nn0inf  12405  fseq1p1m1  13065  fznn0sub2  13098  nn0split  13106  prednn0  13115  fzossnn0  13152  fzennn  13420  hashgf1o  13423  exple1  13625  faclbnd4lem1  13738  bcval5  13763  bcpasc  13766  hashfzo0  13876  hashf1  13902  ccatval2  14014  ccatass  14024  ccatrn  14025  swrdccat2  14113  wrdeqs1cat  14164  cats1un  14165  splfv2a  14200  splval2  14201  revccat  14210  cats1fv  14303  binom1dif  15274  isumnn0nn  15283  climcndslem1  15290  climcnds  15292  harmonic  15300  arisum2  15302  explecnv  15306  geoser  15308  pwdif  15309  geolim  15311  geolim2  15312  geomulcvg  15317  geoisum  15318  geoisumr  15319  mertenslem1  15325  mertenslem2  15326  mertens  15327  fallfacfwd  15475  0fallfac  15476  binomfallfaclem2  15479  bpolylem  15487  bpolysum  15492  bpolydiflem  15493  fsumkthpow  15495  bpoly2  15496  bpoly3  15497  bpoly4  15498  efcllem  15516  ef0lem  15517  eff  15520  efcvg  15523  efcvgfsum  15524  reefcl  15525  ege2le3  15528  efcj  15530  eftlcvg  15544  eftlub  15547  effsumlt  15549  ef4p  15551  efgt1p2  15552  efgt1p  15553  eflegeo  15559  eirrlem  15642  ruclem6  15673  ruclem7  15674  divalglem2  15833  divalglem5  15835  bitsfzolem  15870  bitsfzo  15871  bitsfi  15873  bitsinv1lem  15877  bitsinv1  15878  bitsinvp1  15885  sadcf  15889  sadcp1  15891  sadadd  15903  sadass  15907  bitsres  15909  smupf  15914  smupp1  15916  smuval2  15918  smupval  15924  smueqlem  15926  smumul  15929  alginv  16009  algcvg  16010  algcvga  16013  algfx  16014  eucalgcvga  16020  eucalg  16021  phiprmpw  16206  prmdiv  16215  iserodd  16265  pcfac  16328  prmreclem2  16346  prmreclem4  16348  vdwapun  16403  vdwlem1  16410  ramcl2lem  16438  ramtcl  16439  ramtub  16441  gsumwsubmcl  18110  gsumws1  18111  gsumsgrpccat  18113  gsumccatOLD  18114  gsumwmhm  18119  psgnunilem2  18734  psgnunilem4  18736  sylow1lem1  18834  efginvrel2  18964  efgredleme  18980  efgredlemc  18982  efgcpbllemb  18992  frgpuplem  19009  telgsumfz0s  19223  telgsums  19225  pgpfaclem1  19315  psrbaglefi  20738  psrbaglefiOLD  20739  ltbwe  20848  pmatcollpw3fi1lem1  21530  chfacfisf  21598  chfacfisfcpmat  21599  iscmet3lem3  24035  dyadmax  24343  mbfi1fseqlem3  24462  itgcnlem  24534  dvnff  24667  dvnp1  24669  dvn2bss  24674  cpncn  24680  dveflem  24723  ig1peu  24916  ig1pdvds  24921  ply1termlem  24944  plyeq0lem  24951  plyaddlem1  24954  plymullem1  24955  coeeulem  24965  dgrcl  24974  dgrub  24975  dgrlb  24977  coeid3  24981  plyco  24982  coeeq2  24983  coefv0  24989  coemulhi  24995  coemulc  24996  dvply1  25024  vieta1lem2  25051  vieta1  25052  elqaalem2  25060  elqaalem3  25061  geolim3  25079  dvntaylp  25110  taylthlem1  25112  radcnvlem1  25152  radcnvlem2  25153  radcnvlem3  25154  radcnv0  25155  radcnvlt2  25158  dvradcnv  25160  pserulm  25161  psercn2  25162  pserdvlem2  25167  pserdv2  25169  abelthlem4  25173  abelthlem5  25174  abelthlem6  25175  abelthlem7  25177  abelthlem8  25178  abelthlem9  25179  advlogexp  25390  logtayllem  25394  logtayl  25395  cxpeq  25490  leibpi  25672  leibpisum  25673  log2cnv  25674  log2tlbnd  25675  log2ublem2  25677  birthdaylem3  25683  wilthlem2  25798  ftalem1  25802  ftalem5  25806  basellem2  25811  basellem3  25812  basellem5  25814  musum  25920  0sgmppw  25926  1sgmprm  25927  chtublem  25939  logexprlim  25953  lgseisenlem1  26103  lgsquadlem2  26109  dchrisumlem1  26217  dchrisumlem2  26218  dchrisum0flblem1  26236  ostth2lem3  26363  tgcgr4  26469  clwwlknonex2lem1  28036  eupth2lems  28167  fz2ssnn0  30673  cycpmco2rn  30961  cycpmco2lem6  30967  oddpwdc  31883  eulerpartlemb  31897  sseqfn  31919  sseqf  31921  signsplypnf  32091  signstcl  32106  signstf  32107  signstfvn  32110  signstfvneq0  32113  fsum2dsub  32149  reprsuc  32157  breprexplema  32172  breprexplemc  32174  subfacval2  32712  subfaclim  32713  cvmliftlem7  32816  fwddifnp1  34097  knoppcnlem6  34308  knoppcnlem8  34310  knoppcnlem9  34311  knoppcnlem11  34313  knoppcn  34314  knoppndvlem4  34325  knoppndvlem6  34327  knoppf  34345  poimirlem3  35392  poimirlem4  35393  poimirlem18  35407  poimirlem21  35410  poimirlem22  35411  poimirlem25  35414  poimirlem26  35415  poimirlem27  35416  heiborlem4  35584  heiborlem6  35586  lcmfunnnd  39629  mapfzcons  40094  irrapxlem1  40200  ltrmynn0  40326  ltrmxnn0  40327  acongeq  40361  jm2.23  40374  jm2.26lem3  40379  dfrtrcl3  40871  radcnvrat  41454  bcc0  41480  dvradcnv2  41487  binomcxplemnn0  41489  binomcxplemrat  41490  binomcxplemradcnv  41492  binomcxplemnotnn0  41496  fzssnn0  42378  expfac  42724  dvnmptdivc  43005  dvnmul  43010  dvnprodlem3  43015  stoweidlem17  43084  stoweidlem34  43101  stirlinglem5  43145  stirlinglem7  43147  fourierdlem15  43189  fourierdlem25  43199  fourierdlem48  43221  fourierdlem49  43222  fourierdlem50  43223  fourierdlem52  43225  fourierdlem54  43227  fourierdlem64  43237  fourierdlem65  43238  fourierdlem81  43254  fourierdlem92  43265  fourierdlem102  43275  fourierdlem103  43276  fourierdlem104  43277  fourierdlem113  43286  fourierdlem114  43287  elaa2lem  43300  etransclem4  43305  etransclem10  43311  etransclem14  43315  etransclem15  43316  etransclem23  43324  etransclem24  43325  etransclem31  43332  etransclem32  43333  etransclem35  43336  etransclem44  43345  etransclem46  43347  etransclem48  43349  ssnn0ssfz  45203  itcoval1  45527  itcoval2  45528  itcoval3  45529  itcovalsuc  45531  ackvalsuc1mpt  45542  aacllem  45942