Theorem nn0uz 12912

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {crab 3418   class class class wbr 5111  ‘cfv 6540  0cc0 11111   ≤ cle 11255  ℕ₀cn0 12515  ℤcz 12602  ℤ_≥cuz 12874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  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 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-nn 12245  df-n0 12516  df-z 12603  df-uz 12875

This theorem is used by:  elnn0uz  12915  2eluzge0  12917  eluznn0  12953  nn0inf  12966  fseq1p1m1  13639  fznn0sub2  13676  nn0split  13684  prednn0  13693  fzossnn0  13732  fzennn  14018  hashgf1o  14021  exple1  14227  faclbnd4lem1  14343  bcval5  14368  bcpasc  14371  hashfzo0  14481  hashf1  14508  ccatval2  14629  ccatass  14640  ccatrn  14641  swrdccat2  14725  wrdeqs1cat  14775  cats1un  14776  splfv2a  14811  splval2  14812  revccat  14821  cats1fv  14916  binom1dif  15906  isumnn0nn  15915  climcndslem1  15922  climcnds  15924  harmonic  15932  arisum2  15934  explecnv  15938  geoser  15940  pwdif  15941  geolim  15943  geolim2  15944  geomulcvg  15949  geoisum  15950  geoisumr  15951  mertenslem1  15957  mertenslem2  15958  mertens  15959  fallfacfwd  16108  0fallfac  16109  binomfallfaclem2  16112  bpolylem  16120  bpolysum  16125  bpolydiflem  16126  fsumkthpow  16128  bpoly2  16129  bpoly3  16130  bpoly4  16131  efcllem  16149  ef0lem  16150  eff  16153  efcvg  16157  efcvgfsum  16158  reefcl  16159  ege2le3  16162  efcj  16164  eftlcvg  16180  eftlub  16183  effsumlt  16185  ef4p  16187  efgt1p2  16188  efgt1p  16189  eflegeo  16195  eirrlem  16278  ruclem6  16309  ruclem7  16310  divalglem2  16471  divalglem5  16473  bitsfzolem  16510  bitsfzo  16511  bitsfi  16513  bitsinv1lem  16517  bitsinv1  16518  bitsinvp1  16525  sadcf  16529  sadcp1  16531  sadadd  16543  sadass  16547  bitsres  16549  smupf  16554  smupp1  16556  smuval2  16558  smupval  16564  smueqlem  16566  smumul  16569  alginv  16651  algcvg  16652  algcvga  16655  algfx  16656  eucalgcvga  16662  eucalg  16663  phiprmpw  16853  prmdiv  16862  iserodd  16913  pcfac  16977  prmreclem2  16995  prmreclem4  16997  vdwapun  17052  vdwlem1  17059  ramcl2lem  17087  ramtcl  17088  ramtub  17090  chnccats1  18699  gsumwsubmcl  18920  gsumws1  18921  gsumsgrpccat  18923  gsumwmhm  18928  psgnunilem2  19589  psgnunilem4  19591  sylow1lem1  19692  efginvrel2  19821  efgredleme  19837  efgredlemc  19839  efgcpbllemb  19849  frgpuplem  19866  telgsumfz0s  20085  telgsums  20087  pgpfaclem1  20177  psrbaglefi  22106  ltbwe  22225  pmatcollpw3fi1lem1  22973  chfacfisf  23041  chfacfisfcpmat  23042  iscmet3lem3  25480  dyadmax  25788  mbfi1fseqlem3  25907  itgcnlem  25980  dvnff  26113  dvnp1  26115  dvn2bss  26120  cpncn  26126  dveflem  26169  ig1peu  26363  ig1pdvds  26368  ply1termlem  26391  plyeq0lem  26398  plyaddlem1  26401  plymullem1  26402  coeeulem  26412  dgrcl  26421  dgrub  26422  dgrlb  26424  coeid3  26428  plyco  26429  coeeq2  26430  coefv0  26436  coemulhi  26442  coemulc  26443  dvply1  26476  vieta1lem2  26503  vieta1  26504  elqaalem2  26512  elqaalem3  26513  geolim3  26533  dvntaylp  26565  taylthlem1  26567  radcnvlem1  26607  radcnvlem2  26608  radcnvlem3  26609  radcnv0  26610  radcnvlt2  26613  dvradcnv  26615  pserulm  26616  psercn2  26617  pserdvlem2  26622  pserdv2  26624  abelthlem4  26628  abelthlem5  26629  abelthlem6  26630  abelthlem7  26632  abelthlem8  26633  abelthlem9  26634  advlogexp  26851  logtayllem  26855  logtayl  26856  cxpeq  26953  leibpi  27138  leibpisum  27139  log2cnv  27140  log2tlbnd  27141  log2ublem2  27143  birthdaylem3  27149  wilthlem2  27264  ftalem1  27268  ftalem5  27272  basellem2  27277  basellem3  27278  basellem5  27280  musum  27386  0sgmppw  27393  1sgmprm  27394  chtublem  27406  logexprlim  27420  lgseisenlem1  27570  lgsquadlem2  27576  dchrisumlem1  27684  dchrisumlem2  27685  dchrisum0flblem1  27703  ostth2lem3  27830  tgcgr4  28831  clwwlknonex2lem1  30501  eupth2lems  30636  fz2ssnn0  33176  nn0diffz0  33185  nn0split01  33208  ccatws1f1o  33313  gsummulsubdishift1  33428  gsumwrd2dccat  33438  cycpmco2rn  33485  cycpmco2lem6  33491  evl1deg1  33906  evl1deg2  33907  evl1deg3  33908  ig1pmindeg  33932  vietalem  34009  exsslsb  34027  oddpwdc  34785  eulerpartlemb  34799  sseqfn  34821  sseqf  34823  signsplypnf  34978  signstcl  34993  signstf  34994  signstfvn  34997  signstfvneq0  35000  fsum2dsub  35035  reprsuc  35043  breprexplema  35058  breprexplemc  35060  subfacval2  35692  subfaclim  35693  cvmliftlem7  35796  fwddifnp1  36670  knoppcnlem6  37120  knoppcnlem8  37122  knoppcnlem9  37123  knoppcnlem11  37125  knoppcn  37126  knoppndvlem4  37137  knoppndvlem6  37139  knoppf  37157  poimirlem3  38307  poimirlem4  38308  poimirlem18  38322  poimirlem21  38325  poimirlem22  38326  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  heiborlem4  38498  heiborlem6  38500  lcmfunnnd  42812  mapfzcons  43480  irrapxlem1  43582  ltrmynn0  43708  ltrmxnn0  43709  acongeq  43743  jm2.23  43756  jm2.26lem3  43761  dfrtrcl3  44492  radcnvrat  45057  bcc0  45083  dvradcnv2  45090  binomcxplemnn0  45092  binomcxplemrat  45093  binomcxplemradcnv  45095  binomcxplemnotnn0  45099  fzssnn0  46068  rexanuz2nf  46239  expfac  46404  dvnmptdivc  46685  dvnmul  46690  dvnprodlem3  46695  stoweidlem17  46764  stoweidlem34  46781  stirlinglem5  46825  stirlinglem7  46827  fourierdlem15  46869  fourierdlem25  46879  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem52  46905  fourierdlem54  46907  fourierdlem64  46917  fourierdlem65  46918  fourierdlem81  46934  fourierdlem92  46945  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem113  46966  fourierdlem114  46967  elaa2lem  46980  etransclem4  46985  etransclem10  46991  etransclem14  46995  etransclem15  46996  etransclem23  47004  etransclem24  47005  etransclem31  47012  etransclem32  47013  etransclem35  47016  etransclem44  47025  etransclem46  47027  etransclem48  47029  chnerlem1  47631  chnerlem2  47632  ssnn0ssfz  49162  itcoval1  49476  itcoval2  49477  itcoval3  49478  itcovalsuc  49480  ackvalsuc1mpt  49491  aacllem  50654