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={\mathbb{Z}}_{\ge M}$$
	climadd.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climadd.4	$$⊢\phi \to F⇝A$$
	climsqz.5	$$⊢\phi \to G\in W$$
	climsqz.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
	climsqz.7	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℝ$$
	climsqz.8	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\le G\left(k\right)$$
	climsqz.9	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\le A$$
Assertion	climsqz	$$⊢\phi \to G⇝A$$

Proof

Step	Hyp	Ref	Expression
1		climadd.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climadd.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climadd.4	$$⊢\phi \to F⇝A$$
4		climsqz.5	$$⊢\phi \to G\in W$$
5		climsqz.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
6		climsqz.7	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℝ$$
7		climsqz.8	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\le G\left(k\right)$$
8		climsqz.9	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\le A$$
9	2	adantr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to M\in \mathbb{Z}$$
10		simpr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\in {ℝ}^{+}$$
11		eqidd	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to F\left(k\right)=F\left(k\right)$$
12	3	adantr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to F⇝A$$
13	1 9 10 11 12	climi2	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x$$
14	1	uztrn2	$$⊢\left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to k\in Z$$
15	1 2 3 5	climrecl	$$⊢\phi \to A\in ℝ$$
16	15	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
17	5 6 16 7	lesub2dd	$$⊢\left(\phi \wedge k\in Z\right)\to A-G\left(k\right)\le A-F\left(k\right)$$
18	6 16 8	abssuble0d	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)-A\right|=A-G\left(k\right)$$
19	5 6 16 7 8	letrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\le A$$
20	5 16 19	abssuble0d	$$⊢\left(\phi \wedge k\in Z\right)\to \left|F\left(k\right)-A\right|=A-F\left(k\right)$$
21	17 18 20	3brtr4d	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)-A\right|\le \left|F\left(k\right)-A\right|$$
22	21	adantlr	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to \left|G\left(k\right)-A\right|\le \left|F\left(k\right)-A\right|$$
23	6	adantlr	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to G\left(k\right)\in ℝ$$
24	15	ad2antrr	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to A\in ℝ$$
25	23 24	resubcld	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to G\left(k\right)-A\in ℝ$$
26	25	recnd	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to G\left(k\right)-A\in ℂ$$
27	26	abscld	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to \left|G\left(k\right)-A\right|\in ℝ$$
28	5	adantlr	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
29	28 24	resubcld	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to F\left(k\right)-A\in ℝ$$
30	29	recnd	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to F\left(k\right)-A\in ℂ$$
31	30	abscld	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to \left|F\left(k\right)-A\right|\in ℝ$$
32		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
33	32	ad2antlr	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to x\in ℝ$$
34		lelttr	$$⊢\left(\left|G\left(k\right)-A\right|\in ℝ\wedge \left|F\left(k\right)-A\right|\in ℝ\wedge x\in ℝ\right)\to \left(\left(\left|G\left(k\right)-A\right|\le \left|F\left(k\right)-A\right|\wedge \left|F\left(k\right)-A\right|<x\right)\to \left|G\left(k\right)-A\right|<x\right)$$
35	27 31 33 34	syl3anc	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to \left(\left(\left|G\left(k\right)-A\right|\le \left|F\left(k\right)-A\right|\wedge \left|F\left(k\right)-A\right|<x\right)\to \left|G\left(k\right)-A\right|<x\right)$$
36	22 35	mpand	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge k\in Z\right)\to \left(\left|F\left(k\right)-A\right|<x\to \left|G\left(k\right)-A\right|<x\right)$$
37	14 36	sylan2	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge \left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\right)\to \left(\left|F\left(k\right)-A\right|<x\to \left|G\left(k\right)-A\right|<x\right)$$
38	37	anassrs	$$⊢\left(\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge j\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to \left(\left|F\left(k\right)-A\right|<x\to \left|G\left(k\right)-A\right|<x\right)$$
39	38	ralimdva	$$⊢\left(\left(\phi \wedge x\in {ℝ}^{+}\right)\wedge j\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\to \forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<x\right)$$
40	39	reximdva	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)-A\right|<x\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<x\right)$$
41	13 40	mpd	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<x$$
42	41	ralrimiva	$$⊢\phi \to \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<x$$
43		eqidd	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=G\left(k\right)$$
44	15	recnd	$$⊢\phi \to A\in ℂ$$
45	6	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\in ℂ$$
46	1 2 4 43 44 45	clim2c	$$⊢\phi \to \left(G⇝A\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|G\left(k\right)-A\right|<x\right)$$
47	42 46	mpbird	$$⊢\phi \to G⇝A$$