Theorem climabslem 7148

Description: Lemma for climabs 7149, climcj 7150, climre 7151, and climim 7152.

Hypotheses

Ref	Expression
climabs.1	|- A e. V
climabs.2	|- G e. V
climabs.3	|- M e. ZZ
climabs.4	|- F ~~> A
climabslem.5	|- (k e. (ZZ>` M) -> ((F` k) e. CC /\ (G` k) = (H` (F` k))))
climabslem.6	|- A.x e. CC (H` x) e. CC
climabslem.7	|- (((F` k) e. CC /\ A e. CC) -> (abs` ((H` (F` k)) - (H` A))) <_ (abs` ((F` k) - A)))

Assertion

Ref	Expression
climabslem	|- G ~~> (H` A)

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

Proof of Theorem climabslem

Step	Hyp	Ref	Expression
1		climabs.4	. . . 4 |- F ~~> A
2		climabs.3	. . . . 5 |- M e. ZZ
3		climabs.1	. . . . . 6 |- A e. V
4		climcl 6978	. . . . . 6 |- ((A e. V /\ F ~~> A) -> A e. CC)
5	3, 1, 4	mp2an 697	. . . . 5 |- A e. CC
6		climabslem.5	. . . . . . 7 |- (k e. (ZZ>` M) -> ((F` k) e. CC /\ (G` k) = (H` (F` k))))
7	6	pm3.26d 321	. . . . . 6 |- (k e. (ZZ>` M) -> (F` k) e. CC)
8	7	rgen 1698	. . . . 5 |- A.k e. (ZZ>` M)(F` k) e. CC
9		climrel 6976	. . . . . . . 8 |- Rel ~~>
10	9	brrelexi 3208	. . . . . . 7 |- (F ~~> A -> F e. V)
11	1, 10	ax-mp 7	. . . . . 6 |- F e. V
12	11	clm4at 7090	. . . . 5 |- ((M e. ZZ /\ A e. CC /\ A.k e. (ZZ>` M)(F` k) e. CC) -> (F ~~> A <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` M)(j <_ k -> (abs` ((F` k) - A)) < x))))
13	2, 5, 8, 12	mp3an 916	. . . 4 |- (F ~~> A <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` M)(j <_ k -> (abs` ((F` k) - A)) < x)))
14	1, 13	mpbi 189	. . 3 |- A.x e. RR (0 < x -> E.j e. ZZ A.k e. (ZZ>` M)(j <_ k -> (abs` ((F` k) - A)) < x))
15	6	pm3.27d 325	. . . . . . . . . . . . . . 15 |- (k e. (ZZ>` M) -> (G` k) = (H` (F` k)))
16	15	opreq1d 3975	. . . . . . . . . . . . . 14 |- (k e. (ZZ>` M) -> ((G` k) - (H` A)) = ((H` (F` k)) - (H` A)))
17	16	fveq2d 3728	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> (abs` ((G` k) - (H` A))) = (abs` ((H` (F` k)) - (H` A))))
18		climabslem.7	. . . . . . . . . . . . . . 15 |- (((F` k) e. CC /\ A e. CC) -> (abs` ((H` (F` k)) - (H` A))) <_ (abs` ((F` k) - A)))
19	5, 18	mpan2 696	. . . . . . . . . . . . . 14 |- ((F` k) e. CC -> (abs` ((H` (F` k)) - (H` A))) <_ (abs` ((F` k) - A)))
20	7, 19	syl 10	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> (abs` ((H` (F` k)) - (H` A))) <_ (abs` ((F` k) - A)))
21	17, 20	eqbrtrd 2635	. . . . . . . . . . . 12 |- (k e. (ZZ>` M) -> (abs` ((G` k) - (H` A))) <_ (abs` ((F` k) - A)))
22	21	adantr 389	. . . . . . . . . . 11 |- ((k e. (ZZ>` M) /\ x e. RR) -> (abs` ((G` k) - (H` A))) <_ (abs` ((F` k) - A)))
23		lelttrt 5523	. . . . . . . . . . . . 13 |- (((abs` ((G` k) - (H` A))) e. RR /\ (abs` ((F` k) - A)) e. RR /\ x e. RR) -> (((abs` ((G` k) - (H` A))) <_ (abs` ((F` k) - A)) /\ (abs` ((F` k) - A)) < x) -> (abs` ((G` k) - (H` A))) < x))
24	23	3expa 833	. . . . . . . . . . . 12 |- ((((abs` ((G` k) - (H` A))) e. RR /\ (abs` ((F` k) - A)) e. RR) /\ x e. RR) -> (((abs` ((G` k) - (H` A))) <_ (abs` ((F` k) - A)) /\ (abs` ((F` k) - A)) < x) -> (abs` ((G` k) - (H` A))) < x))
25		fveq2 3724	. . . . . . . . . . . . . . . . . . 19 |- (x = (F` k) -> (H` x) = (H` (F` k)))
26	25	eleq1d 1540	. . . . . . . . . . . . . . . . . 18 |- (x = (F` k) -> ((H` x) e. CC <-> (H` (F` k)) e. CC))
27		climabslem.6	. . . . . . . . . . . . . . . . . 18 |- A.x e. CC (H` x) e. CC
28	26, 27	vtoclri 1859	. . . . . . . . . . . . . . . . 17 |- ((F` k) e. CC -> (H` (F` k)) e. CC)
29	7, 28	syl 10	. . . . . . . . . . . . . . . 16 |- (k e. (ZZ>` M) -> (H` (F` k)) e. CC)
30	15, 29	eqeltrd 1548	. . . . . . . . . . . . . . 15 |- (k e. (ZZ>` M) -> (G` k) e. CC)
31		fveq2 3724	. . . . . . . . . . . . . . . . . . 19 |- (x = A -> (H` x) = (H` A))
32	31	eleq1d 1540	. . . . . . . . . . . . . . . . . 18 |- (x = A -> ((H` x) e. CC <-> (H` A) e. CC))
33	32, 27	vtoclri 1859	. . . . . . . . . . . . . . . . 17 |- (A e. CC -> (H` A) e. CC)
34	5, 33	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (H` A) e. CC
35		subclt 5367	. . . . . . . . . . . . . . . 16 |- (((G` k) e. CC /\ (H` A) e. CC) -> ((G` k) - (H` A)) e. CC)
36	34, 35	mpan2 696	. . . . . . . . . . . . . . 15 |- ((G` k) e. CC -> ((G` k) - (H` A)) e. CC)
37	30, 36	syl 10	. . . . . . . . . . . . . 14 |- (k e. (ZZ>` M) -> ((G` k) - (H` A)) e. CC)
38		absclt 6833	. . . . . . . . . . . . . 14 |- (((G` k) - (H` A)) e. CC -> (abs` ((G` k) - (H` A))) e. RR)
39	37, 38	syl 10	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> (abs` ((G` k) - (H` A))) e. RR)
40		subclt 5367	. . . . . . . . . . . . . . 15 |- (((F` k) e. CC /\ A e. CC) -> ((F` k) - A) e. CC)
41	5, 40	mpan2 696	. . . . . . . . . . . . . 14 |- ((F` k) e. CC -> ((F` k) - A) e. CC)
42		absclt 6833	. . . . . . . . . . . . . 14 |- (((F` k) - A) e. CC -> (abs` ((F` k) - A)) e. RR)
43	7, 41, 42	3syl 20	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> (abs` ((F` k) - A)) e. RR)
44	39, 43	jca 288	. . . . . . . . . . . 12 |- (k e. (ZZ>` M) -> ((abs` ((G` k) - (H` A))) e. RR /\ (abs` ((F` k) - A)) e. RR))
45	24, 44	sylan 448	. . . . . . . . . . 11 |- ((k e. (ZZ>` M) /\ x e. RR) -> (((abs` ((G` k) - (H` A))) <_ (abs` ((F` k) - A)) /\ (abs` ((F` k) - A)) < x) -> (abs` ((G` k) - (H` A))) < x))
46	22, 45	mpand 701	. . . . . . . . . 10 |- ((k e. (ZZ>` M) /\ x e. RR) -> ((abs` ((F` k) - A)) < x -> (abs` ((G` k) - (H` A))) < x))
47	46	imim2d 25	. . . . . . . . 9 |- ((k e. (ZZ>` M) /\ x e. RR) -> ((j <_ k -> (abs` ((F` k) - A)) < x) -> (j <_ k -> (abs` ((G` k) - (H` A))) < x)))
48	47	expcom 374	. . . . . . . 8 |- (x e. RR -> (k e. (ZZ>` M) -> ((j <_ k -> (abs` ((F` k) - A)) < x) -> (j <_ k -> (abs` ((G` k) - (H` A))) < x))))
49	48	r19.21aiv 1713	. . . . . . 7 |- (x e. RR -> A.k e. (ZZ>` M)((j <_ k -> (abs` ((F` k) - A)) < x) -> (j <_ k -> (abs` ((G` k) - (H` A))) < x)))
50		r19.20 1702	. . . . . . 7 |- (A.k e. (ZZ>` M)((j <_ k -> (abs` ((F` k) - A)) < x) -> (j <_ k -> (abs` ((G` k) - (H` A))) < x)) -> (A.k e. (ZZ>` M)(j <_ k -> (abs` ((F` k) - A)) < x) -> A.k e. (ZZ>` M)(j <_ k -> (abs` ((G` k) - (H` A))) < x)))
51	49, 50	syl 10	. . . . . 6 |- (x e. RR -> (A.k e. (ZZ>` M)(j <_ k -> (abs` ((F` k) - A)) < x) -> A.k e. (ZZ>` M)(j <_ k -> (abs`