Metamath Proof Explorer

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 = ℤ ≥ M
climshft2.2 ⊢ φ → M ∈ ℤ
climshft2.3 ⊢ φ → K ∈ ℤ
climshft2.5 ⊢ φ → F ∈ W
climshft2.6 ⊢ φ → G ∈ X
climshft2.7 ⊢ φ ∧ k ∈ Z → G ⁡ k + K = F ⁡ k
Assertion climshft2 ⊢ φ → F ⇝ A ↔ G ⇝ A

Proof

Step Hyp Ref Expression
1 climshft2.1 ⊢ Z = ℤ ≥ M
2 climshft2.2 ⊢ φ → M ∈ ℤ
3 climshft2.3 ⊢ φ → K ∈ ℤ
4 climshft2.5 ⊢ φ → F ∈ W
5 climshft2.6 ⊢ φ → G ∈ X
6 climshft2.7 ⊢ φ ∧ k ∈ Z → G ⁡ k + K = F ⁡ k
7 ovexd ⊢ φ → G shift − K ∈ V
8 3 zcnd ⊢ φ → K ∈ ℂ
9 eluzelz ⊢ k ∈ ℤ ≥ M → k ∈ ℤ
10 9 1 eleq2s ⊢ k ∈ Z → k ∈ ℤ
11 10 zcnd ⊢ k ∈ Z → k ∈ ℂ
12 fvex ⊢ I ⁡ G ∈ V
13 12 shftval4 ⊢ K ∈ ℂ ∧ k ∈ ℂ → I ⁡ G shift − K ⁡ k = I ⁡ G ⁡ K + k
14 8 11 13 syl2an ⊢ φ ∧ k ∈ Z → I ⁡ G shift − K ⁡ k = I ⁡ G ⁡ K + k
15 fvi ⊢ G ∈ X → I ⁡ G = G
16 5 15 syl ⊢ φ → I ⁡ G = G
17 16 adantr ⊢ φ ∧ k ∈ Z → I ⁡ G = G
18 17 oveq1d ⊢ φ ∧ k ∈ Z → I ⁡ G shift − K = G shift − K
19 18 fveq1d ⊢ φ ∧ k ∈ Z → I ⁡ G shift − K ⁡ k = G shift − K ⁡ k
20 addcom ⊢ K ∈ ℂ ∧ k ∈ ℂ → K + k = k + K
21 8 11 20 syl2an ⊢ φ ∧ k ∈ Z → K + k = k + K
22 17 21 fveq12d ⊢ φ ∧ k ∈ Z → I ⁡ G ⁡ K + k = G ⁡ k + K
23 14 19 22 3eqtr3d ⊢ φ ∧ k ∈ Z → G shift − K ⁡ k = G ⁡ k + K
24 23 6 eqtrd ⊢ φ ∧ k ∈ Z → G shift − K ⁡ k = F ⁡ k
25 1 7 4 2 24 climeq ⊢ φ → G shift − K ⇝ A ↔ F ⇝ A
26 3 znegcld ⊢ φ → − K ∈ ℤ
27 climshft ⊢ − K ∈ ℤ ∧ G ∈ X → G shift − K ⇝ A ↔ G ⇝ A
28 26 5 27 syl2anc ⊢ φ → G shift − K ⇝ A ↔ G ⇝ A
29 25 28 bitr3d ⊢ φ → F ⇝ A ↔ G ⇝ A