This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
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 ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )