Metamath Proof Explorer

Theorem mullimc

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

Ref Expression
Hypotheses 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 limCC D ) )
mullimc.y 
|- ( ph -> Y e. ( G limCC D ) )
Assertion mullimc 
|- ( ph -> ( X x. Y ) e. ( H limCC D ) )

Proof

Step Hyp Ref Expression
1 mullimc.f 
 |-  F = ( x e. A |-> B )
2 mullimc.g 
 |-  G = ( x e. A |-> C )
3 mullimc.h 
 |-  H = ( x e. A |-> ( B x. C ) )
4 mullimc.b 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 mullimc.c 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
6 mullimc.x 
 |-  ( ph -> X e. ( F limCC D ) )
7 mullimc.y 
 |-  ( ph -> Y e. ( G limCC D ) )
8 limccl 
 |-  ( F limCC D ) C_ CC
9 8 6 sselid 
 |-  ( ph -> X e. CC )
10 limccl 
 |-  ( G limCC D ) C_ CC
11 10 7 sselid 
 |-  ( ph -> Y e. CC )
12 9 11 mulcld 
 |-  ( ph -> ( X x. Y ) e. CC )
13 simpr 
 |-  ( ( ph /\ w e. RR+ ) -> w e. RR+ )
14 9 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> X e. CC )
15 11 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> Y e. CC )
16 mulcn2 
 |-  ( ( 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 ) )
17 13 14 15 16 syl3anc 
 |-  ( ( 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 ) )
18 4 1 fmptd 
 |-  ( ph -> F : A --> CC )
19 1 4 dmmptd 
 |-  ( ph -> dom F = A )
20 limcrcl 
 |-  ( X e. ( F limCC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
21 6 20 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
22 21 simp2d 
 |-  ( ph -> dom F C_ CC )
23 19 22 eqsstrrd 
 |-  ( ph -> A C_ CC )
24 21 simp3d 
 |-  ( ph -> D e. CC )
25 18 23 24 ellimc3 
 |-  ( ph -> ( X e. ( F limCC 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 ) ) ) )
26 6 25 mpbid 
 |-  ( 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 ) ) )
27 26 simprd 
 |-  ( ph -> A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
28 27 r19.21bi 
 |-  ( ( ph /\ a e. RR+ ) -> E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a ) )
29 28 adantrr 
 |-  ( ( 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 ) )
30 5 2 fmptd 
 |-  ( ph -> G : A --> CC )
31 30 23 24 ellimc3 
 |-  ( ph -> ( Y e. ( G limCC 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 7 31 mpbid 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( 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 reeanv 
 |-  ( 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 ) ) )
37 29 35 36 sylanbrc 
 |-  ( ( 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 ) ) )
38 ifcl 
 |-  ( ( e e. RR+ /\ f e. RR+ ) -> if ( e <_ f , e , f ) e. RR+ )
39 38 3ad2ant2 
 |-  ( ( ( 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+ )
40 nfv 
 |-  F/ z ( ph /\ ( a e. RR+ /\ b e. RR+ ) )
41 nfv 
 |-  F/ z ( e e. RR+ /\ f e. RR+ )
42 nfra1 
 |-  F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - X ) ) < a )
43 nfra1 
 |-  F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - Y ) ) < b )
44 42 43 nfan 
 |-  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 ) )
45 40 41 44 nf3an 
 |-  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 ) ) )
46 simp11l 
 |-  ( ( ( ( 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 )
47 simp1rl 
 |-  ( ( ( 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+ )
48 47 3ad2ant1 
 |-  ( ( ( ( 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+ )
49 46 48 jca 
 |-  ( ( ( ( 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+ ) )
50 simp12 
 |-  ( ( ( ( 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+ ) )
51 simp13l 
 |-  ( ( ( ( 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 ) )
52 49 50 51 jca31 
 |-  ( ( ( ( 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 ) ) )
53 simp1r 
 |-  ( ( ( ( ( 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 ) )
54 simp2 
 |-  ( ( ( ( ( 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 )
55 simp3l 
 |-  ( ( ( ( ( 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 )
56 simplll 
 |-  ( ( ( ( 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 )
57 56 3ad2ant1 
 |-  ( ( ( ( ( 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 )
58 simp1lr 
 |-  ( ( ( ( ( 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+ ) )
59 simp3r 
 |-  ( ( ( ( ( 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 ) )
60 simp1l 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ph )
61 simp2 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> z e. A )
62 23 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. CC )
63 60 61 62 syl2anc 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> z e. CC )
64 60 24 syl 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> D e. CC )
65 63 64 subcld 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( z - D ) e. CC )
66 65 abscld 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) e. RR )
67 rpre 
 |-  ( e e. RR+ -> e e. RR )
68 67 ad2antrl 
 |-  ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) -> e e. RR )
69 68 3ad2ant1 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> e e. RR )
70 rpre 
 |-  ( f e. RR+ -> f e. RR )
71 70 ad2antll 
 |-  ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) -> f e. RR )
72 71 3ad2ant1 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> f e. RR )
73 69 72 ifcld 
 |-  ( ( ( 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 )
74 simp3 
 |-  ( ( ( 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 ) )
75 min1 
 |-  ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) <_ e )
76 69 72 75 syl2anc 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> if ( e <_ f , e , f ) <_ e )
77 66 73 69 74 76 ltletrd 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < e )
78 57 58 54 59 77 syl211anc 
 |-  ( ( ( ( ( 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 )
79 55 78 jca 
 |-  ( ( ( ( ( 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 ) )
80 rsp 
 |-  ( 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 ) ) )
81 53 54 79 80 syl3c 
 |-  ( ( ( ( ( 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 )
82 52 81 syld3an1 
 |-  ( ( ( ( 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 )
83 simp1l 
 |-  ( ( ( 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 )
84 83 47 jca 
 |-  ( ( ( 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+ ) )
85 simp2 
 |-  ( ( ( 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+ ) )
86 simp3r 
 |-  ( ( ( 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 ) )
87 84 85 86 jca31 
 |-  ( ( ( 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 ) ) )
88 simp1r 
 |-  ( ( ( ( ( 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 ) )
89 simp2 
 |-  ( ( ( ( ( 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 )
90 simp3l 
 |-  ( ( ( ( ( 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 )
91 simplll 
 |-  ( ( ( ( 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 )
92 91 3ad2ant1 
 |-  ( ( ( ( ( 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 )
93 simp1lr 
 |-  ( ( ( ( ( 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+ ) )
94 simp3r 
 |-  ( ( ( ( ( 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 ) )
95 min2 
 |-  ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) <_ f )
96 69 72 95 syl2anc 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> if ( e <_ f , e , f ) <_ f )
97 66 73 72 74 96 ltletrd 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < f )
98 92 93 89 94 97 syl211anc 
 |-  ( ( ( ( ( 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 )
99 90 98 jca 
 |-  ( ( ( ( ( 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 ) )
100 rsp 
 |-  ( 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 ) ) )
101 88 89 99 100 syl3c 
 |-  ( ( ( ( ( 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 )
102 87 101 syl3an1 
 |-  ( ( ( ( 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 )
103 82 102 jca 
 |-  ( ( ( ( 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 ) )
104 103 3exp 
 |-  ( ( ( 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 ) ) ) )
105 45 104 ralrimi 
 |-  ( ( ( 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 ) ) )
106 brimralrspcev 
 |-  ( ( 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 ) ) )
107 39 105 106 syl2anc 
 |-  ( ( ( 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 ) ) )
108 107 3exp 
 |-  ( ( 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 ) ) ) ) )
109 108 rexlimdvv 
 |-  ( ( 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 ) ) ) )
110 37 109 mpd 
 |-  ( ( 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 ) ) )
111 110 adantlr 
 |-  ( ( ( 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 ) ) )
112 111 3adant3 
 |-  ( ( ( 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 ) ) )
113 nfv 
 |-  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+ )
114 nfra1 
 |-  F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) )
115 113 114 nfan 
 |-  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 ) ) )
116 simp1l 
 |-  ( ( ( 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 )
117 116 ad2antrr 
 |-  ( ( ( ( ( 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 )
118 117 3ad2ant1 
 |-  ( ( ( ( ( ( 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 )
119 simp2 
 |-  ( ( ( ( ( ( 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 )
120 nfv 
 |-  F/ x ( ph /\ z e. A )
121 nfmpt1 
 |-  F/_ x ( x e. A |-> ( B x. C ) )
122 3 121 nfcxfr 
 |-  F/_ x H
123 nfcv 
 |-  F/_ x z
124 122 123 nffv 
 |-  F/_ x ( H ` z )
125 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
126 1 125 nfcxfr 
 |-  F/_ x F
127 126 123 nffv 
 |-  F/_ x ( F ` z )
128 nfcv 
 |-  F/_ x x.
129 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
130 2 129 nfcxfr 
 |-  F/_ x G
131 130 123 nffv 
 |-  F/_ x ( G ` z )
132 127 128 131 nfov 
 |-  F/_ x ( ( F ` z ) x. ( G ` z ) )
133 124 132 nfeq 
 |-  F/ x ( H ` z ) = ( ( F ` z ) x. ( G ` z ) )
134 120 133 nfim 
 |-  F/ x ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
135 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
136 135 anbi2d 
 |-  ( x = z -> ( ( ph /\ x e. A ) <-> ( ph /\ z e. A ) ) )
137 fveq2 
 |-  ( x = z -> ( H ` x ) = ( H ` z ) )
138 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
139 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
140 138 139 oveq12d 
 |-  ( x = z -> ( ( F ` x ) x. ( G ` x ) ) = ( ( F ` z ) x. ( G ` z ) ) )
141 137 140 eqeq12d 
 |-  ( x = z -> ( ( H ` x ) = ( ( F ` x ) x. ( G ` x ) ) <-> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) ) )
142 136 141 imbi12d 
 |-  ( x = z -> ( ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) x. ( G ` x ) ) ) <-> ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) ) ) )
143 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
144 4 5 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) e. CC )
145 3 fvmpt2 
 |-  ( ( x e. A /\ ( B x. C ) e. CC ) -> ( H ` x ) = ( B x. C ) )
146 143 144 145 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = ( B x. C ) )
147 1 fvmpt2 
 |-  ( ( x e. A /\ B e. CC ) -> ( F ` x ) = B )
148 143 4 147 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
149 148 eqcomd 
 |-  ( ( ph /\ x e. A ) -> B = ( F ` x ) )
150 2 fvmpt2 
 |-  ( ( x e. A /\ C e. CC ) -> ( G ` x ) = C )
151 143 5 150 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = C )
152 151 eqcomd 
 |-  ( ( ph /\ x e. A ) -> C = ( G ` x ) )
153 149 152 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( B x. C ) = ( ( F ` x ) x. ( G ` x ) ) )
154 146 153 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) x. ( G ` x ) ) )
155 134 142 154 chvarfv 
 |-  ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
156 155 fvoveq1d 
 |-  ( ( ph /\ z e. A ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) )
157 118 119 156 syl2anc 
 |-  ( ( ( ( ( ( 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 ) ) ) )
158 18 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
159 30 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( G ` z ) e. CC )
160 158 159 jca 
 |-  ( ( ph /\ z e. A ) -> ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) )
161 118 119 160 syl2anc 
 |-  ( ( ( ( ( ( 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 ) )
162 simpll3 
 |-  ( ( ( ( ( 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 ) )
163 162 3ad2ant1 
 |-  ( ( ( ( ( ( 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 ) )
164 rsp 
 |-  ( 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 ) ) ) )
165 164 3imp 
 |-  ( ( 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 ) )
166 165 3adant1l 
 |-  ( ( ( ( ( ( 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 ) )
167 fvoveq1 
 |-  ( c = ( F ` z ) -> ( abs ` ( c - X ) ) = ( abs ` ( ( F ` z ) - X ) ) )
168 167 breq1d 
 |-  ( c = ( F ` z ) -> ( ( abs ` ( c - X ) ) < a <-> ( abs ` ( ( F ` z ) - X ) ) < a ) )
169 168 anbi1d 
 |-  ( c = ( F ` z ) -> ( ( ( abs ` ( c - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) <-> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) ) )
170 oveq1 
 |-  ( c = ( F ` z ) -> ( c x. d ) = ( ( F ` z ) x. d ) )
171 170 fvoveq1d 
 |-  ( c = ( F ` z ) -> ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) )
172 171 breq1d 
 |-  ( c = ( F ` z ) -> ( ( abs ` ( ( c x. d ) - ( X x. Y ) ) ) < w <-> ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) < w ) )
173 169 172 imbi12d 
 |-  ( 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 ) ) )
174 fvoveq1 
 |-  ( d = ( G ` z ) -> ( abs ` ( d - Y ) ) = ( abs ` ( ( G ` z ) - Y ) ) )
175 174 breq1d 
 |-  ( d = ( G ` z ) -> ( ( abs ` ( d - Y ) ) < b <-> ( abs ` ( ( G ` z ) - Y ) ) < b ) )
176 175 anbi2d 
 |-  ( d = ( G ` z ) -> ( ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( d - Y ) ) < b ) <-> ( ( abs ` ( ( F ` z ) - X ) ) < a /\ ( abs ` ( ( G ` z ) - Y ) ) < b ) ) )
177 oveq2 
 |-  ( d = ( G ` z ) -> ( ( F ` z ) x. d ) = ( ( F ` z ) x. ( G ` z ) ) )
178 177 fvoveq1d 
 |-  ( d = ( G ` z ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) )
179 178 breq1d 
 |-  ( d = ( G ` z ) -> ( ( abs ` ( ( ( F ` z ) x. d ) - ( X x. Y ) ) ) < w <-> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( X x. Y ) ) ) < w ) )
180 176 179 imbi12d 
 |-  ( 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 ) ) )
181 173 180 rspc2v 
 |-  ( ( ( 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 ) ) )
182 161 163 166 181 syl3c 
 |-  ( ( ( ( ( ( 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 )
183 157 182 eqbrtrd 
 |-  ( ( ( ( ( ( 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 )
184 183 3exp 
 |-  ( ( ( ( ( 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 ) ) )
185 115 184 ralrimi 
 |-  ( ( ( ( ( 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 ) )
186 185 ex 
 |-  ( ( ( ( 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 ) ) )
187 186 reximdva 
 |-  ( ( ( 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 ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) ) )
188 112 187 mpd 
 |-  ( ( ( 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 ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) )
189 188 3exp 
 |-  ( ( 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 ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) ) ) )
190 189 rexlimdvv 
 |-  ( ( 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 ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) ) )
191 17 190 mpd 
 |-  ( ( ph /\ w e. RR+ ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) )
192 191 ralrimiva 
 |-  ( ph -> A. w e. RR+ E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) )
193 144 3 fmptd 
 |-  ( ph -> H : A --> CC )
194 193 23 24 ellimc3 
 |-  ( ph -> ( ( X x. Y ) e. ( H limCC D ) <-> ( ( X x. Y ) e. CC /\ A. w e. RR+ E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( X x. Y ) ) ) < w ) ) ) )
195 12 192 194 mpbir2and 
 |-  ( ph -> ( X x. Y ) e. ( H limCC D ) )