Theorem nn0uz 12826

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3389   class class class wbr 5085  ‘cfv 6498  0cc0 11038   ≤ cle 11180  ℕ₀cn0 12437  ℤcz 12524  ℤ_≥cuz 12788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-uz 12789

This theorem is referenced by:  elnn0uz  12829  2eluzge0  12831  eluznn0  12867  nn0inf  12880  fseq1p1m1  13552  fznn0sub2  13589  nn0split  13597  prednn0  13606  fzossnn0  13645  fzennn  13930  hashgf1o  13933  exple1  14139  faclbnd4lem1  14255  bcval5  14280  bcpasc  14283  hashfzo0  14392  hashf1  14419  ccatval2  14540  ccatass  14551  ccatrn  14552  swrdccat2  14632  wrdeqs1cat  14682  cats1un  14683  splfv2a  14718  splval2  14719  revccat  14728  cats1fv  14821  binom1dif  15798  isumnn0nn  15807  climcndslem1  15814  climcnds  15816  harmonic  15824  arisum2  15826  explecnv  15830  geoser  15832  pwdif  15833  geolim  15835  geolim2  15836  geomulcvg  15841  geoisum  15842  geoisumr  15843  mertenslem1  15849  mertenslem2  15850  mertens  15851  fallfacfwd  16001  0fallfac  16002  binomfallfaclem2  16005  bpolylem  16013  bpolysum  16018  bpolydiflem  16019  fsumkthpow  16021  bpoly2  16022  bpoly3  16023  bpoly4  16024  efcllem  16042  ef0lem  16043  eff  16046  efcvg  16050  efcvgfsum  16051  reefcl  16052  ege2le3  16055  efcj  16057  eftlcvg  16073  eftlub  16076  effsumlt  16078  ef4p  16080  efgt1p2  16081  efgt1p  16082  eflegeo  16088  eirrlem  16171  ruclem6  16202  ruclem7  16203  divalglem2  16364  divalglem5  16366  bitsfzolem  16403  bitsfzo  16404  bitsfi  16406  bitsinv1lem  16410  bitsinv1  16411  bitsinvp1  16418  sadcf  16422  sadcp1  16424  sadadd  16436  sadass  16440  bitsres  16442  smupf  16447  smupp1  16449  smuval2  16451  smupval  16457  smueqlem  16459  smumul  16462  alginv  16544  algcvg  16545  algcvga  16548  algfx  16549  eucalgcvga  16555  eucalg  16556  phiprmpw  16746  prmdiv  16755  iserodd  16806  pcfac  16870  prmreclem2  16888  prmreclem4  16890  vdwapun  16945  vdwlem1  16952  ramcl2lem  16980  ramtcl  16981  ramtub  16983  chnccats1  18591  gsumwsubmcl  18805  gsumws1  18806  gsumsgrpccat  18808  gsumwmhm  18813  psgnunilem2  19470  psgnunilem4  19472  sylow1lem1  19573  efginvrel2  19702  efgredleme  19718  efgredlemc  19720  efgcpbllemb  19730  frgpuplem  19747  telgsumfz0s  19966  telgsums  19968  pgpfaclem1  20058  psrbaglefi  21906  ltbwe  22022  pmatcollpw3fi1lem1  22751  chfacfisf  22819  chfacfisfcpmat  22820  iscmet3lem3  25257  dyadmax  25565  mbfi1fseqlem3  25684  itgcnlem  25757  dvnff  25890  dvnp1  25892  dvn2bss  25897  cpncn  25903  dveflem  25946  ig1peu  26140  ig1pdvds  26145  ply1termlem  26168  plyeq0lem  26175  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  dgrcl  26198  dgrub  26199  dgrlb  26201  coeid3  26205  plyco  26206  coeeq2  26207  coefv0  26213  coemulhi  26219  coemulc  26220  dvply1  26250  vieta1lem2  26277  vieta1  26278  elqaalem2  26286  elqaalem3  26287  geolim3  26305  dvntaylp  26336  taylthlem1  26338  radcnvlem1  26378  radcnvlem2  26379  radcnvlem3  26380  radcnv0  26381  radcnvlt2  26384  dvradcnv  26386  pserulm  26387  psercn2  26388  pserdvlem2  26393  pserdv2  26395  abelthlem4  26399  abelthlem5  26400  abelthlem6  26401  abelthlem7  26403  abelthlem8  26404  abelthlem9  26405  advlogexp  26619  logtayllem  26623  logtayl  26624  cxpeq  26721  leibpi  26906  leibpisum  26907  log2cnv  26908  log2tlbnd  26909  log2ublem2  26911  birthdaylem3  26917  wilthlem2  27032  ftalem1  27036  ftalem5  27040  basellem2  27045  basellem3  27046  basellem5  27048  musum  27154  0sgmppw  27161  1sgmprm  27162  chtublem  27174  logexprlim  27188  lgseisenlem1  27338  lgsquadlem2  27344  dchrisumlem1  27452  dchrisumlem2  27453  dchrisum0flblem1  27471  ostth2lem3  27598  tgcgr4  28599  clwwlknonex2lem1  30177  eupth2lems  30308  fz2ssnn0  32858  nn0diffz0  32867  nn0split01  32891  ccatws1f1o  33011  gsummulsubdishift1  33129  gsumwrd2dccat  33139  cycpmco2rn  33186  cycpmco2lem6  33192  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  ig1pmindeg  33662  vietalem  33723  exsslsb  33741  oddpwdc  34498  eulerpartlemb  34512  sseqfn  34534  sseqf  34536  signsplypnf  34694  signstcl  34709  signstf  34710  signstfvn  34713  signstfvneq0  34716  fsum2dsub  34751  reprsuc  34759  breprexplema  34774  breprexplemc  34776  subfacval2  35369  subfaclim  35370  cvmliftlem7  35473  fwddifnp1  36347  knoppcnlem6  36758  knoppcnlem8  36760  knoppcnlem9  36761  knoppcnlem11  36763  knoppcn  36764  knoppndvlem4  36775  knoppndvlem6  36777  knoppf  36795  poimirlem3  37944  poimirlem4  37945  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  heiborlem4  38135  heiborlem6  38137  lcmfunnnd  42451  mapfzcons  43148  irrapxlem1  43250  ltrmynn0  43376  ltrmxnn0  43377  acongeq  43411  jm2.23  43424  jm2.26lem3  43429  dfrtrcl3  44160  radcnvrat  44741  bcc0  44767  dvradcnv2  44774  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemradcnv  44779  binomcxplemnotnn0  44783  fzssnn0  45749  rexanuz2nf  45920  expfac  46085  dvnmptdivc  46366  dvnmul  46371  dvnprodlem3  46376  stoweidlem17  46445  stoweidlem34  46462  stirlinglem5  46506  stirlinglem7  46508  fourierdlem15  46550  fourierdlem25  46560  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem52  46586  fourierdlem54  46588  fourierdlem64  46598  fourierdlem65  46599  fourierdlem81  46615  fourierdlem92  46626  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  fourierdlem114  46648  elaa2lem  46661  etransclem4  46666  etransclem10  46672  etransclem14  46676  etransclem15  46677  etransclem23  46685  etransclem24  46686  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem44  46706  etransclem46  46708  etransclem48  46710  chnerlem1  47312  chnerlem2  47313  ssnn0ssfz  48825  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsuc  49143  ackvalsuc1mpt  49154  aacllem  50276