Theorem climf

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . Similar to clim , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	climf.nf	⊢ Ⅎ 𝑘 𝐹
	climf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climf.fv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
Assertion	climf	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		climf.nf	⊢ Ⅎ 𝑘 𝐹
2		climf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		climf.fv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
4		climrel	⊢ Rel ⇝
5	4	brrelex2i	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ V )
6	5	a1i	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ V ) )
7		elex	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ V )
8	7	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → 𝐴 ∈ V )
9	8	a1i	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → 𝐴 ∈ V ) )
10		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
11	10	eleq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( 𝑦 ∈ ℂ ↔ 𝐴 ∈ ℂ ) )
12		nfv	⊢ Ⅎ 𝑥 ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 )
13	1	nfeq2	⊢ Ⅎ 𝑘 𝑓 = 𝐹
14		nfv	⊢ Ⅎ 𝑘 𝑦 = 𝐴
15	13 14	nfan	⊢ Ⅎ 𝑘 ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 )
16		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
17	16	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
18	17	eleq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
19		oveq12	⊢ ( ( ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ∧ 𝑦 = 𝐴 ) → ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) = ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
20	16 19	sylan	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) = ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
21	20	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
22	21	breq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
23	18 22	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
24	15 23	ralbid	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
25	24	rexbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
26	12 25	ralbid	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
27	11 26	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑦 = 𝐴 ) → ( ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
28		df-clim	⊢ ⇝ = { ⟨ 𝑓 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑓 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑓 ‘ 𝑘 ) − 𝑦 ) ) < 𝑥 ) ) }
29	27 28	brabga	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
30	29	ex	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐴 ∈ V → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) ) )
31	2 30	syl	⊢ ( 𝜑 → ( 𝐴 ∈ V → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) ) )
32	6 9 31	pm5.21ndd	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
33		eluzelz	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑘 ∈ ℤ )
34	3	eleq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
35	3	fvoveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
36	35	breq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
37	34 36	anbi12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
38	33 37	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
39	38	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
40	39	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
41	40	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
42	41	anbi2d	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )
43	32 42	bitrd	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )