lmclim

Description: Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmclim.2	$⊢ J = TopOpen (ℂ_{fld})$
	lmclim.3	$⊢ Z = ℤ_{\geq M}$
Assertion	lmclim	$⊢ (M \in ℤ \land Z \subseteq dom F) \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land F ⇝ P))$

Proof

Step	Hyp	Ref	Expression
1		lmclim.2	$⊢ J = TopOpen (ℂ_{fld})$
2		lmclim.3	$⊢ Z = ℤ_{\geq M}$
3		3anass	$⊢ (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x)) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x)))$
4	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
5		3anass	$⊢ (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (k \in dom F \land (F (k) \in ℂ \land F (k) (abs \circ -) P < x))$
6		simplr	$⊢ ((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \to Z \subseteq dom F$
7	6	sselda	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land k \in Z) \to k \in dom F$
8	7	biantrurd	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land k \in Z) \to ((F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (k \in dom F \land (F (k) \in ℂ \land F (k) (abs \circ -) P < x)))$
9		eqid	$⊢ abs \circ - = abs \circ -$
10	9	cnmetdval	$⊢ (F (k) \in ℂ \land P \in ℂ) \to F (k) (abs \circ -) P = \|F (k) - P\|$
11	10	ancoms	$⊢ (P \in ℂ \land F (k) \in ℂ) \to F (k) (abs \circ -) P = \|F (k) - P\|$
12	11	breq1d	$⊢ (P \in ℂ \land F (k) \in ℂ) \to (F (k) (abs \circ -) P < x \leftrightarrow \|F (k) - P\| < x)$
13	12	pm5.32da	$⊢ P \in ℂ \to ((F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - P\| < x))$
14	13	ad2antlr	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land k \in Z) \to ((F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - P\| < x))$
15	8 14	bitr3d	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land k \in Z) \to ((k \in dom F \land (F (k) \in ℂ \land F (k) (abs \circ -) P < x)) \leftrightarrow (F (k) \in ℂ \land \|F (k) - P\| < x))$
16	5 15	syl5bb	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land k \in Z) \to ((k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - P\| < x))$
17	4 16	sylan2	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land (j \in Z \land k \in ℤ_{\geq j})) \to ((k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - P\| < x))$
18	17	anassrs	$⊢ ((((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - P\| < x))$
19	18	ralbidva	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x))$
20	19	rexbidva	$⊢ ((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x))$
21	20	ralbidv	$⊢ ((M \in ℤ \land Z \subseteq dom F) \land P \in ℂ) \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x))$
22	21	pm5.32da	$⊢ (M \in ℤ \land Z \subseteq dom F) \to ((P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x)) \leftrightarrow (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x)))$
23	22	anbi2d	$⊢ (M \in ℤ \land Z \subseteq dom F) \to ((F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x))) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x))))$
24	3 23	syl5bb	$⊢ (M \in ℤ \land Z \subseteq dom F) \to ((F \in (ℂ ↑_{𝑝𝑚} ℂ) \land P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x)) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x))))$
25	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
26		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
27	26	a1i	$⊢ (M \in ℤ \land Z \subseteq dom F) \to abs \circ - \in ∞Met (ℂ)$
28		simpl	$⊢ (M \in ℤ \land Z \subseteq dom F) \to M \in ℤ$
29	25 27 2 28	lmmbr3	$⊢ (M \in ℤ \land Z \subseteq dom F) \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in ℂ \land F (k) (abs \circ -) P < x)))$
30		simpll	$⊢ ((M \in ℤ \land Z \subseteq dom F) \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to M \in ℤ$
31		simpr	$⊢ ((M \in ℤ \land Z \subseteq dom F) \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
32		eqidd	$⊢ (((M \in ℤ \land Z \subseteq dom F) \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \land k \in Z) \to F (k) = F (k)$
33	2 30 31 32	clim2	$⊢ ((M \in ℤ \land Z \subseteq dom F) \land F \in (ℂ ↑_{𝑝𝑚} ℂ)) \to (F ⇝ P \leftrightarrow (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x)))$
34	33	pm5.32da	$⊢ (M \in ℤ \land Z \subseteq dom F) \to ((F \in (ℂ ↑_{𝑝𝑚} ℂ) \land F ⇝ P) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land (P \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - P\| < x))))$
35	24 29 34	3bitr4d	$⊢ (M \in ℤ \land Z \subseteq dom F) \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℂ) \land F ⇝ P))$

Metamath Proof Explorer

Theorem lmclim

Proof