rlimrecl

Description: The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016)

	Ref	Expression
Hypotheses	rlimcld2.1	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
	rlimcld2.2	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} C$
	rlimrecl.3	$⊢ (φ \land x \in A) \to B \in ℝ$
Assertion	rlimrecl	$⊢ φ \to C \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		rlimcld2.1	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
2		rlimcld2.2	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} C$
3		rlimrecl.3	$⊢ (φ \land x \in A) \to B \in ℝ$
4		ax-resscn	$⊢ ℝ \subseteq ℂ$
5	4	a1i	$⊢ φ \to ℝ \subseteq ℂ$
6		eldifi	$⊢ y \in (ℂ ∖ ℝ) \to y \in ℂ$
7	6	adantl	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to y \in ℂ$
8	7	imcld	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to ℑ (y) \in ℝ$
9	8	recnd	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to ℑ (y) \in ℂ$
10		eldifn	$⊢ y \in (ℂ ∖ ℝ) \to \neg y \in ℝ$
11	10	adantl	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to \neg y \in ℝ$
12		reim0b	$⊢ y \in ℂ \to (y \in ℝ \leftrightarrow ℑ (y) = 0)$
13	7 12	syl	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to (y \in ℝ \leftrightarrow ℑ (y) = 0)$
14	13	necon3bbid	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to (\neg y \in ℝ \leftrightarrow ℑ (y) \neq 0)$
15	11 14	mpbid	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to ℑ (y) \neq 0$
16	9 15	absrpcld	$⊢ (φ \land y \in (ℂ ∖ ℝ)) \to \|ℑ (y)\| \in ℝ^{+}$
17	7	adantr	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to y \in ℂ$
18		simpr	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to z \in ℝ$
19	18	recnd	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to z \in ℂ$
20	17 19	subcld	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to y - z \in ℂ$
21		absimle	$⊢ y - z \in ℂ \to \|ℑ (y - z)\| \leq \|y - z\|$
22	20 21	syl	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to \|ℑ (y - z)\| \leq \|y - z\|$
23	17 19	imsubd	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to ℑ (y - z) = ℑ (y) - ℑ (z)$
24		reim0	$⊢ z \in ℝ \to ℑ (z) = 0$
25	24	adantl	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to ℑ (z) = 0$
26	25	oveq2d	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to ℑ (y) - ℑ (z) = ℑ (y) - 0$
27	9	adantr	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to ℑ (y) \in ℂ$
28	27	subid1d	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to ℑ (y) - 0 = ℑ (y)$
29	23 26 28	3eqtrrd	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to ℑ (y) = ℑ (y - z)$
30	29	fveq2d	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to \|ℑ (y)\| = \|ℑ (y - z)\|$
31	19 17	abssubd	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to \|z - y\| = \|y - z\|$
32	22 30 31	3brtr4d	$⊢ ((φ \land y \in (ℂ ∖ ℝ)) \land z \in ℝ) \to \|ℑ (y)\| \leq \|z - y\|$
33	1 2 5 16 32 3	rlimcld2	$⊢ φ \to C \in ℝ$

Metamath Proof Explorer

Theorem rlimrecl

Proof