Theorem nn0uz 12835

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3405   class class class wbr 5107  ‘cfv 6511  0cc0 11068   ≤ cle 11209  ℕ₀cn0 12442  ℤcz 12529  ℤ_≥cuz 12793

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530  df-uz 12794

This theorem is referenced by:  elnn0uz  12838  2eluzge0  12840  eluznn0  12876  nn0inf  12889  fseq1p1m1  13559  fznn0sub2  13596  nn0split  13604  prednn0  13613  fzossnn0  13651  fzennn  13933  hashgf1o  13936  exple1  14142  faclbnd4lem1  14258  bcval5  14283  bcpasc  14286  hashfzo0  14395  hashf1  14422  ccatval2  14543  ccatass  14553  ccatrn  14554  swrdccat2  14634  wrdeqs1cat  14685  cats1un  14686  splfv2a  14721  splval2  14722  revccat  14731  cats1fv  14825  binom1dif  15799  isumnn0nn  15808  climcndslem1  15815  climcnds  15817  harmonic  15825  arisum2  15827  explecnv  15831  geoser  15833  pwdif  15834  geolim  15836  geolim2  15837  geomulcvg  15842  geoisum  15843  geoisumr  15844  mertenslem1  15850  mertenslem2  15851  mertens  15852  fallfacfwd  16002  0fallfac  16003  binomfallfaclem2  16006  bpolylem  16014  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  bpoly2  16023  bpoly3  16024  bpoly4  16025  efcllem  16043  ef0lem  16044  eff  16047  efcvg  16051  efcvgfsum  16052  reefcl  16053  ege2le3  16056  efcj  16058  eftlcvg  16074  eftlub  16077  effsumlt  16079  ef4p  16081  efgt1p2  16082  efgt1p  16083  eflegeo  16089  eirrlem  16172  ruclem6  16203  ruclem7  16204  divalglem2  16365  divalglem5  16367  bitsfzolem  16404  bitsfzo  16405  bitsfi  16407  bitsinv1lem  16411  bitsinv1  16412  bitsinvp1  16419  sadcf  16423  sadcp1  16425  sadadd  16437  sadass  16441  bitsres  16443  smupf  16448  smupp1  16450  smuval2  16452  smupval  16458  smueqlem  16460  smumul  16463  alginv  16545  algcvg  16546  algcvga  16549  algfx  16550  eucalgcvga  16556  eucalg  16557  phiprmpw  16746  prmdiv  16755  iserodd  16806  pcfac  16870  prmreclem2  16888  prmreclem4  16890  vdwapun  16945  vdwlem1  16952  ramcl2lem  16980  ramtcl  16981  ramtub  16983  gsumwsubmcl  18764  gsumws1  18765  gsumsgrpccat  18767  gsumwmhm  18772  psgnunilem2  19425  psgnunilem4  19427  sylow1lem1  19528  efginvrel2  19657  efgredleme  19673  efgredlemc  19675  efgcpbllemb  19685  frgpuplem  19702  telgsumfz0s  19921  telgsums  19923  pgpfaclem1  20013  psrbaglefi  21835  ltbwe  21951  pmatcollpw3fi1lem1  22673  chfacfisf  22741  chfacfisfcpmat  22742  iscmet3lem3  25190  dyadmax  25499  mbfi1fseqlem3  25618  itgcnlem  25691  dvnff  25825  dvnp1  25827  dvn2bss  25832  cpncn  25838  dveflem  25883  ig1peu  26080  ig1pdvds  26085  ply1termlem  26108  plyeq0lem  26115  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  dgrcl  26138  dgrub  26139  dgrlb  26141  coeid3  26145  plyco  26146  coeeq2  26147  coefv0  26153  coemulhi  26159  coemulc  26160  dvply1  26191  vieta1lem2  26219  vieta1  26220  elqaalem2  26228  elqaalem3  26229  geolim3  26247  dvntaylp  26279  taylthlem1  26281  radcnvlem1  26322  radcnvlem2  26323  radcnvlem3  26324  radcnv0  26325  radcnvlt2  26328  dvradcnv  26330  pserulm  26331  psercn2  26332  psercn2OLD  26333  pserdvlem2  26338  pserdv2  26340  abelthlem4  26344  abelthlem5  26345  abelthlem6  26346  abelthlem7  26348  abelthlem8  26349  abelthlem9  26350  advlogexp  26564  logtayllem  26568  logtayl  26569  cxpeq  26667  leibpi  26852  leibpisum  26853  log2cnv  26854  log2tlbnd  26855  log2ublem2  26857  birthdaylem3  26863  wilthlem2  26979  ftalem1  26983  ftalem5  26987  basellem2  26992  basellem3  26993  basellem5  26995  musum  27101  0sgmppw  27109  1sgmprm  27110  chtublem  27122  logexprlim  27136  lgseisenlem1  27286  lgsquadlem2  27292  dchrisumlem1  27400  dchrisumlem2  27401  dchrisum0flblem1  27419  ostth2lem3  27546  tgcgr4  28458  clwwlknonex2lem1  30036  eupth2lems  30167  fz2ssnn0  32708  nn0split01  32742  ccatws1f1o  32873  chnccats1  32941  gsumwrd2dccat  33007  cycpmco2rn  33082  cycpmco2lem6  33088  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ig1pmindeg  33567  exsslsb  33592  oddpwdc  34345  eulerpartlemb  34359  sseqfn  34381  sseqf  34383  signsplypnf  34541  signstcl  34556  signstf  34557  signstfvn  34560  signstfvneq0  34563  fsum2dsub  34598  reprsuc  34606  breprexplema  34621  breprexplemc  34623  subfacval2  35174  subfaclim  35175  cvmliftlem7  35278  fwddifnp1  36153  knoppcnlem6  36486  knoppcnlem8  36488  knoppcnlem9  36489  knoppcnlem11  36491  knoppcn  36492  knoppndvlem4  36503  knoppndvlem6  36505  knoppf  36523  poimirlem3  37617  poimirlem4  37618  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  heiborlem4  37808  heiborlem6  37810  lcmfunnnd  42000  mapfzcons  42704  irrapxlem1  42810  ltrmynn0  42937  ltrmxnn0  42938  acongeq  42972  jm2.23  42985  jm2.26lem3  42990  dfrtrcl3  43722  radcnvrat  44303  bcc0  44329  dvradcnv2  44336  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemradcnv  44341  binomcxplemnotnn0  44345  fzssnn0  45314  rexanuz2nf  45488  expfac  45655  dvnmptdivc  45936  dvnmul  45941  dvnprodlem3  45946  stoweidlem17  46015  stoweidlem34  46032  stirlinglem5  46076  stirlinglem7  46078  fourierdlem15  46120  fourierdlem25  46130  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem52  46156  fourierdlem54  46158  fourierdlem64  46168  fourierdlem65  46169  fourierdlem81  46185  fourierdlem92  46196  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  fourierdlem114  46218  elaa2lem  46231  etransclem4  46236  etransclem10  46242  etransclem14  46246  etransclem15  46247  etransclem23  46255  etransclem24  46256  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem44  46276  etransclem46  46278  etransclem48  46280  ssnn0ssfz  48337  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667  aacllem  49790