Theorem elfzoelz 13714

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 13712	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13713	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13711	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7541	. . . 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 7413  ℤcz 12615  ..^cfzo 13709

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7986  df-2nd 7987  df-neg 11468  df-z 12616  df-uz 12888  df-fz 13562  df-fzo 13710

This theorem is used by:  elfzo2  13717  elfzole1  13723  elfzolt2  13724  elfzolt3  13725  elfzolt2b  13726  elfzop1le2  13728  elfzouz2  13730  fzonnsub  13740  fzospliti  13747  fzodisj  13749  fzodisjsn  13753  elfzo0subge1  13761  elfzo0suble  13762  fzonmapblen  13764  fzoaddel  13773  elincfzoext  13779  fzosubel  13780  elfzom1elp1fzo1  13823  elfzo1elm1fzo0  13824  elfznelfzob  13830  modaddid  13971  modaddmodup  13998  modaddmodlo  13999  modfzo0difsn  14007  modsumfzodifsn  14008  addmodlteq  14010  ccatval3  14644  ccatlid  14652  ccatass  14654  ccatrn  14655  ccatf1  14656  ccatalpha  14660  swrdfv0  14717  swrdfv2  14731  swrds1  14736  ccatswrd  14738  pfxfv  14752  ccatpfx  14770  swrdswrd  14774  pfxccatin12lem2a  14796  swrdccatin2  14798  pfxccatin12lem2  14800  revccat  14835  revrev  14836  revpfxsfxrev  14837  repswrevw  14858  cshwidxmod  14874  cshwidxmodr  14875  cshwidx0  14877  cshwidxm1  14878  cshweqrep  14892  cshw1  14893  cshimadifsn  14900  cshimadifsn0  14901  cshco  14907  fzomaxdiflem  15430  fzomaxdif  15431  pwdif  15957  pwm1geoser  15958  fzo0dvdseq  16413  fzocongeq  16414  addmodlteqALT  16415  crth  16869  phimullem  16870  eulerthlem1  16872  eulerthlem2  16873  hashgcdlem  16879  hashgcdeq  16881  phisum  16882  reumodprminv  16896  modprm0  16897  nnnn0modprm0  16898  modprmn0modprm0  16899  prmgaplem7  17149  cshwshashlem2  17188  cshwshashlem3  17189  cshwrepswhash1  17194  chnccat  18714  chnrev  18715  chnpof1  18718  psgnunilem5  19621  odf1o2  19700  odngen  19704  znf1o  21764  znunithash  21777  dvfsumle  26248  dvfsumabs  26250  dchrisumlem1  27725  dchrisumlem2  27726  dchrisum  27728  pntlemq  27837  pntlemr  27838  pntlemj  27839  pntlemi  27840  pntlemf  27841  wlk1walk  30098  revwlk  30146  pthdadjvtx  30192  crctcshwlkn0lem3  30280  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  crctcshwlkn0lem6  30283  crctcshlem2  30286  crctcshwlkn0  30289  crctcshtrl  30291  crctcsh  30292  clwwlkccatlem  30459  clwwisshclwwslem  30484  clwwisshclwws  30485  eucrctshift  30723  eucrct2eupth  30725  cshwrnid  33401  poimirlem8  38377  poimirlem18  38387  poimirlem21  38390  poimirlem22  38391  poimirlem24  38393  frlmvscadiccat  43394  iblspltprt  46801  itgspltprt  46807  stoweidlem3  46831  fourierdlem12  46947  fourierdlem20  46955  fourierdlem46  46980  fourierdlem50  46984  fourierdlem54  46988  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem76  47010  fourierdlem79  47013  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem114  47048  iundjiun  47288  carageniuncllem1  47349  caratheodorylem1  47354  ormklocald  47704  ormkglobd  47705  chnsubseq  47708  chnerlem3  47712  nnmul2  48218  zplusmodne  48237  p1modne  48241  m1modne  48242  minusmod5ne  48243  submodlt  48244  minusmodnep2tmod  48247  m1modmmod  48252  modmknepk  48256  mod2addne  48258  modm2nep1  48260  modm1nep2  48262  modm1nem2  48263  modm1p1ne  48264  muldvdsfacgt  48274  muldvdsfacm1  48275  iccpartipre  48321  iccpartiltu  48322  iccpartigtl  48323  iccpartgt  48327  icceuelpartlem  48335  icceuelpart  48336  iccpartnel  48338  fargshiftf1  48341  nprmmul2  48428  nprmmul3  48429  nprmdvdsfacm1lem1  48523  nprmdvdsfacm1lem3  48525  nprmdvdsfacm1lem4  48526  bgoldbtbndlem2  48722  upgrimpthslem2  48824  gpgiedgdmellem  48962  gpgvtx0  48969  gpgvtx1  48970  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedg2iv  48983  gpg5nbgrvtx13starlem2  48988  gpg3nbgrvtx0  48992  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  fllog2  49498  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  nn0mullong  49555