Theorem nn0uz 12846

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 12573	. 2 ⊢ ℕ0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2		0z 12551	. . 3 ⊢ 0 ∈ ℤ
3		uzval 12806	. . 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 2106  {crab 3431   class class class wbr 5141  ‘cfv 6532  0cc0 11092   ≤ cle 11231  ℕ₀cn0 12454  ℤcz 12540  ℤ_≥cuz 12804

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 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-n0 12455  df-z 12541  df-uz 12805

This theorem is referenced by:  elnn0uz  12849  2eluzge0  12859  eluznn0  12883  nn0inf  12896  fseq1p1m1  13557  fznn0sub2  13590  nn0split  13598  prednn0  13607  fzossnn0  13645  fzennn  13915  hashgf1o  13918  exple1  14123  faclbnd4lem1  14235  bcval5  14260  bcpasc  14263  hashfzo0  14372  hashf1  14400  ccatval2  14510  ccatass  14520  ccatrn  14521  swrdccat2  14601  wrdeqs1cat  14652  cats1un  14653  splfv2a  14688  splval2  14689  revccat  14698  cats1fv  14792  binom1dif  15761  isumnn0nn  15770  climcndslem1  15777  climcnds  15779  harmonic  15787  arisum2  15789  explecnv  15793  geoser  15795  pwdif  15796  geolim  15798  geolim2  15799  geomulcvg  15804  geoisum  15805  geoisumr  15806  mertenslem1  15812  mertenslem2  15813  mertens  15814  fallfacfwd  15962  0fallfac  15963  binomfallfaclem2  15966  bpolylem  15974  bpolysum  15979  bpolydiflem  15980  fsumkthpow  15982  bpoly2  15983  bpoly3  15984  bpoly4  15985  efcllem  16003  ef0lem  16004  eff  16007  efcvg  16010  efcvgfsum  16011  reefcl  16012  ege2le3  16015  efcj  16017  eftlcvg  16031  eftlub  16034  effsumlt  16036  ef4p  16038  efgt1p2  16039  efgt1p  16040  eflegeo  16046  eirrlem  16129  ruclem6  16160  ruclem7  16161  divalglem2  16320  divalglem5  16322  bitsfzolem  16357  bitsfzo  16358  bitsfi  16360  bitsinv1lem  16364  bitsinv1  16365  bitsinvp1  16372  sadcf  16376  sadcp1  16378  sadadd  16390  sadass  16394  bitsres  16396  smupf  16401  smupp1  16403  smuval2  16405  smupval  16411  smueqlem  16413  smumul  16416  alginv  16494  algcvg  16495  algcvga  16498  algfx  16499  eucalgcvga  16505  eucalg  16506  phiprmpw  16691  prmdiv  16700  iserodd  16750  pcfac  16814  prmreclem2  16832  prmreclem4  16834  vdwapun  16889  vdwlem1  16896  ramcl2lem  16924  ramtcl  16925  ramtub  16927  gsumwsubmcl  18693  gsumws1  18694  gsumsgrpccat  18696  gsumwmhm  18701  psgnunilem2  19327  psgnunilem4  19329  sylow1lem1  19430  efginvrel2  19559  efgredleme  19575  efgredlemc  19577  efgcpbllemb  19587  frgpuplem  19604  telgsumfz0s  19818  telgsums  19820  pgpfaclem1  19910  psrbaglefi  21416  psrbaglefiOLD  21417  ltbwe  21527  pmatcollpw3fi1lem1  22217  chfacfisf  22285  chfacfisfcpmat  22286  iscmet3lem3  24736  dyadmax  25044  mbfi1fseqlem3  25164  itgcnlem  25236  dvnff  25369  dvnp1  25371  dvn2bss  25376  cpncn  25382  dveflem  25425  ig1peu  25618  ig1pdvds  25623  ply1termlem  25646  plyeq0lem  25653  plyaddlem1  25656  plymullem1  25657  coeeulem  25667  dgrcl  25676  dgrub  25677  dgrlb  25679  coeid3  25683  plyco  25684  coeeq2  25685  coefv0  25691  coemulhi  25697  coemulc  25698  dvply1  25726  vieta1lem2  25753  vieta1  25754  elqaalem2  25762  elqaalem3  25763  geolim3  25781  dvntaylp  25812  taylthlem1  25814  radcnvlem1  25854  radcnvlem2  25855  radcnvlem3  25856  radcnv0  25857  radcnvlt2  25860  dvradcnv  25862  pserulm  25863  psercn2  25864  pserdvlem2  25869  pserdv2  25871  abelthlem4  25875  abelthlem5  25876  abelthlem6  25877  abelthlem7  25879  abelthlem8  25880  abelthlem9  25881  advlogexp  26092  logtayllem  26096  logtayl  26097  cxpeq  26192  leibpi  26374  leibpisum  26375  log2cnv  26376  log2tlbnd  26377  log2ublem2  26379  birthdaylem3  26385  wilthlem2  26500  ftalem1  26504  ftalem5  26508  basellem2  26513  basellem3  26514  basellem5  26516  musum  26622  0sgmppw  26628  1sgmprm  26629  chtublem  26641  logexprlim  26655  lgseisenlem1  26805  lgsquadlem2  26811  dchrisumlem1  26919  dchrisumlem2  26920  dchrisum0flblem1  26938  ostth2lem3  27065  tgcgr4  27647  clwwlknonex2lem1  29225  eupth2lems  29356  fz2ssnn0  31867  cycpmco2rn  32155  cycpmco2lem6  32161  oddpwdc  33184  eulerpartlemb  33198  sseqfn  33220  sseqf  33222  signsplypnf  33392  signstcl  33407  signstf  33408  signstfvn  33411  signstfvneq0  33414  fsum2dsub  33450  reprsuc  33458  breprexplema  33473  breprexplemc  33475  subfacval2  34009  subfaclim  34010  cvmliftlem7  34113  fwddifnp1  34967  knoppcnlem6  35178  knoppcnlem8  35180  knoppcnlem9  35181  knoppcnlem11  35183  knoppcn  35184  knoppndvlem4  35195  knoppndvlem6  35197  knoppf  35215  poimirlem3  36295  poimirlem4  36296  poimirlem18  36310  poimirlem21  36313  poimirlem22  36314  poimirlem25  36317  poimirlem26  36318  poimirlem27  36319  heiborlem4  36487  heiborlem6  36489  lcmfunnnd  40682  mapfzcons  41225  irrapxlem1  41331  ltrmynn0  41458  ltrmxnn0  41459  acongeq  41493  jm2.23  41506  jm2.26lem3  41511  dfrtrcl3  42255  radcnvrat  42844  bcc0  42870  dvradcnv2  42877  binomcxplemnn0  42879  binomcxplemrat  42880  binomcxplemradcnv  42882  binomcxplemnotnn0  42886  fzssnn0  43800  rexanuz2nf  43976  expfac  44146  dvnmptdivc  44427  dvnmul  44432  dvnprodlem3  44437  stoweidlem17  44506  stoweidlem34  44523  stirlinglem5  44567  stirlinglem7  44569  fourierdlem15  44611  fourierdlem25  44621  fourierdlem48  44643  fourierdlem49  44644  fourierdlem50  44645  fourierdlem52  44647  fourierdlem54  44649  fourierdlem64  44659  fourierdlem65  44660  fourierdlem81  44676  fourierdlem92  44687  fourierdlem102  44697  fourierdlem103  44698  fourierdlem104  44699  fourierdlem113  44708  fourierdlem114  44709  elaa2lem  44722  etransclem4  44727  etransclem10  44733  etransclem14  44737  etransclem15  44738  etransclem23  44746  etransclem24  44747  etransclem31  44754  etransclem32  44755  etransclem35  44758  etransclem44  44767  etransclem46  44769  etransclem48  44771  ssnn0ssfz  46673  itcoval1  46997  itcoval2  46998  itcoval3  46999  itcovalsuc  47001  ackvalsuc1mpt  47012  aacllem  47496