Theorem elfzoelz 13695

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 13693	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13694	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13692	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7560	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4613	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3995	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2105  𝒫 cpw 4604  (class class class)co 7430  ℤcz 12610  ..^cfzo 13690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-neg 11492  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691

This theorem is referenced by:  elfzo2  13698  elfzole1  13703  elfzolt2  13704  elfzolt3  13705  elfzolt2b  13706  elfzop1le2  13708  elfzouz2  13710  fzonnsub  13720  fzospliti  13727  fzodisj  13729  fzodisjsn  13733  elfzo0subge1  13741  elfzo0suble  13742  fzonmapblen  13744  fzoaddel  13752  elincfzoext  13758  fzosubel  13759  elfzom1elp1fzo1  13802  elfzo1elm1fzo0  13803  elfznelfzob  13808  modaddmodup  13971  modaddmodlo  13972  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  ccatval3  14613  ccatlid  14620  ccatass  14622  ccatrn  14623  ccatalpha  14627  swrdfv0  14683  swrdfv2  14695  swrds1  14700  ccatswrd  14702  pfxfv  14716  ccatpfx  14735  swrdswrd  14739  pfxccatin12lem2a  14761  swrdccatin2  14763  pfxccatin12lem2  14765  revccat  14800  revrev  14801  repswrevw  14821  cshwidxmod  14837  cshwidxmodr  14838  cshwidx0  14840  cshwidxm1  14841  cshweqrep  14855  cshw1  14856  cshimadifsn  14864  cshimadifsn0  14865  cshco  14871  fzomaxdiflem  15377  fzomaxdif  15378  pwdif  15900  pwm1geoser  15901  fzo0dvdseq  16356  fzocongeq  16357  addmodlteqALT  16358  crth  16811  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  hashgcdlem  16821  hashgcdeq  16822  phisum  16823  reumodprminv  16837  modprm0  16838  nnnn0modprm0  16839  modprmn0modprm0  16840  prmgaplem7  17090  cshwshashlem2  17130  cshwshashlem3  17131  cshwrepswhash1  17136  psgnunilem5  19526  odf1o2  19605  odngen  19609  znf1o  21587  znunithash  21600  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dchrisumlem1  27547  dchrisumlem2  27548  dchrisum  27550  pntlemq  27659  pntlemr  27660  pntlemj  27661  pntlemi  27662  pntlemf  27663  wlk1walk  29671  pthdadjvtx  29762  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  crctcshlem2  29847  crctcshwlkn0  29850  crctcshtrl  29852  crctcsh  29853  clwwlkccatlem  30017  clwwisshclwwslem  30042  clwwisshclwws  30043  eucrctshift  30271  eucrct2eupth  30273  ccatf1  32917  cshwrnid  32930  revpfxsfxrev  35099  revwlk  35108  poimirlem8  37614  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem24  37630  frlmvscadiccat  42492  iblspltprt  45928  itgspltprt  45934  stoweidlem3  45958  fourierdlem12  46074  fourierdlem20  46082  fourierdlem46  46107  fourierdlem50  46111  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem76  46137  fourierdlem79  46140  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  iundjiun  46415  carageniuncllem1  46476  caratheodorylem1  46481  natlocalincr  46829  natglobalincr  46830  zplusmodne  47282  p1modne  47286  m1modne  47287  minusmod5ne  47288  submodlt  47289  minusmodnep2tmod  47292  iccpartipre  47345  iccpartiltu  47346  iccpartigtl  47347  iccpartgt  47351  icceuelpartlem  47359  icceuelpart  47360  iccpartnel  47362  fargshiftf1  47365  bgoldbtbndlem2  47730  gpgedgel  47942  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx0  47953  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg3nbgrvtxlem  47957  gpg5nbgrvtx13starlem2  47962  gpg3nbgrvtx0  47966  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  m1modmmod  48370  fllog2  48417  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0mullong  48474