Theorem nn0uz 9587

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

Syntax hints:   = wceq 1364   ∈ wcel 2160  {crab 2472   class class class wbr 4018  ‘cfv 5232  0cc0 7836   ≤ cle 8018  ℕ₀cn0 9201  ℤcz 9278  ℤ_≥cuz 9553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7927  ax-resscn 7928  ax-1cn 7929  ax-1re 7930  ax-icn 7931  ax-addcl 7932  ax-addrcl 7933  ax-mulcl 7934  ax-addcom 7936  ax-addass 7938  ax-distr 7940  ax-i2m1 7941  ax-0lt1 7942  ax-0id 7944  ax-rnegex 7945  ax-cnre 7947  ax-pre-ltirr 7948  ax-pre-ltwlin 7949  ax-pre-lttrn 7950  ax-pre-ltadd 7952

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-iota 5193  df-fun 5234  df-fv 5240  df-riota 5848  df-ov 5895  df-oprab 5896  df-mpo 5897  df-pnf 8019  df-mnf 8020  df-xr 8021  df-ltxr 8022  df-le 8023  df-sub 8155  df-neg 8156  df-inn 8945  df-n0 9202  df-z 9279  df-uz 9554

This theorem is referenced by:  elnn0uz  9590  2eluzge0  9600  eluznn0  9624  fseq1p1m1  10119  fz01or  10136  fznn0sub2  10153  nn0split  10161  fzossnn0  10200  frecfzennn  10452  frechashgf1o  10454  exple1  10602  bcval5  10770  bcpasc  10773  hashcl  10788  hashfzo0  10830  zfz1isolemsplit  10845  binom1dif  11522  isumnn0nn  11528  arisum2  11534  expcnvre  11538  explecnv  11540  geoserap  11542  geolim  11546  geolim2  11547  geoisum  11552  geoisumr  11553  mertenslemub  11569  mertenslemi1  11570  mertenslem2  11571  mertensabs  11572  efcllemp  11693  ef0lem  11695  efval  11696  eff  11698  efcvg  11701  efcvgfsum  11702  reefcl  11703  ege2le3  11706  efcj  11708  eftlcvg  11722  eftlub  11725  effsumlt  11727  ef4p  11729  efgt1p2  11730  efgt1p  11731  eflegeo  11736  eirraplem  11811  alginv  12074  algcvg  12075  algcvga  12078  algfx  12079  eucalgcvga  12085  eucalg  12086  phiprmpw  12249  prmdiv  12262  pcfac  12377  ennnfonelemh  12450  ennnfonelemp1  12452  ennnfonelemom  12454  ennnfonelemkh  12458  ennnfonelemrn  12465  dveflem  14624  lgseisenlem1  14887