Theorem nn0uz 12842

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3408   class class class wbr 5110  ‘cfv 6514  0cc0 11075   ≤ cle 11216  ℕ₀cn0 12449  ℤcz 12536  ℤ_≥cuz 12800

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537  df-uz 12801

This theorem is referenced by:  elnn0uz  12845  2eluzge0  12847  eluznn0  12883  nn0inf  12896  fseq1p1m1  13566  fznn0sub2  13603  nn0split  13611  prednn0  13620  fzossnn0  13658  fzennn  13940  hashgf1o  13943  exple1  14149  faclbnd4lem1  14265  bcval5  14290  bcpasc  14293  hashfzo0  14402  hashf1  14429  ccatval2  14550  ccatass  14560  ccatrn  14561  swrdccat2  14641  wrdeqs1cat  14692  cats1un  14693  splfv2a  14728  splval2  14729  revccat  14738  cats1fv  14832  binom1dif  15806  isumnn0nn  15815  climcndslem1  15822  climcnds  15824  harmonic  15832  arisum2  15834  explecnv  15838  geoser  15840  pwdif  15841  geolim  15843  geolim2  15844  geomulcvg  15849  geoisum  15850  geoisumr  15851  mertenslem1  15857  mertenslem2  15858  mertens  15859  fallfacfwd  16009  0fallfac  16010  binomfallfaclem2  16013  bpolylem  16021  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  bpoly2  16030  bpoly3  16031  bpoly4  16032  efcllem  16050  ef0lem  16051  eff  16054  efcvg  16058  efcvgfsum  16059  reefcl  16060  ege2le3  16063  efcj  16065  eftlcvg  16081  eftlub  16084  effsumlt  16086  ef4p  16088  efgt1p2  16089  efgt1p  16090  eflegeo  16096  eirrlem  16179  ruclem6  16210  ruclem7  16211  divalglem2  16372  divalglem5  16374  bitsfzolem  16411  bitsfzo  16412  bitsfi  16414  bitsinv1lem  16418  bitsinv1  16419  bitsinvp1  16426  sadcf  16430  sadcp1  16432  sadadd  16444  sadass  16448  bitsres  16450  smupf  16455  smupp1  16457  smuval2  16459  smupval  16465  smueqlem  16467  smumul  16470  alginv  16552  algcvg  16553  algcvga  16556  algfx  16557  eucalgcvga  16563  eucalg  16564  phiprmpw  16753  prmdiv  16762  iserodd  16813  pcfac  16877  prmreclem2  16895  prmreclem4  16897  vdwapun  16952  vdwlem1  16959  ramcl2lem  16987  ramtcl  16988  ramtub  16990  gsumwsubmcl  18771  gsumws1  18772  gsumsgrpccat  18774  gsumwmhm  18779  psgnunilem2  19432  psgnunilem4  19434  sylow1lem1  19535  efginvrel2  19664  efgredleme  19680  efgredlemc  19682  efgcpbllemb  19692  frgpuplem  19709  telgsumfz0s  19928  telgsums  19930  pgpfaclem1  20020  psrbaglefi  21842  ltbwe  21958  pmatcollpw3fi1lem1  22680  chfacfisf  22748  chfacfisfcpmat  22749  iscmet3lem3  25197  dyadmax  25506  mbfi1fseqlem3  25625  itgcnlem  25698  dvnff  25832  dvnp1  25834  dvn2bss  25839  cpncn  25845  dveflem  25890  ig1peu  26087  ig1pdvds  26092  ply1termlem  26115  plyeq0lem  26122  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  dgrcl  26145  dgrub  26146  dgrlb  26148  coeid3  26152  plyco  26153  coeeq2  26154  coefv0  26160  coemulhi  26166  coemulc  26167  dvply1  26198  vieta1lem2  26226  vieta1  26227  elqaalem2  26235  elqaalem3  26236  geolim3  26254  dvntaylp  26286  taylthlem1  26288  radcnvlem1  26329  radcnvlem2  26330  radcnvlem3  26331  radcnv0  26332  radcnvlt2  26335  dvradcnv  26337  pserulm  26338  psercn2  26339  psercn2OLD  26340  pserdvlem2  26345  pserdv2  26347  abelthlem4  26351  abelthlem5  26352  abelthlem6  26353  abelthlem7  26355  abelthlem8  26356  abelthlem9  26357  advlogexp  26571  logtayllem  26575  logtayl  26576  cxpeq  26674  leibpi  26859  leibpisum  26860  log2cnv  26861  log2tlbnd  26862  log2ublem2  26864  birthdaylem3  26870  wilthlem2  26986  ftalem1  26990  ftalem5  26994  basellem2  26999  basellem3  27000  basellem5  27002  musum  27108  0sgmppw  27116  1sgmprm  27117  chtublem  27129  logexprlim  27143  lgseisenlem1  27293  lgsquadlem2  27299  dchrisumlem1  27407  dchrisumlem2  27408  dchrisum0flblem1  27426  ostth2lem3  27553  tgcgr4  28465  clwwlknonex2lem1  30043  eupth2lems  30174  fz2ssnn0  32715  nn0split01  32749  ccatws1f1o  32880  chnccats1  32948  gsumwrd2dccat  33014  cycpmco2rn  33089  cycpmco2lem6  33095  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ig1pmindeg  33574  exsslsb  33599  oddpwdc  34352  eulerpartlemb  34366  sseqfn  34388  sseqf  34390  signsplypnf  34548  signstcl  34563  signstf  34564  signstfvn  34567  signstfvneq0  34570  fsum2dsub  34605  reprsuc  34613  breprexplema  34628  breprexplemc  34630  subfacval2  35181  subfaclim  35182  cvmliftlem7  35285  fwddifnp1  36160  knoppcnlem6  36493  knoppcnlem8  36495  knoppcnlem9  36496  knoppcnlem11  36498  knoppcn  36499  knoppndvlem4  36510  knoppndvlem6  36512  knoppf  36530  poimirlem3  37624  poimirlem4  37625  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  heiborlem4  37815  heiborlem6  37817  lcmfunnnd  42007  mapfzcons  42711  irrapxlem1  42817  ltrmynn0  42944  ltrmxnn0  42945  acongeq  42979  jm2.23  42992  jm2.26lem3  42997  dfrtrcl3  43729  radcnvrat  44310  bcc0  44336  dvradcnv2  44343  binomcxplemnn0  44345  binomcxplemrat  44346  binomcxplemradcnv  44348  binomcxplemnotnn0  44352  fzssnn0  45321  rexanuz2nf  45495  expfac  45662  dvnmptdivc  45943  dvnmul  45948  dvnprodlem3  45953  stoweidlem17  46022  stoweidlem34  46039  stirlinglem5  46083  stirlinglem7  46085  fourierdlem15  46127  fourierdlem25  46137  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem52  46163  fourierdlem54  46165  fourierdlem64  46175  fourierdlem65  46176  fourierdlem81  46192  fourierdlem92  46203  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  fourierdlem114  46225  elaa2lem  46238  etransclem4  46243  etransclem10  46249  etransclem14  46253  etransclem15  46254  etransclem23  46262  etransclem24  46263  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem44  46283  etransclem46  46285  etransclem48  46287  ssnn0ssfz  48341  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsuc  48660  ackvalsuc1mpt  48671  aacllem  49794