Theorem elfzoelz 13631

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 13629	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13630	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13628	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7536	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4611	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3983	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  𝒫 cpw 4602  (class class class)co 7408  ℤcz 12557  ..^cfzo 13626

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-neg 11446  df-z 12558  df-uz 12822  df-fz 13484  df-fzo 13627

This theorem is referenced by:  elfzo2  13634  elfzole1  13639  elfzolt2  13640  elfzolt3  13641  elfzolt2b  13642  elfzop1le2  13644  elfzouz2  13646  fzonnsub  13656  fzospliti  13663  fzodisj  13665  fzodisjsn  13669  fzonmapblen  13677  fzoaddel  13684  elincfzoext  13689  fzosubel  13690  elfzom1elp1fzo1  13731  elfzo1elm1fzo0  13732  elfznelfzob  13737  modaddmodup  13898  modaddmodlo  13899  modfzo0difsn  13907  modsumfzodifsn  13908  addmodlteq  13910  ccatval3  14528  ccatlid  14535  ccatass  14537  ccatrn  14538  ccatalpha  14542  swrdfv0  14598  swrdfv2  14610  swrds1  14615  ccatswrd  14617  pfxfv  14631  ccatpfx  14650  swrdswrd  14654  pfxccatin12lem2a  14676  swrdccatin2  14678  pfxccatin12lem2  14680  revccat  14715  revrev  14716  repswrevw  14736  cshwidxmod  14752  cshwidxmodr  14753  cshwidx0  14755  cshwidxm1  14756  cshweqrep  14770  cshw1  14771  cshimadifsn  14779  cshimadifsn0  14780  cshco  14786  fzomaxdiflem  15288  fzomaxdif  15289  pwdif  15813  pwm1geoser  15814  fzo0dvdseq  16265  fzocongeq  16266  addmodlteqALT  16267  crth  16710  phimullem  16711  eulerthlem1  16713  eulerthlem2  16714  hashgcdlem  16720  hashgcdeq  16721  phisum  16722  reumodprminv  16736  modprm0  16737  nnnn0modprm0  16738  modprmn0modprm0  16739  prmgaplem7  16989  cshwshashlem2  17029  cshwshashlem3  17030  cshwrepswhash1  17035  psgnunilem5  19361  odf1o2  19440  odngen  19444  znf1o  21106  znunithash  21119  dvfsumle  25537  dvfsumabs  25539  dchrisumlem1  26989  dchrisumlem2  26990  dchrisum  26992  pntlemq  27101  pntlemr  27102  pntlemj  27103  pntlemi  27104  pntlemf  27105  wlk1walk  28893  pthdadjvtx  28984  crctcshwlkn0lem3  29063  crctcshwlkn0lem4  29064  crctcshwlkn0lem5  29065  crctcshwlkn0lem6  29066  crctcshlem2  29069  crctcshwlkn0  29072  crctcshtrl  29074  crctcsh  29075  clwwlkccatlem  29239  clwwisshclwwslem  29264  clwwisshclwws  29265  eucrctshift  29493  eucrct2eupth  29495  ccatf1  32110  cshwrnid  32120  revpfxsfxrev  34101  revwlk  34110  gg-dvfsumle  35177  poimirlem8  36491  poimirlem18  36501  poimirlem21  36504  poimirlem22  36505  poimirlem24  36507  frlmvscadiccat  41082  iblspltprt  44679  itgspltprt  44685  stoweidlem3  44709  fourierdlem12  44825  fourierdlem20  44833  fourierdlem46  44858  fourierdlem50  44862  fourierdlem54  44866  fourierdlem63  44875  fourierdlem64  44876  fourierdlem65  44877  fourierdlem76  44888  fourierdlem79  44891  fourierdlem102  44914  fourierdlem103  44915  fourierdlem104  44916  fourierdlem114  44926  iundjiun  45166  carageniuncllem1  45227  caratheodorylem1  45232  natlocalincr  45580  natglobalincr  45581  iccpartipre  46079  iccpartiltu  46080  iccpartigtl  46081  iccpartgt  46085  icceuelpartlem  46093  icceuelpart  46094  iccpartnel  46096  fargshiftf1  46099  bgoldbtbndlem2  46464  m1modmmod  47197  fllog2  47244  nn0sumshdiglemA  47295  nn0sumshdiglemB  47296  nn0mullong  47301