Theorem elfzoelz 12789

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 12787	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 12788	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 12786	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7042	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 579	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4390	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3821	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  𝒫 cpw 4378  (class class class)co 6922  ℤcz 11728  ..^cfzo 12784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-neg 10609  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785

This theorem is referenced by:  elfzo2  12792  elfzole1  12797  elfzolt2  12798  elfzolt3  12799  elfzolt2b  12800  elfzouz2  12803  fzonnsub  12812  fzospliti  12819  fzodisj  12821  fzodisjsn  12825  fzonmapblen  12833  fzoaddel  12840  elincfzoext  12845  fzosubel  12846  elfzom1elp1fzo1  12887  elfzo1elm1fzo0  12888  elfznelfzob  12893  modaddmodup  13052  modaddmodlo  13053  modfzo0difsn  13061  modsumfzodifsn  13062  addmodlteq  13064  wrdexgOLD  13610  ccatval3  13669  ccatlid  13676  ccatass  13678  ccatrn  13679  ccatalpha  13683  swrd0valOLD  13737  swrdfv0  13741  swrdidOLD  13745  swrd0fvOLD  13758  swrdfv2  13765  swrds1  13771  ccatswrd  13776  pfxfv  13791  ccatpfx  13810  swrdswrd  13814  swrdccatin12lem2a  13853  swrdccatin2  13856  pfxccatin12lem2  13858  swrdccatin12lem2OLD  13859  splfv1OLD  13899  splfv2a  13900  splfv2aOLD  13901  revccat  13912  revrev  13913  repswrevw  13933  cshwidxmod  13954  cshwidxmodr  13955  cshwidx0  13957  cshwidxm1  13958  cshweqrep  13972  cshw1  13973  cshimadifsn  13980  cshimadifsn0  13981  cshco  13987  fzomaxdiflem  14489  fzomaxdif  14490  fzo0dvdseq  15452  fzocongeq  15453  addmodlteqALT  15454  crth  15887  phimullem  15888  eulerthlem1  15890  eulerthlem2  15891  hashgcdlem  15897  hashgcdeq  15898  phisum  15899  reumodprminv  15913  modprm0  15914  nnnn0modprm0  15915  modprmn0modprm0  15916  prmgaplem7  16165  cshwshashlem2  16202  cshwshashlem3  16203  cshwrepswhash1  16208  psgnunilem5  18297  psgnunilem5OLD  18298  odf1o2  18372  odngen  18376  efgsp1  18534  efgsresOLD  18536  znf1o  20295  zntoslem  20300  znunithash  20308  dvfsumle  24221  dvfsumabs  24223  dchrisumlem1  25630  dchrisumlem2  25631  dchrisum  25633  pntlemq  25742  pntlemr  25743  pntlemj  25744  pntlemi  25745  pntlemf  25746  wlk1walk  26986  pthdadjvtx  27082  crctcshwlkn0lem3  27161  crctcshwlkn0lem4  27162  crctcshwlkn0lem5  27163  crctcshwlkn0lem6  27164  crctcshlem2  27167  crctcshwlkn0  27170  crctcshtrl  27172  crctcsh  27173  clwwlkccatlem  27369  clwwisshclwwslem  27403  clwwisshclwws  27404  eucrctshift  27647  eucrct2eupthOLD  27650  eucrct2eupth  27651  signsvfn  31261  poimirlem8  34027  poimirlem18  34037  poimirlem21  34040  poimirlem22  34041  poimirlem24  34043  elfzop1le2  40394  iblspltprt  41098  itgspltprt  41104  stoweidlem3  41129  fourierdlem12  41245  fourierdlem20  41253  fourierdlem46  41278  fourierdlem50  41282  fourierdlem54  41286  fourierdlem63  41295  fourierdlem64  41296  fourierdlem65  41297  fourierdlem76  41308  fourierdlem79  41311  fourierdlem102  41334  fourierdlem103  41335  fourierdlem104  41336  fourierdlem114  41346  iundjiun  41583  carageniuncllem1  41644  caratheodorylem1  41649  iccpartipre  42371  iccpartiltu  42372  iccpartigtl  42373  iccpartgt  42377  icceuelpartlem  42385  icceuelpart  42386  iccpartnel  42388  fargshiftf1  42391  pwdif  42504  pwm1geoserALT  42505  bgoldbtbndlem2  42701  m1modmmod  43313  fllog2  43359  nn0sumshdiglemA  43410  nn0sumshdiglemB  43411  nn0mullong  43416