Theorem nn0uz 12279

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

Syntax hints:   = wceq 1533   ∈ wcel 2110  {crab 3142   class class class wbr 5065  ‘cfv 6354  0cc0 10536   ≤ cle 10675  ℕ₀cn0 11896  ℤcz 11980  ℤ_≥cuz 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-nn 11638  df-n0 11897  df-z 11981  df-uz 12243

This theorem is referenced by:  elnn0uz  12282  2eluzge0  12292  eluznn0  12316  nn0inf  12329  fseq1p1m1  12980  fznn0sub2  13013  nn0split  13021  prednn0  13030  fzossnn0  13067  fzennn  13335  hashgf1o  13338  exple1  13539  faclbnd4lem1  13652  bcval5  13677  bcpasc  13680  hashfzo0  13790  hashf1  13814  ccatval2  13931  ccatass  13941  ccatrn  13942  swrdccat2  14030  wrdeqs1cat  14081  cats1un  14082  splfv2a  14117  splval2  14118  revccat  14127  cats1fv  14220  binom1dif  15187  isumnn0nn  15196  climcndslem1  15203  climcnds  15205  harmonic  15213  arisum2  15215  explecnv  15219  geoser  15221  pwdif  15222  geolim  15225  geolim2  15226  geomulcvg  15231  geoisum  15232  geoisumr  15233  mertenslem1  15239  mertenslem2  15240  mertens  15241  fallfacfwd  15389  0fallfac  15390  binomfallfaclem2  15393  bpolylem  15401  bpolysum  15406  bpolydiflem  15407  fsumkthpow  15409  bpoly2  15410  bpoly3  15411  bpoly4  15412  efcllem  15430  ef0lem  15431  eff  15434  efcvg  15437  efcvgfsum  15438  reefcl  15439  ege2le3  15442  efcj  15444  eftlcvg  15458  eftlub  15461  effsumlt  15463  ef4p  15465  efgt1p2  15466  efgt1p  15467  eflegeo  15473  eirrlem  15556  ruclem6  15587  ruclem7  15588  divalglem2  15745  divalglem5  15747  bitsfzolem  15782  bitsfzo  15783  bitsfi  15785  bitsinv1lem  15789  bitsinv1  15790  bitsinvp1  15797  sadcf  15801  sadcp1  15803  sadadd  15815  sadass  15819  bitsres  15821  smupf  15826  smupp1  15828  smuval2  15830  smupval  15836  smueqlem  15838  smumul  15841  alginv  15918  algcvg  15919  algcvga  15922  algfx  15923  eucalgcvga  15929  eucalg  15930  phiprmpw  16112  prmdiv  16121  iserodd  16171  pcfac  16234  prmreclem2  16252  prmreclem4  16254  vdwapun  16309  vdwlem1  16316  ramcl2lem  16344  ramtcl  16345  ramtub  16347  gsumwsubmcl  18000  gsumws1  18001  gsumsgrpccat  18003  gsumccatOLD  18004  gsumwmhm  18009  psgnunilem2  18622  psgnunilem4  18624  sylow1lem1  18722  efginvrel2  18852  efgredleme  18868  efgredlemc  18870  efgcpbllemb  18880  frgpuplem  18897  telgsumfz0s  19110  telgsums  19112  pgpfaclem1  19202  psrbaglefi  20151  ltbwe  20252  pmatcollpw3fi1lem1  21393  chfacfisf  21461  chfacfisfcpmat  21462  iscmet3lem3  23892  dyadmax  24198  mbfi1fseqlem3  24317  itgcnlem  24389  dvnff  24519  dvnp1  24521  dvn2bss  24526  cpncn  24532  dveflem  24575  ig1peu  24764  ig1pdvds  24769  ply1termlem  24792  plyeq0lem  24799  plyaddlem1  24802  plymullem1  24803  coeeulem  24813  dgrcl  24822  dgrub  24823  dgrlb  24825  coeid3  24829  plyco  24830  coeeq2  24831  coefv0  24837  coemulhi  24843  coemulc  24844  dvply1  24872  vieta1lem2  24899  vieta1  24900  elqaalem2  24908  elqaalem3  24909  geolim3  24927  dvntaylp  24958  taylthlem1  24960  radcnvlem1  25000  radcnvlem2  25001  radcnvlem3  25002  radcnv0  25003  radcnvlt2  25006  dvradcnv  25008  pserulm  25009  psercn2  25010  pserdvlem2  25015  pserdv2  25017  abelthlem4  25021  abelthlem5  25022  abelthlem6  25023  abelthlem7  25025  abelthlem8  25026  abelthlem9  25027  advlogexp  25237  logtayllem  25241  logtayl  25242  cxpeq  25337  leibpi  25519  leibpisum  25520  log2cnv  25521  log2tlbnd  25522  log2ublem2  25524  birthdaylem3  25530  wilthlem2  25645  ftalem1  25649  ftalem5  25653  basellem2  25658  basellem3  25659  basellem5  25661  musum  25767  0sgmppw  25773  1sgmprm  25774  chtublem  25786  logexprlim  25800  lgseisenlem1  25950  lgsquadlem2  25956  dchrisumlem1  26064  dchrisumlem2  26065  dchrisum0flblem1  26083  ostth2lem3  26210  tgcgr4  26316  clwwlknonex2lem1  27885  eupth2lems  28016  fz2ssnn0  30507  cycpmco2rn  30767  cycpmco2lem6  30773  oddpwdc  31612  eulerpartlemb  31626  sseqfn  31648  sseqf  31650  signsplypnf  31820  signstcl  31835  signstf  31836  signstfvn  31839  signstfvneq0  31842  fsum2dsub  31878  reprsuc  31886  breprexplema  31901  breprexplemc  31903  subfacval2  32434  subfaclim  32435  cvmliftlem7  32538  fwddifnp1  33626  knoppcnlem6  33837  knoppcnlem8  33839  knoppcnlem9  33840  knoppcnlem11  33842  knoppcn  33843  knoppndvlem4  33854  knoppndvlem6  33856  knoppf  33874  poimirlem3  34894  poimirlem4  34895  poimirlem18  34909  poimirlem21  34912  poimirlem22  34913  poimirlem25  34916  poimirlem26  34917  poimirlem27  34918  heiborlem4  35091  heiborlem6  35093  mapfzcons  39311  irrapxlem1  39417  ltrmynn0  39543  ltrmxnn0  39544  acongeq  39578  jm2.23  39591  jm2.26lem3  39596  dfrtrcl3  40076  radcnvrat  40644  bcc0  40670  dvradcnv2  40677  binomcxplemnn0  40679  binomcxplemrat  40680  binomcxplemradcnv  40682  binomcxplemnotnn0  40686  fzssnn0  41583  expfac  41936  dvnmptdivc  42221  dvnmul  42226  dvnprodlem3  42231  stoweidlem17  42301  stoweidlem34  42318  stirlinglem5  42362  stirlinglem7  42364  fourierdlem15  42406  fourierdlem25  42416  fourierdlem48  42438  fourierdlem49  42439  fourierdlem50  42440  fourierdlem52  42442  fourierdlem54  42444  fourierdlem64  42454  fourierdlem65  42455  fourierdlem81  42471  fourierdlem92  42482  fourierdlem102  42492  fourierdlem103  42493  fourierdlem104  42494  fourierdlem113  42503  fourierdlem114  42504  elaa2lem  42517  etransclem4  42522  etransclem10  42528  etransclem14  42532  etransclem15  42533  etransclem23  42541  etransclem24  42542  etransclem31  42549  etransclem32  42550  etransclem35  42553  etransclem44  42562  etransclem46  42564  etransclem48  42566  ssnn0ssfz  44396  aacllem  44901