Theorem elfzoelz 13699

Description: Reverse closure for half-open integer sets. (Contributed by Stefan O'Rear, 14-Aug-2015.)

Assertion

Ref	Expression
elfzoelz	⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Proof of Theorem elfzoelz

Step	Hyp	Ref	Expression
1		elfzoel1 13697	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13698	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13696	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7561	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4609	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3984	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  𝒫 cpw 4600  (class class class)co 7431  ℤcz 12613  ..^cfzo 13694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-neg 11495  df-z 12614  df-uz 12879  df-fz 13548  df-fzo 13695

This theorem is referenced by:  elfzo2  13702  elfzole1  13707  elfzolt2  13708  elfzolt3  13709  elfzolt2b  13710  elfzop1le2  13712  elfzouz2  13714  fzonnsub  13724  fzospliti  13731  fzodisj  13733  fzodisjsn  13737  elfzo0subge1  13745  elfzo0suble  13746  fzonmapblen  13748  fzoaddel  13756  elincfzoext  13762  fzosubel  13763  elfzom1elp1fzo1  13806  elfzo1elm1fzo0  13807  elfznelfzob  13812  modaddmodup  13975  modaddmodlo  13976  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  ccatval3  14617  ccatlid  14624  ccatass  14626  ccatrn  14627  ccatalpha  14631  swrdfv0  14687  swrdfv2  14699  swrds1  14704  ccatswrd  14706  pfxfv  14720  ccatpfx  14739  swrdswrd  14743  pfxccatin12lem2a  14765  swrdccatin2  14767  pfxccatin12lem2  14769  revccat  14804  revrev  14805  repswrevw  14825  cshwidxmod  14841  cshwidxmodr  14842  cshwidx0  14844  cshwidxm1  14845  cshweqrep  14859  cshw1  14860  cshimadifsn  14868  cshimadifsn0  14869  cshco  14875  fzomaxdiflem  15381  fzomaxdif  15382  pwdif  15904  pwm1geoser  15905  fzo0dvdseq  16360  fzocongeq  16361  addmodlteqALT  16362  crth  16815  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  hashgcdlem  16825  hashgcdeq  16827  phisum  16828  reumodprminv  16842  modprm0  16843  nnnn0modprm0  16844  modprmn0modprm0  16845  prmgaplem7  17095  cshwshashlem2  17134  cshwshashlem3  17135  cshwrepswhash1  17140  psgnunilem5  19512  odf1o2  19591  odngen  19595  znf1o  21570  znunithash  21583  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dchrisumlem1  27533  dchrisumlem2  27534  dchrisum  27536  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemi  27648  pntlemf  27649  wlk1walk  29657  pthdadjvtx  29748  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  crctcshlem2  29838  crctcshwlkn0  29841  crctcshtrl  29843  crctcsh  29844  clwwlkccatlem  30008  clwwisshclwwslem  30033  clwwisshclwws  30034  eucrctshift  30262  eucrct2eupth  30264  ccatf1  32933  cshwrnid  32946  revpfxsfxrev  35121  revwlk  35130  poimirlem8  37635  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem24  37651  frlmvscadiccat  42516  iblspltprt  45988  itgspltprt  45994  stoweidlem3  46018  fourierdlem12  46134  fourierdlem20  46142  fourierdlem46  46167  fourierdlem50  46171  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem76  46197  fourierdlem79  46200  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  iundjiun  46475  carageniuncllem1  46536  caratheodorylem1  46541  ormklocald  46889  ormkglobd  46890  natlocalincr  46891  natglobalincr  46892  zplusmodne  47345  p1modne  47349  m1modne  47350  minusmod5ne  47351  submodlt  47352  minusmodnep2tmod  47355  iccpartipre  47408  iccpartiltu  47409  iccpartigtl  47410  iccpartgt  47414  icceuelpartlem  47422  icceuelpart  47423  iccpartnel  47425  fargshiftf1  47428  bgoldbtbndlem2  47793  gpgedgel  48007  gpgvtx0  48008  gpgvtx1  48009  gpgedgvtx0  48019  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg3nbgrvtxlem  48023  gpg5nbgrvtx13starlem2  48028  gpg3nbgrvtx0  48032  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  m1modmmod  48442  fllog2  48489  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0mullong  48546