Theorem elfzoelz 13587

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 13585	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13586	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13584	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7496	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 585	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4565	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3936	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4556  (class class class)co 7368  ℤcz 12500  ..^cfzo 13582

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 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-neg 11379  df-z 12501  df-uz 12764  df-fz 13436  df-fzo 13583

This theorem is referenced by:  elfzo2  13590  elfzole1  13595  elfzolt2  13596  elfzolt3  13597  elfzolt2b  13598  elfzop1le2  13600  elfzouz2  13602  fzonnsub  13612  fzospliti  13619  fzodisj  13621  fzodisjsn  13625  elfzo0subge1  13633  elfzo0suble  13634  fzonmapblen  13636  fzoaddel  13645  elincfzoext  13651  fzosubel  13652  elfzom1elp1fzo1  13695  elfzo1elm1fzo0  13696  elfznelfzob  13702  modaddid  13842  modaddmodup  13869  modaddmodlo  13870  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  ccatval3  14514  ccatlid  14522  ccatass  14524  ccatrn  14525  ccatalpha  14529  swrdfv0  14585  swrdfv2  14597  swrds1  14602  ccatswrd  14604  pfxfv  14618  ccatpfx  14636  swrdswrd  14640  pfxccatin12lem2a  14662  swrdccatin2  14664  pfxccatin12lem2  14666  revccat  14701  revrev  14702  repswrevw  14722  cshwidxmod  14738  cshwidxmodr  14739  cshwidx0  14741  cshwidxm1  14742  cshweqrep  14756  cshw1  14757  cshimadifsn  14764  cshimadifsn0  14765  cshco  14771  fzomaxdiflem  15278  fzomaxdif  15279  pwdif  15803  pwm1geoser  15804  fzo0dvdseq  16262  fzocongeq  16263  addmodlteqALT  16264  crth  16717  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  hashgcdlem  16727  hashgcdeq  16729  phisum  16730  reumodprminv  16744  modprm0  16745  nnnn0modprm0  16746  modprmn0modprm0  16747  prmgaplem7  16997  cshwshashlem2  17036  cshwshashlem3  17037  cshwrepswhash1  17042  chnccat  18561  chnrev  18562  chnpof1  18565  psgnunilem5  19435  odf1o2  19514  odngen  19518  znf1o  21518  znunithash  21531  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dchrisumlem1  27468  dchrisumlem2  27469  dchrisum  27471  pntlemq  27580  pntlemr  27581  pntlemj  27582  pntlemi  27583  pntlemf  27584  wlk1walk  29724  pthdadjvtx  29813  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  crctcshlem2  29903  crctcshwlkn0  29906  crctcshtrl  29908  crctcsh  29909  clwwlkccatlem  30076  clwwisshclwwslem  30101  clwwisshclwws  30102  eucrctshift  30330  eucrct2eupth  30332  ccatf1  33042  cshwrnid  33054  revpfxsfxrev  35332  revwlk  35341  poimirlem8  37879  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  poimirlem24  37895  frlmvscadiccat  42876  iblspltprt  46331  itgspltprt  46337  stoweidlem3  46361  fourierdlem12  46477  fourierdlem20  46485  fourierdlem46  46510  fourierdlem50  46514  fourierdlem54  46518  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem76  46540  fourierdlem79  46543  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  iundjiun  46818  carageniuncllem1  46879  caratheodorylem1  46884  ormklocald  47232  ormkglobd  47233  natlocalincr  47234  natglobalincr  47235  chnsubseq  47238  chnerlem3  47242  zplusmodne  47703  p1modne  47707  m1modne  47708  minusmod5ne  47709  submodlt  47710  minusmodnep2tmod  47713  m1modmmod  47718  modmknepk  47722  mod2addne  47724  modm2nep1  47726  modm1nep2  47728  modm1nem2  47729  modm1p1ne  47730  iccpartipre  47781  iccpartiltu  47782  iccpartigtl  47783  iccpartgt  47787  icceuelpartlem  47795  icceuelpart  47796  iccpartnel  47798  fargshiftf1  47801  bgoldbtbndlem2  48166  upgrimpthslem2  48268  gpgiedgdmellem  48406  gpgvtx0  48413  gpgvtx1  48414  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgedg2iv  48427  gpg5nbgrvtx13starlem2  48432  gpg3nbgrvtx0  48436  gpg5nbgrvtx03star  48440  gpg5nbgr3star  48441  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  fllog2  48928  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  nn0mullong  48985