Theorem elfzoelz 13686

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 13684	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13685	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13683	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7539	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 595	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4576	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 23	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3946	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2149  𝒫 cpw 4567  (class class class)co 7411  ℤcz 12590  ..^cfzo 13681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-neg 11443  df-z 12591  df-uz 12862  df-fz 13535  df-fzo 13682

This theorem is referenced by:  elfzo2  13689  elfzole1  13695  elfzolt2  13696  elfzolt3  13697  elfzolt2b  13698  elfzop1le2  13700  elfzouz2  13702  fzonnsub  13712  fzospliti  13719  fzodisj  13721  fzodisjsn  13725  elfzo0subge1  13733  elfzo0suble  13734  fzonmapblen  13736  fzoaddel  13745  elincfzoext  13751  fzosubel  13752  elfzom1elp1fzo1  13795  elfzo1elm1fzo0  13796  elfznelfzob  13802  modaddid  13942  modaddmodup  13969  modaddmodlo  13970  modfzo0difsn  13978  modsumfzodifsn  13979  addmodlteq  13981  ccatval3  14615  ccatlid  14623  ccatass  14625  ccatrn  14626  ccatalpha  14630  swrdfv0  14686  swrdfv2  14698  swrds1  14703  ccatswrd  14705  pfxfv  14719  ccatpfx  14737  swrdswrd  14741  pfxccatin12lem2a  14763  swrdccatin2  14765  pfxccatin12lem2  14767  revccat  14802  revrev  14803  repswrevw  14823  cshwidxmod  14839  cshwidxmodr  14840  cshwidx0  14842  cshwidxm1  14843  cshweqrep  14857  cshw1  14858  cshimadifsn  14865  cshimadifsn0  14866  cshco  14872  fzomaxdiflem  15393  fzomaxdif  15394  pwdif  15921  pwm1geoser  15922  fzo0dvdseq  16380  fzocongeq  16381  addmodlteqALT  16382  crth  16836  phimullem  16837  eulerthlem1  16839  eulerthlem2  16840  hashgcdlem  16846  hashgcdeq  16848  phisum  16849  reumodprminv  16863  modprm0  16864  nnnn0modprm0  16865  modprmn0modprm0  16866  prmgaplem7  17116  cshwshashlem2  17155  cshwshashlem3  17156  cshwrepswhash1  17161  chnccat  18681  chnrev  18682  chnpof1  18685  psgnunilem5  19563  odf1o2  19642  odngen  19646  znf1o  21669  znunithash  21682  dvfsumle  26148  dvfsumabs  26150  dchrisumlem1  27618  dchrisumlem2  27619  dchrisum  27621  pntlemq  27730  pntlemr  27731  pntlemj  27732  pntlemi  27733  pntlemf  27734  wlk1walk  29928  pthdadjvtx  30017  crctcshwlkn0lem3  30101  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  crctcshlem2  30107  crctcshwlkn0  30110  crctcshtrl  30112  crctcsh  30113  clwwlkccatlem  30280  clwwisshclwwslem  30305  clwwisshclwws  30306  eucrctshift  30534  eucrct2eupth  30536  ccatf1  33209  cshwrnid  33221  revpfxsfxrev  35505  revwlk  35515  poimirlem8  38166  poimirlem18  38176  poimirlem21  38179  poimirlem22  38180  poimirlem24  38182  frlmvscadiccat  43169  iblspltprt  46578  itgspltprt  46584  stoweidlem3  46608  fourierdlem12  46724  fourierdlem20  46732  fourierdlem46  46757  fourierdlem50  46761  fourierdlem54  46765  fourierdlem63  46774  fourierdlem64  46775  fourierdlem65  46776  fourierdlem76  46787  fourierdlem79  46790  fourierdlem102  46813  fourierdlem103  46814  fourierdlem104  46815  fourierdlem114  46825  iundjiun  47065  carageniuncllem1  47126  caratheodorylem1  47131  ormklocald  47481  ormkglobd  47482  natlocalincr  47483  natglobalincr  47484  chnsubseq  47487  chnerlem3  47491  nnmul2  47955  zplusmodne  47974  p1modne  47978  m1modne  47979  minusmod5ne  47980  submodlt  47981  minusmodnep2tmod  47984  m1modmmod  47989  modmknepk  47993  mod2addne  47995  modm2nep1  47997  modm1nep2  47999  modm1nem2  48000  modm1p1ne  48001  muldvdsfacgt  48011  muldvdsfacm1  48012  iccpartipre  48058  iccpartiltu  48059  iccpartigtl  48060  iccpartgt  48064  icceuelpartlem  48072  icceuelpart  48073  iccpartnel  48075  fargshiftf1  48078  nprmmul2  48165  nprmmul3  48166  nprmdvdsfacm1lem1  48260  nprmdvdsfacm1lem3  48262  nprmdvdsfacm1lem4  48263  bgoldbtbndlem2  48459  upgrimpthslem2  48561  gpgiedgdmellem  48699  gpgvtx0  48706  gpgvtx1  48707  gpgedgvtx0  48714  gpgedgvtx1  48715  gpgvtxedg0  48716  gpgvtxedg1  48717  gpgedg2iv  48720  gpg5nbgrvtx13starlem2  48725  gpg3nbgrvtx0  48729  gpg5nbgrvtx03star  48733  gpg5nbgr3star  48734  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  fllog2  49232  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  nn0mullong  49289