Theorem climsqueeze2 7085

Description: Convergence of a sequence sandwiched between another converging sequence and its limit.

Hypotheses

Ref	Expression
climsqueeze.1	|- F e. V
climsqueeze.2	|- G e. V
climsqueeze.3	|- A e. V

Assertion

Ref	Expression
climsqueeze2	|- ((F ~~> A /\ M e. ZZ /\ A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> G ~~> A)

Distinct variable groups:   A,k   k,F   k,G   k,M

Proof of Theorem climsqueeze2

Step	Hyp	Ref	Expression
1		climsqueeze.3	. . . . 5 |- A e. V
2	1	climrecl 7055	. . . 4 |- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)(F` k) e. RR) -> A e. RR)
3		simpll 412	. . . . 5 |- ((((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k))) -> (F` k) e. RR)
4	3	r19.20si 1703	. . . 4 |- (A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k))) -> A.k e. (ZZ>` M)(F` k) e. RR)
5	2, 4	syl3an3 860	. . 3 |- ((M e. ZZ /\ F ~~> A /\ A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> A e. RR)
6		lesub1t 5641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((G` k) e. RR /\ (F` k) e. RR /\ A e. RR) -> ((G` k) <_ (F` k) <-> ((G` k) - A) <_ ((F` k) - A)))
7	6	3com13 837	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. RR /\ (F` k) e. RR /\ (G` k) e. RR) -> ((G` k) <_ (F` k) <-> ((G` k) - A) <_ ((F` k) - A)))
8	7	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (F` k) e. RR /\ (G` k) e. RR) -> ((G` k) <_ (F` k) -> ((G` k) - A) <_ ((F` k) - A)))
9	8	3exp 831	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. RR -> ((F` k) e. RR -> ((G` k) e. RR -> ((G` k) <_ (F` k) -> ((G` k) - A) <_ ((F` k) - A)))))
10	9	imp44 371	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (G` k) <_ (F` k))) -> ((G` k) - A) <_ ((F` k) - A))
11	10	adantrrl 402	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> ((G` k) - A) <_ ((F` k) - A))
12		abssubge0t 6841	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (G` k) e. RR /\ A <_ (G` k)) -> (abs` ((G` k) - A)) = ((G` k) - A))
13	12	3expb 833	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ ((G` k) e. RR /\ A <_ (G` k))) -> (abs` ((G` k) - A)) = ((G` k) - A))
14	13	adantrll 400	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ A <_ (G` k))) -> (abs` ((G` k) - A)) = ((G` k) - A))
15	14	adantrrr 403	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> (abs` ((G` k) - A)) = ((G` k) - A))
16		abssubge0t 6841	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (F` k) e. RR /\ A <_ (F` k)) -> (abs` ((F` k) - A)) = ((F` k) - A))
17		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> A e. RR)
18	3	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> (F` k) e. RR)
19		letrt 5506	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. RR /\ (G` k) e. RR /\ (F` k) e. RR) -> ((A <_ (G` k) /\ (G` k) <_ (F` k)) -> A <_ (F` k)))
20	19	3com23 838	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (F` k) e. RR /\ (G` k) e. RR) -> ((A <_ (G` k) /\ (G` k) <_ (F` k)) -> A <_ (F` k)))
21	20	3exp 831	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. RR -> ((F` k) e. RR -> ((G` k) e. RR -> ((A <_ (G` k) /\ (G` k) <_ (F` k)) -> A <_ (F` k)))))
22	21	imp44 371	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> A <_ (F` k))
23	16, 17, 18, 22	syl3anc 857	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> (abs` ((F` k) - A)) = ((F` k) - A))
24	11, 15, 23	3brtr4d 2640	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> (abs` ((G` k) - A)) <_ (abs` ((F` k) - A)))
25	24	adantlr 393	. . . . . . . . . . . . . . . . . . 19 |- (((A e. RR /\ x e. RR) /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (A <_ (G` k) /\ (G` k) <_ (F` k)))) -> (abs` ((G` k) - A)) <_ (abs` ((F` k) - A)))
26		lelttrt 5504	. . . . . . . . . . . . . . . . . . . . 21 |- (((abs` ((G` k) - A)) e. RR /\ (abs` ((F` k) - A)) e. RR /\ x e. RR) -> (((abs` ((G` k) - A)) <_ (abs` ((F` k) - A)) /\ (abs` ((F` k) - A)) < x) -> (abs` ((G` k) - A)) < x))
27		resubclt 5418	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` k) e. RR /\ A e. RR) -> ((G` k) - A) e. RR)
28	27	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (G` k) e. RR) -> ((G` k) - A) e. RR)
29	28	recnd 5295	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ (G` k) e. RR) -> ((G` k) - A) e. CC)
30		absclt 6776	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((G` k) - A) e. CC -> (abs` ((G` k) - A)) e. RR)
31	29, 30	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (G` k) e. RR) -> (abs` ((G` k) - A)) e. RR)
32	31	ad2ant2rl 411	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. RR /\ x e. RR) /\ ((F` k) e. RR /\ (G` k) e. RR)) -> (abs` ((G` k) - A)) e. RR)
33		resubclt 5418	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` k) e. RR /\ A e. RR) -> ((F` k) - A) e. RR)
34	33	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (F` k) e. RR) -> ((F` k) - A) e. RR)
35	34	recnd 5295	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ (F` k) e. RR) -> ((F` k) - A) e. CC)
36		absclt 6776	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F` k) - A) e. CC -> (abs` ((F` k) - A)) e. RR)
37	35, 36	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (F` k) e. RR) -> (abs` ((F` k) - A)) e. RR)
38	37	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. RR /\ x e. RR) /\ ((F` k) e. RR /\ (G` k) e. RR)) -> (abs` ((F` k) - A)) e. RR)
39		simplr 413	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. RR /\ x e. RR) /\ ((F` k) e. RR /\ (G` k) e. RR)) -> x e. RR)
40	26, 32, 38, 39	syl3anc 857	. . . . . . . . . . . . . . . . . . . 20 |- (((A e. RR /\ x e. RR) /\ ((F` k) e. RR /\ (G`