Theorem nn0uz 13007

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  {crab 3412   class class class wbr 5102  ‘cfv 6539  0cc0 11204   ≤ cle 11348  ℕ₀cn0 12610  ℤcz 12697  ℤ_≥cuz 12969

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280  ax-pre-mulgt0 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-sub 11547  df-neg 11548  df-nn 12340  df-n0 12611  df-z 12698  df-uz 12970

This theorem is used by:  elnn0uz  13010  2eluzge0  13012  eluznn0  13048  nn0inf  13061  fseq1p1m1  13736  fznn0sub2  13773  nn0split  13781  prednn0  13790  fzossnn0  13829  fzennn  14115  hashgf1o  14118  exple1  14324  faclbnd4lem1  14441  bcval5  14466  bcpasc  14469  hashfzo0  14579  hashf1  14606  ccatval2  14727  ccatass  14738  ccatrn  14739  swrdccat2  14824  wrdeqs1cat  14874  cats1un  14875  splfv2a  14910  splval2  14911  revccat  14920  cats1fv  15015  binom1dif  16008  isumnn0nn  16017  climcndslem1  16024  climcnds  16026  harmonic  16034  arisum2  16036  explecnv  16040  geoser  16042  pwdif  16043  geolim  16045  geolim2  16046  geomulcvg  16051  geoisum  16052  geoisumr  16053  mertenslem1  16059  mertenslem2  16060  mertens  16061  fallfacfwd  16208  0fallfac  16209  binomfallfaclem2  16212  bpolylem  16220  bpolysum  16225  bpolydiflem  16226  fsumkthpow  16228  bpoly2  16229  bpoly3  16230  bpoly4  16231  efcllem  16249  ef0lem  16250  eff  16253  efcvg  16257  efcvgfsum  16258  reefcl  16259  ege2le3  16262  efcj  16264  eftlcvg  16280  eftlub  16283  effsumlt  16285  ef4p  16287  efgt1p2  16288  efgt1p  16289  eflegeo  16295  eirrlem  16378  ruclem6  16409  ruclem7  16410  divalglem2  16571  divalglem5  16573  bitsfzolem  16610  bitsfzo  16611  bitsfi  16613  bitsinv1lem  16617  bitsinv1  16618  bitsinvp1  16625  sadcf  16629  sadcp1  16631  sadadd  16643  sadass  16647  bitsres  16649  smupf  16654  smupp1  16656  smuval2  16658  smupval  16664  smueqlem  16666  smumul  16669  alginv  16756  algcvg  16757  algcvga  16760  algfx  16761  eucalgcvga  16767  eucalg  16768  phiprmpw  16959  prmdiv  16968  iserodd  17019  pcfac  17083  prmreclem2  17101  prmreclem4  17103  vdwapun  17158  vdwlem1  17165  ramcl2lem  17193  ramtcl  17194  ramtub  17196  chnccats1  18805  gsumwsubmcl  19039  gsumws1  19040  gsumsgrpccat  19042  gsumwmhm  19047  psgnunilem2  19715  psgnunilem4  19717  sylow1lem1  19818  efginvrel2  19947  efgredleme  19963  efgredlemc  19965  efgcpbllemb  19975  frgpuplem  19992  telgsumfz0s  20211  telgsums  20213  pgpfaclem1  20303  psrbaglefi  22240  ltbwe  22359  pmatcollpw3fi1lem1  23110  chfacfisf  23178  chfacfisfcpmat  23179  iscmet3lem3  25617  dyadmax  25925  mbfi1fseqlem3  26044  itgcnlem  26116  dvnff  26249  dvnp1  26251  dvn2bss  26256  cpncn  26262  dveflem  26305  ig1peu  26499  ig1pdvds  26504  ply1termlem  26527  plyeq0lem  26535  plyaddlem1  26538  plymullem1  26539  coeeulem  26549  dgrcl  26558  dgrub  26559  dgrlb  26561  coeid3  26565  plyco  26566  coeeq2  26567  coefv0  26573  coemulhi  26579  coemulc  26580  dvply1  26611  vieta1lem2  26640  vieta1  26641  elqaalem2  26649  elqaalem3  26650  geolim3  26672  dvntaylp  26704  taylthlem1  26706  radcnvlem1  26746  radcnvlem2  26747  radcnvlem3  26748  radcnv0  26749  radcnvlt2  26752  dvradcnv  26754  pserulm  26755  psercn2  26756  pserdvlem2  26761  pserdv2  26763  abelthlem4  26767  abelthlem5  26768  abelthlem6  26769  abelthlem7  26771  abelthlem8  26772  abelthlem9  26773  advlogexp  26989  logtayllem  26993  logtayl  26994  cxpeq  27091  leibpi  27276  leibpisum  27277  log2cnv  27278  log2tlbnd  27279  log2ublem2  27281  birthdaylem3  27287  wilthlem2  27402  ftalem1  27406  ftalem5  27410  basellem2  27415  basellem3  27416  basellem5  27418  musum  27524  0sgmppw  27531  1sgmprm  27532  chtublem  27544  logexprlim  27558  lgseisenlem1  27708  lgsquadlem2  27714  dchrisumlem1  27822  dchrisumlem2  27823  dchrisum0flblem1  27841  ostth2lem3  27968  tgcgr4  29000  clwwlknonex2lem1  30704  eupth2lems  30845  fz2ssnn0  33424  nn0diffz0  33433  nn0split01  33456  ccatws1f1o  33561  gsummulsubdishift1  33676  gsumwrd2dccat  33686  cycpmco2rn  33733  cycpmco2lem6  33739  evl1deg1  34155  evl1deg2  34156  evl1deg3  34157  ig1pmindeg  34181  vietalem  34258  exsslsb  34276  oddpwdc  35033  eulerpartlemb  35047  sseqfn  35069  sseqf  35071  signsplypnf  35226  signstcl  35241  signstf  35242  signstfvn  35245  signstfvneq0  35248  fsum2dsub  35283  reprsuc  35291  breprexplema  35306  breprexplemc  35308  subfacval2  36039  subfaclim  36040  cvmliftlem7  36143  fwddifnp1  37023  knoppcnlem6  37457  knoppcnlem8  37459  knoppcnlem9  37460  knoppcnlem11  37462  knoppcn  37463  knoppndvlem4  37474  knoppndvlem6  37476  knoppf  37494  poimirlem3  38635  poimirlem4  38636  poimirlem18  38650  poimirlem21  38653  poimirlem22  38654  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  heiborlem4  38842  heiborlem6  38844  lcmfunnnd  43156  mapfzcons  43821  irrapxlem1  43923  ltrmynn0  44049  ltrmxnn0  44050  acongeq  44084  jm2.23  44097  jm2.26lem3  44102  dfrtrcl3  44827  radcnvrat  45392  bcc0  45418  dvradcnv2  45425  binomcxplemnn0  45427  binomcxplemrat  45428  binomcxplemradcnv  45430  binomcxplemnotnn0  45434  fzssnn0  46425  rexanuz2nf  46596  expfac  46761  dvnmptdivc  47042  dvnmul  47047  dvnprodlem3  47052  stoweidlem17  47121  stoweidlem34  47138  stirlinglem5  47182  stirlinglem7  47184  fourierdlem15  47226  fourierdlem25  47236  fourierdlem48  47258  fourierdlem49  47259  fourierdlem50  47260  fourierdlem52  47262  fourierdlem54  47264  fourierdlem64  47274  fourierdlem65  47275  fourierdlem81  47291  fourierdlem92  47302  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem113  47323  fourierdlem114  47324  elaa2lem  47337  etransclem4  47342  etransclem10  47348  etransclem14  47352  etransclem15  47353  etransclem23  47361  etransclem24  47362  etransclem31  47369  etransclem32  47370  etransclem35  47373  etransclem44  47382  etransclem46  47384  etransclem48  47386  ssnn0ssfz  49555  itcoval1  49869  itcoval2  49870  itcoval3  49871  itcovalsuc  49873  ackvalsuc1mpt  49884  aacllem  51108