# Metamath Proof Explorer

## Theorem climsqz2

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008) (Revised by Mario Carneiro, 3-Feb-2014)

Ref Expression
Hypotheses climadd.1 𝑍 = ( ℤ𝑀 )
climadd.2 ( 𝜑𝑀 ∈ ℤ )
climadd.4 ( 𝜑𝐹𝐴 )
climsqz.5 ( 𝜑𝐺𝑊 )
climsqz.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
climsqz.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℝ )
climsqz2.8 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ≤ ( 𝐹𝑘 ) )
climsqz2.9 ( ( 𝜑𝑘𝑍 ) → 𝐴 ≤ ( 𝐺𝑘 ) )
Assertion climsqz2 ( 𝜑𝐺𝐴 )

### Proof

Step Hyp Ref Expression
1 climadd.1 𝑍 = ( ℤ𝑀 )
2 climadd.2 ( 𝜑𝑀 ∈ ℤ )
3 climadd.4 ( 𝜑𝐹𝐴 )
4 climsqz.5 ( 𝜑𝐺𝑊 )
5 climsqz.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
6 climsqz.7 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℝ )
7 climsqz2.8 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ≤ ( 𝐹𝑘 ) )
8 climsqz2.9 ( ( 𝜑𝑘𝑍 ) → 𝐴 ≤ ( 𝐺𝑘 ) )
9 2 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
10 simpr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
11 eqidd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
12 3 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝐹𝐴 )
13 1 9 10 11 12 climi2 ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
14 1 uztrn2 ( ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
15 1 2 3 5 climrecl ( 𝜑𝐴 ∈ ℝ )
16 15 adantr ( ( 𝜑𝑘𝑍 ) → 𝐴 ∈ ℝ )
17 6 5 16 7 lesub1dd ( ( 𝜑𝑘𝑍 ) → ( ( 𝐺𝑘 ) − 𝐴 ) ≤ ( ( 𝐹𝑘 ) − 𝐴 ) )
18 16 6 8 abssubge0d ( ( 𝜑𝑘𝑍 ) → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) = ( ( 𝐺𝑘 ) − 𝐴 ) )
19 16 6 5 8 7 letrd ( ( 𝜑𝑘𝑍 ) → 𝐴 ≤ ( 𝐹𝑘 ) )
20 16 5 19 abssubge0d ( ( 𝜑𝑘𝑍 ) → ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) = ( ( 𝐹𝑘 ) − 𝐴 ) )
21 17 18 20 3brtr4d ( ( 𝜑𝑘𝑍 ) → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) )
22 21 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) )
23 6 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℝ )
24 15 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → 𝐴 ∈ ℝ )
25 23 24 resubcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( 𝐺𝑘 ) − 𝐴 ) ∈ ℝ )
26 25 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( 𝐺𝑘 ) − 𝐴 ) ∈ ℂ )
27 26 abscld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) ∈ ℝ )
28 5 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
29 28 24 resubcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( 𝐹𝑘 ) − 𝐴 ) ∈ ℝ )
30 29 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( 𝐹𝑘 ) − 𝐴 ) ∈ ℂ )
31 30 abscld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) ∈ ℝ )
32 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
33 32 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → 𝑥 ∈ ℝ )
34 lelttr ( ( ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
35 27 31 33 34 syl3anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
36 22 35 mpand ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
37 14 36 sylan2 ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
38 37 anassrs ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
39 38 ralimdva ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
40 39 reximdva ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
41 13 40 mpd ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 )
42 41 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 )
43 eqidd ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( 𝐺𝑘 ) )
44 15 recnd ( 𝜑𝐴 ∈ ℂ )
45 6 recnd ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℂ )
46 1 2 4 43 44 45 clim2c ( 𝜑 → ( 𝐺𝐴 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐺𝑘 ) − 𝐴 ) ) < 𝑥 ) )
47 42 46 mpbird ( 𝜑𝐺𝐴 )