Theorem elfzoelz 13613

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 13611	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13612	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13610	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7495	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 585	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4550	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3922	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4541  (class class class)co 7367  ℤcz 12524  ..^cfzo 13608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-neg 11380  df-z 12525  df-uz 12789  df-fz 13462  df-fzo 13609

This theorem is referenced by:  elfzo2  13616  elfzole1  13622  elfzolt2  13623  elfzolt3  13624  elfzolt2b  13625  elfzop1le2  13627  elfzouz2  13629  fzonnsub  13639  fzospliti  13646  fzodisj  13648  fzodisjsn  13652  elfzo0subge1  13660  elfzo0suble  13661  fzonmapblen  13663  fzoaddel  13672  elincfzoext  13678  fzosubel  13679  elfzom1elp1fzo1  13722  elfzo1elm1fzo0  13723  elfznelfzob  13729  modaddid  13869  modaddmodup  13896  modaddmodlo  13897  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  ccatval3  14541  ccatlid  14549  ccatass  14551  ccatrn  14552  ccatalpha  14556  swrdfv0  14612  swrdfv2  14624  swrds1  14629  ccatswrd  14631  pfxfv  14645  ccatpfx  14663  swrdswrd  14667  pfxccatin12lem2a  14689  swrdccatin2  14691  pfxccatin12lem2  14693  revccat  14728  revrev  14729  repswrevw  14749  cshwidxmod  14765  cshwidxmodr  14766  cshwidx0  14768  cshwidxm1  14769  cshweqrep  14783  cshw1  14784  cshimadifsn  14791  cshimadifsn0  14792  cshco  14798  fzomaxdiflem  15305  fzomaxdif  15306  pwdif  15833  pwm1geoser  15834  fzo0dvdseq  16292  fzocongeq  16293  addmodlteqALT  16294  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  hashgcdlem  16758  hashgcdeq  16760  phisum  16761  reumodprminv  16775  modprm0  16776  nnnn0modprm0  16777  modprmn0modprm0  16778  prmgaplem7  17028  cshwshashlem2  17067  cshwshashlem3  17068  cshwrepswhash1  17073  chnccat  18592  chnrev  18593  chnpof1  18596  psgnunilem5  19469  odf1o2  19548  odngen  19552  znf1o  21531  znunithash  21544  dvfsumle  25988  dvfsumabs  25990  dchrisumlem1  27452  dchrisumlem2  27453  dchrisum  27455  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemi  27567  pntlemf  27568  wlk1walk  29707  pthdadjvtx  29796  crctcshwlkn0lem3  29880  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  crctcshlem2  29886  crctcshwlkn0  29889  crctcshtrl  29891  crctcsh  29892  clwwlkccatlem  30059  clwwisshclwwslem  30084  clwwisshclwws  30085  eucrctshift  30313  eucrct2eupth  30315  ccatf1  33009  cshwrnid  33021  revpfxsfxrev  35298  revwlk  35307  poimirlem8  37949  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem24  37965  frlmvscadiccat  42951  iblspltprt  46401  itgspltprt  46407  stoweidlem3  46431  fourierdlem12  46547  fourierdlem20  46555  fourierdlem46  46580  fourierdlem50  46584  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem76  46610  fourierdlem79  46613  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  iundjiun  46888  carageniuncllem1  46949  caratheodorylem1  46954  ormklocald  47304  ormkglobd  47305  natlocalincr  47306  natglobalincr  47307  chnsubseq  47310  chnerlem3  47314  nnmul2  47778  zplusmodne  47797  p1modne  47801  m1modne  47802  minusmod5ne  47803  submodlt  47804  minusmodnep2tmod  47807  m1modmmod  47812  modmknepk  47816  mod2addne  47818  modm2nep1  47820  modm1nep2  47822  modm1nem2  47823  modm1p1ne  47824  muldvdsfacgt  47834  muldvdsfacm1  47835  iccpartipre  47881  iccpartiltu  47882  iccpartigtl  47883  iccpartgt  47887  icceuelpartlem  47895  icceuelpart  47896  iccpartnel  47898  fargshiftf1  47901  nprmmul2  47988  nprmmul3  47989  nprmdvdsfacm1lem1  48083  nprmdvdsfacm1lem3  48085  nprmdvdsfacm1lem4  48086  bgoldbtbndlem2  48282  upgrimpthslem2  48384  gpgiedgdmellem  48522  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedg2iv  48543  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  fllog2  49044  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0mullong  49101