Theorem nn0uz 12549

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  {crab 3067   class class class wbr 5070  ‘cfv 6418  0cc0 10802   ≤ cle 10941  ℕ₀cn0 12163  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512

This theorem is referenced by:  elnn0uz  12552  2eluzge0  12562  eluznn0  12586  nn0inf  12599  fseq1p1m1  13259  fznn0sub2  13292  nn0split  13300  prednn0  13309  fzossnn0  13346  fzennn  13616  hashgf1o  13619  exple1  13822  faclbnd4lem1  13935  bcval5  13960  bcpasc  13963  hashfzo0  14073  hashf1  14099  ccatval2  14211  ccatass  14221  ccatrn  14222  swrdccat2  14310  wrdeqs1cat  14361  cats1un  14362  splfv2a  14397  splval2  14398  revccat  14407  cats1fv  14500  binom1dif  15473  isumnn0nn  15482  climcndslem1  15489  climcnds  15491  harmonic  15499  arisum2  15501  explecnv  15505  geoser  15507  pwdif  15508  geolim  15510  geolim2  15511  geomulcvg  15516  geoisum  15517  geoisumr  15518  mertenslem1  15524  mertenslem2  15525  mertens  15526  fallfacfwd  15674  0fallfac  15675  binomfallfaclem2  15678  bpolylem  15686  bpolysum  15691  bpolydiflem  15692  fsumkthpow  15694  bpoly2  15695  bpoly3  15696  bpoly4  15697  efcllem  15715  ef0lem  15716  eff  15719  efcvg  15722  efcvgfsum  15723  reefcl  15724  ege2le3  15727  efcj  15729  eftlcvg  15743  eftlub  15746  effsumlt  15748  ef4p  15750  efgt1p2  15751  efgt1p  15752  eflegeo  15758  eirrlem  15841  ruclem6  15872  ruclem7  15873  divalglem2  16032  divalglem5  16034  bitsfzolem  16069  bitsfzo  16070  bitsfi  16072  bitsinv1lem  16076  bitsinv1  16077  bitsinvp1  16084  sadcf  16088  sadcp1  16090  sadadd  16102  sadass  16106  bitsres  16108  smupf  16113  smupp1  16115  smuval2  16117  smupval  16123  smueqlem  16125  smumul  16128  alginv  16208  algcvg  16209  algcvga  16212  algfx  16213  eucalgcvga  16219  eucalg  16220  phiprmpw  16405  prmdiv  16414  iserodd  16464  pcfac  16528  prmreclem2  16546  prmreclem4  16548  vdwapun  16603  vdwlem1  16610  ramcl2lem  16638  ramtcl  16639  ramtub  16641  gsumwsubmcl  18390  gsumws1  18391  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  psgnunilem2  19018  psgnunilem4  19020  sylow1lem1  19118  efginvrel2  19248  efgredleme  19264  efgredlemc  19266  efgcpbllemb  19276  frgpuplem  19293  telgsumfz0s  19507  telgsums  19509  pgpfaclem1  19599  psrbaglefi  21045  psrbaglefiOLD  21046  ltbwe  21155  pmatcollpw3fi1lem1  21843  chfacfisf  21911  chfacfisfcpmat  21912  iscmet3lem3  24359  dyadmax  24667  mbfi1fseqlem3  24787  itgcnlem  24859  dvnff  24992  dvnp1  24994  dvn2bss  24999  cpncn  25005  dveflem  25048  ig1peu  25241  ig1pdvds  25246  ply1termlem  25269  plyeq0lem  25276  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  dgrcl  25299  dgrub  25300  dgrlb  25302  coeid3  25306  plyco  25307  coeeq2  25308  coefv0  25314  coemulhi  25320  coemulc  25321  dvply1  25349  vieta1lem2  25376  vieta1  25377  elqaalem2  25385  elqaalem3  25386  geolim3  25404  dvntaylp  25435  taylthlem1  25437  radcnvlem1  25477  radcnvlem2  25478  radcnvlem3  25479  radcnv0  25480  radcnvlt2  25483  dvradcnv  25485  pserulm  25486  psercn2  25487  pserdvlem2  25492  pserdv2  25494  abelthlem4  25498  abelthlem5  25499  abelthlem6  25500  abelthlem7  25502  abelthlem8  25503  abelthlem9  25504  advlogexp  25715  logtayllem  25719  logtayl  25720  cxpeq  25815  leibpi  25997  leibpisum  25998  log2cnv  25999  log2tlbnd  26000  log2ublem2  26002  birthdaylem3  26008  wilthlem2  26123  ftalem1  26127  ftalem5  26131  basellem2  26136  basellem3  26137  basellem5  26139  musum  26245  0sgmppw  26251  1sgmprm  26252  chtublem  26264  logexprlim  26278  lgseisenlem1  26428  lgsquadlem2  26434  dchrisumlem1  26542  dchrisumlem2  26543  dchrisum0flblem1  26561  ostth2lem3  26688  tgcgr4  26796  clwwlknonex2lem1  28372  eupth2lems  28503  fz2ssnn0  31008  cycpmco2rn  31294  cycpmco2lem6  31300  oddpwdc  32221  eulerpartlemb  32235  sseqfn  32257  sseqf  32259  signsplypnf  32429  signstcl  32444  signstf  32445  signstfvn  32448  signstfvneq0  32451  fsum2dsub  32487  reprsuc  32495  breprexplema  32510  breprexplemc  32512  subfacval2  33049  subfaclim  33050  cvmliftlem7  33153  fwddifnp1  34394  knoppcnlem6  34605  knoppcnlem8  34607  knoppcnlem9  34608  knoppcnlem11  34610  knoppcn  34611  knoppndvlem4  34622  knoppndvlem6  34624  knoppf  34642  poimirlem3  35707  poimirlem4  35708  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  heiborlem4  35899  heiborlem6  35901  lcmfunnnd  39948  mapfzcons  40454  irrapxlem1  40560  ltrmynn0  40686  ltrmxnn0  40687  acongeq  40721  jm2.23  40734  jm2.26lem3  40739  dfrtrcl3  41230  radcnvrat  41821  bcc0  41847  dvradcnv2  41854  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemradcnv  41859  binomcxplemnotnn0  41863  fzssnn0  42746  expfac  43088  dvnmptdivc  43369  dvnmul  43374  dvnprodlem3  43379  stoweidlem17  43448  stoweidlem34  43465  stirlinglem5  43509  stirlinglem7  43511  fourierdlem15  43553  fourierdlem25  43563  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem52  43589  fourierdlem54  43591  fourierdlem64  43601  fourierdlem65  43602  fourierdlem81  43618  fourierdlem92  43629  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  fourierdlem114  43651  elaa2lem  43664  etransclem4  43669  etransclem10  43675  etransclem14  43679  etransclem15  43680  etransclem23  43688  etransclem24  43689  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem44  43709  etransclem46  43711  etransclem48  43713  ssnn0ssfz  45573  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsuc  45901  ackvalsuc1mpt  45912  aacllem  46391