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

Proof

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