Theorem elfzoelz 13041

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 13039	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13040	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13038	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7282	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 586	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4553	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3971	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4542  (class class class)co 7159  ℤcz 11984  ..^cfzo 13036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-cnex 10596  ax-resscn 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-1st 7692  df-2nd 7693  df-neg 10876  df-z 11985  df-uz 12247  df-fz 12896  df-fzo 13037

This theorem is referenced by:  elfzo2  13044  elfzole1  13049  elfzolt2  13050  elfzolt3  13051  elfzolt2b  13052  elfzouz2  13055  fzonnsub  13065  fzospliti  13072  fzodisj  13074  fzodisjsn  13078  fzonmapblen  13086  fzoaddel  13093  elincfzoext  13098  fzosubel  13099  elfzom1elp1fzo1  13140  elfzo1elm1fzo0  13141  elfznelfzob  13146  modaddmodup  13305  modaddmodlo  13306  modfzo0difsn  13314  modsumfzodifsn  13315  addmodlteq  13317  wrdexgOLD  13875  ccatval3  13936  ccatlid  13943  ccatass  13945  ccatrn  13946  ccatalpha  13950  swrdfv0  14014  swrdfv2  14026  swrds1  14031  ccatswrd  14033  pfxfv  14047  ccatpfx  14066  swrdswrd  14070  pfxccatin12lem2a  14092  swrdccatin2  14094  pfxccatin12lem2  14096  revccat  14131  revrev  14132  repswrevw  14152  cshwidxmod  14168  cshwidxmodr  14169  cshwidx0  14171  cshwidxm1  14172  cshweqrep  14186  cshw1  14187  cshimadifsn  14194  cshimadifsn0  14195  cshco  14201  fzomaxdiflem  14705  fzomaxdif  14706  pwdif  15226  pwm1geoser  15227  fzo0dvdseq  15676  fzocongeq  15677  addmodlteqALT  15678  crth  16118  phimullem  16119  eulerthlem1  16121  eulerthlem2  16122  hashgcdlem  16128  hashgcdeq  16129  phisum  16130  reumodprminv  16144  modprm0  16145  nnnn0modprm0  16146  modprmn0modprm0  16147  prmgaplem7  16396  cshwshashlem2  16433  cshwshashlem3  16434  cshwrepswhash1  16439  psgnunilem5  18625  odf1o2  18701  odngen  18705  znf1o  20701  zntoslem  20706  znunithash  20714  dvfsumle  24621  dvfsumabs  24623  dchrisumlem1  26068  dchrisumlem2  26069  dchrisum  26071  pntlemq  26180  pntlemr  26181  pntlemj  26182  pntlemi  26183  pntlemf  26184  wlk1walk  27423  pthdadjvtx  27514  crctcshwlkn0lem3  27593  crctcshwlkn0lem4  27594  crctcshwlkn0lem5  27595  crctcshwlkn0lem6  27596  crctcshlem2  27599  crctcshwlkn0  27602  crctcshtrl  27604  crctcsh  27605  clwwlkccatlem  27770  clwwisshclwwslem  27795  clwwisshclwws  27796  eucrctshift  28025  eucrct2eupth  28027  ccatf1  30629  cshwrnid  30639  revpfxsfxrev  32366  revwlk  32375  poimirlem8  34904  poimirlem18  34914  poimirlem21  34917  poimirlem22  34918  poimirlem24  34920  frlmvscadiccat  39151  elfzop1le2  41562  iblspltprt  42264  itgspltprt  42270  stoweidlem3  42295  fourierdlem12  42411  fourierdlem20  42419  fourierdlem46  42444  fourierdlem50  42448  fourierdlem54  42452  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem76  42474  fourierdlem79  42477  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  iundjiun  42749  carageniuncllem1  42810  caratheodorylem1  42815  iccpartipre  43588  iccpartiltu  43589  iccpartigtl  43590  iccpartgt  43594  icceuelpartlem  43602  icceuelpart  43603  iccpartnel  43605  fargshiftf1  43608  bgoldbtbndlem2  43978  m1modmmod  44588  fllog2  44635  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  nn0mullong  44692