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 𝑀 ) ⇝ 𝐴 ) )