Theorem nn0uz 12917

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  {crab 3432   class class class wbr 5147  ‘cfv 6562  0cc0 11152   ≤ cle 11293  ℕ₀cn0 12523  ℤcz 12610  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611  df-uz 12876

This theorem is referenced by:  elnn0uz  12920  2eluzge0  12932  eluznn0  12956  nn0inf  12969  fseq1p1m1  13634  fznn0sub2  13671  nn0split  13679  prednn0  13688  fzossnn0  13726  fzennn  14005  hashgf1o  14008  exple1  14212  faclbnd4lem1  14328  bcval5  14353  bcpasc  14356  hashfzo0  14465  hashf1  14492  ccatval2  14612  ccatass  14622  ccatrn  14623  swrdccat2  14703  wrdeqs1cat  14754  cats1un  14755  splfv2a  14790  splval2  14791  revccat  14800  cats1fv  14894  binom1dif  15865  isumnn0nn  15874  climcndslem1  15881  climcnds  15883  harmonic  15891  arisum2  15893  explecnv  15897  geoser  15899  pwdif  15900  geolim  15902  geolim2  15903  geomulcvg  15908  geoisum  15909  geoisumr  15910  mertenslem1  15916  mertenslem2  15917  mertens  15918  fallfacfwd  16068  0fallfac  16069  binomfallfaclem2  16072  bpolylem  16080  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  bpoly2  16089  bpoly3  16090  bpoly4  16091  efcllem  16109  ef0lem  16110  eff  16113  efcvg  16117  efcvgfsum  16118  reefcl  16119  ege2le3  16122  efcj  16124  eftlcvg  16138  eftlub  16141  effsumlt  16143  ef4p  16145  efgt1p2  16146  efgt1p  16147  eflegeo  16153  eirrlem  16236  ruclem6  16267  ruclem7  16268  divalglem2  16428  divalglem5  16430  bitsfzolem  16467  bitsfzo  16468  bitsfi  16470  bitsinv1lem  16474  bitsinv1  16475  bitsinvp1  16482  sadcf  16486  sadcp1  16488  sadadd  16500  sadass  16504  bitsres  16506  smupf  16511  smupp1  16513  smuval2  16515  smupval  16521  smueqlem  16523  smumul  16526  alginv  16608  algcvg  16609  algcvga  16612  algfx  16613  eucalgcvga  16619  eucalg  16620  phiprmpw  16809  prmdiv  16818  iserodd  16868  pcfac  16932  prmreclem2  16950  prmreclem4  16952  vdwapun  17007  vdwlem1  17014  ramcl2lem  17042  ramtcl  17043  ramtub  17045  gsumwsubmcl  18862  gsumws1  18863  gsumsgrpccat  18865  gsumwmhm  18870  psgnunilem2  19527  psgnunilem4  19529  sylow1lem1  19630  efginvrel2  19759  efgredleme  19775  efgredlemc  19777  efgcpbllemb  19787  frgpuplem  19804  telgsumfz0s  20023  telgsums  20025  pgpfaclem1  20115  psrbaglefi  21963  ltbwe  22079  pmatcollpw3fi1lem1  22807  chfacfisf  22875  chfacfisfcpmat  22876  iscmet3lem3  25337  dyadmax  25646  mbfi1fseqlem3  25766  itgcnlem  25839  dvnff  25973  dvnp1  25975  dvn2bss  25980  cpncn  25986  dveflem  26031  ig1peu  26228  ig1pdvds  26233  ply1termlem  26256  plyeq0lem  26263  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  dgrcl  26286  dgrub  26287  dgrlb  26289  coeid3  26293  plyco  26294  coeeq2  26295  coefv0  26301  coemulhi  26307  coemulc  26308  dvply1  26339  vieta1lem2  26367  vieta1  26368  elqaalem2  26376  elqaalem3  26377  geolim3  26395  dvntaylp  26427  taylthlem1  26429  radcnvlem1  26470  radcnvlem2  26471  radcnvlem3  26472  radcnv0  26473  radcnvlt2  26476  dvradcnv  26478  pserulm  26479  psercn2  26480  psercn2OLD  26481  pserdvlem2  26486  pserdv2  26488  abelthlem4  26492  abelthlem5  26493  abelthlem6  26494  abelthlem7  26496  abelthlem8  26497  abelthlem9  26498  advlogexp  26711  logtayllem  26715  logtayl  26716  cxpeq  26814  leibpi  26999  leibpisum  27000  log2cnv  27001  log2tlbnd  27002  log2ublem2  27004  birthdaylem3  27010  wilthlem2  27126  ftalem1  27130  ftalem5  27134  basellem2  27139  basellem3  27140  basellem5  27142  musum  27248  0sgmppw  27256  1sgmprm  27257  chtublem  27269  logexprlim  27283  lgseisenlem1  27433  lgsquadlem2  27439  dchrisumlem1  27547  dchrisumlem2  27548  dchrisum0flblem1  27566  ostth2lem3  27693  tgcgr4  28553  clwwlknonex2lem1  30135  eupth2lems  30266  fz2ssnn0  32793  nn0split01  32823  ccatws1f1o  32920  gsumwrd2dccat  33052  cycpmco2rn  33127  cycpmco2lem6  33133  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  ig1pmindeg  33601  oddpwdc  34335  eulerpartlemb  34349  sseqfn  34371  sseqf  34373  signsplypnf  34543  signstcl  34558  signstf  34559  signstfvn  34562  signstfvneq0  34565  fsum2dsub  34600  reprsuc  34608  breprexplema  34623  breprexplemc  34625  subfacval2  35171  subfaclim  35172  cvmliftlem7  35275  fwddifnp1  36146  knoppcnlem6  36480  knoppcnlem8  36482  knoppcnlem9  36483  knoppcnlem11  36485  knoppcn  36486  knoppndvlem4  36497  knoppndvlem6  36499  knoppf  36517  poimirlem3  37609  poimirlem4  37610  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  heiborlem4  37800  heiborlem6  37802  lcmfunnnd  41993  mapfzcons  42703  irrapxlem1  42809  ltrmynn0  42936  ltrmxnn0  42937  acongeq  42971  jm2.23  42984  jm2.26lem3  42989  dfrtrcl3  43722  radcnvrat  44309  bcc0  44335  dvradcnv2  44342  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemradcnv  44347  binomcxplemnotnn0  44351  fzssnn0  45267  rexanuz2nf  45442  expfac  45612  dvnmptdivc  45893  dvnmul  45898  dvnprodlem3  45903  stoweidlem17  45972  stoweidlem34  45989  stirlinglem5  46033  stirlinglem7  46035  fourierdlem15  46077  fourierdlem25  46087  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem52  46113  fourierdlem54  46115  fourierdlem64  46125  fourierdlem65  46126  fourierdlem81  46142  fourierdlem92  46153  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  fourierdlem114  46175  elaa2lem  46188  etransclem4  46193  etransclem10  46199  etransclem14  46203  etransclem15  46204  etransclem23  46212  etransclem24  46213  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem44  46233  etransclem46  46235  etransclem48  46237  ssnn0ssfz  48193  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsuc  48516  ackvalsuc1mpt  48527  aacllem  49031