Theorem nn0uz 12811

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3402   class class class wbr 5102  ‘cfv 6499  0cc0 11044   ≤ cle 11185  ℕ₀cn0 12418  ℤcz 12505  ℤ_≥cuz 12769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506  df-uz 12770

This theorem is referenced by:  elnn0uz  12814  2eluzge0  12816  eluznn0  12852  nn0inf  12865  fseq1p1m1  13535  fznn0sub2  13572  nn0split  13580  prednn0  13589  fzossnn0  13627  fzennn  13909  hashgf1o  13912  exple1  14118  faclbnd4lem1  14234  bcval5  14259  bcpasc  14262  hashfzo0  14371  hashf1  14398  ccatval2  14519  ccatass  14529  ccatrn  14530  swrdccat2  14610  wrdeqs1cat  14661  cats1un  14662  splfv2a  14697  splval2  14698  revccat  14707  cats1fv  14801  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  15978  0fallfac  15979  binomfallfaclem2  15982  bpolylem  15990  bpolysum  15995  bpolydiflem  15996  fsumkthpow  15998  bpoly2  15999  bpoly3  16000  bpoly4  16001  efcllem  16019  ef0lem  16020  eff  16023  efcvg  16027  efcvgfsum  16028  reefcl  16029  ege2le3  16032  efcj  16034  eftlcvg  16050  eftlub  16053  effsumlt  16055  ef4p  16057  efgt1p2  16058  efgt1p  16059  eflegeo  16065  eirrlem  16148  ruclem6  16179  ruclem7  16180  divalglem2  16341  divalglem5  16343  bitsfzolem  16380  bitsfzo  16381  bitsfi  16383  bitsinv1lem  16387  bitsinv1  16388  bitsinvp1  16395  sadcf  16399  sadcp1  16401  sadadd  16413  sadass  16417  bitsres  16419  smupf  16424  smupp1  16426  smuval2  16428  smupval  16434  smueqlem  16436  smumul  16439  alginv  16521  algcvg  16522  algcvga  16525  algfx  16526  eucalgcvga  16532  eucalg  16533  phiprmpw  16722  prmdiv  16731  iserodd  16782  pcfac  16846  prmreclem2  16864  prmreclem4  16866  vdwapun  16921  vdwlem1  16928  ramcl2lem  16956  ramtcl  16957  ramtub  16959  gsumwsubmcl  18740  gsumws1  18741  gsumsgrpccat  18743  gsumwmhm  18748  psgnunilem2  19401  psgnunilem4  19403  sylow1lem1  19504  efginvrel2  19633  efgredleme  19649  efgredlemc  19651  efgcpbllemb  19661  frgpuplem  19678  telgsumfz0s  19897  telgsums  19899  pgpfaclem1  19989  psrbaglefi  21811  ltbwe  21927  pmatcollpw3fi1lem1  22649  chfacfisf  22717  chfacfisfcpmat  22718  iscmet3lem3  25166  dyadmax  25475  mbfi1fseqlem3  25594  itgcnlem  25667  dvnff  25801  dvnp1  25803  dvn2bss  25808  cpncn  25814  dveflem  25859  ig1peu  26056  ig1pdvds  26061  ply1termlem  26084  plyeq0lem  26091  plyaddlem1  26094  plymullem1  26095  coeeulem  26105  dgrcl  26114  dgrub  26115  dgrlb  26117  coeid3  26121  plyco  26122  coeeq2  26123  coefv0  26129  coemulhi  26135  coemulc  26136  dvply1  26167  vieta1lem2  26195  vieta1  26196  elqaalem2  26204  elqaalem3  26205  geolim3  26223  dvntaylp  26255  taylthlem1  26257  radcnvlem1  26298  radcnvlem2  26299  radcnvlem3  26300  radcnv0  26301  radcnvlt2  26304  dvradcnv  26306  pserulm  26307  psercn2  26308  psercn2OLD  26309  pserdvlem2  26314  pserdv2  26316  abelthlem4  26320  abelthlem5  26321  abelthlem6  26322  abelthlem7  26324  abelthlem8  26325  abelthlem9  26326  advlogexp  26540  logtayllem  26544  logtayl  26545  cxpeq  26643  leibpi  26828  leibpisum  26829  log2cnv  26830  log2tlbnd  26831  log2ublem2  26833  birthdaylem3  26839  wilthlem2  26955  ftalem1  26959  ftalem5  26963  basellem2  26968  basellem3  26969  basellem5  26971  musum  27077  0sgmppw  27085  1sgmprm  27086  chtublem  27098  logexprlim  27112  lgseisenlem1  27262  lgsquadlem2  27268  dchrisumlem1  27376  dchrisumlem2  27377  dchrisum0flblem1  27395  ostth2lem3  27522  tgcgr4  28434  clwwlknonex2lem1  30009  eupth2lems  30140  fz2ssnn0  32681  nn0split01  32715  ccatws1f1o  32846  chnccats1  32914  gsumwrd2dccat  32980  cycpmco2rn  33055  cycpmco2lem6  33061  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ig1pmindeg  33540  exsslsb  33565  oddpwdc  34318  eulerpartlemb  34332  sseqfn  34354  sseqf  34356  signsplypnf  34514  signstcl  34529  signstf  34530  signstfvn  34533  signstfvneq0  34536  fsum2dsub  34571  reprsuc  34579  breprexplema  34594  breprexplemc  34596  subfacval2  35147  subfaclim  35148  cvmliftlem7  35251  fwddifnp1  36126  knoppcnlem6  36459  knoppcnlem8  36461  knoppcnlem9  36462  knoppcnlem11  36464  knoppcn  36465  knoppndvlem4  36476  knoppndvlem6  36478  knoppf  36496  poimirlem3  37590  poimirlem4  37591  poimirlem18  37605  poimirlem21  37608  poimirlem22  37609  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  heiborlem4  37781  heiborlem6  37783  lcmfunnnd  41973  mapfzcons  42677  irrapxlem1  42783  ltrmynn0  42910  ltrmxnn0  42911  acongeq  42945  jm2.23  42958  jm2.26lem3  42963  dfrtrcl3  43695  radcnvrat  44276  bcc0  44302  dvradcnv2  44309  binomcxplemnn0  44311  binomcxplemrat  44312  binomcxplemradcnv  44314  binomcxplemnotnn0  44318  fzssnn0  45287  rexanuz2nf  45461  expfac  45628  dvnmptdivc  45909  dvnmul  45914  dvnprodlem3  45919  stoweidlem17  45988  stoweidlem34  46005  stirlinglem5  46049  stirlinglem7  46051  fourierdlem15  46093  fourierdlem25  46103  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem52  46129  fourierdlem54  46131  fourierdlem64  46141  fourierdlem65  46142  fourierdlem81  46158  fourierdlem92  46169  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  fourierdlem114  46191  elaa2lem  46204  etransclem4  46209  etransclem10  46215  etransclem14  46219  etransclem15  46220  etransclem23  46228  etransclem24  46229  etransclem31  46236  etransclem32  46237  etransclem35  46240  etransclem44  46249  etransclem46  46251  etransclem48  46253  ssnn0ssfz  48310  itcoval1  48625  itcoval2  48626  itcoval3  48627  itcovalsuc  48629  ackvalsuc1mpt  48640  aacllem  49763