Theorem elfzoelz 13800

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 13798	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13799	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13797	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7552	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 596	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4565	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 23	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3910	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  𝒫 cpw 4556  (class class class)co 7424  ℤcz 12700  ..^cfzo 13795

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8005  df-2nd 8006  df-neg 11551  df-z 12701  df-uz 12973  df-fz 13647  df-fzo 13796

This theorem is used by:  elfzo2  13803  elfzole1  13809  elfzolt2  13810  elfzolt3  13811  elfzolt2b  13812  elfzop1le2  13814  elfzouz2  13816  fzonnsub  13826  fzospliti  13833  fzodisj  13835  fzodisjsn  13839  elfzo0subge1  13847  elfzo0suble  13848  fzonmapblen  13850  fzoaddel  13859  elincfzoext  13865  fzosubel  13866  elfzom1elp1fzo1  13909  elfzo1elm1fzo0  13910  elfznelfzob  13916  modaddid  14057  modaddmodup  14084  modaddmodlo  14085  modfzo0difsn  14093  modsumfzodifsn  14094  addmodlteq  14096  ccatval3  14731  ccatlid  14739  ccatass  14741  ccatrn  14742  ccatf1  14743  ccatalpha  14747  swrdfv0  14805  swrdfv2  14819  swrds1  14824  ccatswrd  14826  pfxfv  14840  ccatpfx  14858  swrdswrd  14862  pfxccatin12lem2a  14884  swrdccatin2  14886  pfxccatin12lem2  14888  revccat  14923  revrev  14924  revpfxsfxrev  14925  repswrevw  14946  cshwidxmod  14962  cshwidxmodr  14963  cshwidx0  14965  cshwidxm1  14966  cshweqrep  14980  cshw1  14981  cshimadifsn  14988  cshimadifsn0  14989  cshco  14995  fzomaxdiflem  15519  fzomaxdif  15520  pwdif  16046  pwm1geoser  16047  fzo0dvdseq  16502  fzocongeq  16503  addmodlteqALT  16504  crth  16964  phimullem  16965  eulerthlem1  16967  eulerthlem2  16968  hashgcdlem  16974  hashgcdeq  16976  phisum  16977  reumodprminv  16991  modprm0  16992  nnnn0modprm0  16993  modprmn0modprm0  16994  prmgaplem7  17244  cshwshashlem2  17283  cshwshashlem3  17284  cshwrepswhash1  17289  chnccat  18809  chnrev  18810  chnpof1  18813  psgnunilem5  19717  odf1o2  19796  odngen  19800  znf1o  21866  znunithash  21879  dvfsumle  26350  dvfsumabs  26352  dchrisumlem1  27825  dchrisumlem2  27826  dchrisum  27828  pntlemq  27937  pntlemr  27938  pntlemj  27939  pntlemi  27940  pntlemf  27941  wlk1walk  30228  revwlk  30276  pthdadjvtx  30322  crctcshwlkn0lem3  30410  crctcshwlkn0lem4  30411  crctcshwlkn0lem5  30412  crctcshwlkn0lem6  30413  crctcshlem2  30416  crctcshwlkn0  30419  crctcshtrl  30421  crctcsh  30422  clwwlkccatlem  30589  clwwisshclwwslem  30614  clwwisshclwws  30615  eucrctshift  30853  eucrct2eupth  30855  cshwrnid  33572  poimirlem8  38655  poimirlem18  38665  poimirlem21  38668  poimirlem22  38669  poimirlem24  38671  frlmvscadiccat  43682  iblspltprt  47091  itgspltprt  47097  stoweidlem3  47121  fourierdlem12  47237  fourierdlem20  47245  fourierdlem46  47270  fourierdlem50  47274  fourierdlem54  47278  fourierdlem63  47287  fourierdlem64  47288  fourierdlem65  47289  fourierdlem76  47300  fourierdlem79  47303  fourierdlem102  47326  fourierdlem103  47327  fourierdlem104  47328  fourierdlem114  47338  iundjiun  47578  carageniuncllem1  47639  caratheodorylem1  47644  ormklocald  47994  ormkglobd  47995  chnsubseq  47998  chnerlem3  48002  nnmul2  48508  zplusmodne  48527  p1modne  48531  m1modne  48532  minusmod5ne  48533  submodlt  48534  minusmodnep2tmod  48537  m1modmmod  48542  modmknepk  48546  mod2addne  48548  modm2nep1  48550  modm1nep2  48552  modm1nem2  48553  modm1p1ne  48554  muldvdsfacgt  48564  muldvdsfacm1  48565  iccpartipre  48611  iccpartiltu  48612  iccpartigtl  48613  iccpartgt  48617  icceuelpartlem  48625  icceuelpart  48626  iccpartnel  48628  fargshiftf1  48631  nprmmul2  48718  nprmmul3  48719  nprmdvdsfacm1lem1  48813  nprmdvdsfacm1lem3  48815  nprmdvdsfacm1lem4  48816  bgoldbtbndlem2  49012  upgrimpthslem2  49114  gpgiedgdmellem  49252  gpgvtx0  49259  gpgvtx1  49260  gpgedgvtx0  49267  gpgedgvtx1  49268  gpgvtxedg0  49269  gpgvtxedg1  49270  gpgedg2iv  49273  gpg5nbgrvtx13starlem2  49278  gpg3nbgrvtx0  49282  gpg5nbgrvtx03star  49286  gpg5nbgr3star  49287  pgnbgreunbgrlem2lem1  49320  pgnbgreunbgrlem2lem2  49321  pgnbgreunbgrlem2lem3  49322  fllog2  49788  nn0sumshdiglemA  49839  nn0sumshdiglemB  49840  nn0mullong  49845