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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climshft2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climshft2.3	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	climshft2.5	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
	climshft2.6	⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
	climshft2.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) = ( 𝐹 ‘ 𝑘 ) )
Assertion	climshft2	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climshft2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climshft2.3	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
4		climshft2.5	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
5		climshft2.6	⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
6		climshft2.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) = ( 𝐹 ‘ 𝑘 ) )
7		ovexd	⊢ ( 𝜑 → ( 𝐺 shift - 𝐾 ) ∈ V )
8	3	zcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
9		eluzelz	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
10	9 1	eleq2s	⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
11	10	zcnd	⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℂ )
12		fvex	⊢ ( I ‘ 𝐺 ) ∈ V
13	12	shftval4	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( I ‘ 𝐺 ) shift - 𝐾 ) ‘ 𝑘 ) = ( ( I ‘ 𝐺 ) ‘ ( 𝐾 + 𝑘 ) ) )
14	8 11 13	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( I ‘ 𝐺 ) shift - 𝐾 ) ‘ 𝑘 ) = ( ( I ‘ 𝐺 ) ‘ ( 𝐾 + 𝑘 ) ) )
15		fvi	⊢ ( 𝐺 ∈ 𝑋 → ( I ‘ 𝐺 ) = 𝐺 )
16	5 15	syl	⊢ ( 𝜑 → ( I ‘ 𝐺 ) = 𝐺 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( I ‘ 𝐺 ) = 𝐺 )
18	17	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( I ‘ 𝐺 ) shift - 𝐾 ) = ( 𝐺 shift - 𝐾 ) )
19	18	fveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( I ‘ 𝐺 ) shift - 𝐾 ) ‘ 𝑘 ) = ( ( 𝐺 shift - 𝐾 ) ‘ 𝑘 ) )
20		addcom	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐾 + 𝑘 ) = ( 𝑘 + 𝐾 ) )
21	8 11 20	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐾 + 𝑘 ) = ( 𝑘 + 𝐾 ) )
22	17 21	fveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( I ‘ 𝐺 ) ‘ ( 𝐾 + 𝑘 ) ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) )
23	14 19 22	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 shift - 𝐾 ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑘 + 𝐾 ) ) )
24	23 6	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 shift - 𝐾 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
25	1 7 4 2 24	climeq	⊢ ( 𝜑 → ( ( 𝐺 shift - 𝐾 ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
26	3	znegcld	⊢ ( 𝜑 → - 𝐾 ∈ ℤ )
27		climshft	⊢ ( ( - 𝐾 ∈ ℤ ∧ 𝐺 ∈ 𝑋 ) → ( ( 𝐺 shift - 𝐾 ) ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )
28	26 5 27	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 shift - 𝐾 ) ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )
29	25 28	bitr3d	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )