Theorem elfzoelz 13607

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 13605	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13606	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13604	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7489	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 585	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4551	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3923	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4542  (class class class)co 7361  ℤcz 12518  ..^cfzo 13602

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 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-uz 12783  df-fz 13456  df-fzo 13603

This theorem is referenced by:  elfzo2  13610  elfzole1  13616  elfzolt2  13617  elfzolt3  13618  elfzolt2b  13619  elfzop1le2  13621  elfzouz2  13623  fzonnsub  13633  fzospliti  13640  fzodisj  13642  fzodisjsn  13646  elfzo0subge1  13654  elfzo0suble  13655  fzonmapblen  13657  fzoaddel  13666  elincfzoext  13672  fzosubel  13673  elfzom1elp1fzo1  13716  elfzo1elm1fzo0  13717  elfznelfzob  13723  modaddid  13863  modaddmodup  13890  modaddmodlo  13891  modfzo0difsn  13899  modsumfzodifsn  13900  addmodlteq  13902  ccatval3  14535  ccatlid  14543  ccatass  14545  ccatrn  14546  ccatalpha  14550  swrdfv0  14606  swrdfv2  14618  swrds1  14623  ccatswrd  14625  pfxfv  14639  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  14785  cshimadifsn0  14786  cshco  14792  fzomaxdiflem  15299  fzomaxdif  15300  pwdif  15827  pwm1geoser  15828  fzo0dvdseq  16286  fzocongeq  16287  addmodlteqALT  16288  crth  16742  phimullem  16743  eulerthlem1  16745  eulerthlem2  16746  hashgcdlem  16752  hashgcdeq  16754  phisum  16755  reumodprminv  16769  modprm0  16770  nnnn0modprm0  16771  modprmn0modprm0  16772  prmgaplem7  17022  cshwshashlem2  17061  cshwshashlem3  17062  cshwrepswhash1  17067  chnccat  18586  chnrev  18587  chnpof1  18590  psgnunilem5  19463  odf1o2  19542  odngen  19546  znf1o  21544  znunithash  21557  dvfsumle  26001  dvfsumabs  26003  dchrisumlem1  27469  dchrisumlem2  27470  dchrisum  27472  pntlemq  27581  pntlemr  27582  pntlemj  27583  pntlemi  27584  pntlemf  27585  wlk1walk  29725  pthdadjvtx  29814  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  crctcshlem2  29904  crctcshwlkn0  29907  crctcshtrl  29909  crctcsh  29910  clwwlkccatlem  30077  clwwisshclwwslem  30102  clwwisshclwws  30103  eucrctshift  30331  eucrct2eupth  30333  ccatf1  33027  cshwrnid  33039  revpfxsfxrev  35317  revwlk  35326  poimirlem8  37966  poimirlem18  37976  poimirlem21  37979  poimirlem22  37980  poimirlem24  37982  frlmvscadiccat  42968  iblspltprt  46422  itgspltprt  46428  stoweidlem3  46452  fourierdlem12  46568  fourierdlem20  46576  fourierdlem46  46601  fourierdlem50  46605  fourierdlem54  46609  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem76  46631  fourierdlem79  46634  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  iundjiun  46909  carageniuncllem1  46970  caratheodorylem1  46975  ormklocald  47323  ormkglobd  47324  natlocalincr  47325  natglobalincr  47326  chnsubseq  47329  chnerlem3  47333  nnmul2  47793  zplusmodne  47812  p1modne  47816  m1modne  47817  minusmod5ne  47818  submodlt  47819  minusmodnep2tmod  47822  m1modmmod  47827  modmknepk  47831  mod2addne  47833  modm2nep1  47835  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartipre  47896  iccpartiltu  47897  iccpartigtl  47898  iccpartgt  47902  icceuelpartlem  47910  icceuelpart  47911  iccpartnel  47913  fargshiftf1  47916  nprmmul2  48003  nprmmul3  48004  nprmdvdsfacm1lem1  48098  nprmdvdsfacm1lem3  48100  nprmdvdsfacm1lem4  48101  bgoldbtbndlem2  48297  upgrimpthslem2  48399  gpgiedgdmellem  48537  gpgvtx0  48544  gpgvtx1  48545  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgedg2iv  48558  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  gpg5nbgrvtx03star  48571  gpg5nbgr3star  48572  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  fllog2  49059  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0mullong  49116