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

Theorem elfzoelz 13041
Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)
Assertion
Ref Expression
elfzoelz (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Proof of Theorem elfzoelz
StepHypRef Expression
1 elfzoel1 13039 . . . 4 (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2 elfzoel2 13040 . . . 4 (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3 fzof 13038 . . . . 5 ..^:(ℤ × ℤ)⟶𝒫 ℤ
43fovcl 7281 . . . 4 ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
51, 2, 4syl2anc 586 . . 3 (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
65elpwid 4552 . 2 (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7 id 22 . 2 (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
86, 7sseldd 3970 1 (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  𝒫 cpw 4541  (class class class)co 7158  cz 11984  ..^cfzo 13036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-neg 10875  df-z 11985  df-uz 12247  df-fz 12896  df-fzo 13037
This theorem is referenced by:  elfzo2  13044  elfzole1  13049  elfzolt2  13050  elfzolt3  13051  elfzolt2b  13052  elfzouz2  13055  fzonnsub  13065  fzospliti  13072  fzodisj  13074  fzodisjsn  13078  fzonmapblen  13086  fzoaddel  13093  elincfzoext  13098  fzosubel  13099  elfzom1elp1fzo1  13140  elfzo1elm1fzo0  13141  elfznelfzob  13146  modaddmodup  13305  modaddmodlo  13306  modfzo0difsn  13314  modsumfzodifsn  13315  addmodlteq  13317  wrdexgOLD  13875  ccatval3  13935  ccatlid  13942  ccatass  13944  ccatrn  13945  ccatalpha  13949  swrdfv0  14013  swrdfv2  14025  swrds1  14030  ccatswrd  14032  pfxfv  14046  ccatpfx  14065  swrdswrd  14069  pfxccatin12lem2a  14091  swrdccatin2  14093  pfxccatin12lem2  14095  revccat  14130  revrev  14131  repswrevw  14151  cshwidxmod  14167  cshwidxmodr  14168  cshwidx0  14170  cshwidxm1  14171  cshweqrep  14185  cshw1  14186  cshimadifsn  14193  cshimadifsn0  14194  cshco  14200  fzomaxdiflem  14704  fzomaxdif  14705  pwdif  15225  pwm1geoser  15226  fzo0dvdseq  15675  fzocongeq  15676  addmodlteqALT  15677  crth  16117  phimullem  16118  eulerthlem1  16120  eulerthlem2  16121  hashgcdlem  16127  hashgcdeq  16128  phisum  16129  reumodprminv  16143  modprm0  16144  nnnn0modprm0  16145  modprmn0modprm0  16146  prmgaplem7  16395  cshwshashlem2  16432  cshwshashlem3  16433  cshwrepswhash1  16438  psgnunilem5  18624  odf1o2  18700  odngen  18704  znf1o  20700  zntoslem  20705  znunithash  20713  dvfsumle  24620  dvfsumabs  24622  dchrisumlem1  26067  dchrisumlem2  26068  dchrisum  26070  pntlemq  26179  pntlemr  26180  pntlemj  26181  pntlemi  26182  pntlemf  26183  wlk1walk  27422  pthdadjvtx  27513  crctcshwlkn0lem3  27592  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  crctcshwlkn0lem6  27595  crctcshlem2  27598  crctcshwlkn0  27601  crctcshtrl  27603  crctcsh  27604  clwwlkccatlem  27769  clwwisshclwwslem  27794  clwwisshclwws  27795  eucrctshift  28024  eucrct2eupth  28026  ccatf1  30627  cshwrnid  30637  revpfxsfxrev  32364  revwlk  32373  poimirlem8  34902  poimirlem18  34912  poimirlem21  34915  poimirlem22  34916  poimirlem24  34918  frlmvscadiccat  39152  elfzop1le2  41563  iblspltprt  42265  itgspltprt  42271  stoweidlem3  42295  fourierdlem12  42411  fourierdlem20  42419  fourierdlem46  42444  fourierdlem50  42448  fourierdlem54  42452  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem76  42474  fourierdlem79  42477  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  iundjiun  42749  carageniuncllem1  42810  caratheodorylem1  42815  iccpartipre  43588  iccpartiltu  43589  iccpartigtl  43590  iccpartgt  43594  icceuelpartlem  43602  icceuelpart  43603  iccpartnel  43605  fargshiftf1  43608  bgoldbtbndlem2  43978  m1modmmod  44588  fllog2  44635  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  nn0mullong  44692
  Copyright terms: Public domain W3C validator