clim2d

Description: The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	clim2d.k	⊢ Ⅎ 𝑘 𝜑
	clim2d.f	⊢ Ⅎ 𝑘 𝐹
	clim2d.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	clim2d.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	clim2d.c	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	clim2d.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
	clim2d.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
Assertion	clim2d	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		clim2d.k	⊢ Ⅎ 𝑘 𝜑
2		clim2d.f	⊢ Ⅎ 𝑘 𝐹
3		clim2d.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		clim2d.z	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
5		clim2d.c	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
6		clim2d.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
7		clim2d.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
8		climrel	⊢ Rel ⇝
9	8	a1i	⊢ ( 𝜑 → Rel ⇝ )
10		brrelex1	⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ∈ V )
11	9 5 10	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
12	1 2 4 3 11 6	clim2f2	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )
13	5 12	mpbid	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
14	13	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
15		breq2	⊢ ( 𝑥 = 𝑋 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )
16	15	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) )
17	16	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) )
18	17	rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) )
19	18	rspcva	⊢ ( ( 𝑋 ∈ ℝ⁺ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )
20	7 14 19	syl2anc	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )

Metamath Proof Explorer

Theorem clim2d

Proof