Theorem clm4le 7081

Description: Express the predicate F converges to A, with a non-strict ordering requirement.

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
clm4le	|- ((A e. CC /\ A.k e. W (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,x,A   j,F,k,x   j,M,k   k,N   j,W,k,x   j,Z,k,x

Proof of Theorem clm4le

Step	Hyp	Ref	Expression
1		clm1.1	. . . . 5 |- M e. ZZ
2		clm1.2	. . . . 5 |- (ZZ>` M) (_ Z
3		clm1.3	. . . . 5 |- Z (_ ZZ
4		clm1.4	. . . . 5 |- N e. ZZ
5		clm1.5	. . . . 5 |- (ZZ>` N) (_ W
6		clm1.6	. . . . 5 |- W (_ ZZ
7		clm2.7	. . . . 5 |- F e. V
8	1, 2, 3, 4, 5, 6, 7	clm4 7080	. . . 4 |- ((A e. CC /\ A.k e. (Z i^i W)(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))))
9		inss2 2231	. . . . 5 |- (Z i^i W) (_ W
10		ssralv 2114	. . . . 5 |- ((Z i^i W) (_ W -> (A.k e. W (F` k) e. CC -> A.k e. (Z i^i W)(F` k) e. CC))
11	9, 10	ax-mp 7	. . . 4 |- (A.k e. W (F` k) e. CC -> A.k e. (Z i^i W)(F` k) e. CC)
12	8, 11	sylan2 451	. . 3 |- ((A e. CC /\ A.k e. W (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))))
13		ax-17 971	. . . . . . . . 9 |- (A e. CC -> A.k A e. CC)
14		hbra1 1687	. . . . . . . . 9 |- (A.k e. W (F` k) e. CC -> A.kA.k e. W (F` k) e. CC)
15	13, 14	hban 1009	. . . . . . . 8 |- ((A e. CC /\ A.k e. W (F` k) e. CC) -> A.k(A e. CC /\ A.k e. W (F` k) e. CC))
16		ax-17 971	. . . . . . . 8 |- (x e. RR -> A.k x e. RR)
17	15, 16	hban 1009	. . . . . . 7 |- (((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) -> A.k((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR))
18		ltlet 5520	. . . . . . . . 9 |- (((abs` ((F` k) - A)) e. RR /\ x e. RR) -> ((abs` ((F` k) - A)) < x -> (abs` ((F` k) - A)) <_ x))
19		subclt 5367	. . . . . . . . . . . . . 14 |- (((F` k) e. CC /\ A e. CC) -> ((F` k) - A) e. CC)
20	19	ancoms 436	. . . . . . . . . . . . 13 |- ((A e. CC /\ (F` k) e. CC) -> ((F` k) - A) e. CC)
21		absclt 6833	. . . . . . . . . . . . 13 |- (((F` k) - A) e. CC -> (abs` ((F` k) - A)) e. RR)
22	20, 21	syl 10	. . . . . . . . . . . 12 |- ((A e. CC /\ (F` k) e. CC) -> (abs` ((F` k) - A)) e. RR)
23		ra4 1694	. . . . . . . . . . . . 13 |- (A.k e. W (F` k) e. CC -> (k e. W -> (F` k) e. CC))
24	23	imp 350	. . . . . . . . . . . 12 |- ((A.k e. W (F` k) e. CC /\ k e. W) -> (F` k) e. CC)
25	22, 24	sylan2 451	. . . . . . . . . . 11 |- ((A e. CC /\ (A.k e. W (F` k) e. CC /\ k e. W)) -> (abs` ((F` k) - A)) e. RR)
26	25	anassrs 441	. . . . . . . . . 10 |- (((A e. CC /\ A.k e. W (F` k) e. CC) /\ k e. W) -> (abs` ((F` k) - A)) e. RR)
27	26	adantlr 393	. . . . . . . . 9 |- ((((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) /\ k e. W) -> (abs` ((F` k) - A)) e. RR)
28		simplr 413	. . . . . . . . 9 |- ((((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) /\ k e. W) -> x e. RR)
29	18, 27, 28	sylanc 471	. . . . . . . 8 |- ((((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) /\ k e. W) -> ((abs` ((F` k) - A)) < x -> (abs` ((F` k) - A)) <_ x))
30	29	imim2d 25	. . . . . . 7 |- ((((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) /\ k e. W) -> ((j <_ k -> (abs` ((F` k) - A)) < x) -> (j <_ k -> (abs` ((F` k) - A)) <_ x)))
31	17, 30	r19.20da 1708	. . . . . 6 |- (((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) -> (A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x) -> A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x)))
32	31	r19.22sdv 1738	. . . . 5 |- (((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) -> (E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x) -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x)))
33	32	imim2d 25	. . . 4 |- (((A e. CC /\ A.k e. W (F` k) e. CC) /\ x e. RR) -> ((0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x)) -> (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x))))
34	33	r19.20dva 1709	. . 3 |- ((A e. CC /\ A.k e. W (F` k) e. CC) -> (A.x e. RR (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) < x)) -> A.x e. RR (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x))))
35	12, 34	sylbid 203	. 2 |- ((A e. CC /\ A.k e. W (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))))
36		rehalfclt 6034	. . . . . . . . 9 |- (y e. RR -> (y / 2) e. RR)
37		breq2 2623	. . . . . . . . . . 11 |- (x = (y / 2) -> (0 < x <-> 0 < (y / 2)))
38		breq2 2623	. . . . . . . . . . . . 13 |- (x = (y / 2) -> ((abs` ((F` k) - A)) <_ x <-> (abs` ((F` k) - A)) <_ (y / 2)))
39	38	imbi2d 612	. . . . . . . . . . . 12 |- (x = (y / 2) -> ((j <_ k -> (abs` ((F` k) - A)) <_ x) <-> (j <_ k -> (abs` ((F` k) - A)) <_ (y / 2))))
40	39	rexralbidv 1682	. . . . . . . . . . 11 |- (x = (y / 2) -> (E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x) <-> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ (y / 2))))
41	37, 40	imbi12d 626	. . . . . . . . . 10 |- (x = (y / 2) -> ((0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x)) <-> (0 < (y / 2) -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ (y / 2)))))
42	41	rcla4v 1873	. . . . . . . . 9 |- ((y / 2) e. RR -> (A.x e. RR (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x)) -> (0 < (y / 2) -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ (y / 2)))))
43	36, 42	syl 10	. . . . . . . 8 |- (y e. RR -> (A.x e. RR (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x)) -> (0 < (y / 2) -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ (y / 2)))))
44	43	ad2antrr 404	. . . . . . 7 |- (((y e. RR /\ 0 < y) /\ (A e. CC /\ A.k e. W (F` k) e. CC)) -> (A.x e. RR (0 < x -> E.j e. Z A.k e. W (j <_ k -> (abs` ((F` k) - A)) <_ x)) -> (0 < (y /