rlimresb

Description: The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlimresb.1	$⊢ φ \to F : A ⟶ ℂ$
	rlimresb.2	$⊢ φ \to A \subseteq ℝ$
	rlimresb.3	$⊢ φ \to B \in ℝ$
Assertion	rlimresb	$⊢ φ \to (F \underset{ℝ}{⇝} C \leftrightarrow ({F ↾}_{[B, +∞)}) \underset{ℝ}{⇝} C)$

Proof

Step	Hyp	Ref	Expression
1		rlimresb.1	$⊢ φ \to F : A ⟶ ℂ$
2		rlimresb.2	$⊢ φ \to A \subseteq ℝ$
3		rlimresb.3	$⊢ φ \to B \in ℝ$
4		rlimcl	$⊢ (x \in A ⟼ F (x)) \underset{ℝ}{⇝} C \to C \in ℂ$
5	4	a1i	$⊢ φ \to ((x \in A ⟼ F (x)) \underset{ℝ}{⇝} C \to C \in ℂ)$
6		rlimcl	$⊢ (x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C \to C \in ℂ$
7	6	a1i	$⊢ φ \to ((x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C \to C \in ℂ)$
8	2	adantr	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to A \subseteq ℝ$
9		simprrl	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to x \in A$
10	8 9	sseldd	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to x \in ℝ$
11	3	adantr	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to B \in ℝ$
12		elicopnf	$⊢ B \in ℝ \to (z \in [B, +∞) \leftrightarrow (z \in ℝ \land B \leq z))$
13	3 12	syl	$⊢ φ \to (z \in [B, +∞) \leftrightarrow (z \in ℝ \land B \leq z))$
14	13	biimpa	$⊢ (φ \land z \in [B, +∞)) \to (z \in ℝ \land B \leq z)$
15	14	adantrr	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to (z \in ℝ \land B \leq z)$
16	15	simpld	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to z \in ℝ$
17	15	simprd	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to B \leq z$
18		simprrr	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to z \leq x$
19	11 16 10 17 18	letrd	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to B \leq x$
20		elicopnf	$⊢ B \in ℝ \to (x \in [B, +∞) \leftrightarrow (x \in ℝ \land B \leq x))$
21	11 20	syl	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to (x \in [B, +∞) \leftrightarrow (x \in ℝ \land B \leq x))$
22	10 19 21	mpbir2and	$⊢ (φ \land (z \in [B, +∞) \land (x \in A \land z \leq x))) \to x \in [B, +∞)$
23	22	anassrs	$⊢ ((φ \land z \in [B, +∞)) \land (x \in A \land z \leq x)) \to x \in [B, +∞)$
24	23	anassrs	$⊢ (((φ \land z \in [B, +∞)) \land x \in A) \land z \leq x) \to x \in [B, +∞)$
25		biimt	$⊢ x \in [B, +∞) \to (\|F (x) - C\| < y \leftrightarrow (x \in [B, +∞) \to \|F (x) - C\| < y))$
26	24 25	syl	$⊢ (((φ \land z \in [B, +∞)) \land x \in A) \land z \leq x) \to (\|F (x) - C\| < y \leftrightarrow (x \in [B, +∞) \to \|F (x) - C\| < y))$
27	26	pm5.74da	$⊢ ((φ \land z \in [B, +∞)) \land x \in A) \to ((z \leq x \to \|F (x) - C\| < y) \leftrightarrow (z \leq x \to (x \in [B, +∞) \to \|F (x) - C\| < y)))$
28		bi2.04	$⊢ (z \leq x \to (x \in [B, +∞) \to \|F (x) - C\| < y)) \leftrightarrow (x \in [B, +∞) \to (z \leq x \to \|F (x) - C\| < y))$
29	27 28	bitrdi	$⊢ ((φ \land z \in [B, +∞)) \land x \in A) \to ((z \leq x \to \|F (x) - C\| < y) \leftrightarrow (x \in [B, +∞) \to (z \leq x \to \|F (x) - C\| < y)))$
30	29	pm5.74da	$⊢ (φ \land z \in [B, +∞)) \to ((x \in A \to (z \leq x \to \|F (x) - C\| < y)) \leftrightarrow (x \in A \to (x \in [B, +∞) \to (z \leq x \to \|F (x) - C\| < y))))$
31		elin	$⊢ x \in (A \cap [B, +∞)) \leftrightarrow (x \in A \land x \in [B, +∞))$
32	31	imbi1i	$⊢ (x \in (A \cap [B, +∞)) \to (z \leq x \to \|F (x) - C\| < y)) \leftrightarrow ((x \in A \land x \in [B, +∞)) \to (z \leq x \to \|F (x) - C\| < y))$
33		impexp	$⊢ ((x \in A \land x \in [B, +∞)) \to (z \leq x \to \|F (x) - C\| < y)) \leftrightarrow (x \in A \to (x \in [B, +∞) \to (z \leq x \to \|F (x) - C\| < y)))$
34	32 33	bitri	$⊢ (x \in (A \cap [B, +∞)) \to (z \leq x \to \|F (x) - C\| < y)) \leftrightarrow (x \in A \to (x \in [B, +∞) \to (z \leq x \to \|F (x) - C\| < y)))$
35	30 34	bitr4di	$⊢ (φ \land z \in [B, +∞)) \to ((x \in A \to (z \leq x \to \|F (x) - C\| < y)) \leftrightarrow (x \in (A \cap [B, +∞)) \to (z \leq x \to \|F (x) - C\| < y)))$
36	35	ralbidv2	$⊢ (φ \land z \in [B, +∞)) \to (\forall x \in A (z \leq x \to \|F (x) - C\| < y) \leftrightarrow \forall x \in (A \cap [B, +∞)) (z \leq x \to \|F (x) - C\| < y))$
37	36	rexbidva	$⊢ φ \to (\exists z \in [B, +∞) \forall x \in A (z \leq x \to \|F (x) - C\| < y) \leftrightarrow \exists z \in [B, +∞) \forall x \in (A \cap [B, +∞)) (z \leq x \to \|F (x) - C\| < y))$
38	37	ralbidv	$⊢ φ \to (\forall y \in ℝ^{+} \exists z \in [B, +∞) \forall x \in A (z \leq x \to \|F (x) - C\| < y) \leftrightarrow \forall y \in ℝ^{+} \exists z \in [B, +∞) \forall x \in (A \cap [B, +∞)) (z \leq x \to \|F (x) - C\| < y))$
39	38	adantr	$⊢ (φ \land C \in ℂ) \to (\forall y \in ℝ^{+} \exists z \in [B, +∞) \forall x \in A (z \leq x \to \|F (x) - C\| < y) \leftrightarrow \forall y \in ℝ^{+} \exists z \in [B, +∞) \forall x \in (A \cap [B, +∞)) (z \leq x \to \|F (x) - C\| < y))$
40	1	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in ℂ$
41	40	ralrimiva	$⊢ φ \to \forall x \in A F (x) \in ℂ$
42	41	adantr	$⊢ (φ \land C \in ℂ) \to \forall x \in A F (x) \in ℂ$
43	2	adantr	$⊢ (φ \land C \in ℂ) \to A \subseteq ℝ$
44		simpr	$⊢ (φ \land C \in ℂ) \to C \in ℂ$
45	3	adantr	$⊢ (φ \land C \in ℂ) \to B \in ℝ$
46	42 43 44 45	rlim3	$⊢ (φ \land C \in ℂ) \to ((x \in A ⟼ F (x)) \underset{ℝ}{⇝} C \leftrightarrow \forall y \in ℝ^{+} \exists z \in [B, +∞) \forall x \in A (z \leq x \to \|F (x) - C\| < y))$
47		elinel1	$⊢ x \in (A \cap [B, +∞)) \to x \in A$
48	47 40	sylan2	$⊢ (φ \land x \in (A \cap [B, +∞))) \to F (x) \in ℂ$
49	48	ralrimiva	$⊢ φ \to \forall x \in (A \cap [B, +∞)) F (x) \in ℂ$
50	49	adantr	$⊢ (φ \land C \in ℂ) \to \forall x \in (A \cap [B, +∞)) F (x) \in ℂ$
51		inss1	$⊢ A \cap [B, +∞) \subseteq A$
52	51 2	sstrid	$⊢ φ \to A \cap [B, +∞) \subseteq ℝ$
53	52	adantr	$⊢ (φ \land C \in ℂ) \to A \cap [B, +∞) \subseteq ℝ$
54	50 53 44 45	rlim3	$⊢ (φ \land C \in ℂ) \to ((x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C \leftrightarrow \forall y \in ℝ^{+} \exists z \in [B, +∞) \forall x \in (A \cap [B, +∞)) (z \leq x \to \|F (x) - C\| < y))$
55	39 46 54	3bitr4d	$⊢ (φ \land C \in ℂ) \to ((x \in A ⟼ F (x)) \underset{ℝ}{⇝} C \leftrightarrow (x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C)$
56	55	ex	$⊢ φ \to (C \in ℂ \to ((x \in A ⟼ F (x)) \underset{ℝ}{⇝} C \leftrightarrow (x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C))$
57	5 7 56	pm5.21ndd	$⊢ φ \to ((x \in A ⟼ F (x)) \underset{ℝ}{⇝} C \leftrightarrow (x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C)$
58	1	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
59	58	breq1d	$⊢ φ \to (F \underset{ℝ}{⇝} C \leftrightarrow (x \in A ⟼ F (x)) \underset{ℝ}{⇝} C)$
60		resres	$⊢ {({F ↾}_{A}) ↾}_{[B, +∞)} = {F ↾}_{(A \cap [B, +∞))}$
61		ffn	$⊢ F : A ⟶ ℂ \to F Fn A$
62		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
63	1 61 62	3syl	$⊢ φ \to {F ↾}_{A} = F$
64	63	reseq1d	$⊢ φ \to {({F ↾}_{A}) ↾}_{[B, +∞)} = {F ↾}_{[B, +∞)}$
65	58	reseq1d	$⊢ φ \to {F ↾}_{(A \cap [B, +∞))} = {(x \in A ⟼ F (x)) ↾}_{(A \cap [B, +∞))}$
66		resmpt	$⊢ A \cap [B, +∞) \subseteq A \to {(x \in A ⟼ F (x)) ↾}_{(A \cap [B, +∞))} = (x \in (A \cap [B, +∞)) ⟼ F (x))$
67	51 66	ax-mp	$⊢ {(x \in A ⟼ F (x)) ↾}_{(A \cap [B, +∞))} = (x \in (A \cap [B, +∞)) ⟼ F (x))$
68	65 67	eqtrdi	$⊢ φ \to {F ↾}_{(A \cap [B, +∞))} = (x \in (A \cap [B, +∞)) ⟼ F (x))$
69	60 64 68	3eqtr3a	$⊢ φ \to {F ↾}_{[B, +∞)} = (x \in (A \cap [B, +∞)) ⟼ F (x))$
70	69	breq1d	$⊢ φ \to (({F ↾}_{[B, +∞)}) \underset{ℝ}{⇝} C \leftrightarrow (x \in (A \cap [B, +∞)) ⟼ F (x)) \underset{ℝ}{⇝} C)$
71	57 59 70	3bitr4d	$⊢ φ \to (F \underset{ℝ}{⇝} C \leftrightarrow ({F ↾}_{[B, +∞)}) \underset{ℝ}{⇝} C)$

Metamath Proof Explorer

Theorem rlimresb

Proof