Theorem nn0uz 12860

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  {crab 3432   class class class wbr 5147  ‘cfv 6540  0cc0 11106   ≤ cle 11245  ℕ₀cn0 12468  ℤcz 12554  ℤ_≥cuz 12818

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819

This theorem is referenced by:  elnn0uz  12863  2eluzge0  12873  eluznn0  12897  nn0inf  12910  fseq1p1m1  13571  fznn0sub2  13604  nn0split  13612  prednn0  13621  fzossnn0  13659  fzennn  13929  hashgf1o  13932  exple1  14137  faclbnd4lem1  14249  bcval5  14274  bcpasc  14277  hashfzo0  14386  hashf1  14414  ccatval2  14524  ccatass  14534  ccatrn  14535  swrdccat2  14615  wrdeqs1cat  14666  cats1un  14667  splfv2a  14702  splval2  14703  revccat  14712  cats1fv  14806  binom1dif  15775  isumnn0nn  15784  climcndslem1  15791  climcnds  15793  harmonic  15801  arisum2  15803  explecnv  15807  geoser  15809  pwdif  15810  geolim  15812  geolim2  15813  geomulcvg  15818  geoisum  15819  geoisumr  15820  mertenslem1  15826  mertenslem2  15827  mertens  15828  fallfacfwd  15976  0fallfac  15977  binomfallfaclem2  15980  bpolylem  15988  bpolysum  15993  bpolydiflem  15994  fsumkthpow  15996  bpoly2  15997  bpoly3  15998  bpoly4  15999  efcllem  16017  ef0lem  16018  eff  16021  efcvg  16024  efcvgfsum  16025  reefcl  16026  ege2le3  16029  efcj  16031  eftlcvg  16045  eftlub  16048  effsumlt  16050  ef4p  16052  efgt1p2  16053  efgt1p  16054  eflegeo  16060  eirrlem  16143  ruclem6  16174  ruclem7  16175  divalglem2  16334  divalglem5  16336  bitsfzolem  16371  bitsfzo  16372  bitsfi  16374  bitsinv1lem  16378  bitsinv1  16379  bitsinvp1  16386  sadcf  16390  sadcp1  16392  sadadd  16404  sadass  16408  bitsres  16410  smupf  16415  smupp1  16417  smuval2  16419  smupval  16425  smueqlem  16427  smumul  16430  alginv  16508  algcvg  16509  algcvga  16512  algfx  16513  eucalgcvga  16519  eucalg  16520  phiprmpw  16705  prmdiv  16714  iserodd  16764  pcfac  16828  prmreclem2  16846  prmreclem4  16848  vdwapun  16903  vdwlem1  16910  ramcl2lem  16938  ramtcl  16939  ramtub  16941  gsumwsubmcl  18714  gsumws1  18715  gsumsgrpccat  18717  gsumwmhm  18722  psgnunilem2  19357  psgnunilem4  19359  sylow1lem1  19460  efginvrel2  19589  efgredleme  19605  efgredlemc  19607  efgcpbllemb  19617  frgpuplem  19634  telgsumfz0s  19853  telgsums  19855  pgpfaclem1  19945  psrbaglefi  21476  psrbaglefiOLD  21477  ltbwe  21590  pmatcollpw3fi1lem1  22279  chfacfisf  22347  chfacfisfcpmat  22348  iscmet3lem3  24798  dyadmax  25106  mbfi1fseqlem3  25226  itgcnlem  25298  dvnff  25431  dvnp1  25433  dvn2bss  25438  cpncn  25444  dveflem  25487  ig1peu  25680  ig1pdvds  25685  ply1termlem  25708  plyeq0lem  25715  plyaddlem1  25718  plymullem1  25719  coeeulem  25729  dgrcl  25738  dgrub  25739  dgrlb  25741  coeid3  25745  plyco  25746  coeeq2  25747  coefv0  25753  coemulhi  25759  coemulc  25760  dvply1  25788  vieta1lem2  25815  vieta1  25816  elqaalem2  25824  elqaalem3  25825  geolim3  25843  dvntaylp  25874  taylthlem1  25876  radcnvlem1  25916  radcnvlem2  25917  radcnvlem3  25918  radcnv0  25919  radcnvlt2  25922  dvradcnv  25924  pserulm  25925  psercn2  25926  pserdvlem2  25931  pserdv2  25933  abelthlem4  25937  abelthlem5  25938  abelthlem6  25939  abelthlem7  25941  abelthlem8  25942  abelthlem9  25943  advlogexp  26154  logtayllem  26158  logtayl  26159  cxpeq  26254  leibpi  26436  leibpisum  26437  log2cnv  26438  log2tlbnd  26439  log2ublem2  26441  birthdaylem3  26447  wilthlem2  26562  ftalem1  26566  ftalem5  26570  basellem2  26575  basellem3  26576  basellem5  26578  musum  26684  0sgmppw  26690  1sgmprm  26691  chtublem  26703  logexprlim  26717  lgseisenlem1  26867  lgsquadlem2  26873  dchrisumlem1  26981  dchrisumlem2  26982  dchrisum0flblem1  27000  ostth2lem3  27127  tgcgr4  27771  clwwlknonex2lem1  29349  eupth2lems  29480  fz2ssnn0  31983  cycpmco2rn  32271  cycpmco2lem6  32277  ig1pmindeg  32659  oddpwdc  33341  eulerpartlemb  33355  sseqfn  33377  sseqf  33379  signsplypnf  33549  signstcl  33564  signstf  33565  signstfvn  33568  signstfvneq0  33571  fsum2dsub  33607  reprsuc  33615  breprexplema  33630  breprexplemc  33632  subfacval2  34166  subfaclim  34167  cvmliftlem7  34270  fwddifnp1  35125  gg-psercn2  35166  knoppcnlem6  35362  knoppcnlem8  35364  knoppcnlem9  35365  knoppcnlem11  35367  knoppcn  35368  knoppndvlem4  35379  knoppndvlem6  35381  knoppf  35399  poimirlem3  36479  poimirlem4  36480  poimirlem18  36494  poimirlem21  36497  poimirlem22  36498  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  heiborlem4  36670  heiborlem6  36672  lcmfunnnd  40865  mapfzcons  41439  irrapxlem1  41545  ltrmynn0  41672  ltrmxnn0  41673  acongeq  41707  jm2.23  41720  jm2.26lem3  41725  dfrtrcl3  42469  radcnvrat  43058  bcc0  43084  dvradcnv2  43091  binomcxplemnn0  43093  binomcxplemrat  43094  binomcxplemradcnv  43096  binomcxplemnotnn0  43100  fzssnn0  44013  rexanuz2nf  44189  expfac  44359  dvnmptdivc  44640  dvnmul  44645  dvnprodlem3  44650  stoweidlem17  44719  stoweidlem34  44736  stirlinglem5  44780  stirlinglem7  44782  fourierdlem15  44824  fourierdlem25  44834  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem52  44860  fourierdlem54  44862  fourierdlem64  44872  fourierdlem65  44873  fourierdlem81  44889  fourierdlem92  44900  fourierdlem102  44910  fourierdlem103  44911  fourierdlem104  44912  fourierdlem113  44921  fourierdlem114  44922  elaa2lem  44935  etransclem4  44940  etransclem10  44946  etransclem14  44950  etransclem15  44951  etransclem23  44959  etransclem24  44960  etransclem31  44967  etransclem32  44968  etransclem35  44971  etransclem44  44980  etransclem46  44982  etransclem48  44984  ssnn0ssfz  46978  itcoval1  47302  itcoval2  47303  itcoval3  47304  itcovalsuc  47306  ackvalsuc1mpt  47317  aacllem  47801