Theorem nn0uz 12274

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 12005	. 2 ⊢ ℕ0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2		0z 11986	. . 3 ⊢ 0 ∈ ℤ
3		uzval 12239	. . 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 5058  ‘cfv 6349  0cc0 10531   ≤ cle 10670  ℕ₀cn0 11891  ℤcz 11975  ℤ_≥cuz 12237

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 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

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 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976  df-uz 12238

This theorem is referenced by:  elnn0uz  12277  2eluzge0  12287  eluznn0  12311  nn0inf  12324  fseq1p1m1  12975  fznn0sub2  13008  nn0split  13016  prednn0  13025  fzossnn0  13062  fzennn  13330  hashgf1o  13333  exple1  13534  faclbnd4lem1  13647  bcval5  13672  bcpasc  13675  hashfzo0  13785  hashf1  13809  ccatval2  13926  ccatass  13936  ccatrn  13937  swrdccat2  14025  wrdeqs1cat  14076  cats1un  14077  splfv2a  14112  splval2  14113  revccat  14122  cats1fv  14215  binom1dif  15182  isumnn0nn  15191  climcndslem1  15198  climcnds  15200  harmonic  15208  arisum2  15210  explecnv  15214  geoser  15216  pwdif  15217  geolim  15220  geolim2  15221  geomulcvg  15226  geoisum  15227  geoisumr  15228  mertenslem1  15234  mertenslem2  15235  mertens  15236  fallfacfwd  15384  0fallfac  15385  binomfallfaclem2  15388  bpolylem  15396  bpolysum  15401  bpolydiflem  15402  fsumkthpow  15404  bpoly2  15405  bpoly3  15406  bpoly4  15407  efcllem  15425  ef0lem  15426  eff  15429  efcvg  15432  efcvgfsum  15433  reefcl  15434  ege2le3  15437  efcj  15439  eftlcvg  15453  eftlub  15456  effsumlt  15458  ef4p  15460  efgt1p2  15461  efgt1p  15462  eflegeo  15468  eirrlem  15551  ruclem6  15582  ruclem7  15583  divalglem2  15740  divalglem5  15742  bitsfzolem  15777  bitsfzo  15778  bitsfi  15780  bitsinv1lem  15784  bitsinv1  15785  bitsinvp1  15792  sadcf  15796  sadcp1  15798  sadadd  15810  sadass  15814  bitsres  15816  smupf  15821  smupp1  15823  smuval2  15825  smupval  15831  smueqlem  15833  smumul  15836  alginv  15913  algcvg  15914  algcvga  15917  algfx  15918  eucalgcvga  15924  eucalg  15925  phiprmpw  16107  prmdiv  16116  iserodd  16166  pcfac  16229  prmreclem2  16247  prmreclem4  16249  vdwapun  16304  vdwlem1  16311  ramcl2lem  16339  ramtcl  16340  ramtub  16342  gsumwsubmcl  17995  gsumws1  17996  gsumsgrpccat  17998  gsumccatOLD  17999  gsumwmhm  18004  psgnunilem2  18617  psgnunilem4  18619  sylow1lem1  18717  efginvrel2  18847  efgredleme  18863  efgredlemc  18865  efgcpbllemb  18875  frgpuplem  18892  telgsumfz0s  19105  telgsums  19107  pgpfaclem1  19197  psrbaglefi  20146  ltbwe  20247  pmatcollpw3fi1lem1  21388  chfacfisf  21456  chfacfisfcpmat  21457  iscmet3lem3  23887  dyadmax  24193  mbfi1fseqlem3  24312  itgcnlem  24384  dvnff  24514  dvnp1  24516  dvn2bss  24521  cpncn  24527  dveflem  24570  ig1peu  24759  ig1pdvds  24764  ply1termlem  24787  plyeq0lem  24794  plyaddlem1  24797  plymullem1  24798  coeeulem  24808  dgrcl  24817  dgrub  24818  dgrlb  24820  coeid3  24824  plyco  24825  coeeq2  24826  coefv0  24832  coemulhi  24838  coemulc  24839  dvply1  24867  vieta1lem2  24894  vieta1  24895  elqaalem2  24903  elqaalem3  24904  geolim3  24922  dvntaylp  24953  taylthlem1  24955  radcnvlem1  24995  radcnvlem2  24996  radcnvlem3  24997  radcnv0  24998  radcnvlt2  25001  dvradcnv  25003  pserulm  25004  psercn2  25005  pserdvlem2  25010  pserdv2  25012  abelthlem4  25016  abelthlem5  25017  abelthlem6  25018  abelthlem7  25020  abelthlem8  25021  abelthlem9  25022  advlogexp  25232  logtayllem  25236  logtayl  25237  cxpeq  25332  leibpi  25514  leibpisum  25515  log2cnv  25516  log2tlbnd  25517  log2ublem2  25519  birthdaylem3  25525  wilthlem2  25640  ftalem1  25644  ftalem5  25648  basellem2  25653  basellem3  25654  basellem5  25656  musum  25762  0sgmppw  25768  1sgmprm  25769  chtublem  25781  logexprlim  25795  lgseisenlem1  25945  lgsquadlem2  25951  dchrisumlem1  26059  dchrisumlem2  26060  dchrisum0flblem1  26078  ostth2lem3  26205  tgcgr4  26311  clwwlknonex2lem1  27880  eupth2lems  28011  fz2ssnn0  30502  cycpmco2rn  30762  cycpmco2lem6  30768  oddpwdc  31607  eulerpartlemb  31621  sseqfn  31643  sseqf  31645  signsplypnf  31815  signstcl  31830  signstf  31831  signstfvn  31834  signstfvneq0  31837  fsum2dsub  31873  reprsuc  31881  breprexplema  31896  breprexplemc  31898  subfacval2  32429  subfaclim  32430  cvmliftlem7  32533  fwddifnp1  33621  knoppcnlem6  33832  knoppcnlem8  33834  knoppcnlem9  33835  knoppcnlem11  33837  knoppcn  33838  knoppndvlem4  33849  knoppndvlem6  33851  knoppf  33869  poimirlem3  34889  poimirlem4  34890  poimirlem18  34904  poimirlem21  34907  poimirlem22  34908  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  heiborlem4  35086  heiborlem6  35088  mapfzcons  39306  irrapxlem1  39412  ltrmynn0  39538  ltrmxnn0  39539  acongeq  39573  jm2.23  39586  jm2.26lem3  39591  dfrtrcl3  40071  radcnvrat  40639  bcc0  40665  dvradcnv2  40672  binomcxplemnn0  40674  binomcxplemrat  40675  binomcxplemradcnv  40677  binomcxplemnotnn0  40681  fzssnn0  41578  expfac  41931  dvnmptdivc  42216  dvnmul  42221  dvnprodlem3  42226  stoweidlem17  42296  stoweidlem34  42313  stirlinglem5  42357  stirlinglem7  42359  fourierdlem15  42401  fourierdlem25  42411  fourierdlem48  42433  fourierdlem49  42434  fourierdlem50  42435  fourierdlem52  42437  fourierdlem54  42439  fourierdlem64  42449  fourierdlem65  42450  fourierdlem81  42466  fourierdlem92  42477  fourierdlem102  42487  fourierdlem103  42488  fourierdlem104  42489  fourierdlem113  42498  fourierdlem114  42499  elaa2lem  42512  etransclem4  42517  etransclem10  42523  etransclem14  42527  etransclem15  42528  etransclem23  42536  etransclem24  42537  etransclem31  42544  etransclem32  42545  etransclem35  42548  etransclem44  42557  etransclem46  42559  etransclem48  42561  ssnn0ssfz  44391  aacllem  44896