Theorem nn0uz 12901

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  {crab 3416   class class class wbr 5110  ‘cfv 6538  0cc0 11101   ≤ cle 11245  ℕ₀cn0 12505  ℤcz 12592  ℤ_≥cuz 12863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-n0 12506  df-z 12593  df-uz 12864

This theorem is referenced by:  elnn0uz  12904  2eluzge0  12906  eluznn0  12942  nn0inf  12955  fseq1p1m1  13628  fznn0sub2  13665  nn0split  13673  prednn0  13682  fzossnn0  13721  fzennn  14006  hashgf1o  14009  exple1  14215  faclbnd4lem1  14331  bcval5  14356  bcpasc  14359  hashfzo0  14469  hashf1  14496  ccatval2  14617  ccatass  14628  ccatrn  14629  swrdccat2  14709  wrdeqs1cat  14759  cats1un  14760  splfv2a  14795  splval2  14796  revccat  14805  cats1fv  14898  binom1dif  15889  isumnn0nn  15898  climcndslem1  15905  climcnds  15907  harmonic  15915  arisum2  15917  explecnv  15921  geoser  15923  pwdif  15924  geolim  15926  geolim2  15927  geomulcvg  15932  geoisum  15933  geoisumr  15934  mertenslem1  15940  mertenslem2  15941  mertens  15942  fallfacfwd  16091  0fallfac  16092  binomfallfaclem2  16095  bpolylem  16103  bpolysum  16108  bpolydiflem  16109  fsumkthpow  16111  bpoly2  16112  bpoly3  16113  bpoly4  16114  efcllem  16132  ef0lem  16133  eff  16136  efcvg  16140  efcvgfsum  16141  reefcl  16142  ege2le3  16145  efcj  16147  eftlcvg  16163  eftlub  16166  effsumlt  16168  ef4p  16170  efgt1p2  16171  efgt1p  16172  eflegeo  16178  eirrlem  16261  ruclem6  16292  ruclem7  16293  divalglem2  16454  divalglem5  16456  bitsfzolem  16493  bitsfzo  16494  bitsfi  16496  bitsinv1lem  16500  bitsinv1  16501  bitsinvp1  16508  sadcf  16512  sadcp1  16514  sadadd  16526  sadass  16530  bitsres  16532  smupf  16537  smupp1  16539  smuval2  16541  smupval  16547  smueqlem  16549  smumul  16552  alginv  16634  algcvg  16635  algcvga  16638  algfx  16639  eucalgcvga  16645  eucalg  16646  phiprmpw  16836  prmdiv  16845  iserodd  16896  pcfac  16960  prmreclem2  16978  prmreclem4  16980  vdwapun  17035  vdwlem1  17042  ramcl2lem  17070  ramtcl  17071  ramtub  17073  chnccats1  18682  gsumwsubmcl  18897  gsumws1  18898  gsumsgrpccat  18900  gsumwmhm  18905  psgnunilem2  19566  psgnunilem4  19568  sylow1lem1  19669  efginvrel2  19798  efgredleme  19814  efgredlemc  19816  efgcpbllemb  19826  frgpuplem  19843  telgsumfz0s  20062  telgsums  20064  pgpfaclem1  20154  psrbaglefi  22057  ltbwe  22176  pmatcollpw3fi1lem1  22924  chfacfisf  22992  chfacfisfcpmat  22993  iscmet3lem3  25430  dyadmax  25738  mbfi1fseqlem3  25857  itgcnlem  25930  dvnff  26063  dvnp1  26065  dvn2bss  26070  cpncn  26076  dveflem  26119  ig1peu  26313  ig1pdvds  26318  ply1termlem  26341  plyeq0lem  26348  plyaddlem1  26351  plymullem1  26352  coeeulem  26362  dgrcl  26371  dgrub  26372  dgrlb  26374  coeid3  26378  plyco  26379  coeeq2  26380  coefv0  26386  coemulhi  26392  coemulc  26393  dvply1  26426  vieta1lem2  26453  vieta1  26454  elqaalem2  26462  elqaalem3  26463  geolim3  26483  dvntaylp  26515  taylthlem1  26517  radcnvlem1  26557  radcnvlem2  26558  radcnvlem3  26559  radcnv0  26560  radcnvlt2  26563  dvradcnv  26565  pserulm  26566  psercn2  26567  pserdvlem2  26572  pserdv2  26574  abelthlem4  26578  abelthlem5  26579  abelthlem6  26580  abelthlem7  26582  abelthlem8  26583  abelthlem9  26584  advlogexp  26801  logtayllem  26805  logtayl  26806  cxpeq  26903  leibpi  27088  leibpisum  27089  log2cnv  27090  log2tlbnd  27091  log2ublem2  27093  birthdaylem3  27099  wilthlem2  27214  ftalem1  27218  ftalem5  27222  basellem2  27227  basellem3  27228  basellem5  27230  musum  27336  0sgmppw  27343  1sgmprm  27344  chtublem  27356  logexprlim  27370  lgseisenlem1  27520  lgsquadlem2  27526  dchrisumlem1  27634  dchrisumlem2  27635  dchrisum0flblem1  27653  ostth2lem3  27780  tgcgr4  28781  clwwlknonex2lem1  30439  eupth2lems  30570  fz2ssnn0  33111  nn0diffz0  33120  nn0split01  33143  ccatws1f1o  33252  gsummulsubdishift1  33369  gsumwrd2dccat  33379  cycpmco2rn  33426  cycpmco2lem6  33432  evl1deg1  33847  evl1deg2  33848  evl1deg3  33849  ig1pmindeg  33873  vietalem  33950  exsslsb  33968  oddpwdc  34725  eulerpartlemb  34739  sseqfn  34761  sseqf  34763  signsplypnf  34918  signstcl  34933  signstf  34934  signstfvn  34937  signstfvneq0  34940  fsum2dsub  34975  reprsuc  34983  breprexplema  34998  breprexplemc  35000  subfacval2  35660  subfaclim  35661  cvmliftlem7  35764  fwddifnp1  36638  knoppcnlem6  37068  knoppcnlem8  37070  knoppcnlem9  37071  knoppcnlem11  37073  knoppcn  37074  knoppndvlem4  37085  knoppndvlem6  37087  knoppf  37105  poimirlem3  38255  poimirlem4  38256  poimirlem18  38270  poimirlem21  38273  poimirlem22  38274  poimirlem25  38277  poimirlem26  38278  poimirlem27  38279  heiborlem4  38446  heiborlem6  38448  lcmfunnnd  42760  mapfzcons  43430  irrapxlem1  43532  ltrmynn0  43658  ltrmxnn0  43659  acongeq  43693  jm2.23  43706  jm2.26lem3  43711  dfrtrcl3  44442  radcnvrat  45007  bcc0  45033  dvradcnv2  45040  binomcxplemnn0  45042  binomcxplemrat  45043  binomcxplemradcnv  45045  binomcxplemnotnn0  45049  fzssnn0  46018  rexanuz2nf  46189  expfac  46354  dvnmptdivc  46635  dvnmul  46640  dvnprodlem3  46645  stoweidlem17  46714  stoweidlem34  46731  stirlinglem5  46775  stirlinglem7  46777  fourierdlem15  46819  fourierdlem25  46829  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  fourierdlem52  46855  fourierdlem54  46857  fourierdlem64  46867  fourierdlem65  46868  fourierdlem81  46884  fourierdlem92  46895  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem113  46916  fourierdlem114  46917  elaa2lem  46930  etransclem4  46935  etransclem10  46941  etransclem14  46945  etransclem15  46946  etransclem23  46954  etransclem24  46955  etransclem31  46962  etransclem32  46963  etransclem35  46966  etransclem44  46975  etransclem46  46977  etransclem48  46979  chnerlem1  47581  chnerlem2  47582  ssnn0ssfz  49112  itcoval1  49426  itcoval2  49427  itcoval3  49428  itcovalsuc  49430  ackvalsuc1mpt  49441  aacllem  50584