This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimsqz2

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014) (Revised by Mario Carneiro, 20-May-2016)

		Ref	Expression
	Hypotheses	rlimsqz.d	$⊢ φ \to D \in ℝ$
		rlimsqz.m	$⊢ φ \to M \in ℝ$
		rlimsqz.l	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} D$
		rlimsqz.b	$⊢ (φ \land x \in A) \to B \in ℝ$
		rlimsqz.c	$⊢ (φ \land x \in A) \to C \in ℝ$
		rlimsqz2.1	$⊢ (φ \land (x \in A \land M \leq x)) \to C \leq B$
		rlimsqz2.2	$⊢ (φ \land (x \in A \land M \leq x)) \to D \leq C$
	Assertion	rlimsqz2	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} D$

Proof

Step	Hyp	Ref	Expression
1		rlimsqz.d	$⊢ φ \to D \in ℝ$
2		rlimsqz.m	$⊢ φ \to M \in ℝ$
3		rlimsqz.l	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} D$
4		rlimsqz.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		rlimsqz.c	$⊢ (φ \land x \in A) \to C \in ℝ$
6		rlimsqz2.1	$⊢ (φ \land (x \in A \land M \leq x)) \to C \leq B$
7		rlimsqz2.2	$⊢ (φ \land (x \in A \land M \leq x)) \to D \leq C$
8	1	recnd	$⊢ φ \to D \in ℂ$
9	4	recnd	$⊢ (φ \land x \in A) \to B \in ℂ$
10	5	recnd	$⊢ (φ \land x \in A) \to C \in ℂ$
11	5	adantrr	$⊢ (φ \land (x \in A \land M \leq x)) \to C \in ℝ$
12	4	adantrr	$⊢ (φ \land (x \in A \land M \leq x)) \to B \in ℝ$
13	1	adantr	$⊢ (φ \land (x \in A \land M \leq x)) \to D \in ℝ$
14	11 12 13 6	lesub1dd	$⊢ (φ \land (x \in A \land M \leq x)) \to C - D \leq B - D$
15	13 11 7	abssubge0d	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C - D\| = C - D$
16	13 11 12 7 6	letrd	$⊢ (φ \land (x \in A \land M \leq x)) \to D \leq B$
17	13 12 16	abssubge0d	$⊢ (φ \land (x \in A \land M \leq x)) \to \|B - D\| = B - D$
18	14 15 17	3brtr4d	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C - D\| \leq \|B - D\|$
19	2 8 3 9 10 18	rlimsqzlem	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} D$