Theorem clim2cf

Description: Express the predicate F converges to A . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		clim2cf.nf	⊢ Ⅎ 𝑘 𝐹
2		clim2cf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		clim2cf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		clim2cf.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5		clim2cf.fv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
6		clim2cf.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7		clim2cf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
8	6	biantrurd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )
9	2	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
10	7	biantrurd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
11	9 10	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
12	11	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
13	12	ralbidva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
14	13	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
15	14	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
16	1 2 3 4 5	clim2f	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) ) )
17	8 15 16	3bitr4rd	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )