Theorem climmullem8 7330

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

Hypotheses

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

Assertion

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

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

Proof of Theorem climmullem8

Step	Hyp	Ref	Expression
1		climmullem2 7324	. . . . . . . . 9 |- ((B e. CC /\ (v e. RR /\ 0 < v)) -> ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
2		climmul.1	. . . . . . . . . . 11 |- F e. V
3		climmul.2	. . . . . . . . . . 11 |- G e. V
4		climmul.3	. . . . . . . . . . 11 |- H e. V
5		climmul.4	. . . . . . . . . . 11 |- A e. V
6		climmul.5	. . . . . . . . . . 11 |- B e. V
7		climmullem.6	. . . . . . . . . . 11 |- (ph <-> ((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>=` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) x. (G` k)))))
8	2, 3, 4, 5, 6, 7	climmullem7 7329	. . . . . . . . . 10 |- (ph -> (A e. CC /\ B e. CC))
9	8	pm3.27d 323	. . . . . . . . 9 |- (ph -> B e. CC)
10	1, 9	sylan 450	. . . . . . . 8 |- ((ph /\ (v e. RR /\ 0 < v)) -> ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
11		climmullem1 7323	. . . . . . . . 9 |- ((A e. CC /\ (v e. RR /\ 0 < v)) -> (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))
12	8	pm3.26d 319	. . . . . . . . 9 |- (ph -> A e. CC)
13	11, 12	sylan 450	. . . . . . . 8 |- ((ph /\ (v e. RR /\ 0 < v)) -> (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))
14	10, 13	jca 286	. . . . . . 7 |- ((ph /\ (v e. RR /\ 0 < v)) -> (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A))))))
15		0z 6314	. . . . . . . . . . . . 13 |- 0 e. ZZ
16		ssid 2132	. . . . . . . . . . . . 13 |- (ZZ>=` 0) (_ (ZZ>=` 0)
17		uzssz 6557	. . . . . . . . . . . . 13 |- (ZZ>=` M) (_ ZZ
18	15, 16, 17	clmi2i 7290	. . . . . . . . . . . 12 |- (((A e. V /\ F ~~> A) /\ ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))))) -> E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
19	5, 18	mpanl1 710	. . . . . . . . . . 11 |- ((F ~~> A /\ ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))))) -> E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))))
20	15, 16, 17	clmi2i 7290	. . . . . . . . . . . 12 |- (((B e. V /\ G ~~> B) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A))))) -> E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))
21	6, 20	mpanl1 710	. . . . . . . . . . 11 |- ((G ~~> B /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A))))) -> E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))
22	19, 21	anim12i 331	. . . . . . . . . 10 |- (((F ~~> A /\ ((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))))) /\ (G ~~> B /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
23	22	an4s 511	. . . . . . . . 9 |- (((F ~~> A /\ G ~~> B) /\ (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
24	23	adantlr 393	. . . . . . . 8 |- ((((F ~~> A /\ G ~~> B) /\ A.k e. (ZZ>=` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) x. (G` k)))) /\ (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
25	24, 7	sylanb 451	. . . . . . 7 |- ((ph /\ (((1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) e. RR /\ 0 < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (((v / 2) / (1 + (abs` A))) e. RR /\ 0 < ((v / 2) / (1 + (abs` A)))))) -> (E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
26	14, 25	syldan 469	. . . . . 6 |- ((ph /\ (v e. RR /\ 0 < v)) -> (E.u e. (ZZ>=` 0)A.t e. (ZZ>=` M)(u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ E.f e. (ZZ>=` 0)A.g e. (ZZ>=` M)(f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
27		pm3.27 321	. . . . . . . . . . . . . . . . . 18 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> t e. (ZZ>=` M))
28		nn0addge1 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. NN0) -> u <_ (u + f))
29		nn0re 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. NN0 -> u e. RR)
30	28, 29	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> u <_ (u + f))
31	30	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> u <_ (u + f))
32		letr 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ (u + f) e. RR /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
33	32	3expa 839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((u e. RR /\ (u + f) e. RR) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
34		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> u e. RR)
35		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> (u + f) e. RR)
36	34, 35	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (u e. RR /\ (u + f) e. RR))
37		nn0re 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f e. NN0 -> f e. RR)
38	36, 29, 37	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (u e. RR /\ (u + f) e. RR))
39	33, 38	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u <_ (u + f) /\ (u + f) <_ t) -> u <_ t))
40	31, 39	mpand 705	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ t e. RR) -> ((u + f) <_ t -> u <_ t))
41		eluzelz 6550	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. (ZZ>=` M) -> t e. ZZ)
42		zre 6307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. ZZ -> t e. RR)
43	41, 42	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t e. (ZZ>=` M) -> t e. RR)
44	40, 43	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> u <_ t))
45	44	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> ((u + f) <_ t -> u <_ t))
46		nn0addge2 6299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f e. RR /\ u e. NN0) -> f <_ (u + f))
47	46	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. NN0 /\ f e. RR) -> f <_ (u + f))
48	47, 37	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> f <_ (u + f))
49	48	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> f <_ (u + f))
50		letr 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f e. RR /\ (u + f) e. RR /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
51	50	3expa 839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((f e. RR /\ (u + f) e. RR) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
52		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. RR /\ f e. RR) -> f e. RR)
53	52, 35	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((u e. RR /\ f e. RR) -> (f e. RR /\ (u + f) e. RR))
54	53, 29, 37	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. NN0 /\ f e. NN0) -> (f e. RR /\ (u + f) e. RR))
55	51, 54	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((f <_ (u + f) /\ (u + f) <_ g) -> f <_ g))
56	49, 55	mpand 705	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((u e. NN0 /\ f e. NN0) /\ g e. RR) -> ((u + f) <_ g -> f <_ g))
57		eluzelz 6550	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g e. (ZZ>=` M) -> g e. ZZ)
58		zre 6307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g e. ZZ -> g e. RR)
59	57, 58	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g e. (ZZ>=` M) -> g e. RR)
60	56, 59	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. NN0 /\ f e. NN0) /\ g e. (ZZ>=` M)) -> ((u + f) <_ g -> f <_ g))
61	60	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> ((u + f) <_ g -> f <_ g))
62	45, 61	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)))
63		prth 559	. . . . . . . . . . . . . . . . . . . . . 22 |- (((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((u <_ t /\ f <_ g) -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))
64	62, 63	syl9 57	. . . . . . . . . . . . . . . . . . . . 21 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> (((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> (((u + f) <_ t /\ (u + f) <_ g) -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))))
65	64	exp4a 378	. . . . . . . . . . . . . . . . . . . 20 |- ((((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) /\ g e. (ZZ>=` M)) -> (((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))))
66	65	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)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))))))
67		breq2 2696	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g = t -> ((u + f) <_ g <-> (u + f) <_ t))
68		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g = t -> (G` g) = (G` t))
69	68	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (g = t -> ((G` g) - B) = ((G` t) - B))
70	69	fveq2d 3839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (g = t -> (abs` ((G` g) - B)) = (abs` ((G` t) - B)))
71	70	breq1d 2702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g = t -> ((abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))) <-> (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))
72	71	anbi2d 619	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (g = t -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))) <-> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A))))))
73	67, 72	imbi12d 629	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (g = t -> (((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) <-> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
74	73	rcla4v 1919	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t e. (ZZ>=` M) -> (A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
75	74	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (t e. (ZZ>=` M) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
76	75	a2d 13	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. (ZZ>=` M) -> (((u + f) <_ t -> A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
77		r19.21v 1762	. . . . . . . . . . . . . . . . . . . . 21 |- (A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))) <-> ((u + f) <_ t -> A.g e. (ZZ>=` M)((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))))
78	76, 77	syl5ib 204	. . . . . . . . . . . . . . . . . . . 20 |- (t e. (ZZ>=` M) -> (A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
79	78	com12 11	. . . . . . . . . . . . . . . . . . 19 |- (A.g e. (ZZ>=` M)((u + f) <_ t -> ((u + f) <_ g -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A)))))) -> (t e. (ZZ>=` M) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
80	66, 79	syl6 22	. . . . . . . . . . . . . . . . . 18 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> (t e. (ZZ>=` M) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A))))))))
81	27, 80	mpid 47	. . . . . . . . . . . . . . . . 17 |- (((u e. NN0 /\ f e. NN0) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((u + f) <_ t -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
82	81	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)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
83	82	adantll 392	. . . . . . . . . . . . . . 15 |- ((((ph /\ (v e. RR /\ 0 < v)) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))))))
84		climmullem5 7327	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((F` t) e. CC /\ (G` t) e. CC) /\ (A e. CC /\ B e. CC) /\ (v e. RR /\ 0 < v)) -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` (((F` t) x. (G` t)) - (A x. B))) < v))
85	84	3expa 839	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F` t) e. CC /\ (G` t) e. CC) /\ (A e. CC /\ B e. CC)) /\ (v e. RR /\ 0 < v)) -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` (((F` t) x. (G` t)) - (A x. B))) < v))
86	2, 3, 4, 5, 6, 7	climmullem6 7328	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. (ZZ>=` M) /\ ph) -> ((F` t) e. CC /\ (G` t) e. CC /\ (H` t) = ((F` t) x. (G` t))))
87	86	3simp1d 800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> (F` t) e. CC)
88	86	3simp2d 801	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> (G` t) e. CC)
89	87, 88	jca 286	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ ph) -> ((F` t) e. CC /\ (G` t) e. CC))
90	8	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ ph) -> (A e. CC /\ B e. CC))
91	89, 90	jca 286	. . . . . . . . . . . . . . . . . . . . 21 |- ((t e. (ZZ>=` M) /\ ph) -> (((F` t) e. CC /\ (G` t) e. CC) /\ (A e. CC /\ B e. CC)))
92	85, 91	sylan 450	. . . . . . . . . . . . . . . . . . . 20 |- (((t e. (ZZ>=` M) /\ ph) /\ (v e. RR /\ 0 < v)) -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` (((F` t) x. (G` t)) - (A x. B))) < v))
93	92	anasss 442	. . . . . . . . . . . . . . . . . . 19 |- ((t e. (ZZ>=` M) /\ (ph /\ (v e. RR /\ 0 < v))) -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` (((F` t) x. (G` t)) - (A x. B))) < v))
94	86	3simp3d 802	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. (ZZ>=` M) /\ ph) -> (H` t) = ((F` t) x. (G` t)))
95	94	adantrr 395	. . . . . . . . . . . . . . . . . . . . . 22 |- ((t e. (ZZ>=` M) /\ (ph /\ (v e. RR /\ 0 < v))) -> (H` t) = ((F` t) x. (G` t)))
96	95	opreq1d 4033	. . . . . . . . . . . . . . . . . . . . 21 |- ((t e. (ZZ>=` M) /\ (ph /\ (v e. RR /\ 0 < v))) -> ((H` t) - (A x. B)) = (((F` t) x. (G` t)) - (A x. B)))
97	96	fveq2d 3839	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. (ZZ>=` M) /\ (ph /\ (v e. RR /\ 0 < v))) -> (abs` ((H` t) - (A x. B))) = (abs` (((F` t) x. (G` t)) - (A x. B))))
98	97	breq1d 2702	. . . . . . . . . . . . . . . . . . 19 |- ((t e. (ZZ>=` M) /\ (ph /\ (v e. RR /\ 0 < v))) -> ((abs` ((H` t) - (A x. B))) < v <-> (abs` (((F` t) x. (G` t)) - (A x. B))) < v))
99	93, 98	sylibrd 202	. . . . . . . . . . . . . . . . . 18 |- ((t e. (ZZ>=` M) /\ (ph /\ (v e. RR /\ 0 < v))) -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` ((H` t) - (A x. B))) < v))
100	99	ancoms 438	. . . . . . . . . . . . . . . . 17 |- (((ph /\ (v e. RR /\ 0 < v)) /\ t e. (ZZ>=` M)) -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` ((H` t) - (A x. B))) < v))
101	100	a1d 12	. . . . . . . . . . . . . . . 16 |- (((ph /\ (v e. RR /\ 0 < v)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` ((H` t) - (A x. B))) < v)))
102	101	adantlr 393	. . . . . . . . . . . . . . 15 |- ((((ph /\ (v e. RR /\ 0 < v)) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (((abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B)))))) /\ (abs` ((G` t) - B)) < ((v / 2) / (1 + (abs` A)))) -> (abs` ((H` t) - (A x. B))) < v)))
103	83, 102	syldd 50	. . . . . . . . . . . . . 14 |- ((((ph /\ (v e. RR /\ 0 < v)) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> ((u + f) <_ t -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> (abs` ((H` t) - (A x. B))) < v)))
104	103	com23 32	. . . . . . . . . . . . 13 |- ((((ph /\ (v e. RR /\ 0 < v)) /\ (u e. NN0 /\ f e. NN0)) /\ t e. (ZZ>=` M)) -> (A.g e. (ZZ>=` M)((u <_ t -> (abs` ((F` t) - A)) < (1 / (1 + (1 / ((v / 2) / (1 + (abs` B))))))) /\ (f <_ g -> (abs` ((G` g) - B)) < ((v / 2) / (1 + (abs` A))))) -> ((u + f) <_ t -> (abs` ((H` t) - (A x. B))) < v)))
105	104	r19.20dva 1755	. . . . . . . . . . . 12 |- (((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)) < (1 / (1 + (1 / (