Theorem climaddlem3 7319

Description: Lemma for climadd 7320. Warning: The HTML proof page is 3/4 megabyte in size.

Hypotheses

Ref	Expression
climadd.1	|- F e. V
climadd.2	|- G e. V
climadd.3	|- H e. V
climadd.4	|- A e. V
climadd.5	|- B e. V
climaddlem.6	|- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>=` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) + (G` k)))))

Assertion

Ref	Expression
climaddlem3	|- ((M e. ZZ /\ ph) -> H ~~> (A + B))

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

Proof of Theorem climaddlem3

Step	Hyp	Ref	Expression
1		climadd.4	. . . . . . . . . . . 12 |- A e. V
2		0z 6314	. . . . . . . . . . . . 13 |- 0 e. ZZ
3		nn0uz 6565	. . . . . . . . . . . . . 14 |- NN0 = (ZZ>=` 0)
4	3	eqimss2i 2164	. . . . . . . . . . . . 13 |- (ZZ>=` 0) (_ NN0
5		uzssz 6557	. . . . . . . . . . . . 13 |- (ZZ>=` M) (_ ZZ
6	2, 4, 5	clmi2i 7290	. . . . . . . . . . . 12 |- (((A e. V /\ F ~~> A) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)))
7	1, 6	mpanl1 710	. . . . . . . . . . 11 |- ((F ~~> A /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)))
8		climadd.5	. . . . . . . . . . . 12 |- B e. V
9	2, 4, 5	clmi2i 7290	. . . . . . . . . . . 12 |- (((B e. V /\ G ~~> B) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2)))
10	8, 9	mpanl1 710	. . . . . . . . . . 11 |- ((G ~~> B /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2)))
11	7, 10	anim12i 331	. . . . . . . . . 10 |- (((F ~~> A /\ ((v / 2) e. RR /\ 0 < (v / 2))) /\ (G ~~> B /\ ((v / 2) e. RR /\ 0 < (v / 2)))) -> (E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
12	11	anandirs 516	. . . . . . . . 9 |- (((F ~~> A /\ G ~~> B) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> (E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
13	12	adantlr 393	. . . . . . . 8 |- ((((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>=` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) + (G` k)))) /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> (E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
14		climaddlem.6	. . . . . . . 8 |- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>=` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) + (G` k)))))
15	13, 14	sylanb 451	. . . . . . 7 |- ((ph /\ ((v / 2) e. RR /\ 0 < (v / 2))) -> (E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
16		rehalfcl 6180	. . . . . . . . 9 |- (v e. RR -> (v / 2) e. RR)
17	16	adantr 389	. . . . . . . 8 |- ((v e. RR /\ 0 < v) -> (v / 2) e. RR)
18		2re 6125	. . . . . . . . 9 |- 2 e. RR
19		2pos 6135	. . . . . . . . 9 |- 0 < 2
20		divgt0 5999	. . . . . . . . 9 |- (((v e. RR /\ 0 < v) /\ (2 e. RR /\ 0 < 2)) -> 0 < (v / 2))
21	18, 19, 20	mpanr12 715	. . . . . . . 8 |- ((v e. RR /\ 0 < v) -> 0 < (v / 2))
22	17, 21	jca 286	. . . . . . 7 |- ((v e. RR /\ 0 < v) -> ((v / 2) e. RR /\ 0 < (v / 2)))
23	15, 22	sylan2 453	. . . . . 6 |- ((ph /\ (v e. RR /\ 0 < v)) -> (E.u e. NN0 A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ E.f e. NN0 A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < (v / 2))))
24		pm3.27 321	. . . . . . . . . . . . . . . . . 18 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> t e. (ZZ>=` M))
25		nn0addge1 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. NN0) -> u <_ (u + f))
26		nn0re 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. NN0 -> u e. RR)
27	25, 26	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> u <_ (u + f))
28	27	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> u <_ (u + f))
29		letr 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ (u + f) e. RR /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
30	29	3expa 839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((u e. RR /\ (u + f) e. RR) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
31		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> u e. RR)
32		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> (u + f) e. RR)
33	31, 32	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (u e. RR /\ (u + f) e. RR))
34		nn0re 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f e. NN0 -> f e. RR)
35	33, 26, 34	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (u e. RR /\ (u + f) e. RR))
36	30, 35	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
37	28, 36	mpand 705	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u + f) <_ t -> u <_ t))
38		eluzelz 6550	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. (ZZ>=` M) -> t e. ZZ)
39		zre 6307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. ZZ -> t e. RR)
40	38, 39	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t e. (ZZ>=` M) -> t e. RR)
41	37, 40	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> u <_ t))
42	41	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> ((u + f) <_ t -> u <_ t))
43		nn0addge2 6299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f e. RR /\ u e. NN0) -> f <_ (u + f))
44	43	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. NN0 /\ f e. RR) -> f <_ (u + f))
45	44, 34	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> f <_ (u + f))
46	45	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> f <_ (u + f))
47		letr 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f e. RR /\ (u + f) e. RR /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
48	47	3expa 839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((f e. RR /\ (u + f) e. RR) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
49		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> f e. RR)
50	49, 32	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (f e. RR /\ (u + f) e. RR))
51	50, 26, 34	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (f e. RR /\ (u + f) e. RR))
52	48, 51	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
53	46, 52	mpand 705	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((u + f) <_ g -> f <_ g))
54		eluzelz 6550	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g e. (ZZ>=` M) -> g e. ZZ)
55		zre 6307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g e. ZZ -> g e. RR)
56	54, 55	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g e. (ZZ>=` M) -> g e. RR)
57	53, 56	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. NN0 /\ f e. NN0) /\ g e. (ZZ>=` M)) -> ((u + f) <_ g -> f <_ g))
58	57	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> ((u + f) <_ g -> f <_ g))
59	42, 58	anim12d 561	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> (((u + f) <_ t /\ (u + f) <_ g) -> (u <_ t /\ f <_ g)))
60		prth 559	. . . . . . . . . . . . . . . . . . . . . 22 |- (((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> ((u <_ t /\ f <_ g) -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2))))
61	59, 60	syl9 57	. . . . . . . . . . . . . . . . . . . . 21 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> (((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> (((u + f) <_ t /\ (u + f) <_ g) -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)))))
62	61	exp4a 378	. . . . . . . . . . . . . . . . . . . 20 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> (((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> ((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2))))))
63	62	r19.20dva 1755	. . . . . . . . . . . . . . . . . . 19 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2))))))
64		breq2 2696	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g = t -> ((u + f) <_ g <-> (u + f) <_ t))
65		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = t -> (G` g) = (G` t))
66	65	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (g = t -> ((G` g) - B) = ((G` t) - B))
67	66	fveq2d 3839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (g = t -> (abs` ((G` g) - B)) = (abs` ((G` t) - B)))
68	67	breq1d 2702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g = t -> ((abs` ((G` g) - B)) < (v / 2) <-> (abs` ((G` t) - B)) < (v / 2)))
69	68	anbi2d 619	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g = t -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)) <-> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2))))
70	64, 69	imbi12d 629	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (g = t -> (((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2))) <-> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
71	70	rcla4v 1919	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t e. (ZZ>=` M) -> (A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
72	71	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (t e. (ZZ>=` M) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2))) -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
73	72	a2d 13	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. (ZZ>=` M) -> (((u + f) <_ t -> A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
74		r19.21v 1762	. . . . . . . . . . . . . . . . . . . . 21 |- (A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)))) <-> ((u + f) <_ t -> A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)))))
75	73, 74	syl5ib 204	. . . . . . . . . . . . . . . . . . . 20 |- (t e. (ZZ>=` M) -> (A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
76	75	com12 11	. . . . . . . . . . . . . . . . . . 19 |- (A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` g) - B)) < (v / 2)))) -> (t e. (ZZ>=` M) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
77	63, 76	syl6 22	. . . . . . . . . . . . . . . . . 18 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> (t e. (ZZ>=` M) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2))))))
78	24, 77	mpid 47	. . . . . . . . . . . . . . . . 17 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
79	78	com23 32	. . . . . . . . . . . . . . . 16 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
80	79	adantll 392	. . . . . . . . . . . . . . 15 |- ((((ph /\ v e. RR) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> ((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)))))
81		lt2add 5797	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((abs` ((F` t) - A)) e. RR /\ (abs` ((G` t) - B)) e. RR) /\ ((v / 2) e. RR /\ (v / 2) e. RR)) -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < ((v / 2) + (v / 2))))
82		subcl 5521	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` t) e. CC /\ A e. CC) -> ((F` t) - A) e. CC)
83		climadd.1	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- F e. V
84		climadd.2	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- G e. V
85		climadd.3	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- H e. V
86	83, 84, 85, 1, 8, 14	climaddlem1 7317	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t e. (ZZ>=` M) /\ ph) -> ((F` t) e. CC /\ (G` t) e. CC /\ (H` t) = ((F` t) + (G` t))))
87	86	3simp1d 800	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> (F` t) e. CC)
88	83, 84, 85, 1, 8, 14	climaddlem2 7318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (ph -> (A e. CC /\ B e. CC))
89	88	pm3.26d 319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (ph -> A e. CC)
90	89	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> A e. CC)
91	82, 87, 90	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. (ZZ>=` M) /\ ph) -> ((F` t) - A) e. CC)
92		abscl 7035	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F` t) - A) e. CC -> (abs` ((F` t) - A)) e. RR)
93	91, 92	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> (abs` ((F` t) - A)) e. RR)
94		subcl 5521	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` t) e. CC /\ B e. CC) -> ((G` t) - B) e. CC)
95	86	3simp2d 801	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> (G` t) e. CC)
96	88	pm3.27d 323	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (ph -> B e. CC)
97	96	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> B e. CC)
98	94, 95, 97	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. (ZZ>=` M) /\ ph) -> ((G` t) - B) e. CC)
99		abscl 7035	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((G` t) - B) e. CC -> (abs` ((G` t) - B)) e. RR)
100	98, 99	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> (abs` ((G` t) - B)) e. RR)
101	93, 100	jca 286	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ ph) -> ((abs` ((F` t) - A)) e. RR /\ (abs` ((G` t) - B)) e. RR))
102	16, 16	jca 286	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. RR -> ((v / 2) e. RR /\ (v / 2) e. RR))
103	81, 101, 102	syl2an 456	. . . . . . . . . . . . . . . . . . . . 21 |- (((t e. (ZZ>=` M) /\ ph) /\ v e. RR) -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < ((v / 2) + (v / 2))))
104	103	anasss 442	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < ((v / 2) + (v / 2))))
105		recn 5467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((v / 2) e. RR -> (v / 2) e. CC)
106		2times 6150	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((v / 2) e. CC -> (2 x. (v / 2)) = ((v / 2) + (v / 2)))
107	16, 105, 106	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. RR -> (2 x. (v / 2)) = ((v / 2) + (v / 2)))
108		recn 5467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. RR -> v e. CC)
109		2cn 6126	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 e. CC
110		2ne0 6136	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 =/= 0
111		divcan2 5873	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((v e. CC /\ 2 e. CC /\ 2 =/= 0) -> (2 x. (v / 2)) = v)
112	109, 110, 111	mp3an23 914	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. CC -> (2 x. (v / 2)) = v)
113	108, 112	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. RR -> (2 x. (v / 2)) = v)
114	107, 113	eqtr3d 1552	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. RR -> ((v / 2) + (v / 2)) = v)
115	114	ad2antll 407	. . . . . . . . . . . . . . . . . . . . 21 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> ((v / 2) + (v / 2)) = v)
116	115	breq2d 2703	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < ((v / 2) + (v / 2)) <-> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v))
117	104, 116	sylibd 200	. . . . . . . . . . . . . . . . . . 19 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v))
118	86	3simp3d 802	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> (H` t) = ((F` t) + (G` t)))
119	118	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. (ZZ>=` M) /\ ph) -> ((H` t) - (A + B)) = (((F` t) + (G` t)) - (A + B)))
120		addsub4 5627	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((F` t) e. CC /\ (G` t) e. CC) /\ (A e. CC /\ B e. CC)) -> (((F` t) + (G` t)) - (A + B)) = (((F` t) - A) + ((G` t) - B)))
121	87, 95	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> ((F` t) e. CC /\ (G` t) e. CC))
122	88	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> (A e. CC /\ B e. CC))
123	120, 121, 122	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. (ZZ>=` M) /\ ph) -> (((F` t) + (G` t)) - (A + B)) = (((F` t) - A) + ((G` t) - B)))
124	119, 123	eqtrd 1550	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> ((H` t) - (A + B)) = (((F` t) - A) + ((G` t) - B)))
125	124	fveq2d 3839	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ ph) -> (abs` ((H` t) - (A + B))) = (abs` (((F` t) - A) + ((G` t) - B))))
126		abstri 7101	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((F` t) - A) e. CC /\ ((G` t) - B) e. CC) -> (abs` (((F` t) - A) + ((G` t) - B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))))
127	126, 91, 98	sylanc 473	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ ph) -> (abs` (((F` t) - A) + ((G` t) - B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))))
128	125, 127	eqbrtrd 2708	. . . . . . . . . . . . . . . . . . . . 21 |- ((t e. (ZZ>=` M) /\ ph) -> (abs` ((H` t) - (A + B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))))
129	128	adantrr 395	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (abs` ((H` t) - (A + B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))))
130		lelttr 5677	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((abs` ((H` t) - (A + B))) e. RR /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) e. RR /\ v e. RR) -> (((abs` ((H` t) - (A + B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v) -> (abs` ((H` t) - (A + B))) < v))
131	130	3expa 839	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((abs` ((H` t) - (A + B))) e. RR /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) e. RR) /\ v e. RR) -> (((abs` ((H` t) - (A + B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v) -> (abs` ((H` t) - (A + B))) < v))
132		subcl 5521	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((H` t) e. CC /\ (A + B) e. CC) -> ((H` t) - (A + B)) e. CC)
133		addcl 5455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` t) e. CC /\ (G` t) e. CC) -> ((F` t) + (G` t)) e. CC)
134	133, 87, 95	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t e. (ZZ>=` M) /\ ph) -> ((F` t) + (G` t)) e. CC)
135	118, 134	eqeltrd 1591	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> (H` t) e. CC)
136		addcl 5455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
137	136, 90, 97	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((t e. (ZZ>=` M) /\ ph) -> (A + B) e. CC)
138	132, 135, 137	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. (ZZ>=` M) /\ ph) -> ((H` t) - (A + B)) e. CC)
139		abscl 7035	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((H` t) - (A + B)) e. CC -> (abs` ((H` t) - (A + B))) e. RR)
140	138, 139	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> (abs` ((H` t) - (A + B))) e. RR)
141		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((abs` ((F` t) - A)) e. RR /\ (abs` ((G` t) - B)) e. RR) -> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) e. RR)
142	141, 93, 100	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) e. RR)
143	140, 142	jca 286	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ ph) -> ((abs` ((H` t) - (A + B))) e. RR /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) e. RR))
144	131, 143	sylan 450	. . . . . . . . . . . . . . . . . . . . 21 |- (((t e. (ZZ>=` M) /\ ph) /\ v e. RR) -> (((abs` ((H` t) - (A + B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v) -> (abs` ((H` t) - (A + B))) < v))
145	144	anasss 442	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (((abs` ((H` t) - (A + B))) <_ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) /\ ((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v) -> (abs` ((H` t) - (A + B))) < v))
146	129, 145	mpand 705	. . . . . . . . . . . . . . . . . . 19 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (((abs` ((F` t) - A)) + (abs` ((G` t) - B))) < v -> (abs` ((H` t) - (A + B))) < v))
147	117, 146	syld 27	. . . . . . . . . . . . . . . . . 18 |- ((t e. (ZZ>=` M) /\ (ph /\ v e. RR)) -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> (abs` ((H` t) - (A + B))) < v))
148	147	ancoms 438	. . . . . . . . . . . . . . . . 17 |- (((ph /\ v e. RR) /\ t e. (ZZ>=` M)) -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> (abs` ((H` t) - (A + B))) < v))
149	148	a1d 12	. . . . . . . . . . . . . . . 16 |- (((ph /\ v e. RR) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> (abs` ((H` t) - (A + B))) < v)))
150	149	adantlr 393	. . . . . . . . . . . . . . 15 |- ((((ph /\ v e. RR) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (((abs` ((F` t) - A)) < (v / 2) /\ (abs` ((G` t) - B)) < (v / 2)) -> (abs` ((H` t) - (A + B))) < v)))
151	80, 150	syldd 50	. . . . . . . . . . . . . 14 |- ((((ph /\ v e. RR) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> (abs` ((H` t) - (A + B))) < v)))
152	151	com23 32	. . . . . . . . . . . . 13 |- ((((ph /\ v e. RR) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> ((u + f) <_ t -> (abs` ((H` t) - (A + B))) < v)))
153	152	r19.20dva 1755	. . . . . . . . . . . 12 |- (((ph /\ v e. RR) /\ (u e. NN0 /\ f e. NN0)) -> (A.t e. (ZZ>=` M)A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> A.t e. (ZZ>=` M)((u + f) <_ t -> (abs` ((H` t) - (A + B))) < v)))
154	153	adantlrr 399	. . . . . . . . . . 11 |- (((ph /\ (v e. RR /\ 0 < v)) /\ (u e. NN0 /\ f e. NN0)) -> (A.t e. (ZZ>=` M)A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (v / 2)) /\ (f <_ g -> (abs` ((G` g) - B)) < (v / 2))) -> A.t e. (ZZ>=` M)((u + f) <_ t -> (abs` ((H` t) - (A + B))) < v)))
155		breq1 2695	. . . . . . . . . . . . . . . . 17 |- (h = (u + f) -> (h <_ t <-> (u + f) <_ t))
156	155	imbi1d 616	. . . . . . . . . . . . . . . 16 |- (h = (u + f) -> ((h <_ t -> (abs` ((H` t) - (A + B))) < v) <-> ((u + f) <_ t -> (abs` ((H` t) - (A + B))) < v)))
157	156	ralbidv 1709	. . . . . . . . . . . . . . 15 |- (h = (u + f) -> (A.t e. (ZZ>=` M)(h