Metamath Proof Explorer


Theorem ulmres

Description: A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmres.z 𝑍 = ( ℤ𝑀 )
ulmres.w 𝑊 = ( ℤ𝑁 )
ulmres.m ( 𝜑𝑁𝑍 )
ulmres.f ( 𝜑𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
Assertion ulmres ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ulmres.z 𝑍 = ( ℤ𝑀 )
2 ulmres.w 𝑊 = ( ℤ𝑁 )
3 ulmres.m ( 𝜑𝑁𝑍 )
4 ulmres.f ( 𝜑𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
5 ulmscl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝑆 ∈ V )
6 ulmcl ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )
7 5 6 jca ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) )
8 7 a1i ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) )
9 ulmscl ( ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺𝑆 ∈ V )
10 ulmcl ( ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )
11 9 10 jca ( ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) )
12 11 a1i ( 𝜑 → ( ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) )
13 3 1 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
14 13 adantr ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝑁 ∈ ( ℤ𝑀 ) )
15 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
16 14 15 syl ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝑀 ∈ ℤ )
17 1 rexuz3 ( 𝑀 ∈ ℤ → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
18 16 17 syl ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
19 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
20 14 19 syl ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝑁 ∈ ℤ )
21 2 rexuz3 ( 𝑁 ∈ ℤ → ( ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
22 20 21 syl ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
23 18 22 bitr4d ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∃ 𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
24 23 ralbidv ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( ∀ 𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∀ 𝑟 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
25 4 adantr ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
26 eqidd ( ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) ∧ ( 𝑘𝑍𝑧𝑆 ) ) → ( ( 𝐹𝑘 ) ‘ 𝑧 ) = ( ( 𝐹𝑘 ) ‘ 𝑧 ) )
27 eqidd ( ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) ∧ 𝑧𝑆 ) → ( 𝐺𝑧 ) = ( 𝐺𝑧 ) )
28 simprr ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝐺 : 𝑆 ⟶ ℂ )
29 simprl ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝑆 ∈ V )
30 1 16 25 26 27 28 29 ulm2 ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∀ 𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
31 uzss ( 𝑁 ∈ ( ℤ𝑀 ) → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )
32 14 31 syl ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )
33 32 2 1 3sstr4g ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → 𝑊𝑍 )
34 25 33 fssresd ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( 𝐹𝑊 ) : 𝑊 ⟶ ( ℂ ↑m 𝑆 ) )
35 fvres ( 𝑘𝑊 → ( ( 𝐹𝑊 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
36 35 ad2antrl ( ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) ∧ ( 𝑘𝑊𝑧𝑆 ) ) → ( ( 𝐹𝑊 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
37 36 fveq1d ( ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) ∧ ( 𝑘𝑊𝑧𝑆 ) ) → ( ( ( 𝐹𝑊 ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹𝑘 ) ‘ 𝑧 ) )
38 2 20 34 37 27 28 29 ulm2 ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 ↔ ∀ 𝑟 ∈ ℝ+𝑗𝑊𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
39 24 30 38 3bitr4d ( ( 𝜑 ∧ ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) ) → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 ) )
40 39 ex ( 𝜑 → ( ( 𝑆 ∈ V ∧ 𝐺 : 𝑆 ⟶ ℂ ) → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 ) ) )
41 8 12 40 pm5.21ndd ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ( 𝐹𝑊 ) ( ⇝𝑢𝑆 ) 𝐺 ) )