Theorem elfzoelz 13704

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 13702	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13703	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13701	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7547	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 596	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4573	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 23	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3939	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  𝒫 cpw 4564  (class class class)co 7419  ℤcz 12606  ..^cfzo 13699

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-neg 11459  df-z 12607  df-uz 12879  df-fz 13552  df-fzo 13700

This theorem is used by:  elfzo2  13707  elfzole1  13713  elfzolt2  13714  elfzolt3  13715  elfzolt2b  13716  elfzop1le2  13718  elfzouz2  13720  fzonnsub  13730  fzospliti  13737  fzodisj  13739  fzodisjsn  13743  elfzo0subge1  13751  elfzo0suble  13752  fzonmapblen  13754  fzoaddel  13763  elincfzoext  13769  fzosubel  13770  elfzom1elp1fzo1  13813  elfzo1elm1fzo0  13814  elfznelfzob  13820  modaddid  13961  modaddmodup  13988  modaddmodlo  13989  modfzo0difsn  13997  modsumfzodifsn  13998  addmodlteq  14000  ccatval3  14634  ccatlid  14642  ccatass  14644  ccatrn  14645  ccatf1  14646  ccatalpha  14650  swrdfv0  14707  swrdfv2  14721  swrds1  14726  ccatswrd  14728  pfxfv  14742  ccatpfx  14760  swrdswrd  14764  pfxccatin12lem2a  14786  swrdccatin2  14788  pfxccatin12lem2  14790  revccat  14825  revrev  14826  revpfxsfxrev  14827  repswrevw  14848  cshwidxmod  14864  cshwidxmodr  14865  cshwidx0  14867  cshwidxm1  14868  cshweqrep  14882  cshw1  14883  cshimadifsn  14890  cshimadifsn0  14891  cshco  14897  fzomaxdiflem  15418  fzomaxdif  15419  pwdif  15945  pwm1geoser  15946  fzo0dvdseq  16403  fzocongeq  16404  addmodlteqALT  16405  crth  16859  phimullem  16860  eulerthlem1  16862  eulerthlem2  16863  hashgcdlem  16869  hashgcdeq  16871  phisum  16872  reumodprminv  16886  modprm0  16887  nnnn0modprm0  16888  modprmn0modprm0  16889  prmgaplem7  17139  cshwshashlem2  17178  cshwshashlem3  17179  cshwrepswhash1  17184  chnccat  18704  chnrev  18705  chnpof1  18708  psgnunilem5  19608  odf1o2  19687  odngen  19691  znf1o  21751  znunithash  21764  dvfsumle  26231  dvfsumabs  26233  dchrisumlem1  27704  dchrisumlem2  27705  dchrisum  27707  pntlemq  27816  pntlemr  27817  pntlemj  27818  pntlemi  27819  pntlemf  27820  wlk1walk  30046  revwlk  30094  pthdadjvtx  30140  crctcshwlkn0lem3  30228  crctcshwlkn0lem4  30229  crctcshwlkn0lem5  30230  crctcshwlkn0lem6  30231  crctcshlem2  30234  crctcshwlkn0  30237  crctcshtrl  30239  crctcsh  30240  clwwlkccatlem  30407  clwwisshclwwslem  30432  clwwisshclwws  30433  eucrctshift  30665  eucrct2eupth  30667  cshwrnid  33345  poimirlem8  38336  poimirlem18  38346  poimirlem21  38349  poimirlem22  38350  poimirlem24  38352  frlmvscadiccat  43338  iblspltprt  46745  itgspltprt  46751  stoweidlem3  46775  fourierdlem12  46891  fourierdlem20  46899  fourierdlem46  46924  fourierdlem50  46928  fourierdlem54  46932  fourierdlem63  46941  fourierdlem64  46942  fourierdlem65  46943  fourierdlem76  46954  fourierdlem79  46957  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem114  46992  iundjiun  47232  carageniuncllem1  47293  caratheodorylem1  47298  ormklocald  47648  ormkglobd  47649  natlocalincr  47650  natglobalincr  47651  chnsubseq  47654  chnerlem3  47658  nnmul2  48125  zplusmodne  48144  p1modne  48148  m1modne  48149  minusmod5ne  48150  submodlt  48151  minusmodnep2tmod  48154  m1modmmod  48159  modmknepk  48163  mod2addne  48165  modm2nep1  48167  modm1nep2  48169  modm1nem2  48170  modm1p1ne  48171  muldvdsfacgt  48181  muldvdsfacm1  48182  iccpartipre  48228  iccpartiltu  48229  iccpartigtl  48230  iccpartgt  48234  icceuelpartlem  48242  icceuelpart  48243  iccpartnel  48245  fargshiftf1  48248  nprmmul2  48335  nprmmul3  48336  nprmdvdsfacm1lem1  48430  nprmdvdsfacm1lem3  48432  nprmdvdsfacm1lem4  48433  bgoldbtbndlem2  48629  upgrimpthslem2  48731  gpgiedgdmellem  48869  gpgvtx0  48876  gpgvtx1  48877  gpgedgvtx0  48884  gpgedgvtx1  48885  gpgvtxedg0  48886  gpgvtxedg1  48887  gpgedg2iv  48890  gpg5nbgrvtx13starlem2  48895  gpg3nbgrvtx0  48899  gpg5nbgrvtx03star  48903  gpg5nbgr3star  48904  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  pgnbgreunbgrlem2lem3  48939  fllog2  49405  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457  nn0mullong  49462