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