Theorem clm3 7017

Description: A sufficient existence condition for convergence of a complex number sequence F.

Hypotheses

Ref	Expression
clm1.1	|- M e. ZZ
clm1.2	|- (ZZ>` M) (_ Z
clm1.3	|- Z (_ ZZ
clm1.4	|- N e. ZZ
clm1.5	|- (ZZ>` N) (_ W
clm1.6	|- W (_ ZZ
clm2.7	|- F e. V

Assertion

Ref	Expression
clm3	|- ((A e. CC /\ E.m e. Z A.k e. W (m <_ k -> (F` k) e. CC)) -> (F ~~> A <-> A.x e. RR (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x))))

Distinct variable groups:   j,k,m,x,A   j,F,k,m,x   j,M,k,m   k,N   j,W,k,m,x   j,Z,k,m,x

Proof of Theorem clm3

Step	Hyp	Ref	Expression
1		clm1.1	. . 3 |- M e. ZZ
2		clm1.2	. . 3 |- (ZZ>` M) (_ Z
3		clm1.3	. . 3 |- Z (_ ZZ
4		clm1.4	. . 3 |- N e. ZZ
5		clm1.5	. . 3 |- (ZZ>` N) (_ W
6		clm1.6	. . 3 |- W (_ ZZ
7		clm2.7	. . 3 |- F e. V
8	1, 2, 3, 4, 5, 6, 7	clm2 7016	. 2 |- (A e. CC -> (F ~~> A <-> A.x e. RR (0 < x -> E.n e. Z A.k e. W (n <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x)))))
9		pm3.27 323	. . . . . . . . 9 |- (((F` k) e. CC /\ (abs` ((F` k) - A)) < x) -> (abs` ((F` k) - A)) < x)
10	9	imim2i 17	. . . . . . . 8 |- ((n <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x)) -> (n <_ k -> (abs` ((F` k) - A)) < x))
11	10	r19.20si 1698	. . . . . . 7 |- (A.k e. W (n <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x)) -> A.k e. W (n <_ k -> (abs` ((F` k) - A)) < x))
12	11	r19.22si 1726	. . . . . 6 |- (E.n e. Z A.k e. W (n <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x)) -> E.n e. Z A.k e. W (n <_ k -> (abs` ((F` k) - A)) < x))
13		breq1 2612	. . . . . . . . 9 |- (n = j -> (n <_ k <-> j <_ k))
14	13	imbi1d 611	. . . . . . . 8 |- (n = j -> ((n <_ k -> (abs` ((F` k) - A)) < x) <-> (j <_ k -> (abs` ((F` k) - A)) < x)))
15	14	ralbidv 1655	. . . . . . 7 |- (n = j -> (A.k e. W (n <_ k -> (abs` ((F` k) - A)) < x) <-> A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x)))
16	15	cbvrexv 1792	. . . . . 6 |- (E.n e. Z A.k e. W (n <_ k -> (abs` ((F` k) - A)) < x) <-> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x))
17	12, 16	sylib 198	. . . . 5 |- (E.n e. Z A.k e. W (n <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x)) -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x))
18		ifcl 2370	. . . . . . . . . . . . . . 15 |- ((j e. Z /\ m e. Z) -> if(m <_ j, j, m) e. Z)
19	18	expcom 374	. . . . . . . . . . . . . 14 |- (m e. Z -> (j e. Z -> if(m <_ j, j, m) e. Z))
20	19	adantr 389	. . . . . . . . . . . . 13 |- ((m e. Z /\ A.k e. W ((m <_ k -> (F` k) e. CC) /\ (j <_ k -> (abs` ((F` k) - A)) < x))) -> (j e. Z -> if(m <_ j, j, m) e. Z))
21		max1 5863	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. RR /\ j e. RR) -> m <_ if(m <_ j, j, m))
22	21	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> m <_ if(m <_ j, j, m))
23		letrt 5498	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((m e. RR /\ if(m <_ j, j, m) e. RR /\ k e. RR) -> ((m <_ if(m <_ j, j, m) /\ if(m <_ j, j, m) <_ k) -> m <_ k))
24	23	3expa 831	. . . . . . . . . . . . . . . . . . . . . 22 |- (((m e. RR /\ if(m <_ j, j, m) e. RR) /\ k e. RR) -> ((m <_ if(m <_ j, j, m) /\ if(m <_ j, j, m) <_ k) -> m <_ k))
25		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((m e. RR /\ j e. RR) -> m e. RR)
26		ifcl 2370	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((j e. RR /\ m e. RR) -> if(m <_ j, j, m) e. RR)
27	26	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((m e. RR /\ j e. RR) -> if(m <_ j, j, m) e. RR)
28	25, 27	jca 288	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. RR /\ j e. RR) -> (m e. RR /\ if(m <_ j, j, m) e. RR))
29	24, 28	sylan 448	. . . . . . . . . . . . . . . . . . . . 21 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> ((m <_ if(m <_ j, j, m) /\ if(m <_ j, j, m) <_ k) -> m <_ k))
30	22, 29	mpand 699	. . . . . . . . . . . . . . . . . . . 20 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> (if(m <_ j, j, m) <_ k -> m <_ k))
31		max2 5865	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. RR /\ j e. RR) -> j <_ if(m <_ j, j, m))
32	31	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> j <_ if(m <_ j, j, m))
33		letrt 5498	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j e. RR /\ if(m <_ j, j, m) e. RR /\ k e. RR) -> ((j <_ if(m <_ j, j, m) /\ if(m <_ j, j, m) <_ k) -> j <_ k))
34	33	3expa 831	. . . . . . . . . . . . . . . . . . . . . 22 |- (((j e. RR /\ if(m <_ j, j, m) e. RR) /\ k e. RR) -> ((j <_ if(m <_ j, j, m) /\ if(m <_ j, j, m) <_ k) -> j <_ k))
35		pm3.27 323	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((m e. RR /\ j e. RR) -> j e. RR)
36	35, 27	jca 288	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. RR /\ j e. RR) -> (j e. RR /\ if(m <_ j, j, m) e. RR))
37	34, 36	sylan 448	. . . . . . . . . . . . . . . . . . . . 21 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> ((j <_ if(m <_ j, j, m) /\ if(m <_ j, j, m) <_ k) -> j <_ k))
38	32, 37	mpand 699	. . . . . . . . . . . . . . . . . . . 20 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> (if(m <_ j, j, m) <_ k -> j <_ k))
39	30, 38	jcad 598	. . . . . . . . . . . . . . . . . . 19 |- (((m e. RR /\ j e. RR) /\ k e. RR) -> (if(m <_ j, j, m) <_ k -> (m <_ k /\ j <_ k)))
40		zssre 6089	. . . . . . . . . . . . . . . . . . . . . 22 |- ZZ (_ RR
41	3, 40	sstri 2063	. . . . . . . . . . . . . . . . . . . . 21 |- Z (_ RR
42	41	sseli 2055	. . . . . . . . . . . . . . . . . . . 20 |- (m e. Z -> m e. RR)
43	41	sseli 2055	. . . . . . . . . . . . . . . . . . . 20 |- (j e. Z -> j e. RR)
44	42, 43	anim12i 333	. . . . . . . . . . . . . . . . . . 19 |- ((m e. Z /\ j e. Z) -> (m e. RR /\ j e. RR))
45	6, 40	sstri 2063	. . . . . . . . . . . . . . . . . . . 20 |- W (_ RR
46	45	sseli 2055	. . . . . . . . . . . . . . . . . . 19 |- (k e. W -> k e. RR)
47	39, 44, 46	syl2an 454	. . . . . . . . . . . . . . . . . 18 |- (((m e. Z /\ j e. Z) /\ k e. W) -> (if(m <_ j, j, m) <_ k -> (m <_ k /\ j <_ k)))
48		prth 554	. . . . . . . . . . . . . . . . . 18 |- (((m <_ k -> (F` k) e. CC) /\ (j <_ k -> (abs` ((F` k) - A)) < x)) -> ((m <_ k /\ j <_ k) -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x)))
49	47, 48	syl9 57	. . . . . . . . . . . . . . . . 17 |- (((m e. Z /\ j e. Z) /\ k e. W) -> (((m <_ k -> (F` k) e. CC) /\ (j <_ k -> (abs` ((F` k) - A)) < x)) -> (if(m <_ j, j, m) <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x))))
50	49	r19.20dva 1701	. . . . . . . . . . . . . . . 16 |- ((m e. Z /\ j e. Z) -> (A.k e. W ((m <_ k -> (F` k) e. CC) /\ (j <_ k -> (abs` ((F` k) - A)) < x)) -> A.k e. W (if(m <_ j, j, m) <_ k -> ((F` k) e. CC /\ (abs` ((F` k) - A)) < x))))
51	50	ex 373	. . . . . . . . . . . . . . 15 |- (m e. Z -> (j e. Z -> (A.k e. W ((m <_ k -> (F` k) e. CC) /\ (j <_ k -> (abs` ((F` k) - A)) < x)) -> A.k e. W (if(m <_ j, j, m) <_ k -> ((F` k) e. CC /\ (abs`