Theorem elfzoelz 13786

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 13784	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13785	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13783	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7546	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 596	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4566	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 23	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3932	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  𝒫 cpw 4557  (class class class)co 7418  ℤcz 12686  ..^cfzo 13781

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000  df-neg 11537  df-z 12687  df-uz 12959  df-fz 13633  df-fzo 13782

This theorem is used by:  elfzo2  13789  elfzole1  13795  elfzolt2  13796  elfzolt3  13797  elfzolt2b  13798  elfzop1le2  13800  elfzouz2  13802  fzonnsub  13812  fzospliti  13819  fzodisj  13821  fzodisjsn  13825  elfzo0subge1  13833  elfzo0suble  13834  fzonmapblen  13836  fzoaddel  13845  elincfzoext  13851  fzosubel  13852  elfzom1elp1fzo1  13895  elfzo1elm1fzo0  13896  elfznelfzob  13902  modaddid  14043  modaddmodup  14070  modaddmodlo  14071  modfzo0difsn  14079  modsumfzodifsn  14080  addmodlteq  14082  ccatval3  14717  ccatlid  14725  ccatass  14727  ccatrn  14728  ccatf1  14729  ccatalpha  14733  swrdfv0  14790  swrdfv2  14804  swrds1  14809  ccatswrd  14811  pfxfv  14825  ccatpfx  14843  swrdswrd  14847  pfxccatin12lem2a  14869  swrdccatin2  14871  pfxccatin12lem2  14873  revccat  14908  revrev  14909  revpfxsfxrev  14910  repswrevw  14931  cshwidxmod  14947  cshwidxmodr  14948  cshwidx0  14950  cshwidxm1  14951  cshweqrep  14965  cshw1  14966  cshimadifsn  14973  cshimadifsn0  14974  cshco  14980  fzomaxdiflem  15503  fzomaxdif  15504  pwdif  16030  pwm1geoser  16031  fzo0dvdseq  16486  fzocongeq  16487  addmodlteqALT  16488  crth  16948  phimullem  16949  eulerthlem1  16951  eulerthlem2  16952  hashgcdlem  16958  hashgcdeq  16960  phisum  16961  reumodprminv  16975  modprm0  16976  nnnn0modprm0  16977  modprmn0modprm0  16978  prmgaplem7  17228  cshwshashlem2  17267  cshwshashlem3  17268  cshwrepswhash1  17273  chnccat  18793  chnrev  18794  chnpof1  18797  psgnunilem5  19701  odf1o2  19780  odngen  19784  znf1o  21850  znunithash  21863  dvfsumle  26334  dvfsumabs  26336  dchrisumlem1  27809  dchrisumlem2  27810  dchrisum  27812  pntlemq  27921  pntlemr  27922  pntlemj  27923  pntlemi  27924  pntlemf  27925  wlk1walk  30212  revwlk  30260  pthdadjvtx  30306  crctcshwlkn0lem3  30394  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  crctcshwlkn0lem6  30397  crctcshlem2  30400  crctcshwlkn0  30403  crctcshtrl  30405  crctcsh  30406  clwwlkccatlem  30573  clwwisshclwwslem  30598  clwwisshclwws  30599  eucrctshift  30837  eucrct2eupth  30839  cshwrnid  33515  poimirlem8  38526  poimirlem18  38536  poimirlem21  38539  poimirlem22  38540  poimirlem24  38542  frlmvscadiccat  43553  iblspltprt  46952  itgspltprt  46958  stoweidlem3  46982  fourierdlem12  47098  fourierdlem20  47106  fourierdlem46  47131  fourierdlem50  47135  fourierdlem54  47139  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem76  47161  fourierdlem79  47164  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem114  47199  iundjiun  47439  carageniuncllem1  47500  caratheodorylem1  47505  ormklocald  47855  ormkglobd  47856  chnsubseq  47859  chnerlem3  47863  nnmul2  48369  zplusmodne  48388  p1modne  48392  m1modne  48393  minusmod5ne  48394  submodlt  48395  minusmodnep2tmod  48398  m1modmmod  48403  modmknepk  48407  mod2addne  48409  modm2nep1  48411  modm1nep2  48413  modm1nem2  48414  modm1p1ne  48415  muldvdsfacgt  48425  muldvdsfacm1  48426  iccpartipre  48472  iccpartiltu  48473  iccpartigtl  48474  iccpartgt  48478  icceuelpartlem  48486  icceuelpart  48487  iccpartnel  48489  fargshiftf1  48492  nprmmul2  48579  nprmmul3  48580  nprmdvdsfacm1lem1  48674  nprmdvdsfacm1lem3  48676  nprmdvdsfacm1lem4  48677  bgoldbtbndlem2  48873  upgrimpthslem2  48975  gpgiedgdmellem  49113  gpgvtx0  49120  gpgvtx1  49121  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgedg2iv  49134  gpg5nbgrvtx13starlem2  49139  gpg3nbgrvtx0  49143  gpg5nbgrvtx03star  49147  gpg5nbgr3star  49148  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  fllog2  49649  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  nn0mullong  49706