rlimsqzlem

	Ref	Expression
Hypotheses	rlimsqzlem.m	$⊢ φ \to M \in ℝ$
	rlimsqzlem.e	$⊢ φ \to E \in ℂ$
	rlimsqzlem.1	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} D$
	rlimsqzlem.2	$⊢ (φ \land x \in A) \to B \in ℂ$
	rlimsqzlem.3	$⊢ (φ \land x \in A) \to C \in ℂ$
	rlimsqzlem.4	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C - E\| \leq \|B - D\|$
Assertion	rlimsqzlem	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} E$

Proof

Step	Hyp	Ref	Expression
1		rlimsqzlem.m	$⊢ φ \to M \in ℝ$
2		rlimsqzlem.e	$⊢ φ \to E \in ℂ$
3		rlimsqzlem.1	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} D$
4		rlimsqzlem.2	$⊢ (φ \land x \in A) \to B \in ℂ$
5		rlimsqzlem.3	$⊢ (φ \land x \in A) \to C \in ℂ$
6		rlimsqzlem.4	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C - E\| \leq \|B - D\|$
7	1	ad3antrrr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to M \in ℝ$
8	1	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land x \in A) \to M \in ℝ$
9		elicopnf	$⊢ M \in ℝ \to (z \in [M, +∞) \leftrightarrow (z \in ℝ \land M \leq z))$
10	8 9	syl	$⊢ ((φ \land y \in ℝ^{+}) \land x \in A) \to (z \in [M, +∞) \leftrightarrow (z \in ℝ \land M \leq z))$
11	10	simprbda	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land z \in [M, +∞)) \to z \in ℝ$
12	11	adantrr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to z \in ℝ$
13		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
14	13 4	dmmptd	$⊢ φ \to dom (x \in A ⟼ B) = A$
15		rlimss	$⊢ (x \in A ⟼ B) \underset{ℝ}{⇝} D \to dom (x \in A ⟼ B) \subseteq ℝ$
16	3 15	syl	$⊢ φ \to dom (x \in A ⟼ B) \subseteq ℝ$
17	14 16	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
18	17	adantr	$⊢ (φ \land y \in ℝ^{+}) \to A \subseteq ℝ$
19	18	sselda	$⊢ ((φ \land y \in ℝ^{+}) \land x \in A) \to x \in ℝ$
20	19	adantr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to x \in ℝ$
21	10	simplbda	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land z \in [M, +∞)) \to M \leq z$
22	21	adantrr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to M \leq z$
23		simprr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to z \leq x$
24	7 12 20 22 23	letrd	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to M \leq x$
25	6	anassrs	$⊢ ((φ \land x \in A) \land M \leq x) \to \|C - E\| \leq \|B - D\|$
26	25	adantllr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land M \leq x) \to \|C - E\| \leq \|B - D\|$
27	24 26	syldan	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to \|C - E\| \leq \|B - D\|$
28	2	adantr	$⊢ (φ \land x \in A) \to E \in ℂ$
29	5 28	subcld	$⊢ (φ \land x \in A) \to C - E \in ℂ$
30	29	abscld	$⊢ (φ \land x \in A) \to \|C - E\| \in ℝ$
31	30	ad4ant13	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to \|C - E\| \in ℝ$
32		rlimcl	$⊢ (x \in A ⟼ B) \underset{ℝ}{⇝} D \to D \in ℂ$
33	3 32	syl	$⊢ φ \to D \in ℂ$
34	33	adantr	$⊢ (φ \land x \in A) \to D \in ℂ$
35	4 34	subcld	$⊢ (φ \land x \in A) \to B - D \in ℂ$
36	35	abscld	$⊢ (φ \land x \in A) \to \|B - D\| \in ℝ$
37	36	ad4ant13	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to \|B - D\| \in ℝ$
38		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
39	38	ad3antlr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to y \in ℝ$
40		lelttr	$⊢ (\|C - E\| \in ℝ \land \|B - D\| \in ℝ \land y \in ℝ) \to ((\|C - E\| \leq \|B - D\| \land \|B - D\| < y) \to \|C - E\| < y)$
41	31 37 39 40	syl3anc	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to ((\|C - E\| \leq \|B - D\| \land \|B - D\| < y) \to \|C - E\| < y)$
42	27 41	mpand	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land (z \in [M, +∞) \land z \leq x)) \to (\|B - D\| < y \to \|C - E\| < y)$
43	42	expr	$⊢ (((φ \land y \in ℝ^{+}) \land x \in A) \land z \in [M, +∞)) \to (z \leq x \to (\|B - D\| < y \to \|C - E\| < y))$
44	43	an32s	$⊢ (((φ \land y \in ℝ^{+}) \land z \in [M, +∞)) \land x \in A) \to (z \leq x \to (\|B - D\| < y \to \|C - E\| < y))$
45	44	a2d	$⊢ (((φ \land y \in ℝ^{+}) \land z \in [M, +∞)) \land x \in A) \to ((z \leq x \to \|B - D\| < y) \to (z \leq x \to \|C - E\| < y))$
46	45	ralimdva	$⊢ ((φ \land y \in ℝ^{+}) \land z \in [M, +∞)) \to (\forall x \in A (z \leq x \to \|B - D\| < y) \to \forall x \in A (z \leq x \to \|C - E\| < y))$
47	46	reximdva	$⊢ (φ \land y \in ℝ^{+}) \to (\exists z \in [M, +∞) \forall x \in A (z \leq x \to \|B - D\| < y) \to \exists z \in [M, +∞) \forall x \in A (z \leq x \to \|C - E\| < y))$
48	47	ralimdva	$⊢ φ \to (\forall y \in ℝ^{+} \exists z \in [M, +∞) \forall x \in A (z \leq x \to \|B - D\| < y) \to \forall y \in ℝ^{+} \exists z \in [M, +∞) \forall x \in A (z \leq x \to \|C - E\| < y))$
49	4	ralrimiva	$⊢ φ \to \forall x \in A B \in ℂ$
50	49 17 33 1	rlim3	$⊢ φ \to ((x \in A ⟼ B) \underset{ℝ}{⇝} D \leftrightarrow \forall y \in ℝ^{+} \exists z \in [M, +∞) \forall x \in A (z \leq x \to \|B - D\| < y))$
51	5	ralrimiva	$⊢ φ \to \forall x \in A C \in ℂ$
52	51 17 2 1	rlim3	$⊢ φ \to ((x \in A ⟼ C) \underset{ℝ}{⇝} E \leftrightarrow \forall y \in ℝ^{+} \exists z \in [M, +∞) \forall x \in A (z \leq x \to \|C - E\| < y))$
53	48 50 52	3imtr4d	$⊢ φ \to ((x \in A ⟼ B) \underset{ℝ}{⇝} D \to (x \in A ⟼ C) \underset{ℝ}{⇝} E)$
54	3 53	mpd	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} E$

Metamath Proof Explorer

Theorem rlimsqzlem

Proof