rlimo1

Description: Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014)

		Ref	Expression
	Assertion	rlimo1	$⊢ F \underset{ℝ}{⇝} A \to F \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rlimf	$⊢ F \underset{ℝ}{⇝} A \to F : dom F ⟶ ℂ$
2	1	ffvelcdmda	$⊢ (F \underset{ℝ}{⇝} A \land z \in dom F) \to F (z) \in ℂ$
3	2	ralrimiva	$⊢ F \underset{ℝ}{⇝} A \to \forall z \in dom F F (z) \in ℂ$
4		1rp	$⊢ 1 \in ℝ^{+}$
5	4	a1i	$⊢ F \underset{ℝ}{⇝} A \to 1 \in ℝ^{+}$
6	1	feqmptd	$⊢ F \underset{ℝ}{⇝} A \to F = (z \in dom F ⟼ F (z))$
7		id	$⊢ F \underset{ℝ}{⇝} A \to F \underset{ℝ}{⇝} A$
8	6 7	eqbrtrrd	$⊢ F \underset{ℝ}{⇝} A \to (z \in dom F ⟼ F (z)) \underset{ℝ}{⇝} A$
9	3 5 8	rlimi	$⊢ F \underset{ℝ}{⇝} A \to \exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < 1)$
10		rlimcl	$⊢ F \underset{ℝ}{⇝} A \to A \in ℂ$
11	10	adantr	$⊢ (F \underset{ℝ}{⇝} A \land y \in ℝ) \to A \in ℂ$
12	11	abscld	$⊢ (F \underset{ℝ}{⇝} A \land y \in ℝ) \to \|A\| \in ℝ$
13		peano2re	$⊢ \|A\| \in ℝ \to \|A\| + 1 \in ℝ$
14	12 13	syl	$⊢ (F \underset{ℝ}{⇝} A \land y \in ℝ) \to \|A\| + 1 \in ℝ$
15	2	adantlr	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to F (z) \in ℂ$
16	11	adantr	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to A \in ℂ$
17	15 16	abs2difd	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to \|F (z)\| - \|A\| \leq \|F (z) - A\|$
18	15	abscld	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to \|F (z)\| \in ℝ$
19	12	adantr	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to \|A\| \in ℝ$
20	18 19	resubcld	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to \|F (z)\| - \|A\| \in ℝ$
21	15 16	subcld	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to F (z) - A \in ℂ$
22	21	abscld	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to \|F (z) - A\| \in ℝ$
23		1red	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to 1 \in ℝ$
24		lelttr	$⊢ (\|F (z)\| - \|A\| \in ℝ \land \|F (z) - A\| \in ℝ \land 1 \in ℝ) \to ((\|F (z)\| - \|A\| \leq \|F (z) - A\| \land \|F (z) - A\| < 1) \to \|F (z)\| - \|A\| < 1)$
25	20 22 23 24	syl3anc	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to ((\|F (z)\| - \|A\| \leq \|F (z) - A\| \land \|F (z) - A\| < 1) \to \|F (z)\| - \|A\| < 1)$
26	17 25	mpand	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to (\|F (z) - A\| < 1 \to \|F (z)\| - \|A\| < 1)$
27	18 19 23	ltsubadd2d	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to (\|F (z)\| - \|A\| < 1 \leftrightarrow \|F (z)\| < \|A\| + 1)$
28	26 27	sylibd	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to (\|F (z) - A\| < 1 \to \|F (z)\| < \|A\| + 1)$
29	14	adantr	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to \|A\| + 1 \in ℝ$
30		ltle	$⊢ (\|F (z)\| \in ℝ \land \|A\| + 1 \in ℝ) \to (\|F (z)\| < \|A\| + 1 \to \|F (z)\| \leq \|A\| + 1)$
31	18 29 30	syl2anc	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to (\|F (z)\| < \|A\| + 1 \to \|F (z)\| \leq \|A\| + 1)$
32	28 31	syld	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to (\|F (z) - A\| < 1 \to \|F (z)\| \leq \|A\| + 1)$
33	32	imim2d	$⊢ ((F \underset{ℝ}{⇝} A \land y \in ℝ) \land z \in dom F) \to ((y \leq z \to \|F (z) - A\| < 1) \to (y \leq z \to \|F (z)\| \leq \|A\| + 1))$
34	33	ralimdva	$⊢ (F \underset{ℝ}{⇝} A \land y \in ℝ) \to (\forall z \in dom F (y \leq z \to \|F (z) - A\| < 1) \to \forall z \in dom F (y \leq z \to \|F (z)\| \leq \|A\| + 1))$
35		breq2	$⊢ w = \|A\| + 1 \to (\|F (z)\| \leq w \leftrightarrow \|F (z)\| \leq \|A\| + 1)$
36	35	imbi2d	$⊢ w = \|A\| + 1 \to ((y \leq z \to \|F (z)\| \leq w) \leftrightarrow (y \leq z \to \|F (z)\| \leq \|A\| + 1))$
37	36	ralbidv	$⊢ w = \|A\| + 1 \to (\forall z \in dom F (y \leq z \to \|F (z)\| \leq w) \leftrightarrow \forall z \in dom F (y \leq z \to \|F (z)\| \leq \|A\| + 1))$
38	37	rspcev	$⊢ (\|A\| + 1 \in ℝ \land \forall z \in dom F (y \leq z \to \|F (z)\| \leq \|A\| + 1)) \to \exists w \in ℝ \forall z \in dom F (y \leq z \to \|F (z)\| \leq w)$
39	14 34 38	syl6an	$⊢ (F \underset{ℝ}{⇝} A \land y \in ℝ) \to (\forall z \in dom F (y \leq z \to \|F (z) - A\| < 1) \to \exists w \in ℝ \forall z \in dom F (y \leq z \to \|F (z)\| \leq w))$
40	39	reximdva	$⊢ F \underset{ℝ}{⇝} A \to (\exists y \in ℝ \forall z \in dom F (y \leq z \to \|F (z) - A\| < 1) \to \exists y \in ℝ \exists w \in ℝ \forall z \in dom F (y \leq z \to \|F (z)\| \leq w))$
41	9 40	mpd	$⊢ F \underset{ℝ}{⇝} A \to \exists y \in ℝ \exists w \in ℝ \forall z \in dom F (y \leq z \to \|F (z)\| \leq w)$
42		rlimss	$⊢ F \underset{ℝ}{⇝} A \to dom F \subseteq ℝ$
43		elo12	$⊢ (F : dom F ⟶ ℂ \land dom F \subseteq ℝ) \to (F \in 𝑂 (1) \leftrightarrow \exists y \in ℝ \exists w \in ℝ \forall z \in dom F (y \leq z \to \|F (z)\| \leq w))$
44	1 42 43	syl2anc	$⊢ F \underset{ℝ}{⇝} A \to (F \in 𝑂 (1) \leftrightarrow \exists y \in ℝ \exists w \in ℝ \forall z \in dom F (y \leq z \to \|F (z)\| \leq w))$
45	41 44	mpbird	$⊢ F \underset{ℝ}{⇝} A \to F \in 𝑂 (1)$

Metamath Proof Explorer

Theorem rlimo1

Proof