Theorem nn0uz 12996

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {crab 3413   class class class wbr 5103  ‘cfv 6537  0cc0 11193   ≤ cle 11337  ℕ₀cn0 12599  ℤcz 12686  ℤ_≥cuz 12958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687  df-uz 12959

This theorem is used by:  elnn0uz  12999  2eluzge0  13001  eluznn0  13037  nn0inf  13050  fseq1p1m1  13725  fznn0sub2  13762  nn0split  13770  prednn0  13779  fzossnn0  13818  fzennn  14104  hashgf1o  14107  exple1  14313  faclbnd4lem1  14430  bcval5  14455  bcpasc  14458  hashfzo0  14568  hashf1  14595  ccatval2  14716  ccatass  14727  ccatrn  14728  swrdccat2  14812  wrdeqs1cat  14862  cats1un  14863  splfv2a  14898  splval2  14899  revccat  14908  cats1fv  15003  binom1dif  15995  isumnn0nn  16004  climcndslem1  16011  climcnds  16013  harmonic  16021  arisum2  16023  explecnv  16027  geoser  16029  pwdif  16030  geolim  16032  geolim2  16033  geomulcvg  16038  geoisum  16039  geoisumr  16040  mertenslem1  16046  mertenslem2  16047  mertens  16048  fallfacfwd  16195  0fallfac  16196  binomfallfaclem2  16199  bpolylem  16207  bpolysum  16212  bpolydiflem  16213  fsumkthpow  16215  bpoly2  16216  bpoly3  16217  bpoly4  16218  efcllem  16236  ef0lem  16237  eff  16240  efcvg  16244  efcvgfsum  16245  reefcl  16246  ege2le3  16249  efcj  16251  eftlcvg  16267  eftlub  16270  effsumlt  16272  ef4p  16274  efgt1p2  16275  efgt1p  16276  eflegeo  16282  eirrlem  16365  ruclem6  16396  ruclem7  16397  divalglem2  16558  divalglem5  16560  bitsfzolem  16597  bitsfzo  16598  bitsfi  16600  bitsinv1lem  16604  bitsinv1  16605  bitsinvp1  16612  sadcf  16616  sadcp1  16618  sadadd  16630  sadass  16634  bitsres  16636  smupf  16641  smupp1  16643  smuval2  16645  smupval  16651  smueqlem  16653  smumul  16656  alginv  16743  algcvg  16744  algcvga  16747  algfx  16748  eucalgcvga  16754  eucalg  16755  phiprmpw  16946  prmdiv  16955  iserodd  17006  pcfac  17070  prmreclem2  17088  prmreclem4  17090  vdwapun  17145  vdwlem1  17152  ramcl2lem  17180  ramtcl  17181  ramtub  17183  chnccats1  18792  gsumwsubmcl  19026  gsumws1  19027  gsumsgrpccat  19029  gsumwmhm  19034  psgnunilem2  19702  psgnunilem4  19704  sylow1lem1  19805  efginvrel2  19934  efgredleme  19950  efgredlemc  19952  efgcpbllemb  19962  frgpuplem  19979  telgsumfz0s  20198  telgsums  20200  pgpfaclem1  20290  psrbaglefi  22227  ltbwe  22346  pmatcollpw3fi1lem1  23097  chfacfisf  23165  chfacfisfcpmat  23166  iscmet3lem3  25604  dyadmax  25912  mbfi1fseqlem3  26031  itgcnlem  26103  dvnff  26236  dvnp1  26238  dvn2bss  26243  cpncn  26249  dveflem  26292  ig1peu  26486  ig1pdvds  26491  ply1termlem  26514  plyeq0lem  26522  plyaddlem1  26525  plymullem1  26526  coeeulem  26536  dgrcl  26545  dgrub  26546  dgrlb  26548  coeid3  26552  plyco  26553  coeeq2  26554  coefv0  26560  coemulhi  26566  coemulc  26567  dvply1  26598  vieta1lem2  26627  vieta1  26628  elqaalem2  26636  elqaalem3  26637  geolim3  26659  dvntaylp  26691  taylthlem1  26693  radcnvlem1  26733  radcnvlem2  26734  radcnvlem3  26735  radcnv0  26736  radcnvlt2  26739  dvradcnv  26741  pserulm  26742  psercn2  26743  pserdvlem2  26748  pserdv2  26750  abelthlem4  26754  abelthlem5  26755  abelthlem6  26756  abelthlem7  26758  abelthlem8  26759  abelthlem9  26760  advlogexp  26976  logtayllem  26980  logtayl  26981  cxpeq  27078  leibpi  27263  leibpisum  27264  log2cnv  27265  log2tlbnd  27266  log2ublem2  27268  birthdaylem3  27274  wilthlem2  27389  ftalem1  27393  ftalem5  27397  basellem2  27402  basellem3  27403  basellem5  27405  musum  27511  0sgmppw  27518  1sgmprm  27519  chtublem  27531  logexprlim  27545  lgseisenlem1  27695  lgsquadlem2  27701  dchrisumlem1  27809  dchrisumlem2  27810  dchrisum0flblem1  27828  ostth2lem3  27955  tgcgr4  28987  clwwlknonex2lem1  30691  eupth2lems  30832  fz2ssnn0  33370  nn0diffz0  33379  nn0split01  33402  ccatws1f1o  33507  gsummulsubdishift1  33622  gsumwrd2dccat  33632  cycpmco2rn  33679  cycpmco2lem6  33685  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  ig1pmindeg  34127  vietalem  34204  exsslsb  34222  oddpwdc  34979  eulerpartlemb  34993  sseqfn  35015  sseqf  35017  signsplypnf  35172  signstcl  35187  signstf  35188  signstfvn  35191  signstfvneq0  35194  fsum2dsub  35229  reprsuc  35237  breprexplema  35252  breprexplemc  35254  subfacval2  35931  subfaclim  35932  cvmliftlem7  36035  fwddifnp1  36910  knoppcnlem6  37344  knoppcnlem8  37346  knoppcnlem9  37347  knoppcnlem11  37349  knoppcn  37350  knoppndvlem4  37361  knoppndvlem6  37363  knoppf  37381  poimirlem3  38521  poimirlem4  38522  poimirlem18  38536  poimirlem21  38539  poimirlem22  38540  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  heiborlem4  38728  heiborlem6  38730  lcmfunnnd  43042  mapfzcons  43706  irrapxlem1  43808  ltrmynn0  43934  ltrmxnn0  43935  acongeq  43969  jm2.23  43982  jm2.26lem3  43987  dfrtrcl3  44718  radcnvrat  45283  bcc0  45309  dvradcnv2  45316  binomcxplemnn0  45318  binomcxplemrat  45319  binomcxplemradcnv  45321  binomcxplemnotnn0  45325  fzssnn0  46300  rexanuz2nf  46471  expfac  46636  dvnmptdivc  46917  dvnmul  46922  dvnprodlem3  46927  stoweidlem17  46996  stoweidlem34  47013  stirlinglem5  47057  stirlinglem7  47059  fourierdlem15  47101  fourierdlem25  47111  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem52  47137  fourierdlem54  47139  fourierdlem64  47149  fourierdlem65  47150  fourierdlem81  47166  fourierdlem92  47177  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem113  47198  fourierdlem114  47199  elaa2lem  47212  etransclem4  47217  etransclem10  47223  etransclem14  47227  etransclem15  47228  etransclem23  47236  etransclem24  47237  etransclem31  47244  etransclem32  47245  etransclem35  47248  etransclem44  47257  etransclem46  47259  etransclem48  47261  ssnn0ssfz  49430  itcoval1  49744  itcoval2  49745  itcoval3  49746  itcovalsuc  49748  ackvalsuc1mpt  49759  aacllem  50908