Metamath Proof Explorer

Theorem mullimcf

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

Ref Expression
Hypotheses mullimcf.f 
|- ( ph -> F : A --> CC )
mullimcf.g 
|- ( ph -> G : A --> CC )
mullimcf.h 
|- H = ( x e. A |-> ( ( F ` x ) x. ( G ` x ) ) )
mullimcf.b 
|- ( ph -> B e. ( F limCC D ) )
mullimcf.c 
|- ( ph -> C e. ( G limCC D ) )
Assertion mullimcf 
|- ( ph -> ( B x. C ) e. ( H limCC D ) )

Proof

Step Hyp Ref Expression
1 mullimcf.f 
 |-  ( ph -> F : A --> CC )
2 mullimcf.g 
 |-  ( ph -> G : A --> CC )
3 mullimcf.h 
 |-  H = ( x e. A |-> ( ( F ` x ) x. ( G ` x ) ) )
4 mullimcf.b 
 |-  ( ph -> B e. ( F limCC D ) )
5 mullimcf.c 
 |-  ( ph -> C e. ( G limCC D ) )
6 limccl 
 |-  ( F limCC D ) C_ CC
7 6 4 sselid 
 |-  ( ph -> B e. CC )
8 limccl 
 |-  ( G limCC D ) C_ CC
9 8 5 sselid 
 |-  ( ph -> C e. CC )
10 7 9 mulcld 
 |-  ( ph -> ( B x. C ) e. CC )
11 simpr 
 |-  ( ( ph /\ w e. RR+ ) -> w e. RR+ )
12 7 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> B e. CC )
13 9 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> C e. CC )
14 mulcn2 
 |-  ( ( w e. RR+ /\ B e. CC /\ C e. CC ) -> E. a e. RR+ E. b e. RR+ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) )
15 11 12 13 14 syl3anc 
 |-  ( ( ph /\ w e. RR+ ) -> E. a e. RR+ E. b e. RR+ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) )
16 1 fdmd 
 |-  ( ph -> dom F = A )
17 limcrcl 
 |-  ( B e. ( F limCC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
18 4 17 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
19 18 simp2d 
 |-  ( ph -> dom F C_ CC )
20 16 19 eqsstrrd 
 |-  ( ph -> A C_ CC )
21 18 simp3d 
 |-  ( ph -> D e. CC )
22 1 20 21 ellimc3 
 |-  ( ph -> ( B e. ( F limCC D ) <-> ( B e. CC /\ A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) ) )
23 4 22 mpbid 
 |-  ( ph -> ( B e. CC /\ A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) )
24 23 simprd 
 |-  ( ph -> A. a e. RR+ E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) )
25 24 r19.21bi 
 |-  ( ( ph /\ a e. RR+ ) -> E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) )
26 25 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 ) - B ) ) < a ) )
27 2 20 21 ellimc3 
 |-  ( ph -> ( C e. ( G limCC D ) <-> ( C e. CC /\ A. b e. RR+ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) )
28 5 27 mpbid 
 |-  ( ph -> ( C e. CC /\ A. b e. RR+ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
29 28 simprd 
 |-  ( ph -> A. b e. RR+ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) )
30 29 r19.21bi 
 |-  ( ( ph /\ b e. RR+ ) -> E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) )
31 30 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 ) - C ) ) < b ) )
32 reeanv 
 |-  ( E. e e. RR+ E. f e. RR+ ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) <-> ( E. e e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) /\ E. f e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
33 26 31 32 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
34 ifcl 
 |-  ( ( e e. RR+ /\ f e. RR+ ) -> if ( e <_ f , e , f ) e. RR+ )
35 34 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> if ( e <_ f , e , f ) e. RR+ )
36 nfv 
 |-  F/ z ( ph /\ ( a e. RR+ /\ b e. RR+ ) )
37 nfv 
 |-  F/ z ( e e. RR+ /\ f e. RR+ )
38 nfra1 
 |-  F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a )
39 nfra1 
 |-  F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b )
40 38 39 nfan 
 |-  F/ z ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) )
41 36 37 40 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
42 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ph )
43 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> a e. RR+ )
44 43 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> a e. RR+ )
45 42 44 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ph /\ a e. RR+ ) )
46 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
47 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < 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 ) - B ) ) < a ) )
48 45 46 47 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < 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 ) - B ) ) < a ) ) )
49 simp1r 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < 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 ) - B ) ) < a ) )
50 simp2 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z e. A )
51 simp3l 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z =/= D )
52 simplll 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) -> ph )
53 52 3ad2ant1 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ph )
54 simp1lr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
55 simp3r 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) )
56 simp1l 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ph )
57 simp2 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> z e. A )
58 20 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. CC )
59 56 57 58 syl2anc 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> z e. CC )
60 56 21 syl 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> D e. CC )
61 59 60 subcld 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( z - D ) e. CC )
62 61 abscld 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) e. RR )
63 rpre 
 |-  ( e e. RR+ -> e e. RR )
64 63 ad2antrl 
 |-  ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) -> e e. RR )
65 64 3ad2ant1 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> e e. RR )
66 rpre 
 |-  ( f e. RR+ -> f e. RR )
67 66 ad2antll 
 |-  ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) -> f e. RR )
68 67 3ad2ant1 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> f e. RR )
69 65 68 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 )
70 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 ) )
71 min1 
 |-  ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) <_ e )
72 65 68 71 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 )
73 62 69 65 70 72 ltletrd 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < e )
74 53 54 50 55 73 syl211anc 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < e )
75 51 74 jca 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( z =/= D /\ ( abs ` ( z - D ) ) < e ) )
76 rsp 
 |-  ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) )
77 49 50 75 76 syl3c 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < e ) -> ( abs ` ( ( F ` z ) - B ) ) < a ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( F ` z ) - B ) ) < a )
78 48 77 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( F ` z ) - B ) ) < a )
79 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ph )
80 79 43 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ( ph /\ a e. RR+ ) )
81 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
82 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) )
83 80 81 82 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
84 simp1r 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < 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 ) - C ) ) < b ) )
85 simp2 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z e. A )
86 simp3l 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> z =/= D )
87 simplll 
 |-  ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) -> ph )
88 87 3ad2ant1 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ph )
89 simp1lr 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( e e. RR+ /\ f e. RR+ ) )
90 simp3r 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) )
91 min2 
 |-  ( ( e e. RR /\ f e. RR ) -> if ( e <_ f , e , f ) <_ f )
92 65 68 91 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 )
93 62 69 68 70 92 ltletrd 
 |-  ( ( ( ph /\ ( e e. RR+ /\ f e. RR+ ) ) /\ z e. A /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( abs ` ( z - D ) ) < f )
94 88 89 85 90 93 syl211anc 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( z - D ) ) < f )
95 86 94 jca 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( z =/= D /\ ( abs ` ( z - D ) ) < f ) )
96 rsp 
 |-  ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
97 84 85 95 96 syl3c 
 |-  ( ( ( ( ( ph /\ a e. RR+ ) /\ ( e e. RR+ /\ f e. RR+ ) ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( G ` z ) - C ) ) < b )
98 83 97 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( abs ` ( ( G ` z ) - C ) ) < b )
99 78 98 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) )
100 99 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) )
101 41 100 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < if ( e <_ f , e , f ) ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
102 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 ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
103 35 101 102 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) ) )
105 104 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 ) - B ) ) < a ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < f ) -> ( abs ` ( ( G ` z ) - C ) ) < b ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) )
106 33 105 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 ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
107 106 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 ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
108 107 3adant3 
 |-  ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
109 nfv 
 |-  F/ z ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ )
110 nfra1 
 |-  F/ z A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) )
111 109 110 nfan 
 |-  F/ z ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
112 simp1l 
 |-  ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) -> ph )
113 112 ad2antrr 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ph )
114 113 3ad2ant1 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ph )
115 simp2 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> z e. A )
116 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
117 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
118 116 117 oveq12d 
 |-  ( x = z -> ( ( F ` x ) x. ( G ` x ) ) = ( ( F ` z ) x. ( G ` z ) ) )
119 simpr 
 |-  ( ( ph /\ z e. A ) -> z e. A )
120 1 ffvelcdmda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
121 2 ffvelcdmda 
 |-  ( ( ph /\ z e. A ) -> ( G ` z ) e. CC )
122 120 121 mulcld 
 |-  ( ( ph /\ z e. A ) -> ( ( F ` z ) x. ( G ` z ) ) e. CC )
123 3 118 119 122 fvmptd3 
 |-  ( ( ph /\ z e. A ) -> ( H ` z ) = ( ( F ` z ) x. ( G ` z ) ) )
124 123 fvoveq1d 
 |-  ( ( ph /\ z e. A ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) )
125 114 115 124 syl2anc 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) )
126 120 121 jca 
 |-  ( ( ph /\ z e. A ) -> ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) )
127 114 115 126 syl2anc 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) )
128 simpll3 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) )
129 128 3ad2ant1 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) )
130 rsp 
 |-  ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) )
131 130 3imp 
 |-  ( ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) )
132 131 3adant1l 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) )
133 fvoveq1 
 |-  ( c = ( F ` z ) -> ( abs ` ( c - B ) ) = ( abs ` ( ( F ` z ) - B ) ) )
134 133 breq1d 
 |-  ( c = ( F ` z ) -> ( ( abs ` ( c - B ) ) < a <-> ( abs ` ( ( F ` z ) - B ) ) < a ) )
135 134 anbi1d 
 |-  ( c = ( F ` z ) -> ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) <-> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) ) )
136 oveq1 
 |-  ( c = ( F ` z ) -> ( c x. d ) = ( ( F ` z ) x. d ) )
137 136 fvoveq1d 
 |-  ( c = ( F ` z ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) = ( abs ` ( ( ( F ` z ) x. d ) - ( B x. C ) ) ) )
138 137 breq1d 
 |-  ( c = ( F ` z ) -> ( ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w <-> ( abs ` ( ( ( F ` z ) x. d ) - ( B x. C ) ) ) < w ) )
139 135 138 imbi12d 
 |-  ( c = ( F ` z ) -> ( ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) <-> ( ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( B x. C ) ) ) < w ) ) )
140 fvoveq1 
 |-  ( d = ( G ` z ) -> ( abs ` ( d - C ) ) = ( abs ` ( ( G ` z ) - C ) ) )
141 140 breq1d 
 |-  ( d = ( G ` z ) -> ( ( abs ` ( d - C ) ) < b <-> ( abs ` ( ( G ` z ) - C ) ) < b ) )
142 141 anbi2d 
 |-  ( d = ( G ` z ) -> ( ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) <-> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) )
143 oveq2 
 |-  ( d = ( G ` z ) -> ( ( F ` z ) x. d ) = ( ( F ` z ) x. ( G ` z ) ) )
144 143 fvoveq1d 
 |-  ( d = ( G ` z ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( B x. C ) ) ) = ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) )
145 144 breq1d 
 |-  ( d = ( G ` z ) -> ( ( abs ` ( ( ( F ` z ) x. d ) - ( B x. C ) ) ) < w <-> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) < w ) )
146 142 145 imbi12d 
 |-  ( d = ( G ` z ) -> ( ( ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. d ) - ( B x. C ) ) ) < w ) <-> ( ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) < w ) ) )
147 139 146 rspc2v 
 |-  ( ( ( F ` z ) e. CC /\ ( G ` z ) e. CC ) -> ( A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) -> ( ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) -> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) < w ) ) )
148 127 129 132 147 syl3c 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( abs ` ( ( ( F ` z ) x. ( G ` z ) ) - ( B x. C ) ) ) < w )
149 125 148 eqbrtrd 
 |-  ( ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) /\ z e. A /\ ( z =/= D /\ ( abs ` ( z - D ) ) < y ) ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w )
150 149 3exp 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> ( z e. A -> ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) ) )
151 111 150 ralrimi 
 |-  ( ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) /\ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) )
152 151 ex 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) /\ y e. RR+ ) -> ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) -> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) ) )
153 152 reximdva 
 |-  ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) -> ( E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( ( abs ` ( ( F ` z ) - B ) ) < a /\ ( abs ` ( ( G ` z ) - C ) ) < b ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) ) )
154 108 153 mpd 
 |-  ( ( ( ph /\ w e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) )
155 154 3exp 
 |-  ( ( ph /\ w e. RR+ ) -> ( ( a e. RR+ /\ b e. RR+ ) -> ( A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) ) ) )
156 155 rexlimdvv 
 |-  ( ( ph /\ w e. RR+ ) -> ( E. a e. RR+ E. b e. RR+ A. c e. CC A. d e. CC ( ( ( abs ` ( c - B ) ) < a /\ ( abs ` ( d - C ) ) < b ) -> ( abs ` ( ( c x. d ) - ( B x. C ) ) ) < w ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) ) )
157 15 156 mpd 
 |-  ( ( ph /\ w e. RR+ ) -> E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) )
158 157 ralrimiva 
 |-  ( ph -> A. w e. RR+ E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) )
159 1 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. CC )
160 2 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. CC )
161 159 160 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) x. ( G ` x ) ) e. CC )
162 161 3 fmptd 
 |-  ( ph -> H : A --> CC )
163 162 20 21 ellimc3 
 |-  ( ph -> ( ( B x. C ) e. ( H limCC D ) <-> ( ( B x. C ) e. CC /\ A. w e. RR+ E. y e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < y ) -> ( abs ` ( ( H ` z ) - ( B x. C ) ) ) < w ) ) ) )
164 10 158 163 mpbir2and 
 |-  ( ph -> ( B x. C ) e. ( H limCC D ) )