Theorem elfzoelz 13575

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 13573	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐵 ∈ ℤ)
2		elfzoel2 13574	. . . 4 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐶 ∈ ℤ)
3		fzof 13572	. . . . 5 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
4	3	fovcl 7486	. . . 4 ⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
5	1, 2, 4	syl2anc 584	. . 3 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ∈ 𝒫 ℤ)
6	5	elpwid 4563	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → (𝐵..^𝐶) ⊆ ℤ)
7		id 22	. 2 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ (𝐵..^𝐶))
8	6, 7	sseldd 3934	1 ⊢ (𝐴 ∈ (𝐵..^𝐶) → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4554  (class class class)co 7358  ℤcz 12488  ..^cfzo 13570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-neg 11367  df-z 12489  df-uz 12752  df-fz 13424  df-fzo 13571

This theorem is referenced by:  elfzo2  13578  elfzole1  13583  elfzolt2  13584  elfzolt3  13585  elfzolt2b  13586  elfzop1le2  13588  elfzouz2  13590  fzonnsub  13600  fzospliti  13607  fzodisj  13609  fzodisjsn  13613  elfzo0subge1  13621  elfzo0suble  13622  fzonmapblen  13624  fzoaddel  13633  elincfzoext  13639  fzosubel  13640  elfzom1elp1fzo1  13683  elfzo1elm1fzo0  13684  elfznelfzob  13690  modaddid  13830  modaddmodup  13857  modaddmodlo  13858  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  ccatval3  14502  ccatlid  14510  ccatass  14512  ccatrn  14513  ccatalpha  14517  swrdfv0  14573  swrdfv2  14585  swrds1  14590  ccatswrd  14592  pfxfv  14606  ccatpfx  14624  swrdswrd  14628  pfxccatin12lem2a  14650  swrdccatin2  14652  pfxccatin12lem2  14654  revccat  14689  revrev  14690  repswrevw  14710  cshwidxmod  14726  cshwidxmodr  14727  cshwidx0  14729  cshwidxm1  14730  cshweqrep  14744  cshw1  14745  cshimadifsn  14752  cshimadifsn0  14753  cshco  14759  fzomaxdiflem  15266  fzomaxdif  15267  pwdif  15791  pwm1geoser  15792  fzo0dvdseq  16250  fzocongeq  16251  addmodlteqALT  16252  crth  16705  phimullem  16706  eulerthlem1  16708  eulerthlem2  16709  hashgcdlem  16715  hashgcdeq  16717  phisum  16718  reumodprminv  16732  modprm0  16733  nnnn0modprm0  16734  modprmn0modprm0  16735  prmgaplem7  16985  cshwshashlem2  17024  cshwshashlem3  17025  cshwrepswhash1  17030  chnccat  18549  chnrev  18550  chnpof1  18553  psgnunilem5  19423  odf1o2  19502  odngen  19506  znf1o  21506  znunithash  21519  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dchrisumlem1  27456  dchrisumlem2  27457  dchrisum  27459  pntlemq  27568  pntlemr  27569  pntlemj  27570  pntlemi  27571  pntlemf  27572  wlk1walk  29712  pthdadjvtx  29801  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  crctcshlem2  29891  crctcshwlkn0  29894  crctcshtrl  29896  crctcsh  29897  clwwlkccatlem  30064  clwwisshclwwslem  30089  clwwisshclwws  30090  eucrctshift  30318  eucrct2eupth  30320  ccatf1  33031  cshwrnid  33043  revpfxsfxrev  35310  revwlk  35319  poimirlem8  37829  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem24  37845  frlmvscadiccat  42761  iblspltprt  46217  itgspltprt  46223  stoweidlem3  46247  fourierdlem12  46363  fourierdlem20  46371  fourierdlem46  46396  fourierdlem50  46400  fourierdlem54  46404  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem76  46426  fourierdlem79  46429  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  iundjiun  46704  carageniuncllem1  46765  caratheodorylem1  46770  ormklocald  47118  ormkglobd  47119  natlocalincr  47120  natglobalincr  47121  chnsubseq  47124  chnerlem3  47128  zplusmodne  47589  p1modne  47593  m1modne  47594  minusmod5ne  47595  submodlt  47596  minusmodnep2tmod  47599  m1modmmod  47604  modmknepk  47608  mod2addne  47610  modm2nep1  47612  modm1nep2  47614  modm1nem2  47615  modm1p1ne  47616  iccpartipre  47667  iccpartiltu  47668  iccpartigtl  47669  iccpartgt  47673  icceuelpartlem  47681  icceuelpart  47682  iccpartnel  47684  fargshiftf1  47687  bgoldbtbndlem2  48052  upgrimpthslem2  48154  gpgiedgdmellem  48292  gpgvtx0  48299  gpgvtx1  48300  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedg2iv  48313  gpg5nbgrvtx13starlem2  48318  gpg3nbgrvtx0  48322  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  fllog2  48814  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  nn0mullong  48871