Theorem elfzoelz 13667

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 13665	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13666	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13664	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7549	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 582	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4613	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3977	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2098  𝒫 cpw 4604  (class class class)co 7419  ℤcz 12591  ..^cfzo 13662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-neg 11479  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663

This theorem is referenced by:  elfzo2  13670  elfzole1  13675  elfzolt2  13676  elfzolt3  13677  elfzolt2b  13678  elfzop1le2  13680  elfzouz2  13682  fzonnsub  13692  fzospliti  13699  fzodisj  13701  fzodisjsn  13705  fzonmapblen  13713  fzoaddel  13720  elincfzoext  13725  fzosubel  13726  elfzom1elp1fzo1  13768  elfzo1elm1fzo0  13769  elfznelfzob  13774  modaddmodup  13935  modaddmodlo  13936  modfzo0difsn  13944  modsumfzodifsn  13945  addmodlteq  13947  ccatval3  14565  ccatlid  14572  ccatass  14574  ccatrn  14575  ccatalpha  14579  swrdfv0  14635  swrdfv2  14647  swrds1  14652  ccatswrd  14654  pfxfv  14668  ccatpfx  14687  swrdswrd  14691  pfxccatin12lem2a  14713  swrdccatin2  14715  pfxccatin12lem2  14717  revccat  14752  revrev  14753  repswrevw  14773  cshwidxmod  14789  cshwidxmodr  14790  cshwidx0  14792  cshwidxm1  14793  cshweqrep  14807  cshw1  14808  cshimadifsn  14816  cshimadifsn0  14817  cshco  14823  fzomaxdiflem  15325  fzomaxdif  15326  pwdif  15850  pwm1geoser  15851  fzo0dvdseq  16303  fzocongeq  16304  addmodlteqALT  16305  crth  16750  phimullem  16751  eulerthlem1  16753  eulerthlem2  16754  hashgcdlem  16760  hashgcdeq  16761  phisum  16762  reumodprminv  16776  modprm0  16777  nnnn0modprm0  16778  modprmn0modprm0  16779  prmgaplem7  17029  cshwshashlem2  17069  cshwshashlem3  17070  cshwrepswhash1  17075  psgnunilem5  19461  odf1o2  19540  odngen  19544  znf1o  21502  znunithash  21515  dvfsumle  25998  dvfsumleOLD  25999  dvfsumabs  26001  dchrisumlem1  27467  dchrisumlem2  27468  dchrisum  27470  pntlemq  27579  pntlemr  27580  pntlemj  27581  pntlemi  27582  pntlemf  27583  wlk1walk  29525  pthdadjvtx  29616  crctcshwlkn0lem3  29695  crctcshwlkn0lem4  29696  crctcshwlkn0lem5  29697  crctcshwlkn0lem6  29698  crctcshlem2  29701  crctcshwlkn0  29704  crctcshtrl  29706  crctcsh  29707  clwwlkccatlem  29871  clwwisshclwwslem  29896  clwwisshclwws  29897  eucrctshift  30125  eucrct2eupth  30127  ccatf1  32759  cshwrnid  32771  revpfxsfxrev  34856  revwlk  34865  poimirlem8  37232  poimirlem18  37242  poimirlem21  37245  poimirlem22  37246  poimirlem24  37248  frlmvscadiccat  41884  iblspltprt  45499  itgspltprt  45505  stoweidlem3  45529  fourierdlem12  45645  fourierdlem20  45653  fourierdlem46  45678  fourierdlem50  45682  fourierdlem54  45686  fourierdlem63  45695  fourierdlem64  45696  fourierdlem65  45697  fourierdlem76  45708  fourierdlem79  45711  fourierdlem102  45734  fourierdlem103  45735  fourierdlem104  45736  fourierdlem114  45746  iundjiun  45986  carageniuncllem1  46047  caratheodorylem1  46052  natlocalincr  46400  natglobalincr  46401  iccpartipre  46898  iccpartiltu  46899  iccpartigtl  46900  iccpartgt  46904  icceuelpartlem  46912  icceuelpart  46913  iccpartnel  46915  fargshiftf1  46918  bgoldbtbndlem2  47283  m1modmmod  47780  fllog2  47827  nn0sumshdiglemA  47878  nn0sumshdiglemB  47879  nn0mullong  47884