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

Theorem nn0uz 12812
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 12539 . 2 0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2 0z 12517 . . 3 0 ∈ ℤ
3 uzval 12772 . . 3 (0 ∈ ℤ → (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
51, 4eqtr4i 2768 1 0 = (ℤ‘0)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {crab 3410   class class class wbr 5110  cfv 6501  0cc0 11058  cle 11197  0cn0 12420  cz 12506  cuz 12770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-n0 12421  df-z 12507  df-uz 12771
This theorem is referenced by:  elnn0uz  12815  2eluzge0  12825  eluznn0  12849  nn0inf  12862  fseq1p1m1  13522  fznn0sub2  13555  nn0split  13563  prednn0  13572  fzossnn0  13610  fzennn  13880  hashgf1o  13883  exple1  14088  faclbnd4lem1  14200  bcval5  14225  bcpasc  14228  hashfzo0  14337  hashf1  14363  ccatval2  14473  ccatass  14483  ccatrn  14484  swrdccat2  14564  wrdeqs1cat  14615  cats1un  14616  splfv2a  14651  splval2  14652  revccat  14661  cats1fv  14755  binom1dif  15725  isumnn0nn  15734  climcndslem1  15741  climcnds  15743  harmonic  15751  arisum2  15753  explecnv  15757  geoser  15759  pwdif  15760  geolim  15762  geolim2  15763  geomulcvg  15768  geoisum  15769  geoisumr  15770  mertenslem1  15776  mertenslem2  15777  mertens  15778  fallfacfwd  15926  0fallfac  15927  binomfallfaclem2  15930  bpolylem  15938  bpolysum  15943  bpolydiflem  15944  fsumkthpow  15946  bpoly2  15947  bpoly3  15948  bpoly4  15949  efcllem  15967  ef0lem  15968  eff  15971  efcvg  15974  efcvgfsum  15975  reefcl  15976  ege2le3  15979  efcj  15981  eftlcvg  15995  eftlub  15998  effsumlt  16000  ef4p  16002  efgt1p2  16003  efgt1p  16004  eflegeo  16010  eirrlem  16093  ruclem6  16124  ruclem7  16125  divalglem2  16284  divalglem5  16286  bitsfzolem  16321  bitsfzo  16322  bitsfi  16324  bitsinv1lem  16328  bitsinv1  16329  bitsinvp1  16336  sadcf  16340  sadcp1  16342  sadadd  16354  sadass  16358  bitsres  16360  smupf  16365  smupp1  16367  smuval2  16369  smupval  16375  smueqlem  16377  smumul  16380  alginv  16458  algcvg  16459  algcvga  16462  algfx  16463  eucalgcvga  16469  eucalg  16470  phiprmpw  16655  prmdiv  16664  iserodd  16714  pcfac  16778  prmreclem2  16796  prmreclem4  16798  vdwapun  16853  vdwlem1  16860  ramcl2lem  16888  ramtcl  16889  ramtub  16891  gsumwsubmcl  18654  gsumws1  18655  gsumsgrpccat  18657  gsumwmhm  18662  psgnunilem2  19284  psgnunilem4  19286  sylow1lem1  19387  efginvrel2  19516  efgredleme  19532  efgredlemc  19534  efgcpbllemb  19544  frgpuplem  19561  telgsumfz0s  19775  telgsums  19777  pgpfaclem1  19867  psrbaglefi  21350  psrbaglefiOLD  21351  ltbwe  21461  pmatcollpw3fi1lem1  22151  chfacfisf  22219  chfacfisfcpmat  22220  iscmet3lem3  24670  dyadmax  24978  mbfi1fseqlem3  25098  itgcnlem  25170  dvnff  25303  dvnp1  25305  dvn2bss  25310  cpncn  25316  dveflem  25359  ig1peu  25552  ig1pdvds  25557  ply1termlem  25580  plyeq0lem  25587  plyaddlem1  25590  plymullem1  25591  coeeulem  25601  dgrcl  25610  dgrub  25611  dgrlb  25613  coeid3  25617  plyco  25618  coeeq2  25619  coefv0  25625  coemulhi  25631  coemulc  25632  dvply1  25660  vieta1lem2  25687  vieta1  25688  elqaalem2  25696  elqaalem3  25697  geolim3  25715  dvntaylp  25746  taylthlem1  25748  radcnvlem1  25788  radcnvlem2  25789  radcnvlem3  25790  radcnv0  25791  radcnvlt2  25794  dvradcnv  25796  pserulm  25797  psercn2  25798  pserdvlem2  25803  pserdv2  25805  abelthlem4  25809  abelthlem5  25810  abelthlem6  25811  abelthlem7  25813  abelthlem8  25814  abelthlem9  25815  advlogexp  26026  logtayllem  26030  logtayl  26031  cxpeq  26126  leibpi  26308  leibpisum  26309  log2cnv  26310  log2tlbnd  26311  log2ublem2  26313  birthdaylem3  26319  wilthlem2  26434  ftalem1  26438  ftalem5  26442  basellem2  26447  basellem3  26448  basellem5  26450  musum  26556  0sgmppw  26562  1sgmprm  26563  chtublem  26575  logexprlim  26589  lgseisenlem1  26739  lgsquadlem2  26745  dchrisumlem1  26853  dchrisumlem2  26854  dchrisum0flblem1  26872  ostth2lem3  26999  tgcgr4  27515  clwwlknonex2lem1  29093  eupth2lems  29224  fz2ssnn0  31730  cycpmco2rn  32016  cycpmco2lem6  32022  oddpwdc  32994  eulerpartlemb  33008  sseqfn  33030  sseqf  33032  signsplypnf  33202  signstcl  33217  signstf  33218  signstfvn  33221  signstfvneq0  33224  fsum2dsub  33260  reprsuc  33268  breprexplema  33283  breprexplemc  33285  subfacval2  33821  subfaclim  33822  cvmliftlem7  33925  fwddifnp1  34779  knoppcnlem6  34990  knoppcnlem8  34992  knoppcnlem9  34993  knoppcnlem11  34995  knoppcn  34996  knoppndvlem4  35007  knoppndvlem6  35009  knoppf  35027  poimirlem3  36110  poimirlem4  36111  poimirlem18  36125  poimirlem21  36128  poimirlem22  36129  poimirlem25  36132  poimirlem26  36133  poimirlem27  36134  heiborlem4  36302  heiborlem6  36304  lcmfunnnd  40498  mapfzcons  41068  irrapxlem1  41174  ltrmynn0  41301  ltrmxnn0  41302  acongeq  41336  jm2.23  41349  jm2.26lem3  41354  dfrtrcl3  42079  radcnvrat  42668  bcc0  42694  dvradcnv2  42701  binomcxplemnn0  42703  binomcxplemrat  42704  binomcxplemradcnv  42706  binomcxplemnotnn0  42710  fzssnn0  43625  rexanuz2nf  43802  expfac  43972  dvnmptdivc  44253  dvnmul  44258  dvnprodlem3  44263  stoweidlem17  44332  stoweidlem34  44349  stirlinglem5  44393  stirlinglem7  44395  fourierdlem15  44437  fourierdlem25  44447  fourierdlem48  44469  fourierdlem49  44470  fourierdlem50  44471  fourierdlem52  44473  fourierdlem54  44475  fourierdlem64  44485  fourierdlem65  44486  fourierdlem81  44502  fourierdlem92  44513  fourierdlem102  44523  fourierdlem103  44524  fourierdlem104  44525  fourierdlem113  44534  fourierdlem114  44535  elaa2lem  44548  etransclem4  44553  etransclem10  44559  etransclem14  44563  etransclem15  44564  etransclem23  44572  etransclem24  44573  etransclem31  44580  etransclem32  44581  etransclem35  44584  etransclem44  44593  etransclem46  44595  etransclem48  44597  ssnn0ssfz  46499  itcoval1  46823  itcoval2  46824  itcoval3  46825  itcovalsuc  46827  ackvalsuc1mpt  46838  aacllem  47322
  Copyright terms: Public domain W3C validator