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	⊢ ( 𝜑 → ( 𝐹 ( ⇝_𝑢 ‘ 𝑆 ) 𝐺 ↔ ( 𝐹 ↾ 𝑊 ) ( ⇝_𝑢 ‘ 𝑆 ) 𝐺 ) )

Metamath Proof Explorer

Theorem ulmres

Proof