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

Theorem nn0uz 12258
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 11989 . 2 0 = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
2 0z 11970 . . 3 0 ∈ ℤ
3 uzval 12223 . . 3 (0 ∈ ℤ → (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘})
42, 3ax-mp 5 . 2 (ℤ‘0) = {𝑘 ∈ ℤ ∣ 0 ≤ 𝑘}
51, 4eqtr4i 2847 1 0 = (ℤ‘0)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  {crab 3130   class class class wbr 5039  cfv 6328  0cc0 10514  cle 10653  0cn0 11875  cz 11959  cuz 12221
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-nn 11616  df-n0 11876  df-z 11960  df-uz 12222
This theorem is referenced by:  elnn0uz  12261  2eluzge0  12271  eluznn0  12295  nn0inf  12308  fseq1p1m1  12964  fznn0sub2  12997  nn0split  13005  prednn0  13014  fzossnn0  13051  fzennn  13319  hashgf1o  13322  exple1  13524  faclbnd4lem1  13637  bcval5  13662  bcpasc  13665  hashfzo0  13775  hashf1  13799  ccatval2  13911  ccatass  13921  ccatrn  13922  swrdccat2  14010  wrdeqs1cat  14061  cats1un  14062  splfv2a  14097  splval2  14098  revccat  14107  cats1fv  14200  binom1dif  15167  isumnn0nn  15176  climcndslem1  15183  climcnds  15185  harmonic  15193  arisum2  15195  explecnv  15199  geoser  15201  pwdif  15202  geolim  15205  geolim2  15206  geomulcvg  15211  geoisum  15212  geoisumr  15213  mertenslem1  15219  mertenslem2  15220  mertens  15221  fallfacfwd  15369  0fallfac  15370  binomfallfaclem2  15373  bpolylem  15381  bpolysum  15386  bpolydiflem  15387  fsumkthpow  15389  bpoly2  15390  bpoly3  15391  bpoly4  15392  efcllem  15410  ef0lem  15411  eff  15414  efcvg  15417  efcvgfsum  15418  reefcl  15419  ege2le3  15422  efcj  15424  eftlcvg  15438  eftlub  15441  effsumlt  15443  ef4p  15445  efgt1p2  15446  efgt1p  15447  eflegeo  15453  eirrlem  15536  ruclem6  15567  ruclem7  15568  divalglem2  15723  divalglem5  15725  bitsfzolem  15760  bitsfzo  15761  bitsfi  15763  bitsinv1lem  15767  bitsinv1  15768  bitsinvp1  15775  sadcf  15779  sadcp1  15781  sadadd  15793  sadass  15797  bitsres  15799  smupf  15804  smupp1  15806  smuval2  15808  smupval  15814  smueqlem  15816  smumul  15819  alginv  15896  algcvg  15897  algcvga  15900  algfx  15901  eucalgcvga  15907  eucalg  15908  phiprmpw  16090  prmdiv  16099  iserodd  16149  pcfac  16212  prmreclem2  16230  prmreclem4  16232  vdwapun  16287  vdwlem1  16294  ramcl2lem  16322  ramtcl  16323  ramtub  16325  gsumwsubmcl  17980  gsumws1  17981  gsumsgrpccat  17983  gsumccatOLD  17984  gsumwmhm  17989  psgnunilem2  18602  psgnunilem4  18604  sylow1lem1  18702  efginvrel2  18832  efgredleme  18848  efgredlemc  18850  efgcpbllemb  18860  frgpuplem  18877  telgsumfz0s  19090  telgsums  19092  pgpfaclem1  19182  psrbaglefi  20128  ltbwe  20229  pmatcollpw3fi1lem1  21370  chfacfisf  21438  chfacfisfcpmat  21439  iscmet3lem3  23873  dyadmax  24181  mbfi1fseqlem3  24300  itgcnlem  24372  dvnff  24505  dvnp1  24507  dvn2bss  24512  cpncn  24518  dveflem  24561  ig1peu  24751  ig1pdvds  24756  ply1termlem  24779  plyeq0lem  24786  plyaddlem1  24789  plymullem1  24790  coeeulem  24800  dgrcl  24809  dgrub  24810  dgrlb  24812  coeid3  24816  plyco  24817  coeeq2  24818  coefv0  24824  coemulhi  24830  coemulc  24831  dvply1  24859  vieta1lem2  24886  vieta1  24887  elqaalem2  24895  elqaalem3  24896  geolim3  24914  dvntaylp  24945  taylthlem1  24947  radcnvlem1  24987  radcnvlem2  24988  radcnvlem3  24989  radcnv0  24990  radcnvlt2  24993  dvradcnv  24995  pserulm  24996  psercn2  24997  pserdvlem2  25002  pserdv2  25004  abelthlem4  25008  abelthlem5  25009  abelthlem6  25010  abelthlem7  25012  abelthlem8  25013  abelthlem9  25014  advlogexp  25225  logtayllem  25229  logtayl  25230  cxpeq  25325  leibpi  25507  leibpisum  25508  log2cnv  25509  log2tlbnd  25510  log2ublem2  25512  birthdaylem3  25518  wilthlem2  25633  ftalem1  25637  ftalem5  25641  basellem2  25646  basellem3  25647  basellem5  25649  musum  25755  0sgmppw  25761  1sgmprm  25762  chtublem  25774  logexprlim  25788  lgseisenlem1  25938  lgsquadlem2  25944  dchrisumlem1  26052  dchrisumlem2  26053  dchrisum0flblem1  26071  ostth2lem3  26198  tgcgr4  26304  clwwlknonex2lem1  27871  eupth2lems  28002  fz2ssnn0  30495  cycpmco2rn  30775  cycpmco2lem6  30781  oddpwdc  31620  eulerpartlemb  31634  sseqfn  31656  sseqf  31658  signsplypnf  31828  signstcl  31843  signstf  31844  signstfvn  31847  signstfvneq0  31850  fsum2dsub  31886  reprsuc  31894  breprexplema  31909  breprexplemc  31911  subfacval2  32442  subfaclim  32443  cvmliftlem7  32546  fwddifnp1  33634  knoppcnlem6  33845  knoppcnlem8  33847  knoppcnlem9  33848  knoppcnlem11  33850  knoppcn  33851  knoppndvlem4  33862  knoppndvlem6  33864  knoppf  33882  poimirlem3  34946  poimirlem4  34947  poimirlem18  34961  poimirlem21  34964  poimirlem22  34965  poimirlem25  34968  poimirlem26  34969  poimirlem27  34970  heiborlem4  35138  heiborlem6  35140  lcmfunnnd  39179  mapfzcons  39468  irrapxlem1  39574  ltrmynn0  39700  ltrmxnn0  39701  acongeq  39735  jm2.23  39748  jm2.26lem3  39753  dfrtrcl3  40245  radcnvrat  40833  bcc0  40859  dvradcnv2  40866  binomcxplemnn0  40868  binomcxplemrat  40869  binomcxplemradcnv  40871  binomcxplemnotnn0  40875  fzssnn0  41771  expfac  42122  dvnmptdivc  42403  dvnmul  42408  dvnprodlem3  42413  stoweidlem17  42482  stoweidlem34  42499  stirlinglem5  42543  stirlinglem7  42545  fourierdlem15  42587  fourierdlem25  42597  fourierdlem48  42619  fourierdlem49  42620  fourierdlem50  42621  fourierdlem52  42623  fourierdlem54  42625  fourierdlem64  42635  fourierdlem65  42636  fourierdlem81  42652  fourierdlem92  42663  fourierdlem102  42673  fourierdlem103  42674  fourierdlem104  42675  fourierdlem113  42684  fourierdlem114  42685  elaa2lem  42698  etransclem4  42703  etransclem10  42709  etransclem14  42713  etransclem15  42714  etransclem23  42722  etransclem24  42723  etransclem31  42730  etransclem32  42731  etransclem35  42734  etransclem44  42743  etransclem46  42745  etransclem48  42747  ssnn0ssfz  44573  itcoval1  44888  itcoval2  44889  itcoval3  44890  itcovalsuc  44892  ackvalsuc1mpt  44903  aacllem  45140
  Copyright terms: Public domain W3C validator