MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0uz Structured version   Visualization version   GIF version

Theorem nn0uz 11551
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
StepHypRef Expression
1 nn0zrab 11236 . 2 0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2 0z 11218 . . 3 0 ∈ ℤ
3 uzval 11518 . . 3 (0 ∈ ℤ → (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
51, 4eqtr4i 2631 1 0 = (ℤ‘0)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  {crab 2896   class class class wbr 4574  cfv 5787  0cc0 9789  cle 9928  0cn0 11136  cz 11207  cuz 11516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-nn 10865  df-n0 11137  df-z 11208  df-uz 11517
This theorem is referenced by:  elnn0uz  11554  2eluzge0  11562  eluznn0  11586  nn0inf  11599  fseq1p1m1  12235  fznn0sub2  12267  nn0split  12275  prednn0  12284  fzossnn0  12320  fzennn  12581  hashgf1o  12584  exple1  12734  faclbnd4lem1  12894  bcval5  12919  bcpasc  12922  hashfzo0  13026  hashf1  13047  ccatval2  13158  ccatass  13167  ccatrn  13168  swrdccat1  13252  swrdccat2  13253  wrdeqs1cat  13269  cats1un  13270  splfv2a  13301  splval2  13302  revccat  13309  cats1fv  13398  binom1dif  14347  isumnn0nn  14356  climcndslem1  14363  climcnds  14365  harmonic  14373  arisum2  14375  explecnv  14379  geoser  14381  geolim  14383  geolim2  14384  geomulcvg  14389  geoisum  14390  geoisumr  14391  mertenslem1  14398  mertenslem2  14399  mertens  14400  fallfacfwd  14549  0fallfac  14550  binomfallfaclem2  14553  bpolylem  14561  bpolysum  14566  bpolydiflem  14567  fsumkthpow  14569  bpoly2  14570  bpoly3  14571  bpoly4  14572  efcllem  14590  ef0lem  14591  eff  14594  efcvg  14597  efcvgfsum  14598  reefcl  14599  ege2le3  14602  efcj  14604  eftlcvg  14618  eftlub  14621  effsumlt  14623  ef4p  14625  efgt1p2  14626  efgt1p  14627  eflegeo  14633  eirrlem  14714  ruclem6  14746  ruclem7  14747  divalglem2  14899  divalglem5  14901  bitsfzolem  14937  bitsfzo  14938  bitsfi  14940  bitsinv1lem  14944  bitsinv1  14945  bitsinvp1  14952  sadcf  14956  sadcp1  14958  sadadd  14970  sadass  14974  bitsres  14976  smupf  14981  smupp1  14983  smuval2  14985  smupval  14991  smueqlem  14993  smumul  14996  alginv  15069  algcvg  15070  algcvga  15073  algfx  15074  eucalgcvga  15080  eucalg  15081  phiprmpw  15262  prmdiv  15271  iserodd  15321  pcfac  15384  prmreclem2  15402  prmreclem4  15404  vdwapun  15459  vdwlem1  15466  ramcl2lem  15494  ramtcl  15495  ramtub  15497  gsumwsubmcl  17141  gsumws1  17142  gsumccat  17144  gsumwmhm  17148  psgnunilem2  17681  psgnunilem4  17683  sylow1lem1  17779  efginvrel2  17906  efgredleme  17922  efgredlemc  17924  efgcpbllemb  17934  frgpuplem  17951  telgsumfz0s  18154  telgsums  18156  pgpfaclem1  18246  psrbaglefi  19136  ltbwe  19236  pmatcollpw3fi1lem1  20349  chfacfisf  20417  chfacfisfcpmat  20418  iscmet3lem3  22811  dyadmax  23086  mbfi1fseqlem3  23204  itgcnlem  23276  dvnff  23406  dvnp1  23408  dvn2bss  23413  cpncn  23419  dveflem  23460  ig1peu  23649  ig1pdvds  23654  ply1termlem  23677  plyeq0lem  23684  plyaddlem1  23687  plymullem1  23688  coeeulem  23698  dgrcl  23707  dgrub  23708  dgrlb  23710  coeid3  23714  plyco  23715  coeeq2  23716  coefv0  23722  coemulhi  23728  coemulc  23729  dvply1  23757  vieta1lem2  23784  vieta1  23785  elqaalem2  23793  elqaalem3  23794  geolim3  23812  dvntaylp  23843  taylthlem1  23845  radcnvlem1  23885  radcnvlem2  23886  radcnvlem3  23887  radcnv0  23888  radcnvlt2  23891  dvradcnv  23893  pserulm  23894  psercn2  23895  pserdvlem2  23900  pserdv2  23902  abelthlem4  23906  abelthlem5  23907  abelthlem6  23908  abelthlem7  23910  abelthlem8  23911  abelthlem9  23912  advlogexp  24115  logtayllem  24119  logtayl  24120  cxpeq  24212  leibpi  24383  leibpisum  24384  log2cnv  24385  log2tlbnd  24386  log2ublem2  24388  birthdaylem3  24394  wilthlem2  24509  ftalem1  24513  ftalem5  24517  basellem2  24522  basellem3  24523  basellem5  24525  musum  24631  0sgmppw  24637  1sgmprm  24638  chtublem  24650  logexprlim  24664  lgseisenlem1  24814  lgsquadlem2  24820  dchrisumlem1  24892  dchrisumlem2  24893  dchrisum0flblem1  24911  ostth2lem3  25038  tgcgr4  25141  eupares  26265  eupap1  26266  eupath2lem3  26269  eupath2  26270  konigsberg  26277  oddpwdc  29546  eulerpartlemb  29560  sseqfn  29582  sseqf  29584  signsplypnf  29756  signstcl  29771  signstf  29772  signstfvn  29775  signstfvneq0  29778  subfacval2  30226  subfaclim  30227  cvmliftlem7  30330  fwddifnp1  31245  knoppcnlem6  31461  knoppcnlem8  31463  knoppcnlem9  31464  knoppcnlem11  31466  knoppcn  31467  knoppndvlem4  31479  knoppndvlem6  31481  knoppf  31499  poimirlem3  32382  poimirlem4  32383  poimirlem18  32397  poimirlem21  32400  poimirlem22  32401  poimirlem25  32404  poimirlem26  32405  poimirlem27  32406  heiborlem4  32583  heiborlem6  32585  mapfzcons  36097  irrapxlem1  36204  ltrmynn0  36333  ltrmxnn0  36334  acongeq  36368  jm2.23  36381  jm2.26lem3  36386  dfrtrcl3  36844  radcnvrat  37335  bcc0  37361  dvradcnv2  37368  binomcxplemnn0  37370  binomcxplemrat  37371  binomcxplemradcnv  37373  binomcxplemnotnn0  37377  fzssnn0  38275  expfac  38525  dvnmptdivc  38629  dvnmul  38634  dvnprodlem3  38639  stoweidlem17  38711  stoweidlem34  38728  stirlinglem5  38772  stirlinglem7  38774  fourierdlem15  38816  fourierdlem25  38826  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem52  38852  fourierdlem54  38854  fourierdlem64  38864  fourierdlem65  38865  fourierdlem81  38881  fourierdlem92  38892  fourierdlem102  38902  fourierdlem103  38903  fourierdlem104  38904  fourierdlem113  38913  fourierdlem114  38914  elaa2lem  38927  etransclem4  38932  etransclem10  38938  etransclem14  38942  etransclem15  38943  etransclem23  38951  etransclem24  38952  etransclem31  38959  etransclem32  38960  etransclem35  38963  etransclem44  38972  etransclem46  38974  etransclem48  38976  pwdif  39841  eupth2lems  41405  ssnn0ssfz  41919  aacllem  42316
  Copyright terms: Public domain W3C validator