rlim

Description: Express the predicate: The limit of complex number function F is C , or F converges to C , in the real sense. This means that for any real x , no matter how small, there always exists a number y such that the absolute difference of any number in the function beyond y and the limit is less than x . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Hypotheses	rlim.1	$⊢ φ \to F : A ⟶ ℂ$
	rlim.2	$⊢ φ \to A \subseteq ℝ$
	rlim.4	$⊢ (φ \land z \in A) \to F (z) = B$
Assertion	rlim	$⊢ φ \to (F \underset{ℝ}{⇝} C \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x)))$

Proof

Step	Hyp	Ref	Expression
1		rlim.1	$⊢ φ \to F : A ⟶ ℂ$
2		rlim.2	$⊢ φ \to A \subseteq ℝ$
3		rlim.4	$⊢ (φ \land z \in A) \to F (z) = B$
4		rlimrel	$⊢ Rel \underset{ℝ}{⇝}$
5	4	brrelex2i	$⊢ F \underset{ℝ}{⇝} C \to C \in V$
6	5	a1i	$⊢ φ \to (F \underset{ℝ}{⇝} C \to C \in V)$
7		elex	$⊢ C \in ℂ \to C \in V$
8	7	ad2antrl	$⊢ (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))) \to C \in V$
9	8	a1i	$⊢ φ \to ((F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))) \to C \in V)$
10		cnex	$⊢ ℂ \in V$
11		reex	$⊢ ℝ \in V$
12		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
13	10 11 12	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
14	1 2 13	syl2anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
15		eleq1	$⊢ f = F \to (f \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow F \in (ℂ ↑_{𝑝𝑚} ℝ))$
16		eleq1	$⊢ w = C \to (w \in ℂ \leftrightarrow C \in ℂ)$
17	15 16	bi2anan9	$⊢ (f = F \land w = C) \to ((f \in (ℂ ↑_{𝑝𝑚} ℝ) \land w \in ℂ) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land C \in ℂ))$
18		simpl	$⊢ (f = F \land w = C) \to f = F$
19	18	dmeqd	$⊢ (f = F \land w = C) \to dom f = dom F$
20		fveq1	$⊢ f = F \to f (z) = F (z)$
21		oveq12	$⊢ (f (z) = F (z) \land w = C) \to f (z) - w = F (z) - C$
22	20 21	sylan	$⊢ (f = F \land w = C) \to f (z) - w = F (z) - C$
23	22	fveq2d	$⊢ (f = F \land w = C) \to \|f (z) - w\| = \|F (z) - C\|$
24	23	breq1d	$⊢ (f = F \land w = C) \to (\|f (z) - w\| < x \leftrightarrow \|F (z) - C\| < x)$
25	24	imbi2d	$⊢ (f = F \land w = C) \to ((y \leq z \to \|f (z) - w\| < x) \leftrightarrow (y \leq z \to \|F (z) - C\| < x))$
26	19 25	raleqbidv	$⊢ (f = F \land w = C) \to (\forall z \in dom f (y \leq z \to \|f (z) - w\| < x) \leftrightarrow \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))$
27	26	rexbidv	$⊢ (f = F \land w = C) \to (\exists y \in ℝ \forall z \in dom f (y \leq z \to \|f (z) - w\| < x) \leftrightarrow \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))$
28	27	ralbidv	$⊢ (f = F \land w = C) \to (\forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom f (y \leq z \to \|f (z) - w\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))$
29	17 28	anbi12d	$⊢ (f = F \land w = C) \to (((f \in (ℂ ↑_{𝑝𝑚} ℝ) \land w \in ℂ) \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom f (y \leq z \to \|f (z) - w\| < x)) \leftrightarrow ((F \in (ℂ ↑_{𝑝𝑚} ℝ) \land C \in ℂ) \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)))$
30		df-rlim	$⊢ \underset{ℝ}{⇝} = \{⟨f, w⟩ \| ((f \in (ℂ ↑_{𝑝𝑚} ℝ) \land w \in ℂ) \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom f (y \leq z \to \|f (z) - w\| < x))\}$
31	29 30	brabga	$⊢ (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land C \in V) \to (F \underset{ℝ}{⇝} C \leftrightarrow ((F \in (ℂ ↑_{𝑝𝑚} ℝ) \land C \in ℂ) \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)))$
32		anass	$⊢ ((F \in (ℂ ↑_{𝑝𝑚} ℝ) \land C \in ℂ) \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)))$
33	31 32	bitrdi	$⊢ (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land C \in V) \to (F \underset{ℝ}{⇝} C \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))))$
34	33	ex	$⊢ F \in (ℂ ↑_{𝑝𝑚} ℝ) \to (C \in V \to (F \underset{ℝ}{⇝} C \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)))))$
35	14 34	syl	$⊢ φ \to (C \in V \to (F \underset{ℝ}{⇝} C \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)))))$
36	6 9 35	pm5.21ndd	$⊢ φ \to (F \underset{ℝ}{⇝} C \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))))$
37	14	biantrurd	$⊢ φ \to ((C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x))))$
38	1	fdmd	$⊢ φ \to dom F = A$
39	38	raleqdv	$⊢ φ \to (\forall z \in dom F (y \leq z \to \|F (z) - C\| < x) \leftrightarrow \forall z \in A (y \leq z \to \|F (z) - C\| < x))$
40	3	fvoveq1d	$⊢ (φ \land z \in A) \to \|F (z) - C\| = \|B - C\|$
41	40	breq1d	$⊢ (φ \land z \in A) \to (\|F (z) - C\| < x \leftrightarrow \|B - C\| < x)$
42	41	imbi2d	$⊢ (φ \land z \in A) \to ((y \leq z \to \|F (z) - C\| < x) \leftrightarrow (y \leq z \to \|B - C\| < x))$
43	42	ralbidva	$⊢ φ \to (\forall z \in A (y \leq z \to \|F (z) - C\| < x) \leftrightarrow \forall z \in A (y \leq z \to \|B - C\| < x))$
44	39 43	bitrd	$⊢ φ \to (\forall z \in dom F (y \leq z \to \|F (z) - C\| < x) \leftrightarrow \forall z \in A (y \leq z \to \|B - C\| < x))$
45	44	rexbidv	$⊢ φ \to (\exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x) \leftrightarrow \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x))$
46	45	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x))$
47	46	anbi2d	$⊢ φ \to ((C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - C\| < x)) \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x)))$
48	36 37 47	3bitr2d	$⊢ φ \to (F \underset{ℝ}{⇝} C \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x)))$

Metamath Proof Explorer

Theorem rlim

Proof