Theorem nn0uz 12789

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3399   class class class wbr 5098  ‘cfv 6492  0cc0 11026   ≤ cle 11167  ℕ₀cn0 12401  ℤcz 12488  ℤ_≥cuz 12751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  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 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489  df-uz 12752

This theorem is referenced by:  elnn0uz  12792  2eluzge0  12794  eluznn0  12830  nn0inf  12843  fseq1p1m1  13514  fznn0sub2  13551  nn0split  13559  prednn0  13568  fzossnn0  13606  fzennn  13891  hashgf1o  13894  exple1  14100  faclbnd4lem1  14216  bcval5  14241  bcpasc  14244  hashfzo0  14353  hashf1  14380  ccatval2  14501  ccatass  14512  ccatrn  14513  swrdccat2  14593  wrdeqs1cat  14643  cats1un  14644  splfv2a  14679  splval2  14680  revccat  14689  cats1fv  14782  binom1dif  15756  isumnn0nn  15765  climcndslem1  15772  climcnds  15774  harmonic  15782  arisum2  15784  explecnv  15788  geoser  15790  pwdif  15791  geolim  15793  geolim2  15794  geomulcvg  15799  geoisum  15800  geoisumr  15801  mertenslem1  15807  mertenslem2  15808  mertens  15809  fallfacfwd  15959  0fallfac  15960  binomfallfaclem2  15963  bpolylem  15971  bpolysum  15976  bpolydiflem  15977  fsumkthpow  15979  bpoly2  15980  bpoly3  15981  bpoly4  15982  efcllem  16000  ef0lem  16001  eff  16004  efcvg  16008  efcvgfsum  16009  reefcl  16010  ege2le3  16013  efcj  16015  eftlcvg  16031  eftlub  16034  effsumlt  16036  ef4p  16038  efgt1p2  16039  efgt1p  16040  eflegeo  16046  eirrlem  16129  ruclem6  16160  ruclem7  16161  divalglem2  16322  divalglem5  16324  bitsfzolem  16361  bitsfzo  16362  bitsfi  16364  bitsinv1lem  16368  bitsinv1  16369  bitsinvp1  16376  sadcf  16380  sadcp1  16382  sadadd  16394  sadass  16398  bitsres  16400  smupf  16405  smupp1  16407  smuval2  16409  smupval  16415  smueqlem  16417  smumul  16420  alginv  16502  algcvg  16503  algcvga  16506  algfx  16507  eucalgcvga  16513  eucalg  16514  phiprmpw  16703  prmdiv  16712  iserodd  16763  pcfac  16827  prmreclem2  16845  prmreclem4  16847  vdwapun  16902  vdwlem1  16909  ramcl2lem  16937  ramtcl  16938  ramtub  16940  chnccats1  18548  gsumwsubmcl  18762  gsumws1  18763  gsumsgrpccat  18765  gsumwmhm  18770  psgnunilem2  19424  psgnunilem4  19426  sylow1lem1  19527  efginvrel2  19656  efgredleme  19672  efgredlemc  19674  efgcpbllemb  19684  frgpuplem  19701  telgsumfz0s  19920  telgsums  19922  pgpfaclem1  20012  psrbaglefi  21882  ltbwe  21999  pmatcollpw3fi1lem1  22730  chfacfisf  22798  chfacfisfcpmat  22799  iscmet3lem3  25246  dyadmax  25555  mbfi1fseqlem3  25674  itgcnlem  25747  dvnff  25881  dvnp1  25883  dvn2bss  25888  cpncn  25894  dveflem  25939  ig1peu  26136  ig1pdvds  26141  ply1termlem  26164  plyeq0lem  26171  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  dgrcl  26194  dgrub  26195  dgrlb  26197  coeid3  26201  plyco  26202  coeeq2  26203  coefv0  26209  coemulhi  26215  coemulc  26216  dvply1  26247  vieta1lem2  26275  vieta1  26276  elqaalem2  26284  elqaalem3  26285  geolim3  26303  dvntaylp  26335  taylthlem1  26337  radcnvlem1  26378  radcnvlem2  26379  radcnvlem3  26380  radcnv0  26381  radcnvlt2  26384  dvradcnv  26386  pserulm  26387  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  pserdv2  26396  abelthlem4  26400  abelthlem5  26401  abelthlem6  26402  abelthlem7  26404  abelthlem8  26405  abelthlem9  26406  advlogexp  26620  logtayllem  26624  logtayl  26625  cxpeq  26723  leibpi  26908  leibpisum  26909  log2cnv  26910  log2tlbnd  26911  log2ublem2  26913  birthdaylem3  26919  wilthlem2  27035  ftalem1  27039  ftalem5  27043  basellem2  27048  basellem3  27049  basellem5  27051  musum  27157  0sgmppw  27165  1sgmprm  27166  chtublem  27178  logexprlim  27192  lgseisenlem1  27342  lgsquadlem2  27348  dchrisumlem1  27456  dchrisumlem2  27457  dchrisum0flblem1  27475  ostth2lem3  27602  tgcgr4  28603  clwwlknonex2lem1  30182  eupth2lems  30313  fz2ssnn0  32865  nn0diffz0  32874  nn0split01  32898  ccatws1f1o  33033  gsummulsubdishift1  33151  gsumwrd2dccat  33160  cycpmco2rn  33207  cycpmco2lem6  33213  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  ig1pmindeg  33683  vietalem  33735  exsslsb  33753  oddpwdc  34511  eulerpartlemb  34525  sseqfn  34547  sseqf  34549  signsplypnf  34707  signstcl  34722  signstf  34723  signstfvn  34726  signstfvneq0  34729  fsum2dsub  34764  reprsuc  34772  breprexplema  34787  breprexplemc  34789  subfacval2  35381  subfaclim  35382  cvmliftlem7  35485  fwddifnp1  36359  knoppcnlem6  36698  knoppcnlem8  36700  knoppcnlem9  36701  knoppcnlem11  36703  knoppcn  36704  knoppndvlem4  36715  knoppndvlem6  36717  knoppf  36735  poimirlem3  37824  poimirlem4  37825  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  heiborlem4  38015  heiborlem6  38017  lcmfunnnd  42266  mapfzcons  42958  irrapxlem1  43064  ltrmynn0  43190  ltrmxnn0  43191  acongeq  43225  jm2.23  43238  jm2.26lem3  43243  dfrtrcl3  43974  radcnvrat  44555  bcc0  44581  dvradcnv2  44588  binomcxplemnn0  44590  binomcxplemrat  44591  binomcxplemradcnv  44593  binomcxplemnotnn0  44597  fzssnn0  45564  rexanuz2nf  45736  expfac  45901  dvnmptdivc  46182  dvnmul  46187  dvnprodlem3  46192  stoweidlem17  46261  stoweidlem34  46278  stirlinglem5  46322  stirlinglem7  46324  fourierdlem15  46366  fourierdlem25  46376  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem52  46402  fourierdlem54  46404  fourierdlem64  46414  fourierdlem65  46415  fourierdlem81  46431  fourierdlem92  46442  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  fourierdlem114  46464  elaa2lem  46477  etransclem4  46482  etransclem10  46488  etransclem14  46492  etransclem15  46493  etransclem23  46501  etransclem24  46502  etransclem31  46509  etransclem32  46510  etransclem35  46513  etransclem44  46522  etransclem46  46524  etransclem48  46526  chnerlem1  47126  chnerlem2  47127  ssnn0ssfz  48595  itcoval1  48909  itcoval2  48910  itcoval3  48911  itcovalsuc  48913  ackvalsuc1mpt  48924  aacllem  50046