Theorem climsqueeze 7084

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
climsqueeze	|- ((F ~~> A /\ M e. ZZ /\ A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> G ~~> A)

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

Proof of Theorem climsqueeze

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) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A)) -> (F` k) e. RR)
4	3	r19.20si 1703	. . . 4 |- (A.k e. (ZZ>` M)(((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A)) -> 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) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> A e. RR)
6		lesub2t 5642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` k) e. RR /\ (G` k) e. RR /\ A e. RR) -> ((F` k) <_ (G` k) <-> (A - (G` k)) <_ (A - (F` k))))
7	6	3comr 840	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. RR /\ (F` k) e. RR /\ (G` k) e. RR) -> ((F` k) <_ (G` k) <-> (A - (G` k)) <_ (A - (F` k))))
8	7	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (F` k) e. RR /\ (G` k) e. RR) -> ((F` k) <_ (G` k) -> (A - (G` k)) <_ (A - (F` k))))
9	8	3exp 831	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. RR -> ((F` k) e. RR -> ((G` k) e. RR -> ((F` k) <_ (G` k) -> (A - (G` k)) <_ (A - (F` k))))))
10	9	imp44 371	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ (F` k) <_ (G` k))) -> (A - (G` k)) <_ (A - (F` k)))
11	10	adantrrr 403	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (A - (G` k)) <_ (A - (F` k)))
12		abssuble0t 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` k) e. RR /\ A e. RR /\ (G` k) <_ A) -> (abs` ((G` k) - A)) = (A - (G` k)))
13	12	3com12 836	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (G` k) e. RR /\ (G` k) <_ A) -> (abs` ((G` k) - A)) = (A - (G` k)))
14	13	3expb 833	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ ((G` k) e. RR /\ (G` k) <_ A)) -> (abs` ((G` k) - A)) = (A - (G` k)))
15	14	adantrrl 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ ((G` k) e. RR /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (abs` ((G` k) - A)) = (A - (G` k)))
16	15	adantrll 400	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (abs` ((G` k) - A)) = (A - (G` k)))
17		abssuble0t 6842	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` k) e. RR /\ A e. RR /\ (F` k) <_ A) -> (abs` ((F` k) - A)) = (A - (F` k)))
18	3	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (F` k) e. RR)
19		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> A e. RR)
20		letrt 5506	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` k) e. RR /\ (G` k) e. RR /\ A e. RR) -> (((F` k) <_ (G` k) /\ (G` k) <_ A) -> (F` k) <_ A))
21	20	3comr 840	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (F` k) e. RR /\ (G` k) e. RR) -> (((F` k) <_ (G` k) /\ (G` k) <_ A) -> (F` k) <_ A))
22	21	3exp 831	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. RR -> ((F` k) e. RR -> ((G` k) e. RR -> (((F` k) <_ (G` k) /\ (G` k) <_ A) -> (F` k) <_ A))))
23	22	imp44 371	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (F` k) <_ A)
24	17, 18, 19, 23	syl3anc 857	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (abs` ((F` k) - A)) = (A - (F` k)))
25	11, 16, 24	3brtr4d 2640	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. RR /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (abs` ((G` k) - A)) <_ (abs` ((F` k) - A)))
26	25	adantlr 393	. . . . . . . . . . . . . . . . . . 19 |- (((A e. RR /\ x e. RR) /\ (((F` k) e. RR /\ (G` k) e. RR) /\ ((F` k) <_ (G` k) /\ (G` k) <_ A))) -> (abs` ((G` k) - A)) <_ (abs` ((F` k) - A)))
27		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))
28		resubclt 5418	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` k) e. RR /\ A e. RR) -> ((G` k) - A) e. RR)
29	28	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (G` k) e. RR) -> ((G` k) - A) e. RR)
30	29	recnd 5295	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ (G` k) e. RR) -> ((G` k) - A) e. CC)
31		absclt 6776	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((G` k) - A) e. CC -> (abs` ((G` k) - A)) e. RR)
32	30, 31	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (G` k) e. RR) -> (abs` ((G` k) - A)) e. RR)
33	32	ad2ant2rl 411	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. RR /\ x e. RR) /\ ((F` k) e. RR /\ (G` k) e. RR)) -> (abs` ((G` k) - A)) e. RR)
34		resubclt 5418	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` k) e. RR /\ A e. RR) -> ((F` k) - A) e. RR)
35	34	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ (F` k) e. RR) -> ((F` k) - A) e. RR)
36	35	recnd 5295	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ (F` k) e. RR) -> ((F` k) - A) e. CC)
37		absclt 6776	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F` k) - A) e. CC -> (abs` ((F` k) - A)) e. RR)
38	36, 37	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ (F` k) e. RR) -> (abs` ((F` k) - A)) e. RR)
39	38	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. RR /\ x e. RR) /\ ((F` k) e. RR /\ (G` k) e. RR)) -> (abs` ((F` k) - A)) e. RR)
40		simplr 413	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. RR /\