Theorem elfzoelz 13032

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

Syntax hints:   → wi 4   ∈ wcel 2110  𝒫 cpw 4539  (class class class)co 7150  ℤcz 11975  ..^cfzo 13027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-neg 10867  df-z 11976  df-uz 12238  df-fz 12887  df-fzo 13028

This theorem is referenced by:  elfzo2  13035  elfzole1  13040  elfzolt2  13041  elfzolt3  13042  elfzolt2b  13043  elfzouz2  13046  fzonnsub  13056  fzospliti  13063  fzodisj  13065  fzodisjsn  13069  fzonmapblen  13077  fzoaddel  13084  elincfzoext  13089  fzosubel  13090  elfzom1elp1fzo1  13131  elfzo1elm1fzo0  13132  elfznelfzob  13137  modaddmodup  13296  modaddmodlo  13297  modfzo0difsn  13305  modsumfzodifsn  13306  addmodlteq  13308  wrdexgOLD  13866  ccatval3  13927  ccatlid  13934  ccatass  13936  ccatrn  13937  ccatalpha  13941  swrdfv0  14005  swrdfv2  14017  swrds1  14022  ccatswrd  14024  pfxfv  14038  ccatpfx  14057  swrdswrd  14061  pfxccatin12lem2a  14083  swrdccatin2  14085  pfxccatin12lem2  14087  revccat  14122  revrev  14123  repswrevw  14143  cshwidxmod  14159  cshwidxmodr  14160  cshwidx0  14162  cshwidxm1  14163  cshweqrep  14177  cshw1  14178  cshimadifsn  14185  cshimadifsn0  14186  cshco  14192  fzomaxdiflem  14696  fzomaxdif  14697  pwdif  15217  pwm1geoser  15218  fzo0dvdseq  15667  fzocongeq  15668  addmodlteqALT  15669  crth  16109  phimullem  16110  eulerthlem1  16112  eulerthlem2  16113  hashgcdlem  16119  hashgcdeq  16120  phisum  16121  reumodprminv  16135  modprm0  16136  nnnn0modprm0  16137  modprmn0modprm0  16138  prmgaplem7  16387  cshwshashlem2  16424  cshwshashlem3  16425  cshwrepswhash1  16430  psgnunilem5  18616  odf1o2  18692  odngen  18696  znf1o  20692  zntoslem  20697  znunithash  20705  dvfsumle  24612  dvfsumabs  24614  dchrisumlem1  26059  dchrisumlem2  26060  dchrisum  26062  pntlemq  26171  pntlemr  26172  pntlemj  26173  pntlemi  26174  pntlemf  26175  wlk1walk  27414  pthdadjvtx  27505  crctcshwlkn0lem3  27584  crctcshwlkn0lem4  27585  crctcshwlkn0lem5  27586  crctcshwlkn0lem6  27587  crctcshlem2  27590  crctcshwlkn0  27593  crctcshtrl  27595  crctcsh  27596  clwwlkccatlem  27761  clwwisshclwwslem  27786  clwwisshclwws  27787  eucrctshift  28016  eucrct2eupth  28018  ccatf1  30620  cshwrnid  30630  revpfxsfxrev  32357  revwlk  32366  poimirlem8  34894  poimirlem18  34904  poimirlem21  34907  poimirlem22  34908  poimirlem24  34910  frlmvscadiccat  39138  elfzop1le2  41548  iblspltprt  42250  itgspltprt  42256  stoweidlem3  42281  fourierdlem12  42397  fourierdlem20  42405  fourierdlem46  42430  fourierdlem50  42434  fourierdlem54  42438  fourierdlem63  42447  fourierdlem64  42448  fourierdlem65  42449  fourierdlem76  42460  fourierdlem79  42463  fourierdlem102  42486  fourierdlem103  42487  fourierdlem104  42488  fourierdlem114  42498  iundjiun  42735  carageniuncllem1  42796  caratheodorylem1  42801  iccpartipre  43574  iccpartiltu  43575  iccpartigtl  43576  iccpartgt  43580  icceuelpartlem  43588  icceuelpart  43589  iccpartnel  43591  fargshiftf1  43594  bgoldbtbndlem2  43964  m1modmmod  44574  fllog2  44621  nn0sumshdiglemA  44672  nn0sumshdiglemB  44673  nn0mullong  44678