Theorem nn0uz 12629

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  {crab 3069   class class class wbr 5075  ‘cfv 6437  0cc0 10880   ≤ cle 11019  ℕ₀cn0 12242  ℤcz 12328  ℤ_≥cuz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329  df-uz 12592

This theorem is referenced by:  elnn0uz  12632  2eluzge0  12642  eluznn0  12666  nn0inf  12679  fseq1p1m1  13339  fznn0sub2  13372  nn0split  13380  prednn0  13389  fzossnn0  13427  fzennn  13697  hashgf1o  13700  exple1  13903  faclbnd4lem1  14016  bcval5  14041  bcpasc  14044  hashfzo0  14154  hashf1  14180  ccatval2  14292  ccatass  14302  ccatrn  14303  swrdccat2  14391  wrdeqs1cat  14442  cats1un  14443  splfv2a  14478  splval2  14479  revccat  14488  cats1fv  14581  binom1dif  15554  isumnn0nn  15563  climcndslem1  15570  climcnds  15572  harmonic  15580  arisum2  15582  explecnv  15586  geoser  15588  pwdif  15589  geolim  15591  geolim2  15592  geomulcvg  15597  geoisum  15598  geoisumr  15599  mertenslem1  15605  mertenslem2  15606  mertens  15607  fallfacfwd  15755  0fallfac  15756  binomfallfaclem2  15759  bpolylem  15767  bpolysum  15772  bpolydiflem  15773  fsumkthpow  15775  bpoly2  15776  bpoly3  15777  bpoly4  15778  efcllem  15796  ef0lem  15797  eff  15800  efcvg  15803  efcvgfsum  15804  reefcl  15805  ege2le3  15808  efcj  15810  eftlcvg  15824  eftlub  15827  effsumlt  15829  ef4p  15831  efgt1p2  15832  efgt1p  15833  eflegeo  15839  eirrlem  15922  ruclem6  15953  ruclem7  15954  divalglem2  16113  divalglem5  16115  bitsfzolem  16150  bitsfzo  16151  bitsfi  16153  bitsinv1lem  16157  bitsinv1  16158  bitsinvp1  16165  sadcf  16169  sadcp1  16171  sadadd  16183  sadass  16187  bitsres  16189  smupf  16194  smupp1  16196  smuval2  16198  smupval  16204  smueqlem  16206  smumul  16209  alginv  16289  algcvg  16290  algcvga  16293  algfx  16294  eucalgcvga  16300  eucalg  16301  phiprmpw  16486  prmdiv  16495  iserodd  16545  pcfac  16609  prmreclem2  16627  prmreclem4  16629  vdwapun  16684  vdwlem1  16691  ramcl2lem  16719  ramtcl  16720  ramtub  16722  gsumwsubmcl  18484  gsumws1  18485  gsumsgrpccat  18487  gsumccatOLD  18488  gsumwmhm  18493  psgnunilem2  19112  psgnunilem4  19114  sylow1lem1  19212  efginvrel2  19342  efgredleme  19358  efgredlemc  19360  efgcpbllemb  19370  frgpuplem  19387  telgsumfz0s  19601  telgsums  19603  pgpfaclem1  19693  psrbaglefi  21144  psrbaglefiOLD  21145  ltbwe  21254  pmatcollpw3fi1lem1  21944  chfacfisf  22012  chfacfisfcpmat  22013  iscmet3lem3  24463  dyadmax  24771  mbfi1fseqlem3  24891  itgcnlem  24963  dvnff  25096  dvnp1  25098  dvn2bss  25103  cpncn  25109  dveflem  25152  ig1peu  25345  ig1pdvds  25350  ply1termlem  25373  plyeq0lem  25380  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  dgrcl  25403  dgrub  25404  dgrlb  25406  coeid3  25410  plyco  25411  coeeq2  25412  coefv0  25418  coemulhi  25424  coemulc  25425  dvply1  25453  vieta1lem2  25480  vieta1  25481  elqaalem2  25489  elqaalem3  25490  geolim3  25508  dvntaylp  25539  taylthlem1  25541  radcnvlem1  25581  radcnvlem2  25582  radcnvlem3  25583  radcnv0  25584  radcnvlt2  25587  dvradcnv  25589  pserulm  25590  psercn2  25591  pserdvlem2  25596  pserdv2  25598  abelthlem4  25602  abelthlem5  25603  abelthlem6  25604  abelthlem7  25606  abelthlem8  25607  abelthlem9  25608  advlogexp  25819  logtayllem  25823  logtayl  25824  cxpeq  25919  leibpi  26101  leibpisum  26102  log2cnv  26103  log2tlbnd  26104  log2ublem2  26106  birthdaylem3  26112  wilthlem2  26227  ftalem1  26231  ftalem5  26235  basellem2  26240  basellem3  26241  basellem5  26243  musum  26349  0sgmppw  26355  1sgmprm  26356  chtublem  26368  logexprlim  26382  lgseisenlem1  26532  lgsquadlem2  26538  dchrisumlem1  26646  dchrisumlem2  26647  dchrisum0flblem1  26665  ostth2lem3  26792  tgcgr4  26901  clwwlknonex2lem1  28480  eupth2lems  28611  fz2ssnn0  31115  cycpmco2rn  31401  cycpmco2lem6  31407  oddpwdc  32330  eulerpartlemb  32344  sseqfn  32366  sseqf  32368  signsplypnf  32538  signstcl  32553  signstf  32554  signstfvn  32557  signstfvneq0  32560  fsum2dsub  32596  reprsuc  32604  breprexplema  32619  breprexplemc  32621  subfacval2  33158  subfaclim  33159  cvmliftlem7  33262  fwddifnp1  34476  knoppcnlem6  34687  knoppcnlem8  34689  knoppcnlem9  34690  knoppcnlem11  34692  knoppcn  34693  knoppndvlem4  34704  knoppndvlem6  34706  knoppf  34724  poimirlem3  35789  poimirlem4  35790  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  heiborlem4  35981  heiborlem6  35983  lcmfunnnd  40027  mapfzcons  40545  irrapxlem1  40651  ltrmynn0  40777  ltrmxnn0  40778  acongeq  40812  jm2.23  40825  jm2.26lem3  40830  dfrtrcl3  41348  radcnvrat  41939  bcc0  41965  dvradcnv2  41972  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemradcnv  41977  binomcxplemnotnn0  41981  fzssnn0  42863  expfac  43205  dvnmptdivc  43486  dvnmul  43491  dvnprodlem3  43496  stoweidlem17  43565  stoweidlem34  43582  stirlinglem5  43626  stirlinglem7  43628  fourierdlem15  43670  fourierdlem25  43680  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem52  43706  fourierdlem54  43708  fourierdlem64  43718  fourierdlem65  43719  fourierdlem81  43735  fourierdlem92  43746  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem113  43767  fourierdlem114  43768  elaa2lem  43781  etransclem4  43786  etransclem10  43792  etransclem14  43796  etransclem15  43797  etransclem23  43805  etransclem24  43806  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem44  43826  etransclem46  43828  etransclem48  43830  ssnn0ssfz  45696  itcoval1  46020  itcoval2  46021  itcoval3  46022  itcovalsuc  46024  ackvalsuc1mpt  46035  aacllem  46516