Metamath Proof Explorer

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	$⊢ \underline{Ⅎ} k F$
		clim2cf.z	$⊢ Z = ℤ_{\geq M}$
		clim2cf.m	$⊢ φ \to M \in ℤ$
		clim2cf.f	$⊢ φ \to F \in V$
		clim2cf.fv	$⊢ (φ \land k \in Z) \to F (k) = B$
		clim2cf.a	$⊢ φ \to A \in ℂ$
		clim2cf.b	$⊢ (φ \land k \in Z) \to B \in ℂ$
	Assertion	clim2cf	$⊢ φ \to (F ⇝ A \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|B - A\| < x)$

Proof

Step	Hyp	Ref	Expression
1		clim2cf.nf	$⊢ \underline{Ⅎ} k F$
2		clim2cf.z	$⊢ Z = ℤ_{\geq M}$
3		clim2cf.m	$⊢ φ \to M \in ℤ$
4		clim2cf.f	$⊢ φ \to F \in V$
5		clim2cf.fv	$⊢ (φ \land k \in Z) \to F (k) = B$
6		clim2cf.a	$⊢ φ \to A \in ℂ$
7		clim2cf.b	$⊢ (φ \land k \in Z) \to B \in ℂ$
8	6	biantrurd	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$
9	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
10	7	biantrurd	$⊢ (φ \land k \in Z) \to (\|B - A\| < x \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
11	9 10	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (\|B - A\| < x \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
12	11	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (\|B - A\| < x \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
13	12	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \|B - A\| < x \leftrightarrow \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
14	13	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} \|B - A\| < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
15	14	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|B - A\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
16	1 2 3 4 5	clim2f	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$
17	8 15 16	3bitr4rd	$⊢ φ \to (F ⇝ A \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|B - A\| < x)$