Theorem elfzoelz 13833

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 13831	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13832	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13830	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7579	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 596	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4569	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 23	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3914	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  𝒫 cpw 4560  (class class class)co 7451  ℤcz 12733  ..^cfzo 13828

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-neg 11583  df-z 12734  df-uz 13006  df-fz 13680  df-fzo 13829

This theorem is used by:  elfzo2  13836  elfzole1  13842  elfzolt2  13843  elfzolt3  13844  elfzolt2b  13845  elfzop1le2  13847  elfzouz2  13849  fzonnsub  13859  fzospliti  13866  fzodisj  13868  fzodisjsn  13872  elfzo0subge1  13880  elfzo0suble  13881  fzonmapblen  13883  fzoaddel  13892  elincfzoext  13898  fzosubel  13899  elfzom1elp1fzo1  13942  elfzo1elm1fzo0  13943  elfznelfzob  13949  modaddid  14090  modaddmodup  14117  modaddmodlo  14118  modfzo0difsn  14126  modsumfzodifsn  14127  addmodlteq  14129  ccatval3  14765  ccatlid  14773  ccatass  14775  ccatrn  14776  ccatf1  14777  ccatalpha  14781  swrdfv0  14839  swrdfv2  14853  swrds1  14858  ccatswrd  14860  pfxfv  14874  ccatpfx  14892  swrdswrd  14896  pfxccatin12lem2a  14918  swrdccatin2  14920  pfxccatin12lem2  14922  revccat  14957  revrev  14958  revpfxsfxrev  14959  repswrevw  14980  cshwidxmod  14996  cshwidxmodr  14997  cshwidx0  14999  cshwidxm1  15000  cshweqrep  15014  cshw1  15015  cshimadifsn  15022  cshimadifsn0  15023  cshco  15029  fzomaxdiflem  15554  fzomaxdif  15555  pwdif  16081  pwm1geoser  16082  fzo0dvdseq  16537  fzocongeq  16538  addmodlteqALT  16539  crth  16999  phimullem  17000  eulerthlem1  17002  eulerthlem2  17003  hashgcdlem  17009  hashgcdeq  17011  phisum  17012  reumodprminv  17026  modprm0  17027  nnnn0modprm0  17028  modprmn0modprm0  17029  prmgaplem7  17279  cshwshashlem2  17318  cshwshashlem3  17319  cshwrepswhash1  17324  chnccat  18850  chnrev  18851  chnpof1  18854  psgnunilem5  19759  odf1o2  19838  odngen  19842  znf1o  21912  znunithash  21925  dvfsumle  26396  dvfsumabs  26398  dchrisumlem1  27873  dchrisumlem2  27874  dchrisum  27876  pntlemq  27985  pntlemr  27986  pntlemj  27987  pntlemi  27988  pntlemf  27989  wlk1walk  30276  revwlk  30324  pthdadjvtx  30370  crctcshwlkn0lem3  30458  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  crctcshwlkn0lem6  30461  crctcshlem2  30464  crctcshwlkn0  30467  crctcshtrl  30469  crctcsh  30470  clwwlkccatlem  30637  clwwisshclwwslem  30662  clwwisshclwws  30663  eucrctshift  30901  eucrct2eupth  30903  cshwrnid  33618  poimirlem8  38814  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem24  38830  frlmvscadiccat  43839  iblspltprt  47256  itgspltprt  47262  stoweidlem3  47286  fourierdlem12  47402  fourierdlem20  47410  fourierdlem46  47435  fourierdlem50  47439  fourierdlem54  47443  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem76  47465  fourierdlem79  47468  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  iundjiun  47743  carageniuncllem1  47804  caratheodorylem1  47809  ormklocald  48159  ormkglobd  48160  chnsubseq  48163  chnerlem3  48167  nnmul2  48673  zplusmodne  48692  p1modne  48696  m1modne  48697  minusmod5ne  48698  submodlt  48699  minusmodnep2tmod  48702  m1modmmod  48707  modmknepk  48711  mod2addne  48713  modm2nep1  48715  modm1nep2  48717  modm1nem2  48718  modm1p1ne  48719  muldvdsfacgt  48729  muldvdsfacm1  48730  iccpartipre  48776  iccpartiltu  48777  iccpartigtl  48778  iccpartgt  48782  icceuelpartlem  48790  icceuelpart  48791  iccpartnel  48793  fargshiftf1  48796  nprmmul2  48883  nprmmul3  48884  nprmdvdsfacm1lem1  48978  nprmdvdsfacm1lem3  48980  nprmdvdsfacm1lem4  48981  bgoldbtbndlem2  49177  upgrimpthslem2  49279  gpgiedgdmellem  49417  gpgvtx0  49424  gpgvtx1  49425  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgedg2iv  49438  gpg5nbgrvtx13starlem2  49443  gpg3nbgrvtx0  49447  gpg5nbgrvtx03star  49451  gpg5nbgr3star  49452  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  fllog2  50011  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0mullong  50068