Theorem elfzoelz 13638

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 13636	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13637	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13635	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7533	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 583	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4606	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3978	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2098  𝒫 cpw 4597  (class class class)co 7405  ℤcz 12562  ..^cfzo 13633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7974  df-2nd 7975  df-neg 11451  df-z 12563  df-uz 12827  df-fz 13491  df-fzo 13634

This theorem is referenced by:  elfzo2  13641  elfzole1  13646  elfzolt2  13647  elfzolt3  13648  elfzolt2b  13649  elfzop1le2  13651  elfzouz2  13653  fzonnsub  13663  fzospliti  13670  fzodisj  13672  fzodisjsn  13676  fzonmapblen  13684  fzoaddel  13691  elincfzoext  13696  fzosubel  13697  elfzom1elp1fzo1  13738  elfzo1elm1fzo0  13739  elfznelfzob  13744  modaddmodup  13905  modaddmodlo  13906  modfzo0difsn  13914  modsumfzodifsn  13915  addmodlteq  13917  ccatval3  14535  ccatlid  14542  ccatass  14544  ccatrn  14545  ccatalpha  14549  swrdfv0  14605  swrdfv2  14617  swrds1  14622  ccatswrd  14624  pfxfv  14638  ccatpfx  14657  swrdswrd  14661  pfxccatin12lem2a  14683  swrdccatin2  14685  pfxccatin12lem2  14687  revccat  14722  revrev  14723  repswrevw  14743  cshwidxmod  14759  cshwidxmodr  14760  cshwidx0  14762  cshwidxm1  14763  cshweqrep  14777  cshw1  14778  cshimadifsn  14786  cshimadifsn0  14787  cshco  14793  fzomaxdiflem  15295  fzomaxdif  15296  pwdif  15820  pwm1geoser  15821  fzo0dvdseq  16273  fzocongeq  16274  addmodlteqALT  16275  crth  16720  phimullem  16721  eulerthlem1  16723  eulerthlem2  16724  hashgcdlem  16730  hashgcdeq  16731  phisum  16732  reumodprminv  16746  modprm0  16747  nnnn0modprm0  16748  modprmn0modprm0  16749  prmgaplem7  16999  cshwshashlem2  17039  cshwshashlem3  17040  cshwrepswhash1  17045  psgnunilem5  19414  odf1o2  19493  odngen  19497  znf1o  21446  znunithash  21459  dvfsumle  25909  dvfsumleOLD  25910  dvfsumabs  25912  dchrisumlem1  27377  dchrisumlem2  27378  dchrisum  27380  pntlemq  27489  pntlemr  27490  pntlemj  27491  pntlemi  27492  pntlemf  27493  wlk1walk  29405  pthdadjvtx  29496  crctcshwlkn0lem3  29575  crctcshwlkn0lem4  29576  crctcshwlkn0lem5  29577  crctcshwlkn0lem6  29578  crctcshlem2  29581  crctcshwlkn0  29584  crctcshtrl  29586  crctcsh  29587  clwwlkccatlem  29751  clwwisshclwwslem  29776  clwwisshclwws  29777  eucrctshift  30005  eucrct2eupth  30007  ccatf1  32620  cshwrnid  32630  revpfxsfxrev  34634  revwlk  34643  poimirlem8  37009  poimirlem18  37019  poimirlem21  37022  poimirlem22  37023  poimirlem24  37025  frlmvscadiccat  41641  iblspltprt  45261  itgspltprt  45267  stoweidlem3  45291  fourierdlem12  45407  fourierdlem20  45415  fourierdlem46  45440  fourierdlem50  45444  fourierdlem54  45448  fourierdlem63  45457  fourierdlem64  45458  fourierdlem65  45459  fourierdlem76  45470  fourierdlem79  45473  fourierdlem102  45496  fourierdlem103  45497  fourierdlem104  45498  fourierdlem114  45508  iundjiun  45748  carageniuncllem1  45809  caratheodorylem1  45814  natlocalincr  46162  natglobalincr  46163  iccpartipre  46661  iccpartiltu  46662  iccpartigtl  46663  iccpartgt  46667  icceuelpartlem  46675  icceuelpart  46676  iccpartnel  46678  fargshiftf1  46681  bgoldbtbndlem2  47046  m1modmmod  47482  fllog2  47529  nn0sumshdiglemA  47580  nn0sumshdiglemB  47581  nn0mullong  47586