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	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
	rlimsqz.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	rlimsqz.l	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
	rlimsqz.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	rlimsqz.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
	rlimsqz.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐶 )
	rlimsqz.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐷 )
Assertion	rlimsqz	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		rlimsqz.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
2		rlimsqz.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
3		rlimsqz.l	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
4		rlimsqz.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
5		rlimsqz.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
6		rlimsqz.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐶 )
7		rlimsqz.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐷 )
8	1	recnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
9	4	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
10	5	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
11	4	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐵 ∈ ℝ )
12	5	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ∈ ℝ )
13	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐷 ∈ ℝ )
14	11 12 13 6	lesub2dd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( 𝐷 − 𝐶 ) ≤ ( 𝐷 − 𝐵 ) )
15	12 13 7	abssuble0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) = ( 𝐷 − 𝐶 ) )
16	11 12 13 6 7	letrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐷 )
17	11 13 16	abssuble0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐵 − 𝐷 ) ) = ( 𝐷 − 𝐵 ) )
18	14 15 17	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) )
19	2 8 3 9 10 18	rlimsqzlem	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )