Theorem elfzoelz 13683

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 13681	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13682	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13680	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7538	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 595	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4571	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 23	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3938	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2143  𝒫 cpw 4562  (class class class)co 7410  ℤcz 12586  ..^cfzo 13678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531  df-fzo 13679

This theorem is referenced by:  elfzo2  13686  elfzole1  13692  elfzolt2  13693  elfzolt3  13694  elfzolt2b  13695  elfzop1le2  13697  elfzouz2  13699  fzonnsub  13709  fzospliti  13716  fzodisj  13718  fzodisjsn  13722  elfzo0subge1  13730  elfzo0suble  13731  fzonmapblen  13733  fzoaddel  13742  elincfzoext  13748  fzosubel  13749  elfzom1elp1fzo1  13792  elfzo1elm1fzo0  13793  elfznelfzob  13799  modaddid  13939  modaddmodup  13966  modaddmodlo  13967  modfzo0difsn  13975  modsumfzodifsn  13976  addmodlteq  13978  ccatval3  14612  ccatlid  14620  ccatass  14622  ccatrn  14623  ccatalpha  14627  swrdfv0  14683  swrdfv2  14695  swrds1  14700  ccatswrd  14702  pfxfv  14716  ccatpfx  14734  swrdswrd  14738  pfxccatin12lem2a  14760  swrdccatin2  14762  pfxccatin12lem2  14764  revccat  14799  revrev  14800  repswrevw  14820  cshwidxmod  14836  cshwidxmodr  14837  cshwidx0  14839  cshwidxm1  14840  cshweqrep  14854  cshw1  14855  cshimadifsn  14862  cshimadifsn0  14863  cshco  14869  fzomaxdiflem  15390  fzomaxdif  15391  pwdif  15918  pwm1geoser  15919  fzo0dvdseq  16376  fzocongeq  16377  addmodlteqALT  16378  crth  16832  phimullem  16833  eulerthlem1  16835  eulerthlem2  16836  hashgcdlem  16842  hashgcdeq  16844  phisum  16845  reumodprminv  16859  modprm0  16860  nnnn0modprm0  16861  modprmn0modprm0  16862  prmgaplem7  17112  cshwshashlem2  17151  cshwshashlem3  17152  cshwrepswhash1  17157  chnccat  18677  chnrev  18678  chnpof1  18681  psgnunilem5  19559  odf1o2  19638  odngen  19642  znf1o  21701  znunithash  21714  dvfsumle  26180  dvfsumabs  26182  dchrisumlem1  27653  dchrisumlem2  27654  dchrisum  27656  pntlemq  27765  pntlemr  27766  pntlemj  27767  pntlemi  27768  pntlemf  27769  wlk1walk  29988  pthdadjvtx  30077  crctcshwlkn0lem3  30161  crctcshwlkn0lem4  30162  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  crctcshlem2  30167  crctcshwlkn0  30170  crctcshtrl  30172  crctcsh  30173  clwwlkccatlem  30340  clwwisshclwwslem  30365  clwwisshclwws  30366  eucrctshift  30594  eucrct2eupth  30596  ccatf1  33269  cshwrnid  33281  revpfxsfxrev  35607  revwlk  35617  poimirlem8  38279  poimirlem18  38289  poimirlem21  38292  poimirlem22  38293  poimirlem24  38295  frlmvscadiccat  43280  iblspltprt  46687  itgspltprt  46693  stoweidlem3  46717  fourierdlem12  46833  fourierdlem20  46841  fourierdlem46  46866  fourierdlem50  46870  fourierdlem54  46874  fourierdlem63  46883  fourierdlem64  46884  fourierdlem65  46885  fourierdlem76  46896  fourierdlem79  46899  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem114  46934  iundjiun  47174  carageniuncllem1  47235  caratheodorylem1  47240  ormklocald  47590  ormkglobd  47591  natlocalincr  47592  natglobalincr  47593  chnsubseq  47596  chnerlem3  47600  nnmul2  48067  zplusmodne  48086  p1modne  48090  m1modne  48091  minusmod5ne  48092  submodlt  48093  minusmodnep2tmod  48096  m1modmmod  48101  modmknepk  48105  mod2addne  48107  modm2nep1  48109  modm1nep2  48111  modm1nem2  48112  modm1p1ne  48113  muldvdsfacgt  48123  muldvdsfacm1  48124  iccpartipre  48170  iccpartiltu  48171  iccpartigtl  48172  iccpartgt  48176  icceuelpartlem  48184  icceuelpart  48185  iccpartnel  48187  fargshiftf1  48190  nprmmul2  48277  nprmmul3  48278  nprmdvdsfacm1lem1  48372  nprmdvdsfacm1lem3  48374  nprmdvdsfacm1lem4  48375  bgoldbtbndlem2  48571  upgrimpthslem2  48673  gpgiedgdmellem  48811  gpgvtx0  48818  gpgvtx1  48819  gpgedgvtx0  48826  gpgedgvtx1  48827  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgedg2iv  48832  gpg5nbgrvtx13starlem2  48837  gpg3nbgrvtx0  48841  gpg5nbgrvtx03star  48845  gpg5nbgr3star  48846  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  fllog2  49348  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  nn0mullong  49405