Metamath Proof Explorer


Theorem climsqz

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

Ref Expression
Hypotheses climadd.1 Z = M
climadd.2 φ M
climadd.4 φ F A
climsqz.5 φ G W
climsqz.6 φ k Z F k
climsqz.7 φ k Z G k
climsqz.8 φ k Z F k G k
climsqz.9 φ k Z G k A
Assertion climsqz φ G A

Proof

Step Hyp Ref Expression
1 climadd.1 Z = M
2 climadd.2 φ M
3 climadd.4 φ F A
4 climsqz.5 φ G W
5 climsqz.6 φ k Z F k
6 climsqz.7 φ k Z G k
7 climsqz.8 φ k Z F k G k
8 climsqz.9 φ k Z G k A
9 2 adantr φ x + M
10 simpr φ x + x +
11 eqidd φ x + k Z F k = F k
12 3 adantr φ x + F A
13 1 9 10 11 12 climi2 φ x + j Z k j F k A < x
14 1 uztrn2 j Z k j k Z
15 1 2 3 5 climrecl φ A
16 15 adantr φ k Z A
17 5 6 16 7 lesub2dd φ k Z A G k A F k
18 6 16 8 abssuble0d φ k Z G k A = A G k
19 5 6 16 7 8 letrd φ k Z F k A
20 5 16 19 abssuble0d φ k Z F k A = A F k
21 17 18 20 3brtr4d φ k Z G k A F k A
22 21 adantlr φ x + k Z G k A F k A
23 6 adantlr φ x + k Z G k
24 15 ad2antrr φ x + k Z A
25 23 24 resubcld φ x + k Z G k A
26 25 recnd φ x + k Z G k A
27 26 abscld φ x + k Z G k A
28 5 adantlr φ x + k Z F k
29 28 24 resubcld φ x + k Z F k A
30 29 recnd φ x + k Z F k A
31 30 abscld φ x + k Z F k A
32 rpre x + x
33 32 ad2antlr φ x + k Z x
34 lelttr G k A F k A x G k A F k A F k A < x G k A < x
35 27 31 33 34 syl3anc φ x + k Z G k A F k A F k A < x G k A < x
36 22 35 mpand φ x + k Z F k A < x G k A < x
37 14 36 sylan2 φ x + j Z k j F k A < x G k A < x
38 37 anassrs φ x + j Z k j F k A < x G k A < x
39 38 ralimdva φ x + j Z k j F k A < x k j G k A < x
40 39 reximdva φ x + j Z k j F k A < x j Z k j G k A < x
41 13 40 mpd φ x + j Z k j G k A < x
42 41 ralrimiva φ x + j Z k j G k A < x
43 eqidd φ k Z G k = G k
44 15 recnd φ A
45 6 recnd φ k Z G k
46 1 2 4 43 44 45 clim2c φ G A x + j Z k j G k A < x
47 42 46 mpbird φ G A