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 ( 𝜑𝐷 ∈ ℝ )
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 ( 𝜑 → ( 𝑥𝐴𝐶 ) ⇝𝑟 𝐷 )