climf2

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 ph k and F k . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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

Metamath Proof Explorer

Theorem climf2

Proof