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

Metamath Proof Explorer

Theorem rlimsqz

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 18-Sep-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 ℝ$
		rlimsqz.1	$⊢ (φ \land (x \in A \land M \leq x)) \to B \leq C$
		rlimsqz.2	$⊢ (φ \land (x \in A \land M \leq x)) \to C \leq D$
	Assertion	rlimsqz	$⊢ φ \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		rlimsqz.1	$⊢ (φ \land (x \in A \land M \leq x)) \to B \leq C$
7		rlimsqz.2	$⊢ (φ \land (x \in A \land M \leq x)) \to C \leq D$
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	4	adantrr	$⊢ (φ \land (x \in A \land M \leq x)) \to B \in ℝ$
12	5	adantrr	$⊢ (φ \land (x \in A \land M \leq x)) \to C \in ℝ$
13	1	adantr	$⊢ (φ \land (x \in A \land M \leq x)) \to D \in ℝ$
14	11 12 13 6	lesub2dd	$⊢ (φ \land (x \in A \land M \leq x)) \to D - C \leq D - B$
15	12 13 7	abssuble0d	$⊢ (φ \land (x \in A \land M \leq x)) \to \|C - D\| = D - C$
16	11 12 13 6 7	letrd	$⊢ (φ \land (x \in A \land M \leq x)) \to B \leq D$
17	11 13 16	abssuble0d	$⊢ (φ \land (x \in A \land M \leq x)) \to \|B - D\| = D - B$
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$