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	$$⊢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 ℝ$$
	climsqz2.8	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\le F\left(k\right)$$
	climsqz2.9	$$⊢\left(\phi \wedge k\in Z\right)\to A\le G\left(k\right)$$
Assertion	climsqz2	$$⊢\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		climsqz2.8	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)\le F\left(k\right)$$
8		climsqz2.9	$$⊢\left(\phi \wedge k\in Z\right)\to A\le G\left(k\right)$$
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	6 5 16 7	lesub1dd	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)-A\le F\left(k\right)-A$$
18	16 6 8	abssubge0d	$$⊢\left(\phi \wedge k\in Z\right)\to \left|G\left(k\right)-A\right|=G\left(k\right)-A$$
19	16 6 5 8 7	letrd	$$⊢\left(\phi \wedge k\in Z\right)\to A\le F\left(k\right)$$
20	16 5 19	abssubge0d	$$⊢\left(\phi \wedge k\in Z\right)\to \left|F\left(k\right)-A\right|=F\left(k\right)-A$$
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$$