Theorem climshft2

Description: A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007) (Revised by Mario Carneiro, 6-Feb-2014)

	Ref	Expression
Hypotheses	climshft2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climshft2.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climshft2.3	$$⊢\phi \to K\in \mathbb{Z}$$
	climshft2.5	$$⊢\phi \to F\in W$$
	climshft2.6	$$⊢\phi \to G\in X$$
	climshft2.7	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k+K\right)=F\left(k\right)$$
Assertion	climshft2	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climshft2.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climshft2.3	$$⊢\phi \to K\in \mathbb{Z}$$
4		climshft2.5	$$⊢\phi \to F\in W$$
5		climshft2.6	$$⊢\phi \to G\in X$$
6		climshft2.7	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k+K\right)=F\left(k\right)$$
7		ovexd	$$⊢\phi \to G\mathrm{shift}\left(-K\right)\in \mathrm{V}$$
8	3	zcnd	$$⊢\phi \to K\in ℂ$$
9		eluzelz	$$⊢k\in {\mathbb{Z}}_{\ge M}\to k\in \mathbb{Z}$$
10	9 1	eleq2s	$$⊢k\in Z\to k\in \mathbb{Z}$$
11	10	zcnd	$$⊢k\in Z\to k\in ℂ$$
12		fvex	$$⊢\mathrm{I}\left(G\right)\in \mathrm{V}$$
13	12	shftval4	$$⊢\left(K\in ℂ\wedge k\in ℂ\right)\to \left(\mathrm{I}\left(G\right)\mathrm{shift}\left(-K\right)\right)\left(k\right)=\mathrm{I}\left(G\right)\left(K+k\right)$$
14	8 11 13	syl2an	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\mathrm{I}\left(G\right)\mathrm{shift}\left(-K\right)\right)\left(k\right)=\mathrm{I}\left(G\right)\left(K+k\right)$$
15		fvi	$$⊢G\in X\to \mathrm{I}\left(G\right)=G$$
16	5 15	syl	$$⊢\phi \to \mathrm{I}\left(G\right)=G$$
17	16	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{I}\left(G\right)=G$$
18	17	oveq1d	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{I}\left(G\right)\mathrm{shift}\left(-K\right)=G\mathrm{shift}\left(-K\right)$$
19	18	fveq1d	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\mathrm{I}\left(G\right)\mathrm{shift}\left(-K\right)\right)\left(k\right)=\left(G\mathrm{shift}\left(-K\right)\right)\left(k\right)$$
20		addcom	$$⊢\left(K\in ℂ\wedge k\in ℂ\right)\to K+k=k+K$$
21	8 11 20	syl2an	$$⊢\left(\phi \wedge k\in Z\right)\to K+k=k+K$$
22	17 21	fveq12d	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{I}\left(G\right)\left(K+k\right)=G\left(k+K\right)$$
23	14 19 22	3eqtr3d	$$⊢\left(\phi \wedge k\in Z\right)\to \left(G\mathrm{shift}\left(-K\right)\right)\left(k\right)=G\left(k+K\right)$$
24	23 6	eqtrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(G\mathrm{shift}\left(-K\right)\right)\left(k\right)=F\left(k\right)$$
25	1 7 4 2 24	climeq	$$⊢\phi \to \left(\left(G\mathrm{shift}\left(-K\right)\right)⇝A\leftrightarrow F⇝A\right)$$
26	3	znegcld	$$⊢\phi \to -K\in \mathbb{Z}$$
27		climshft	$$⊢\left(-K\in \mathbb{Z}\wedge G\in X\right)\to \left(\left(G\mathrm{shift}\left(-K\right)\right)⇝A\leftrightarrow G⇝A\right)$$
28	26 5 27	syl2anc	$$⊢\phi \to \left(\left(G\mathrm{shift}\left(-K\right)\right)⇝A\leftrightarrow G⇝A\right)$$
29	25 28	bitr3d	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$