Theorem nn0uz 12817

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  {crab 3391   class class class wbr 5072  ‘cfv 6485  0cc0 11029   ≤ cle 11171  ℕ₀cn0 12428  ℤcz 12515  ℤ_≥cuz 12779

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780

This theorem is referenced by:  elnn0uz  12820  2eluzge0  12822  eluznn0  12858  nn0inf  12871  fseq1p1m1  13543  fznn0sub2  13580  nn0split  13588  prednn0  13597  fzossnn0  13636  fzennn  13921  hashgf1o  13924  exple1  14130  faclbnd4lem1  14246  bcval5  14271  bcpasc  14274  hashfzo0  14383  hashf1  14410  ccatval2  14531  ccatass  14542  ccatrn  14543  swrdccat2  14623  wrdeqs1cat  14673  cats1un  14674  splfv2a  14709  splval2  14710  revccat  14719  cats1fv  14812  binom1dif  15789  isumnn0nn  15798  climcndslem1  15805  climcnds  15807  harmonic  15815  arisum2  15817  explecnv  15821  geoser  15823  pwdif  15824  geolim  15826  geolim2  15827  geomulcvg  15832  geoisum  15833  geoisumr  15834  mertenslem1  15840  mertenslem2  15841  mertens  15842  fallfacfwd  15992  0fallfac  15993  binomfallfaclem2  15996  bpolylem  16004  bpolysum  16009  bpolydiflem  16010  fsumkthpow  16012  bpoly2  16013  bpoly3  16014  bpoly4  16015  efcllem  16033  ef0lem  16034  eff  16037  efcvg  16041  efcvgfsum  16042  reefcl  16043  ege2le3  16046  efcj  16048  eftlcvg  16064  eftlub  16067  effsumlt  16069  ef4p  16071  efgt1p2  16072  efgt1p  16073  eflegeo  16079  eirrlem  16162  ruclem6  16193  ruclem7  16194  divalglem2  16355  divalglem5  16357  bitsfzolem  16394  bitsfzo  16395  bitsfi  16397  bitsinv1lem  16401  bitsinv1  16402  bitsinvp1  16409  sadcf  16413  sadcp1  16415  sadadd  16427  sadass  16431  bitsres  16433  smupf  16438  smupp1  16440  smuval2  16442  smupval  16448  smueqlem  16450  smumul  16453  alginv  16535  algcvg  16536  algcvga  16539  algfx  16540  eucalgcvga  16546  eucalg  16547  phiprmpw  16737  prmdiv  16746  iserodd  16797  pcfac  16861  prmreclem2  16879  prmreclem4  16881  vdwapun  16936  vdwlem1  16943  ramcl2lem  16971  ramtcl  16972  ramtub  16974  chnccats1  18582  gsumwsubmcl  18796  gsumws1  18797  gsumsgrpccat  18799  gsumwmhm  18804  psgnunilem2  19461  psgnunilem4  19463  sylow1lem1  19564  efginvrel2  19693  efgredleme  19709  efgredlemc  19711  efgcpbllemb  19721  frgpuplem  19738  telgsumfz0s  19957  telgsums  19959  pgpfaclem1  20049  psrbaglefi  21901  ltbwe  22020  pmatcollpw3fi1lem1  22769  chfacfisf  22837  chfacfisfcpmat  22838  iscmet3lem3  25275  dyadmax  25583  mbfi1fseqlem3  25702  itgcnlem  25775  dvnff  25908  dvnp1  25910  dvn2bss  25915  cpncn  25921  dveflem  25964  ig1peu  26158  ig1pdvds  26163  ply1termlem  26186  plyeq0lem  26193  plyaddlem1  26196  plymullem1  26197  coeeulem  26207  dgrcl  26216  dgrub  26217  dgrlb  26219  coeid3  26223  plyco  26224  coeeq2  26225  coefv0  26231  coemulhi  26237  coemulc  26238  dvply1  26268  vieta1lem2  26295  vieta1  26296  elqaalem2  26304  elqaalem3  26305  geolim3  26323  dvntaylp  26354  taylthlem1  26356  radcnvlem1  26396  radcnvlem2  26397  radcnvlem3  26398  radcnv0  26399  radcnvlt2  26402  dvradcnv  26404  pserulm  26405  psercn2  26406  pserdvlem2  26411  pserdv2  26413  abelthlem4  26417  abelthlem5  26418  abelthlem6  26419  abelthlem7  26421  abelthlem8  26422  abelthlem9  26423  advlogexp  26637  logtayllem  26641  logtayl  26642  cxpeq  26739  leibpi  26924  leibpisum  26925  log2cnv  26926  log2tlbnd  26927  log2ublem2  26929  birthdaylem3  26935  wilthlem2  27050  ftalem1  27054  ftalem5  27058  basellem2  27063  basellem3  27064  basellem5  27066  musum  27172  0sgmppw  27179  1sgmprm  27180  chtublem  27192  logexprlim  27206  lgseisenlem1  27356  lgsquadlem2  27362  dchrisumlem1  27470  dchrisumlem2  27471  dchrisum0flblem1  27489  ostth2lem3  27616  tgcgr4  28617  clwwlknonex2lem1  30195  eupth2lems  30326  fz2ssnn0  32877  nn0diffz0  32886  nn0split01  32910  ccatws1f1o  33030  gsummulsubdishift1  33149  gsumwrd2dccat  33159  cycpmco2rn  33206  cycpmco2lem6  33212  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ig1pmindeg  33685  vietalem  33763  exsslsb  33781  oddpwdc  34538  eulerpartlemb  34552  sseqfn  34574  sseqf  34576  signsplypnf  34734  signstcl  34749  signstf  34750  signstfvn  34753  signstfvneq0  34756  fsum2dsub  34791  reprsuc  34799  breprexplema  34814  breprexplemc  34816  subfacval2  35415  subfaclim  35416  cvmliftlem7  35519  fwddifnp1  36393  knoppcnlem6  36804  knoppcnlem8  36806  knoppcnlem9  36807  knoppcnlem11  36809  knoppcn  36810  knoppndvlem4  36821  knoppndvlem6  36823  knoppf  36841  poimirlem3  37990  poimirlem4  37991  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  heiborlem4  38181  heiborlem6  38183  lcmfunnnd  42497  mapfzcons  43165  irrapxlem1  43267  ltrmynn0  43393  ltrmxnn0  43394  acongeq  43428  jm2.23  43441  jm2.26lem3  43446  dfrtrcl3  44177  radcnvrat  44758  bcc0  44784  dvradcnv2  44791  binomcxplemnn0  44793  binomcxplemrat  44794  binomcxplemradcnv  44796  binomcxplemnotnn0  44800  fzssnn0  45764  rexanuz2nf  45935  expfac  46100  dvnmptdivc  46381  dvnmul  46386  dvnprodlem3  46391  stoweidlem17  46460  stoweidlem34  46477  stirlinglem5  46521  stirlinglem7  46523  fourierdlem15  46565  fourierdlem25  46575  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem52  46601  fourierdlem54  46603  fourierdlem64  46613  fourierdlem65  46614  fourierdlem81  46630  fourierdlem92  46641  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem113  46662  fourierdlem114  46663  elaa2lem  46676  etransclem4  46681  etransclem10  46687  etransclem14  46691  etransclem15  46692  etransclem23  46700  etransclem24  46701  etransclem31  46708  etransclem32  46709  etransclem35  46712  etransclem44  46721  etransclem46  46723  etransclem48  46725  chnerlem1  47327  chnerlem2  47328  ssnn0ssfz  48840  itcoval1  49154  itcoval2  49155  itcoval3  49156  itcovalsuc  49158  ackvalsuc1mpt  49169  aacllem  50291