Metamath Proof Explorer


Theorem climshftlem

Description: A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013)

Ref Expression
Hypothesis climshft.1 𝐹 ∈ V
Assertion climshftlem ( 𝑀 ∈ ℤ → ( 𝐹𝐴 → ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climshft.1 𝐹 ∈ V
2 zaddcl ( ( 𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑘 + 𝑀 ) ∈ ℤ )
3 2 ancoms ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 + 𝑀 ) ∈ ℤ )
4 eluzsub ( ( 𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( 𝑛𝑀 ) ∈ ( ℤ𝑘 ) )
5 4 3com12 ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( 𝑛𝑀 ) ∈ ( ℤ𝑘 ) )
6 5 3expa ( ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( 𝑛𝑀 ) ∈ ( ℤ𝑘 ) )
7 fveq2 ( 𝑚 = ( 𝑛𝑀 ) → ( 𝐹𝑚 ) = ( 𝐹 ‘ ( 𝑛𝑀 ) ) )
8 7 eleq1d ( 𝑚 = ( 𝑛𝑀 ) → ( ( 𝐹𝑚 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ) )
9 7 fvoveq1d ( 𝑚 = ( 𝑛𝑀 ) → ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) )
10 9 breq1d ( 𝑚 = ( 𝑛𝑀 ) → ( ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) )
11 8 10 anbi12d ( 𝑚 = ( 𝑛𝑀 ) → ( ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) ) )
12 11 rspcv ( ( 𝑛𝑀 ) ∈ ( ℤ𝑘 ) → ( ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) ) )
13 6 12 syl ( ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) ) )
14 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
15 eluzelcn ( 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) → 𝑛 ∈ ℂ )
16 1 shftval ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑛𝑀 ) ) )
17 16 eleq1d ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ) )
18 16 fvoveq1d ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) )
19 18 breq1d ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) )
20 17 19 anbi12d ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) ) )
21 14 15 20 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) ) )
22 21 adantlr ( ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ ( 𝑛𝑀 ) ) − 𝐴 ) ) < 𝑥 ) ) )
23 13 22 sylibrd ( ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) )
24 23 ralrimdva ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) )
25 fveq2 ( 𝑚 = ( 𝑘 + 𝑀 ) → ( ℤ𝑚 ) = ( ℤ ‘ ( 𝑘 + 𝑀 ) ) )
26 25 raleqdv ( 𝑚 = ( 𝑘 + 𝑀 ) → ( ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) )
27 26 rspcev ( ( ( 𝑘 + 𝑀 ) ∈ ℤ ∧ ∀ 𝑛 ∈ ( ℤ ‘ ( 𝑘 + 𝑀 ) ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) )
28 3 24 27 syl6an ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) )
29 28 rexlimdva ( 𝑀 ∈ ℤ → ( ∃ 𝑘 ∈ ℤ ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑚 ∈ ℤ ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) )
30 29 ralimdv ( 𝑀 ∈ ℤ → ( ∀ 𝑥 ∈ ℝ+𝑘 ∈ ℤ ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑚 ∈ ℤ ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) )
31 30 anim2d ( 𝑀 ∈ ℤ → ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑘 ∈ ℤ ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) ) → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ℤ ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) ) )
32 1 a1i ( 𝑀 ∈ ℤ → 𝐹 ∈ V )
33 eqidd ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝐹𝑚 ) = ( 𝐹𝑚 ) )
34 32 33 clim ( 𝑀 ∈ ℤ → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑘 ∈ ℤ ∀ 𝑚 ∈ ( ℤ𝑘 ) ( ( 𝐹𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑚 ) − 𝐴 ) ) < 𝑥 ) ) ) )
35 ovexd ( 𝑀 ∈ ℤ → ( 𝐹 shift 𝑀 ) ∈ V )
36 eqidd ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) = ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) )
37 35 36 clim ( 𝑀 ∈ ℤ → ( ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ℤ ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝐹 shift 𝑀 ) ‘ 𝑛 ) − 𝐴 ) ) < 𝑥 ) ) ) )
38 31 34 37 3imtr4d ( 𝑀 ∈ ℤ → ( 𝐹𝐴 → ( 𝐹 shift 𝑀 ) ⇝ 𝐴 ) )