Theorem elfzoelz 13604

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 13602	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13603	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13601	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7484	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 590	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4538	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3916	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2119  𝒫 cpw 4529  (class class class)co 7356  ℤcz 12515  ..^cfzo 13599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-neg 11371  df-z 12516  df-uz 12780  df-fz 13453  df-fzo 13600

This theorem is referenced by:  elfzo2  13607  elfzole1  13613  elfzolt2  13614  elfzolt3  13615  elfzolt2b  13616  elfzop1le2  13618  elfzouz2  13620  fzonnsub  13630  fzospliti  13637  fzodisj  13639  fzodisjsn  13643  elfzo0subge1  13651  elfzo0suble  13652  fzonmapblen  13654  fzoaddel  13663  elincfzoext  13669  fzosubel  13670  elfzom1elp1fzo1  13713  elfzo1elm1fzo0  13714  elfznelfzob  13720  modaddid  13860  modaddmodup  13887  modaddmodlo  13888  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  ccatval3  14532  ccatlid  14540  ccatass  14542  ccatrn  14543  ccatalpha  14547  swrdfv0  14603  swrdfv2  14615  swrds1  14620  ccatswrd  14622  pfxfv  14636  ccatpfx  14654  swrdswrd  14658  pfxccatin12lem2a  14680  swrdccatin2  14682  pfxccatin12lem2  14684  revccat  14719  revrev  14720  repswrevw  14740  cshwidxmod  14756  cshwidxmodr  14757  cshwidx0  14759  cshwidxm1  14760  cshweqrep  14774  cshw1  14775  cshimadifsn  14782  cshimadifsn0  14783  cshco  14789  fzomaxdiflem  15296  fzomaxdif  15297  pwdif  15824  pwm1geoser  15825  fzo0dvdseq  16283  fzocongeq  16284  addmodlteqALT  16285  crth  16739  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  hashgcdlem  16749  hashgcdeq  16751  phisum  16752  reumodprminv  16766  modprm0  16767  nnnn0modprm0  16768  modprmn0modprm0  16769  prmgaplem7  17019  cshwshashlem2  17058  cshwshashlem3  17059  cshwrepswhash1  17064  chnccat  18583  chnrev  18584  chnpof1  18587  psgnunilem5  19460  odf1o2  19539  odngen  19543  znf1o  21526  znunithash  21539  dvfsumle  26006  dvfsumabs  26008  dchrisumlem1  27470  dchrisumlem2  27471  dchrisum  27473  pntlemq  27582  pntlemr  27583  pntlemj  27584  pntlemi  27585  pntlemf  27586  wlk1walk  29725  pthdadjvtx  29814  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  crctcshlem2  29904  crctcshwlkn0  29907  crctcshtrl  29909  crctcsh  29910  clwwlkccatlem  30077  clwwisshclwwslem  30102  clwwisshclwws  30103  eucrctshift  30331  eucrct2eupth  30333  ccatf1  33028  cshwrnid  33040  revpfxsfxrev  35344  revwlk  35353  poimirlem8  37995  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem24  38011  frlmvscadiccat  42996  iblspltprt  46416  itgspltprt  46422  stoweidlem3  46446  fourierdlem12  46562  fourierdlem20  46570  fourierdlem46  46595  fourierdlem50  46599  fourierdlem54  46603  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem76  46625  fourierdlem79  46628  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  iundjiun  46903  carageniuncllem1  46964  caratheodorylem1  46969  ormklocald  47319  ormkglobd  47320  natlocalincr  47321  natglobalincr  47322  chnsubseq  47325  chnerlem3  47329  nnmul2  47793  zplusmodne  47812  p1modne  47816  m1modne  47817  minusmod5ne  47818  submodlt  47819  minusmodnep2tmod  47822  m1modmmod  47827  modmknepk  47831  mod2addne  47833  modm2nep1  47835  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartipre  47896  iccpartiltu  47897  iccpartigtl  47898  iccpartgt  47902  icceuelpartlem  47910  icceuelpart  47911  iccpartnel  47913  fargshiftf1  47916  nprmmul2  48003  nprmmul3  48004  nprmdvdsfacm1lem1  48098  nprmdvdsfacm1lem3  48100  nprmdvdsfacm1lem4  48101  bgoldbtbndlem2  48297  upgrimpthslem2  48399  gpgiedgdmellem  48537  gpgvtx0  48544  gpgvtx1  48545  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgedg2iv  48558  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  gpg5nbgrvtx03star  48571  gpg5nbgr3star  48572  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  fllog2  49059  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0mullong  49116