rlim3

Description: Restrict the range of the domain bound to reals greater than some D e. RR . (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlim2.1	$⊢ φ \to \forall z \in A B \in ℂ$
	rlim2.2	$⊢ φ \to A \subseteq ℝ$
	rlim2.3	$⊢ φ \to C \in ℂ$
	rlim3.4	$⊢ φ \to D \in ℝ$
Assertion	rlim3	$⊢ φ \to ((z \in A ⟼ B) \underset{ℝ}{⇝} C \leftrightarrow \forall x \in ℝ^{+} \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x))$

Proof

Step	Hyp	Ref	Expression
1		rlim2.1	$⊢ φ \to \forall z \in A B \in ℂ$
2		rlim2.2	$⊢ φ \to A \subseteq ℝ$
3		rlim2.3	$⊢ φ \to C \in ℂ$
4		rlim3.4	$⊢ φ \to D \in ℝ$
5	1 2 3	rlim2	$⊢ φ \to ((z \in A ⟼ B) \underset{ℝ}{⇝} C \leftrightarrow \forall x \in ℝ^{+} \exists w \in ℝ \forall z \in A (w \leq z \to \|B - C\| < x))$
6		simpr	$⊢ (φ \land w \in ℝ) \to w \in ℝ$
7	4	adantr	$⊢ (φ \land w \in ℝ) \to D \in ℝ$
8	6 7	ifcld	$⊢ (φ \land w \in ℝ) \to if (D \leq w, w, D) \in ℝ$
9		max1	$⊢ (D \in ℝ \land w \in ℝ) \to D \leq if (D \leq w, w, D)$
10	4 9	sylan	$⊢ (φ \land w \in ℝ) \to D \leq if (D \leq w, w, D)$
11		elicopnf	$⊢ D \in ℝ \to (if (D \leq w, w, D) \in [D, +∞) \leftrightarrow (if (D \leq w, w, D) \in ℝ \land D \leq if (D \leq w, w, D)))$
12	7 11	syl	$⊢ (φ \land w \in ℝ) \to (if (D \leq w, w, D) \in [D, +∞) \leftrightarrow (if (D \leq w, w, D) \in ℝ \land D \leq if (D \leq w, w, D)))$
13	8 10 12	mpbir2and	$⊢ (φ \land w \in ℝ) \to if (D \leq w, w, D) \in [D, +∞)$
14	2 4	jca	$⊢ φ \to (A \subseteq ℝ \land D \in ℝ)$
15		max2	$⊢ (D \in ℝ \land w \in ℝ) \to w \leq if (D \leq w, w, D)$
16	15	ad4ant23	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to w \leq if (D \leq w, w, D)$
17		simplr	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to w \in ℝ$
18		simpllr	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to D \in ℝ$
19	17 18	ifcld	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to if (D \leq w, w, D) \in ℝ$
20		simpll	$⊢ ((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \to A \subseteq ℝ$
21	20	sselda	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to z \in ℝ$
22		letr	$⊢ (w \in ℝ \land if (D \leq w, w, D) \in ℝ \land z \in ℝ) \to ((w \leq if (D \leq w, w, D) \land if (D \leq w, w, D) \leq z) \to w \leq z)$
23	17 19 21 22	syl3anc	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to ((w \leq if (D \leq w, w, D) \land if (D \leq w, w, D) \leq z) \to w \leq z)$
24	16 23	mpand	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to (if (D \leq w, w, D) \leq z \to w \leq z)$
25	24	imim1d	$⊢ (((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \land z \in A) \to ((w \leq z \to \|B - C\| < x) \to (if (D \leq w, w, D) \leq z \to \|B - C\| < x))$
26	25	ralimdva	$⊢ ((A \subseteq ℝ \land D \in ℝ) \land w \in ℝ) \to (\forall z \in A (w \leq z \to \|B - C\| < x) \to \forall z \in A (if (D \leq w, w, D) \leq z \to \|B - C\| < x))$
27	14 26	sylan	$⊢ (φ \land w \in ℝ) \to (\forall z \in A (w \leq z \to \|B - C\| < x) \to \forall z \in A (if (D \leq w, w, D) \leq z \to \|B - C\| < x))$
28		breq1	$⊢ y = if (D \leq w, w, D) \to (y \leq z \leftrightarrow if (D \leq w, w, D) \leq z)$
29	28	rspceaimv	$⊢ (if (D \leq w, w, D) \in [D, +∞) \land \forall z \in A (if (D \leq w, w, D) \leq z \to \|B - C\| < x)) \to \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x)$
30	13 27 29	syl6an	$⊢ (φ \land w \in ℝ) \to (\forall z \in A (w \leq z \to \|B - C\| < x) \to \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x))$
31	30	rexlimdva	$⊢ φ \to (\exists w \in ℝ \forall z \in A (w \leq z \to \|B - C\| < x) \to \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x))$
32	31	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists w \in ℝ \forall z \in A (w \leq z \to \|B - C\| < x) \to \forall x \in ℝ^{+} \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x))$
33	5 32	sylbid	$⊢ φ \to ((z \in A ⟼ B) \underset{ℝ}{⇝} C \to \forall x \in ℝ^{+} \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x))$
34		pnfxr	$⊢ +∞ \in ℝ^{*}$
35		icossre	$⊢ (D \in ℝ \land +∞ \in ℝ^{*}) \to [D, +∞) \subseteq ℝ$
36	4 34 35	sylancl	$⊢ φ \to [D, +∞) \subseteq ℝ$
37		ssrexv	$⊢ [D, +∞) \subseteq ℝ \to (\exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x) \to \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x))$
38	36 37	syl	$⊢ φ \to (\exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x) \to \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x))$
39	38	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x) \to \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x))$
40	1 2 3	rlim2	$⊢ φ \to ((z \in A ⟼ B) \underset{ℝ}{⇝} C \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ \forall z \in A (y \leq z \to \|B - C\| < x))$
41	39 40	sylibrd	$⊢ φ \to (\forall x \in ℝ^{+} \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x) \to (z \in A ⟼ B) \underset{ℝ}{⇝} C)$
42	33 41	impbid	$⊢ φ \to ((z \in A ⟼ B) \underset{ℝ}{⇝} C \leftrightarrow \forall x \in ℝ^{+} \exists y \in [D, +∞) \forall z \in A (y \leq z \to \|B - C\| < x))$

Metamath Proof Explorer

Theorem rlim3

Proof