Metamath Proof Explorer

Theorem climshft

Description: A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion climshft ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 shift 𝑀 ) = ( 𝐹 shift 𝑀 ) )
2 1 breq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 ↔ ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ) )
3 breq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
4 2 3 bibi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 ↔ 𝑓 ⇝ 𝐴 ) ↔ ( ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) ) )
5 4 imbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑀 ∈ ℤ → ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 ↔ 𝑓 ⇝ 𝐴 ) ) ↔ ( 𝑀 ∈ ℤ → ( ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) ) ) )
6 znegcl ⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
7 ovex ⊢ ( 𝑓 shift 𝑀 ) ∈ V
8 7 climshftlem ⊢ ( - 𝑀 ∈ ℤ → ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 → ( ( 𝑓 shift 𝑀 ) shift - 𝑀 ) ⇝ 𝐴 ) )
9 6 8 syl ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 → ( ( 𝑓 shift 𝑀 ) shift - 𝑀 ) ⇝ 𝐴 ) )
10 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
11 ovexd ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 shift 𝑀 ) shift - 𝑀 ) ∈ V )
12 vex ⊢ 𝑓 ∈ V
13 12 a1i ⊢ ( 𝑀 ∈ ℤ → 𝑓 ∈ V )
14 id ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℤ )
15 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
16 eluzelcn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℂ )
17 12 shftcan1 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑓 shift 𝑀 ) shift - 𝑀 ) ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
18 15 16 17 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝑓 shift 𝑀 ) shift - 𝑀 ) ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
19 10 11 13 14 18 climeq ⊢ ( 𝑀 ∈ ℤ → ( ( ( 𝑓 shift 𝑀 ) shift - 𝑀 ) ⇝ 𝐴 ↔ 𝑓 ⇝ 𝐴 ) )
20 9 19 sylibd ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 → 𝑓 ⇝ 𝐴 ) )
21 12 climshftlem ⊢ ( 𝑀 ∈ ℤ → ( 𝑓 ⇝ 𝐴 → ( 𝑓 shift 𝑀 ) ⇝ 𝐴 ) )
22 20 21 impbid ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑓 shift 𝑀 ) ⇝ 𝐴 ↔ 𝑓 ⇝ 𝐴 ) )
23 5 22 vtoclg ⊢ ( 𝐹 ∈ 𝑉 → ( 𝑀 ∈ ℤ → ( ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) ) )
24 23 impcom ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )