This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climd

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypotheses	climd.1	⊢ Ⅎ 𝑘 𝜑
		climd.2	⊢ Ⅎ 𝑘 𝐹
		climd.3	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
		climd.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
		climd.5	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
		climd.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
		climd.7	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
	Assertion	climd	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		climd.1	⊢ Ⅎ 𝑘 𝜑
2		climd.2	⊢ Ⅎ 𝑘 𝐹
3		climd.3	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
4		climd.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climd.5	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
6		climd.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
7		climd.7	⊢ ( 𝜑 → 𝑋 ∈ ℝ⁺ )
8		climrel	⊢ Rel ⇝
9	8	brrelex1i	⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ∈ V )
10	5 9	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
11	1 2 3 4 10 6	clim2f2	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )
12	5 11	mpbid	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
13	12	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
14		breq2	⊢ ( 𝑥 = 𝑋 → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )
15	14	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) )
16	15	rexralbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) ) )
17	16	rspcva	⊢ ( ( 𝑋 ∈ ℝ⁺ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )
18	7 13 17	syl2anc	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑋 ) )