Theorem elfzoelz 13596

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 13594	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13595	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13593	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7497	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4568	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3944	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4559  (class class class)co 7369  ℤcz 12505  ..^cfzo 13591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-neg 11384  df-z 12506  df-uz 12770  df-fz 13445  df-fzo 13592

This theorem is referenced by:  elfzo2  13599  elfzole1  13604  elfzolt2  13605  elfzolt3  13606  elfzolt2b  13607  elfzop1le2  13609  elfzouz2  13611  fzonnsub  13621  fzospliti  13628  fzodisj  13630  fzodisjsn  13634  elfzo0subge1  13642  elfzo0suble  13643  fzonmapblen  13645  fzoaddel  13654  elincfzoext  13660  fzosubel  13661  elfzom1elp1fzo1  13704  elfzo1elm1fzo0  13705  elfznelfzob  13710  modaddid  13848  modaddmodup  13875  modaddmodlo  13876  modfzo0difsn  13884  modsumfzodifsn  13885  addmodlteq  13887  ccatval3  14520  ccatlid  14527  ccatass  14529  ccatrn  14530  ccatalpha  14534  swrdfv0  14590  swrdfv2  14602  swrds1  14607  ccatswrd  14609  pfxfv  14623  ccatpfx  14642  swrdswrd  14646  pfxccatin12lem2a  14668  swrdccatin2  14670  pfxccatin12lem2  14672  revccat  14707  revrev  14708  repswrevw  14728  cshwidxmod  14744  cshwidxmodr  14745  cshwidx0  14747  cshwidxm1  14748  cshweqrep  14762  cshw1  14763  cshimadifsn  14771  cshimadifsn0  14772  cshco  14778  fzomaxdiflem  15285  fzomaxdif  15286  pwdif  15810  pwm1geoser  15811  fzo0dvdseq  16269  fzocongeq  16270  addmodlteqALT  16271  crth  16724  phimullem  16725  eulerthlem1  16727  eulerthlem2  16728  hashgcdlem  16734  hashgcdeq  16736  phisum  16737  reumodprminv  16751  modprm0  16752  nnnn0modprm0  16753  modprmn0modprm0  16754  prmgaplem7  17004  cshwshashlem2  17043  cshwshashlem3  17044  cshwrepswhash1  17049  psgnunilem5  19400  odf1o2  19479  odngen  19483  znf1o  21437  znunithash  21450  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dchrisumlem1  27376  dchrisumlem2  27377  dchrisum  27379  pntlemq  27488  pntlemr  27489  pntlemj  27490  pntlemi  27491  pntlemf  27492  wlk1walk  29542  pthdadjvtx  29631  crctcshwlkn0lem3  29715  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  crctcshwlkn0lem6  29718  crctcshlem2  29721  crctcshwlkn0  29724  crctcshtrl  29726  crctcsh  29727  clwwlkccatlem  29891  clwwisshclwwslem  29916  clwwisshclwws  29917  eucrctshift  30145  eucrct2eupth  30147  ccatf1  32843  cshwrnid  32856  revpfxsfxrev  35076  revwlk  35085  poimirlem8  37595  poimirlem18  37605  poimirlem21  37608  poimirlem22  37609  poimirlem24  37611  frlmvscadiccat  42467  iblspltprt  45944  itgspltprt  45950  stoweidlem3  45974  fourierdlem12  46090  fourierdlem20  46098  fourierdlem46  46123  fourierdlem50  46127  fourierdlem54  46131  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem76  46153  fourierdlem79  46156  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  iundjiun  46431  carageniuncllem1  46492  caratheodorylem1  46497  ormklocald  46845  ormkglobd  46846  natlocalincr  46847  natglobalincr  46848  zplusmodne  47317  p1modne  47321  m1modne  47322  minusmod5ne  47323  submodlt  47324  minusmodnep2tmod  47327  m1modmmod  47332  modmknepk  47336  mod2addne  47338  modm2nep1  47340  modm1nep2  47342  modm1nem2  47343  modm1p1ne  47344  iccpartipre  47395  iccpartiltu  47396  iccpartigtl  47397  iccpartgt  47401  icceuelpartlem  47409  icceuelpart  47410  iccpartnel  47412  fargshiftf1  47415  bgoldbtbndlem2  47780  upgrimpthslem2  47881  gpgiedgdmellem  48010  gpgvtx0  48017  gpgvtx1  48018  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgedg2iv  48031  gpg5nbgrvtx13starlem2  48036  gpg3nbgrvtx0  48040  gpg5nbgrvtx03star  48044  gpg5nbgr3star  48045  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  fllog2  48530  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0mullong  48587