Theorem elfzoelz 13573

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 13571	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13572	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13570	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7484	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4561	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3932	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4552  (class class class)co 7356  ℤcz 12486  ..^cfzo 13568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-neg 11365  df-z 12487  df-uz 12750  df-fz 13422  df-fzo 13569

This theorem is referenced by:  elfzo2  13576  elfzole1  13581  elfzolt2  13582  elfzolt3  13583  elfzolt2b  13584  elfzop1le2  13586  elfzouz2  13588  fzonnsub  13598  fzospliti  13605  fzodisj  13607  fzodisjsn  13611  elfzo0subge1  13619  elfzo0suble  13620  fzonmapblen  13622  fzoaddel  13631  elincfzoext  13637  fzosubel  13638  elfzom1elp1fzo1  13681  elfzo1elm1fzo0  13682  elfznelfzob  13688  modaddid  13828  modaddmodup  13855  modaddmodlo  13856  modfzo0difsn  13864  modsumfzodifsn  13865  addmodlteq  13867  ccatval3  14500  ccatlid  14508  ccatass  14510  ccatrn  14511  ccatalpha  14515  swrdfv0  14571  swrdfv2  14583  swrds1  14588  ccatswrd  14590  pfxfv  14604  ccatpfx  14622  swrdswrd  14626  pfxccatin12lem2a  14648  swrdccatin2  14650  pfxccatin12lem2  14652  revccat  14687  revrev  14688  repswrevw  14708  cshwidxmod  14724  cshwidxmodr  14725  cshwidx0  14727  cshwidxm1  14728  cshweqrep  14742  cshw1  14743  cshimadifsn  14750  cshimadifsn0  14751  cshco  14757  fzomaxdiflem  15264  fzomaxdif  15265  pwdif  15789  pwm1geoser  15790  fzo0dvdseq  16248  fzocongeq  16249  addmodlteqALT  16250  crth  16703  phimullem  16704  eulerthlem1  16706  eulerthlem2  16707  hashgcdlem  16713  hashgcdeq  16715  phisum  16716  reumodprminv  16730  modprm0  16731  nnnn0modprm0  16732  modprmn0modprm0  16733  prmgaplem7  16983  cshwshashlem2  17022  cshwshashlem3  17023  cshwrepswhash1  17028  chnccat  18547  chnrev  18548  chnpof1  18551  psgnunilem5  19421  odf1o2  19500  odngen  19504  znf1o  21504  znunithash  21517  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dchrisumlem1  27454  dchrisumlem2  27455  dchrisum  27457  pntlemq  27566  pntlemr  27567  pntlemj  27568  pntlemi  27569  pntlemf  27570  wlk1walk  29661  pthdadjvtx  29750  crctcshwlkn0lem3  29834  crctcshwlkn0lem4  29835  crctcshwlkn0lem5  29836  crctcshwlkn0lem6  29837  crctcshlem2  29840  crctcshwlkn0  29843  crctcshtrl  29845  crctcsh  29846  clwwlkccatlem  30013  clwwisshclwwslem  30038  clwwisshclwws  30039  eucrctshift  30267  eucrct2eupth  30269  ccatf1  32980  cshwrnid  32992  revpfxsfxrev  35259  revwlk  35268  poimirlem8  37768  poimirlem18  37778  poimirlem21  37781  poimirlem22  37782  poimirlem24  37784  frlmvscadiccat  42703  iblspltprt  46159  itgspltprt  46165  stoweidlem3  46189  fourierdlem12  46305  fourierdlem20  46313  fourierdlem46  46338  fourierdlem50  46342  fourierdlem54  46346  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem76  46368  fourierdlem79  46371  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem114  46406  iundjiun  46646  carageniuncllem1  46707  caratheodorylem1  46712  ormklocald  47060  ormkglobd  47061  natlocalincr  47062  natglobalincr  47063  chnsubseq  47066  chnerlem3  47070  zplusmodne  47531  p1modne  47535  m1modne  47536  minusmod5ne  47537  submodlt  47538  minusmodnep2tmod  47541  m1modmmod  47546  modmknepk  47550  mod2addne  47552  modm2nep1  47554  modm1nep2  47556  modm1nem2  47557  modm1p1ne  47558  iccpartipre  47609  iccpartiltu  47610  iccpartigtl  47611  iccpartgt  47615  icceuelpartlem  47623  icceuelpart  47624  iccpartnel  47626  fargshiftf1  47629  bgoldbtbndlem2  47994  upgrimpthslem2  48096  gpgiedgdmellem  48234  gpgvtx0  48241  gpgvtx1  48242  gpgedgvtx0  48249  gpgedgvtx1  48250  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgedg2iv  48255  gpg5nbgrvtx13starlem2  48260  gpg3nbgrvtx0  48264  gpg5nbgrvtx03star  48268  gpg5nbgr3star  48269  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  fllog2  48756  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0mullong  48813