clim

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . This means that for any real x , no matter how small, there always exists an integer j such that the absolute difference of any later complex number in the sequence and the limit is less than x . (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

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

Metamath Proof Explorer

Theorem clim

Proof