Theorem mullimc 31481

Description: Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
mullimc.f	|- F = ( x e. A |-> B )
mullimc.g	|- G = ( x e. A |-> C )
mullimc.h	|- H = ( x e. A |-> ( B x. C ) )
mullimc.b	|- ( ( ph /\ x e. A ) -> B e. CC )
mullimc.c	|- ( ( ph /\ x e. A ) -> C e. CC )
mullimc.x	|- ( ph -> X e. ( F lim CC D ) )
mullimc.y	|- ( ph -> Y e. ( G lim CC D ) )

Assertion

Ref	Expression
mullimc	|- ( ph -> ( X x. Y ) e. ( H lim CC D ) )

Distinct variable groups:   x, A   x, D   x, X   ph, x

Allowed substitution hints:   B( x)   C( x)   F( x)   G( x)   H( x)   Y( x)

Proof of Theorem mullimc

Dummy variables a b e f y z w c d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limccl 22147	. . . . 5 |- ( F lim CC D ) C_ CC
2		mullimc.x	. . . . 5 |- ( ph -> X e. ( F lim CC D ) )
3	1, 2	sseldi 3507	. . . 4 |- ( ph -> X e. CC )
4		limccl 22147	. . . . 5 |- ( G lim CC D ) C_ CC
5		mullimc.y	. . . . 5 |- ( ph -> Y e. ( G lim CC D ) )
6	4, 5	sseldi 3507	. . . 4 |- ( ph -> Y e. CC )
7	3, 6	mulcld 9628	. . 3 |- ( ph -> ( X x. Y ) e. CC )
8		simpr 461	. . . . . 6 |- ( ( ph /\ w e. RR+ ) -> w e. RR+ )
9	3	adantr 465	. . . . . 6 |- ( ( ph /\ w e. RR+ ) -> X e. CC )
10	6	adantr 465	. . . . . 6 |- ( ( ph /\ w e. RR+ ) -> Y e. CC )
11		mulcn2 13398	. . . . . 6 |- ( ( w e. RR+ /\ X e. CC /\ Y e. CC ) -> E. a e. RR+ E. b e. RR+ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) )
12	8, 9, 10, 11	syl3anc 1228	. . . . 5 |- ( ( ph /\ w e. RR+ ) -> E. a e. RR+ E. b e. RR+ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) )
13		mullimc.b	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> B e. CC )
14		mullimc.f	. . . . . . . . . . . . . . . . . . 19 |- F = ( x e. A |-> B )
15	13, 14	fmptd 6056	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F : A --> CC )
16		fdm 5741	. . . . . . . . . . . . . . . . . . . 20 |- ( F : A --> CC -> dom F = A )
17	15, 16	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> dom F = A )
18		limcrcl 22146	. . . . . . . . . . . . . . . . . . . . 21 |- ( X e. ( F lim CC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
19	2, 18	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
20	19	simp2d 1009	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> dom F C_ CC )
21	17, 20	eqsstr3d 3544	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A C_ CC )
22	19	simp3d 1010	. . . . . . . . . . . . . . . . . 18 |- ( ph -> D e. CC )
23	15, 21, 22	ellimc3 22151	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( X e. ( F lim CC D ) <-> ( X e. CC /\ A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) ) )
24	2, 23	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X e. CC /\ A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) )
25	24	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
26	25	r19.21bi 2836	. . . . . . . . . . . . . 14 |- ( ( ph /\ a e. RR+ ) -> E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
27	26	adantrr 716	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
28		mullimc.c	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> C e. CC )
29		mullimc.g	. . . . . . . . . . . . . . . . . . 19 |- G = ( x e. A |-> C )
30	28, 29	fmptd 6056	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G : A --> CC )
31	30, 21, 22	ellimc3 22151	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( Y e. ( G lim CC D ) <-> ( Y e. CC /\ A. b e. RR+ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) )
32	5, 31	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Y e. CC /\ A. b e. RR+ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
33	32	simprd 463	. . . . . . . . . . . . . . 15 |- ( ph -> A. b e. RR+ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
34	33	r19.21bi 2836	. . . . . . . . . . . . . 14 |- ( ( ph /\ b e. RR+ ) -> E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
35	34	adantrl 715	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
36	27, 35	jca 532	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
37		reeanv 3034	. . . . . . . . . . . 12 |- ( E. e e. RR+ E. f e. RR+ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) <-> ( E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
38	36, 37	sylibr 212	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> E. e e. RR+ E. f e. RR+ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
39		simp2l 1022	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> e e. RR+ )
40		simp2r 1023	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> f e. RR+ )
41		ifcl 3987	. . . . . . . . . . . . . . 15 |- ( ( e e. RR+ /\ f e. RR+ ) -> if ( e <_ f , e , f ) e. RR+ )
42	39, 40, 41	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> if ( e <_ f , e , f ) e. RR+ )
43		nfv 1683	. . . . . . . . . . . . . . . 16 |- F/ z ( ph /\ ( a e. RR+ /\ b e. RR+ ) )
44		nfv 1683	. . . . . . . . . . . . . . . 16 |- F/ z ( e e. RR+ /\ f e. RR+ )
45		nfra1 2848	. . . . . . . . . . . . . . . . 17 |- F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a )
46		nfra1 2848	. . . . . . . . . . . . . . . . 17 |- F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b )
47	45, 46	nfan 1875	. . . . . . . . . . . . . . . 16 |- F/ z ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
48	43, 44, 47	nf3an 1877	. . . . . . . . . . . . . . 15 |- F/ z ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
49		simp11l 1107	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ph )
50		simp1rl 1061	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> a e. RR+ )
51	50	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> a e. RR+ )
52	49, 51	jca 532	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ph /\ a e. RR+ ) )
53		simp12 1027	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
54	52, 53	jca 532	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) )
55		simp13l 1111	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
56	54, 55	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) )
57		simp2 997	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z e. A )
58		simp3 998	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) )
59	56, 57, 58	3jca 1176	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) )
60		simp3l 1024	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z =/= D )
61		simplll 757	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) -> ph )
62	61	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ph )
63		simp1lr 1060	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
64	62, 63	jca 532	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) )
65		simp2 997	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z e. A )
66		simp3r 1025	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) )
67		simp1l 1020	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ph )
68		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> z e. A )
69	21	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. A ) -> z e. CC )
70	67, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> z e. CC )
71	67, 22	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> D e. CC )
72	70, 71	subcld 9942	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( z - D ) e. CC )
73	72	abscld 13247	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) e. RR )
74		rpre 11238	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( e e. RR+ -> e e. RR )
75	74	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) -> e e. RR )
76	75	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> e e. RR )
77		rpre 11238	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f e. RR+ -> f e. RR )
78	77	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) -> f e. RR )
79	78	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> f e. RR )
80		ifcl 3987	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) e. RR )
81	76, 79, 80	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> if ( e <_ f , e , f ) e. RR )
82		simp3 998	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) )
83		min1 11401	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) <_ e )
84	76, 79, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> if ( e <_ f , e , f ) <_ e )
85	73, 81, 76, 82, 84	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < e )
86	64, 65, 66, 85	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < e )
87	60, 86	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( z =/= D /\ ( abs ` ( z - D ) ) < e ) )
88		simp1r 1021	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
89		rsp 2833	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) )
90	89	imp 429	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ z e. A ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
91	88, 65, 90	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
92	87, 91	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( F ` z ) - X ) ) < a )
93	59, 92	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( F ` z ) - X ) ) < a )
94		simp1l 1020	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ph )
95	94, 50	jca 532	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ( ph /\ a e. RR+ ) )
96		simp2 997	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
97		simp3r 1025	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
98	95, 96, 97	jca31 534	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
99	98	3anim1i 1182	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) )
100		simp3l 1024	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z =/= D )
101		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) -> ph )
102	101	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ph )
103		simp1lr 1060	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
104	102, 103	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) )
105		simp2 997	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z e. A )
106		simp3r 1025	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) )
107	104, 105, 106	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) )
108		min2 11402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) <_ f )
109	76, 79, 108	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> if ( e <_ f , e , f ) <_ f )
110	73, 81, 79, 82, 109	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < f )
111	107, 110	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < f )
112	100, 111	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( z =/= D /\ ( abs ` ( z - D ) ) < f ) )
113		simp1r 1021	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
114		rsp 2833	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
115	114	imp 429	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) /\ z e. A ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
116	113, 105, 115	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
117	112, 116	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( G ` z ) - Y ) ) < b )
118	99, 117	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( G ` z ) - Y ) ) < b )
119	93, 118	jca 532	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) )
120	119	3exp 1195	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) )
121	48, 120	ralrimi 2867	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
122		nfv 1683	. . . . . . . . . . . . . . . 16 |- F/ z y = if ( e <_ f , e , f )
123		breq2 4457	. . . . . . . . . . . . . . . . . 18 |- ( y = if ( e <_ f , e , f ) -> ( ( abs ` ( z - D ) ) < y <-> ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) )
124	123	anbi2d 703	. . . . . . . . . . . . . . . . 17 |- ( y = if ( e <_ f , e , f ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) <-> ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) )
125	124	imbi1d 317	. . . . . . . . . . . . . . . 16 |- ( y = if ( e <_ f , e , f ) -> ( ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) <-> ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) )
126	122, 125	ralbid 2901	. . . . . . . . . . . . . . 15 |- ( y = if ( e <_ f , e , f ) -> ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) <-> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) )
127	126	rspcev 3219	. . . . . . . . . . . . . 14 |- ( ( if ( e <_ f , e , f ) e. RR+ /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
128	42, 121, 127	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) /\ ( e e. RR+ /\ f e. RR+ ) /\ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
129	128	3exp 1195	. . . . . . . . . . . 12 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( ( e e. RR+ /\ f e. RR+ ) -> ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) ) )
130	129	rexlimdvv 2965	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( E. e e. RR+ E. f e. RR+ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) )
131	38, 130	mpd 15	. . . . . . . . . 10 |- ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
132	131	adantlr 714	. . . . . . . . 9 |- ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
133	132	3adant3 1016	. . . . . . . 8 |- ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
134		nfv 1683	. . . . . . . . . . . 12 |- F/ z ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ )
135		nfra1 2848	. . . . . . . . . . . 12 |- F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) )
136	134, 135	nfan 1875	. . . . . . . . . . 11 |- F/ z ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
137		simp1l 1020	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) -> ph )
138	137	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ph )
139	138	3ad2ant1 1017	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ph )
140		simp2 997	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> z e. A )
141		nfv 1683	. . . . . . . . . . . . . . . . . 18 |- F/ x ( ph /\ z e. A )
142		mullimc.h	. . . . . . . . . . . . . . . . . . . . 21 |- H = ( x e. A |-> ( B x. C ) )
143		nfmpt1 4542	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x ( x e. A |-> ( B x. C ) )
144	142, 143	nfcxfr 2627	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x H
145		nfcv 2629	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x z
146	144, 145	nffv 5879	. . . . . . . . . . . . . . . . . . 19 |- F/_ x ( H ` z )
147		nfmpt1 4542	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ x ( x e. A |-> B )
148	14, 147	nfcxfr 2627	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x F
149	148, 145	nffv 5879	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x ( F ` z )
150		nfcv 2629	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x x.
151		nfmpt1 4542	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ x ( x e. A |-> C )
152	29, 151	nfcxfr 2627	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ x G
153	152, 145	nffv 5879	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x ( G ` z )
154	149, 150, 153	nfov 6318	. . . . . . . . . . . . . . . . . . 19 |- F/_ x ( ( F ` z ) x. ( G ` z ) )
155	146, 154	nfeq 2640	. . . . . . . . . . . . . . . . . 18 |- F/ x ( H ` z ) = ( ( F ` z ) x. ( G ` z ) )
156	141, 155	nfim 1867	. . . . . . . . . . . . . . . . 17 |- F/ x ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
157		eleq1 2539	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> ( x e. A <-> z e. A ) )
158	157	anbi2d 703	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( ( ph /\ x e. A ) <-> ( ph /\ z e. A ) ) )
159		fveq2 5872	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> ( H ` x ) = ( H ` z ) )
160		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( x = z -> ( F ` x ) = ( F ` z ) )
161		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( x = z -> ( G ` x ) = ( G ` z ) )
162	160, 161	oveq12d 6313	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> ( ( F ` x ) x. ( G ` x ) ) = ( ( F ` z ) x. ( G ` z ) ) )
163	159, 162	eqeq12d 2489	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( ( H ` x ) = ( ( F ` x ) x. ( G ` x ) ) <-> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) ) )
164	158, 163	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( x = z -> ( ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) x. ( G ` x ) ) ) <-> ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) ) ) )
165		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> x e. A )
166	13, 28	mulcld 9628	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> ( B x. C ) e. CC )
167	142	fvmpt2 5964	. . . . . . . . . . . . . . . . . . 19 |- ( ( x e. A /\ ( B x. C ) e. CC ) -> ( H ` x ) = ( B x. C ) )
168	165, 166, 167	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. A ) -> ( H ` x ) = ( B x. C ) )
169	14	fvmpt2 5964	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. A /\ B e. CC ) -> ( F ` x ) = B )
170	165, 13, 169	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
171	170	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> B = ( F ` x ) )
172	29	fvmpt2 5964	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. A /\ C e. CC ) -> ( G ` x ) = C )
173	165, 28, 172	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. A ) -> ( G ` x ) = C )
174	173	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> C = ( G ` x ) )
175	171, 174	oveq12d 6313	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. A ) -> ( B x. C ) = ( ( F ` x ) x. ( G ` x ) ) )
176	168, 175	eqtrd 2508	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) x. ( G ` x ) ) )
177	156, 164, 176	chvar 1982	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
178	177	oveq1d 6310	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. A ) -> ( ( H ` z ) - ( X x. Y ) ) = ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) )
179	178	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. A ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) )
180	139, 140, 179	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) )
181		nfcv 2629	. . . . . . . . . . . . . . . . . . 19 |- F/_ x CC
182	149, 181	nfel 2642	. . . . . . . . . . . . . . . . . 18 |- F/ x ( F ` z ) e. CC
183	141, 182	nfim 1867	. . . . . . . . . . . . . . . . 17 |- F/ x ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
184	160	eleq1d 2536	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( ( F ` x ) e. CC <-> ( F ` z ) e. CC ) )
185	158, 184	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( x = z -> ( ( ( ph /\ x e. A ) -> ( F ` x ) e. CC ) <-> ( ( ph /\ z e. A ) -> ( F ` z ) e. CC ) ) )
186	15	ffvelrnda 6032	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A ) -> ( F ` x ) e. CC )
187	183, 185, 186	chvar 1982	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
188	30	ffvelrnda 6032	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. A ) -> ( G ` z ) e. CC )
189	187, 188	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. A ) -> ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) )
190	139, 140, 189	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) )
191		simpll3 1037	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) )
192	191	3ad2ant1 1017	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) )
193		rsp 2833	. . . . . . . . . . . . . . . . . 18 |- ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) )
194	193	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
195	194	3adant3 1016	. . . . . . . . . . . . . . . 16 |- ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
196		pm2.27 39	. . . . . . . . . . . . . . . . 17 |- ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
197	196	3ad2ant3 1019	. . . . . . . . . . . . . . . 16 |- ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
198	195, 197	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) )
199	198	3adant1l 1220	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) )
200		oveq1 6302	. . . . . . . . . . . . . . . . . . 19 |- ( c = ( F ` z ) -> ( c - X ) = ( ( F ` z ) - X ) )
201	200	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( c = ( F ` z ) -> ( abs ` ( c - X ) ) = ( abs ` ( ( F ` z ) - X ) ) )
202	201	breq1d 4463	. . . . . . . . . . . . . . . . 17 |- ( c = ( F ` z ) -> ( ( abs ` ( c - X ) ) < a <-> ( abs ` ( ( F ` z ) - X ) ) < a ) )
203	202	anbi1d 704	. . . . . . . . . . . . . . . 16 |- ( c = ( F ` z ) -> ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) <-> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) ) )
204		oveq1 6302	. . . . . . . . . . . . . . . . . . 19 |- ( c = ( F ` z ) -> ( c x. d ) = ( ( F ` z ) x. d ) )
205	204	oveq1d 6310	. . . . . . . . . . . . . . . . . 18 |- ( c = ( F ` z ) -> ( ( c x. d ) - ( X x. Y ) ) = ( ( ( F ` z ) x. d ) - ( X x. Y ) ) )
206	205	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( c = ( F ` z ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) )
207	206	breq1d 4463	. . . . . . . . . . . . . . . 16 |- ( c = ( F ` z ) -> ( ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w <-> ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) < w ) )
208	203, 207	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( c = ( F ` z ) -> ( ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) <-> ( ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) < w ) ) )
209		oveq1 6302	. . . . . . . . . . . . . . . . . . 19 |- ( d = ( G ` z ) -> ( d - Y ) = ( ( G ` z ) - Y ) )
210	209	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( d = ( G ` z ) -> ( abs ` ( d - Y ) ) = ( abs ` ( ( G ` z ) - Y ) ) )
211	210	breq1d 4463	. . . . . . . . . . . . . . . . 17 |- ( d = ( G ` z ) -> ( ( abs ` ( d - Y ) ) < b <-> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
212	211	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( d = ( G ` z ) -> ( ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) <-> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
213		oveq2 6303	. . . . . . . . . . . . . . . . . . 19 |- ( d = ( G ` z ) -> ( ( F ` z ) x. d ) = ( ( F ` z ) x. ( G ` z ) ) )
214	213	oveq1d 6310	. . . . . . . . . . . . . . . . . 18 |- ( d = ( G ` z ) -> ( ( ( F ` z ) x. d ) - ( X x. Y ) ) = ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) )
215	214	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( d = ( G ` z ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) )
216	215	breq1d 4463	. . . . . . . . . . . . . . . 16 |- ( d = ( G ` z ) -> ( ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) < w <-> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) < w ) )
217	212, 216	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( d = ( G ` z ) -> ( ( ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) < w ) <-> ( ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) < w ) ) )
218	208, 217	rspc2v 3228	. . . . . . . . . . . . . 14 |- ( ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) -> ( A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) -> ( ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) < w ) ) )
219	190, 192, 199, 218	syl3c 61	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) < w )
220	180, 219	eqbrtrd 4473	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w )
221	220	3exp 1195	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) ) )
222	136, 221	ralrimi 2867	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) )
223	222	ex 434	. . . . . . . . 9 |- ( ( ( ( ph /\ w e. RR+ ) /\ ( a e.