Theorem elfzoelz 13559

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 13557	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13558	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13556	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7474	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4556	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3930	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2111  𝒫 cpw 4547  (class class class)co 7346  ℤcz 12468  ..^cfzo 13554

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-neg 11347  df-z 12469  df-uz 12733  df-fz 13408  df-fzo 13555

This theorem is referenced by:  elfzo2  13562  elfzole1  13567  elfzolt2  13568  elfzolt3  13569  elfzolt2b  13570  elfzop1le2  13572  elfzouz2  13574  fzonnsub  13584  fzospliti  13591  fzodisj  13593  fzodisjsn  13597  elfzo0subge1  13605  elfzo0suble  13606  fzonmapblen  13608  fzoaddel  13617  elincfzoext  13623  fzosubel  13624  elfzom1elp1fzo1  13667  elfzo1elm1fzo0  13668  elfznelfzob  13674  modaddid  13814  modaddmodup  13841  modaddmodlo  13842  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  ccatval3  14486  ccatlid  14494  ccatass  14496  ccatrn  14497  ccatalpha  14501  swrdfv0  14557  swrdfv2  14569  swrds1  14574  ccatswrd  14576  pfxfv  14590  ccatpfx  14608  swrdswrd  14612  pfxccatin12lem2a  14634  swrdccatin2  14636  pfxccatin12lem2  14638  revccat  14673  revrev  14674  repswrevw  14694  cshwidxmod  14710  cshwidxmodr  14711  cshwidx0  14713  cshwidxm1  14714  cshweqrep  14728  cshw1  14729  cshimadifsn  14736  cshimadifsn0  14737  cshco  14743  fzomaxdiflem  15250  fzomaxdif  15251  pwdif  15775  pwm1geoser  15776  fzo0dvdseq  16234  fzocongeq  16235  addmodlteqALT  16236  crth  16689  phimullem  16690  eulerthlem1  16692  eulerthlem2  16693  hashgcdlem  16699  hashgcdeq  16701  phisum  16702  reumodprminv  16716  modprm0  16717  nnnn0modprm0  16718  modprmn0modprm0  16719  prmgaplem7  16969  cshwshashlem2  17008  cshwshashlem3  17009  cshwrepswhash1  17014  chnccat  18532  chnrev  18533  chnpof1  18536  psgnunilem5  19406  odf1o2  19485  odngen  19489  znf1o  21488  znunithash  21501  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dchrisumlem1  27427  dchrisumlem2  27428  dchrisum  27430  pntlemq  27539  pntlemr  27540  pntlemj  27541  pntlemi  27542  pntlemf  27543  wlk1walk  29617  pthdadjvtx  29706  crctcshwlkn0lem3  29790  crctcshwlkn0lem4  29791  crctcshwlkn0lem5  29792  crctcshwlkn0lem6  29793  crctcshlem2  29796  crctcshwlkn0  29799  crctcshtrl  29801  crctcsh  29802  clwwlkccatlem  29969  clwwisshclwwslem  29994  clwwisshclwws  29995  eucrctshift  30223  eucrct2eupth  30225  ccatf1  32930  cshwrnid  32942  revpfxsfxrev  35160  revwlk  35169  poimirlem8  37676  poimirlem18  37686  poimirlem21  37689  poimirlem22  37690  poimirlem24  37692  frlmvscadiccat  42547  iblspltprt  46019  itgspltprt  46025  stoweidlem3  46049  fourierdlem12  46165  fourierdlem20  46173  fourierdlem46  46198  fourierdlem50  46202  fourierdlem54  46206  fourierdlem63  46215  fourierdlem64  46216  fourierdlem65  46217  fourierdlem76  46228  fourierdlem79  46231  fourierdlem102  46254  fourierdlem103  46255  fourierdlem104  46256  fourierdlem114  46266  iundjiun  46506  carageniuncllem1  46567  caratheodorylem1  46572  ormklocald  46920  ormkglobd  46921  natlocalincr  46922  natglobalincr  46923  zplusmodne  47382  p1modne  47386  m1modne  47387  minusmod5ne  47388  submodlt  47389  minusmodnep2tmod  47392  m1modmmod  47397  modmknepk  47401  mod2addne  47403  modm2nep1  47405  modm1nep2  47407  modm1nem2  47408  modm1p1ne  47409  iccpartipre  47460  iccpartiltu  47461  iccpartigtl  47462  iccpartgt  47466  icceuelpartlem  47474  icceuelpart  47475  iccpartnel  47477  fargshiftf1  47480  bgoldbtbndlem2  47845  upgrimpthslem2  47947  gpgiedgdmellem  48085  gpgvtx0  48092  gpgvtx1  48093  gpgedgvtx0  48100  gpgedgvtx1  48101  gpgvtxedg0  48102  gpgvtxedg1  48103  gpgedg2iv  48106  gpg5nbgrvtx13starlem2  48111  gpg3nbgrvtx0  48115  gpg5nbgrvtx03star  48119  gpg5nbgr3star  48120  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  pgnbgreunbgrlem2lem3  48155  fllog2  48608  nn0sumshdiglemA  48659  nn0sumshdiglemB  48660  nn0mullong  48665