Theorem nn0uz 12268

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  {crab 3110   class class class wbr 5030  ‘cfv 6324  0cc0 10526   ≤ cle 10665  ℕ₀cn0 11885  ℤcz 11969  ℤ_≥cuz 12231

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232

This theorem is referenced by:  elnn0uz  12271  2eluzge0  12281  eluznn0  12305  nn0inf  12318  fseq1p1m1  12976  fznn0sub2  13009  nn0split  13017  prednn0  13026  fzossnn0  13063  fzennn  13331  hashgf1o  13334  exple1  13536  faclbnd4lem1  13649  bcval5  13674  bcpasc  13677  hashfzo0  13787  hashf1  13811  ccatval2  13923  ccatass  13933  ccatrn  13934  swrdccat2  14022  wrdeqs1cat  14073  cats1un  14074  splfv2a  14109  splval2  14110  revccat  14119  cats1fv  14212  binom1dif  15180  isumnn0nn  15189  climcndslem1  15196  climcnds  15198  harmonic  15206  arisum2  15208  explecnv  15212  geoser  15214  pwdif  15215  geolim  15218  geolim2  15219  geomulcvg  15224  geoisum  15225  geoisumr  15226  mertenslem1  15232  mertenslem2  15233  mertens  15234  fallfacfwd  15382  0fallfac  15383  binomfallfaclem2  15386  bpolylem  15394  bpolysum  15399  bpolydiflem  15400  fsumkthpow  15402  bpoly2  15403  bpoly3  15404  bpoly4  15405  efcllem  15423  ef0lem  15424  eff  15427  efcvg  15430  efcvgfsum  15431  reefcl  15432  ege2le3  15435  efcj  15437  eftlcvg  15451  eftlub  15454  effsumlt  15456  ef4p  15458  efgt1p2  15459  efgt1p  15460  eflegeo  15466  eirrlem  15549  ruclem6  15580  ruclem7  15581  divalglem2  15736  divalglem5  15738  bitsfzolem  15773  bitsfzo  15774  bitsfi  15776  bitsinv1lem  15780  bitsinv1  15781  bitsinvp1  15788  sadcf  15792  sadcp1  15794  sadadd  15806  sadass  15810  bitsres  15812  smupf  15817  smupp1  15819  smuval2  15821  smupval  15827  smueqlem  15829  smumul  15832  alginv  15909  algcvg  15910  algcvga  15913  algfx  15914  eucalgcvga  15920  eucalg  15921  phiprmpw  16103  prmdiv  16112  iserodd  16162  pcfac  16225  prmreclem2  16243  prmreclem4  16245  vdwapun  16300  vdwlem1  16307  ramcl2lem  16335  ramtcl  16336  ramtub  16338  gsumwsubmcl  17993  gsumws1  17994  gsumsgrpccat  17996  gsumccatOLD  17997  gsumwmhm  18002  psgnunilem2  18615  psgnunilem4  18617  sylow1lem1  18715  efginvrel2  18845  efgredleme  18861  efgredlemc  18863  efgcpbllemb  18873  frgpuplem  18890  telgsumfz0s  19104  telgsums  19106  pgpfaclem1  19196  psrbaglefi  20610  ltbwe  20712  pmatcollpw3fi1lem1  21391  chfacfisf  21459  chfacfisfcpmat  21460  iscmet3lem3  23894  dyadmax  24202  mbfi1fseqlem3  24321  itgcnlem  24393  dvnff  24526  dvnp1  24528  dvn2bss  24533  cpncn  24539  dveflem  24582  ig1peu  24772  ig1pdvds  24777  ply1termlem  24800  plyeq0lem  24807  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  dgrcl  24830  dgrub  24831  dgrlb  24833  coeid3  24837  plyco  24838  coeeq2  24839  coefv0  24845  coemulhi  24851  coemulc  24852  dvply1  24880  vieta1lem2  24907  vieta1  24908  elqaalem2  24916  elqaalem3  24917  geolim3  24935  dvntaylp  24966  taylthlem1  24968  radcnvlem1  25008  radcnvlem2  25009  radcnvlem3  25010  radcnv0  25011  radcnvlt2  25014  dvradcnv  25016  pserulm  25017  psercn2  25018  pserdvlem2  25023  pserdv2  25025  abelthlem4  25029  abelthlem5  25030  abelthlem6  25031  abelthlem7  25033  abelthlem8  25034  abelthlem9  25035  advlogexp  25246  logtayllem  25250  logtayl  25251  cxpeq  25346  leibpi  25528  leibpisum  25529  log2cnv  25530  log2tlbnd  25531  log2ublem2  25533  birthdaylem3  25539  wilthlem2  25654  ftalem1  25658  ftalem5  25662  basellem2  25667  basellem3  25668  basellem5  25670  musum  25776  0sgmppw  25782  1sgmprm  25783  chtublem  25795  logexprlim  25809  lgseisenlem1  25959  lgsquadlem2  25965  dchrisumlem1  26073  dchrisumlem2  26074  dchrisum0flblem1  26092  ostth2lem3  26219  tgcgr4  26325  clwwlknonex2lem1  27892  eupth2lems  28023  fz2ssnn0  30534  cycpmco2rn  30817  cycpmco2lem6  30823  oddpwdc  31722  eulerpartlemb  31736  sseqfn  31758  sseqf  31760  signsplypnf  31930  signstcl  31945  signstf  31946  signstfvn  31949  signstfvneq0  31952  fsum2dsub  31988  reprsuc  31996  breprexplema  32011  breprexplemc  32013  subfacval2  32547  subfaclim  32548  cvmliftlem7  32651  fwddifnp1  33739  knoppcnlem6  33950  knoppcnlem8  33952  knoppcnlem9  33953  knoppcnlem11  33955  knoppcn  33956  knoppndvlem4  33967  knoppndvlem6  33969  knoppf  33987  poimirlem3  35060  poimirlem4  35061  poimirlem18  35075  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  heiborlem4  35252  heiborlem6  35254  lcmfunnnd  39300  mapfzcons  39657  irrapxlem1  39763  ltrmynn0  39889  ltrmxnn0  39890  acongeq  39924  jm2.23  39937  jm2.26lem3  39942  dfrtrcl3  40434  radcnvrat  41018  bcc0  41044  dvradcnv2  41051  binomcxplemnn0  41053  binomcxplemrat  41054  binomcxplemradcnv  41056  binomcxplemnotnn0  41060  fzssnn0  41949  expfac  42299  dvnmptdivc  42580  dvnmul  42585  dvnprodlem3  42590  stoweidlem17  42659  stoweidlem34  42676  stirlinglem5  42720  stirlinglem7  42722  fourierdlem15  42764  fourierdlem25  42774  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem52  42800  fourierdlem54  42802  fourierdlem64  42812  fourierdlem65  42813  fourierdlem81  42829  fourierdlem92  42840  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem113  42861  fourierdlem114  42862  elaa2lem  42875  etransclem4  42880  etransclem10  42886  etransclem14  42890  etransclem15  42891  etransclem23  42899  etransclem24  42900  etransclem31  42907  etransclem32  42908  etransclem35  42911  etransclem44  42920  etransclem46  42922  etransclem48  42924  ssnn0ssfz  44751  itcoval1  45077  itcoval2  45078  itcoval3  45079  itcovalsuc  45081  ackvalsuc1mpt  45092  aacllem  45329