Theorem nn0uz 12780

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3396   class class class wbr 5095  ‘cfv 6489  0cc0 11017   ≤ cle 11158  ℕ₀cn0 12392  ℤcz 12479  ℤ_≥cuz 12742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-nn 12137  df-n0 12393  df-z 12480  df-uz 12743

This theorem is referenced by:  elnn0uz  12783  2eluzge0  12785  eluznn0  12821  nn0inf  12834  fseq1p1m1  13505  fznn0sub2  13542  nn0split  13550  prednn0  13559  fzossnn0  13597  fzennn  13882  hashgf1o  13885  exple1  14091  faclbnd4lem1  14207  bcval5  14232  bcpasc  14235  hashfzo0  14344  hashf1  14371  ccatval2  14492  ccatass  14503  ccatrn  14504  swrdccat2  14584  wrdeqs1cat  14634  cats1un  14635  splfv2a  14670  splval2  14671  revccat  14680  cats1fv  14773  binom1dif  15747  isumnn0nn  15756  climcndslem1  15763  climcnds  15765  harmonic  15773  arisum2  15775  explecnv  15779  geoser  15781  pwdif  15782  geolim  15784  geolim2  15785  geomulcvg  15790  geoisum  15791  geoisumr  15792  mertenslem1  15798  mertenslem2  15799  mertens  15800  fallfacfwd  15950  0fallfac  15951  binomfallfaclem2  15954  bpolylem  15962  bpolysum  15967  bpolydiflem  15968  fsumkthpow  15970  bpoly2  15971  bpoly3  15972  bpoly4  15973  efcllem  15991  ef0lem  15992  eff  15995  efcvg  15999  efcvgfsum  16000  reefcl  16001  ege2le3  16004  efcj  16006  eftlcvg  16022  eftlub  16025  effsumlt  16027  ef4p  16029  efgt1p2  16030  efgt1p  16031  eflegeo  16037  eirrlem  16120  ruclem6  16151  ruclem7  16152  divalglem2  16313  divalglem5  16315  bitsfzolem  16352  bitsfzo  16353  bitsfi  16355  bitsinv1lem  16359  bitsinv1  16360  bitsinvp1  16367  sadcf  16371  sadcp1  16373  sadadd  16385  sadass  16389  bitsres  16391  smupf  16396  smupp1  16398  smuval2  16400  smupval  16406  smueqlem  16408  smumul  16411  alginv  16493  algcvg  16494  algcvga  16497  algfx  16498  eucalgcvga  16504  eucalg  16505  phiprmpw  16694  prmdiv  16703  iserodd  16754  pcfac  16818  prmreclem2  16836  prmreclem4  16838  vdwapun  16893  vdwlem1  16900  ramcl2lem  16928  ramtcl  16929  ramtub  16931  chnccats1  18539  gsumwsubmcl  18753  gsumws1  18754  gsumsgrpccat  18756  gsumwmhm  18761  psgnunilem2  19415  psgnunilem4  19417  sylow1lem1  19518  efginvrel2  19647  efgredleme  19663  efgredlemc  19665  efgcpbllemb  19675  frgpuplem  19692  telgsumfz0s  19911  telgsums  19913  pgpfaclem1  20003  psrbaglefi  21873  ltbwe  21990  pmatcollpw3fi1lem1  22721  chfacfisf  22789  chfacfisfcpmat  22790  iscmet3lem3  25237  dyadmax  25546  mbfi1fseqlem3  25665  itgcnlem  25738  dvnff  25872  dvnp1  25874  dvn2bss  25879  cpncn  25885  dveflem  25930  ig1peu  26127  ig1pdvds  26132  ply1termlem  26155  plyeq0lem  26162  plyaddlem1  26165  plymullem1  26166  coeeulem  26176  dgrcl  26185  dgrub  26186  dgrlb  26188  coeid3  26192  plyco  26193  coeeq2  26194  coefv0  26200  coemulhi  26206  coemulc  26207  dvply1  26238  vieta1lem2  26266  vieta1  26267  elqaalem2  26275  elqaalem3  26276  geolim3  26294  dvntaylp  26326  taylthlem1  26328  radcnvlem1  26369  radcnvlem2  26370  radcnvlem3  26371  radcnv0  26372  radcnvlt2  26375  dvradcnv  26377  pserulm  26378  psercn2  26379  psercn2OLD  26380  pserdvlem2  26385  pserdv2  26387  abelthlem4  26391  abelthlem5  26392  abelthlem6  26393  abelthlem7  26395  abelthlem8  26396  abelthlem9  26397  advlogexp  26611  logtayllem  26615  logtayl  26616  cxpeq  26714  leibpi  26899  leibpisum  26900  log2cnv  26901  log2tlbnd  26902  log2ublem2  26904  birthdaylem3  26910  wilthlem2  27026  ftalem1  27030  ftalem5  27034  basellem2  27039  basellem3  27040  basellem5  27042  musum  27148  0sgmppw  27156  1sgmprm  27157  chtublem  27169  logexprlim  27183  lgseisenlem1  27333  lgsquadlem2  27339  dchrisumlem1  27447  dchrisumlem2  27448  dchrisum0flblem1  27466  ostth2lem3  27593  tgcgr4  28529  clwwlknonex2lem1  30108  eupth2lems  30239  fz2ssnn0  32793  nn0diffz0  32802  nn0split01  32826  ccatws1f1o  32961  gsummulsubdishift1  33079  gsumwrd2dccat  33088  cycpmco2rn  33135  cycpmco2lem6  33141  evl1deg1  33585  evl1deg2  33586  evl1deg3  33587  ig1pmindeg  33611  vietalem  33663  exsslsb  33681  oddpwdc  34439  eulerpartlemb  34453  sseqfn  34475  sseqf  34477  signsplypnf  34635  signstcl  34650  signstf  34651  signstfvn  34654  signstfvneq0  34657  fsum2dsub  34692  reprsuc  34700  breprexplema  34715  breprexplemc  34717  subfacval2  35303  subfaclim  35304  cvmliftlem7  35407  fwddifnp1  36281  knoppcnlem6  36614  knoppcnlem8  36616  knoppcnlem9  36617  knoppcnlem11  36619  knoppcn  36620  knoppndvlem4  36631  knoppndvlem6  36633  knoppf  36651  poimirlem3  37736  poimirlem4  37737  poimirlem18  37751  poimirlem21  37754  poimirlem22  37755  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  heiborlem4  37927  heiborlem6  37929  lcmfunnnd  42178  mapfzcons  42873  irrapxlem1  42979  ltrmynn0  43105  ltrmxnn0  43106  acongeq  43140  jm2.23  43153  jm2.26lem3  43158  dfrtrcl3  43890  radcnvrat  44471  bcc0  44497  dvradcnv2  44504  binomcxplemnn0  44506  binomcxplemrat  44507  binomcxplemradcnv  44509  binomcxplemnotnn0  44513  fzssnn0  45480  rexanuz2nf  45652  expfac  45817  dvnmptdivc  46098  dvnmul  46103  dvnprodlem3  46108  stoweidlem17  46177  stoweidlem34  46194  stirlinglem5  46238  stirlinglem7  46240  fourierdlem15  46282  fourierdlem25  46292  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem52  46318  fourierdlem54  46320  fourierdlem64  46330  fourierdlem65  46331  fourierdlem81  46347  fourierdlem92  46358  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem113  46379  fourierdlem114  46380  elaa2lem  46393  etransclem4  46398  etransclem10  46404  etransclem14  46408  etransclem15  46409  etransclem23  46417  etransclem24  46418  etransclem31  46425  etransclem32  46426  etransclem35  46429  etransclem44  46438  etransclem46  46440  etransclem48  46442  chnerlem1  47042  chnerlem2  47043  ssnn0ssfz  48511  itcoval1  48825  itcoval2  48826  itcoval3  48827  itcovalsuc  48829  ackvalsuc1mpt  48840  aacllem  49962