Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mullimc Structured version   Unicode version

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.
StepHypRef Expression
1 limccl 22147 . . . . 5  |-  ( F lim
CC  D )  C_  CC
2 mullimc.x . . . . 5  |-  ( ph  ->  X  e.  ( F lim
CC  D ) )
31, 2sseldi 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 ) )
64, 5sseldi 3507 . . . 4  |-  ( ph  ->  Y  e.  CC )
73, 6mulcld 9628 . . 3  |-  ( ph  ->  ( X  x.  Y
)  e.  CC )
8 simpr 461 . . . . . 6  |-  ( (
ph  /\  w  e.  RR+ )  ->  w  e.  RR+ )
93adantr 465 . . . . . 6  |-  ( (
ph  /\  w  e.  RR+ )  ->  X  e.  CC )
106adantr 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 ) )
128, 9, 10, 11syl3anc 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 )
1513, 14fmptd 6056 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : A --> CC )
16 fdm 5741 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : A --> CC  ->  dom 
F  =  A )
1715, 16syl 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 ) )
192, 18syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( F : dom  F --> CC  /\  dom  F  C_  CC  /\  D  e.  CC ) )
2019simp2d 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  dom  F  C_  CC )
2117, 20eqsstr3d 3544 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  C_  CC )
2219simp3d 1010 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  D  e.  CC )
2315, 21, 22ellimc3 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 ) ) ) )
242, 23mpbid 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 ) ) )
2524simprd 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 ) )
2625r19.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 ) )
2726adantrr 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 )
3028, 29fmptd 6056 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G : A --> CC )
3130, 21, 22ellimc3 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 ) ) ) )
325, 31mpbid 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 ) ) )
3332simprd 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 ) )
3433r19.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 ) )
3534adantrl 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 ) )
3627, 35jca 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
) ) )
3836, 37sylibr 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+ )
4239, 40, 41syl2anc 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
)
4745, 46nfan 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 ) )
4843, 44, 47nf3an 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+ )
51503ad2ant1 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+ )
5249, 51jca 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+ ) )
5452, 53jca 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 ) )
5654, 55jca 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 ) ) )
5956, 57, 583jca 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 )
62613ad2ant1 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+ ) )
6462, 63jca 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
)
6921sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  A )  ->  z  e.  CC )
7067, 68, 69syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
e  e.  RR+  /\  f  e.  RR+ ) )  /\  z  e.  A  /\  ( abs `  ( z  -  D ) )  <  if ( e  <_  f ,  e ,  f ) )  ->  z  e.  CC )
7167, 22syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
e  e.  RR+  /\  f  e.  RR+ ) )  /\  z  e.  A  /\  ( abs `  ( z  -  D ) )  <  if ( e  <_  f ,  e ,  f ) )  ->  D  e.  CC )
7270, 71subcld 9942 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
e  e.  RR+  /\  f  e.  RR+ ) )  /\  z  e.  A  /\  ( abs `  ( z  -  D ) )  <  if ( e  <_  f ,  e ,  f ) )  ->  ( z  -  D )  e.  CC )
7372abscld 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 )
7574ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( e  e.  RR+  /\  f  e.  RR+ ) )  ->  e  e.  RR )
76753ad2ant1 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 )
7877ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( e  e.  RR+  /\  f  e.  RR+ ) )  ->  f  e.  RR )
79783ad2ant1 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 )
8176, 79, 80syl2anc 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
)
8476, 79, 83syl2anc 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 )
8573, 81, 76, 82, 84ltletrd 9753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
e  e.  RR+  /\  f  e.  RR+ ) )  /\  z  e.  A  /\  ( abs `  ( z  -  D ) )  <  if ( e  <_  f ,  e ,  f ) )  ->  ( abs `  (
z  -  D ) )  <  e )
8664, 65, 66, 85syl3anc 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 )
8760, 86jca 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 ) ) )
9089imp 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 ) )
9188, 65, 90syl2anc 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 ) )
9287, 91mpd 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 )
9359, 92syl 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 )
9594, 50jca 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 ) )
9895, 96, 97jca31 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 ) ) )
99983anim1i 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 )
1021013ad2ant1 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+ ) )
104102, 103jca 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 ) )
107104, 105, 1063jca 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
)
10976, 79, 108syl2anc 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 )
11073, 81, 79, 82, 109ltletrd 9753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
e  e.  RR+  /\  f  e.  RR+ ) )  /\  z  e.  A  /\  ( abs `  ( z  -  D ) )  <  if ( e  <_  f ,  e ,  f ) )  ->  ( abs `  (
z  -  D ) )  <  f )
111107, 110syl 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 )
112100, 111jca 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 ) ) )
115114imp 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 ) )
116113, 105, 115syl2anc 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 ) )
117112, 116mpd 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 )
11899, 117syl 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
)
11993, 118jca 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
) )
1201193exp 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 ) ) ) )
12148, 120ralrimi 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 ) ) )
124123anbi2d 703 . . . . . . . . . . . . . . . . 17  |-  ( y  =  if ( e  <_  f ,  e ,  f )  -> 
( ( z  =/= 
D  /\  ( abs `  ( z  -  D
) )  <  y
)  <->  ( z  =/= 
D  /\  ( abs `  ( z  -  D
) )  <  if ( e  <_  f ,  e ,  f ) ) ) )
125124imbi1d 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 ) ) ) )
126122, 125ralbid 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 ) ) ) )
127126rspcev 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 ) ) )
12842, 121, 127syl2anc 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 ) ) )
1291283exp 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 ) ) ) ) )
130129rexlimdvv 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 ) ) ) )
13138, 130mpd 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 ) ) )
132131adantlr 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 ) ) )
1331323adant3 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
) )
136134, 135nfan 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 )
138137ad2antrr 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 )
1391383ad2ant1 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
) )
144142, 143nfcxfr 2627 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x H
145 nfcv 2629 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
z
146144, 145nffv 5879 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( H `  z
)
147 nfmpt1 4542 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x
( x  e.  A  |->  B )
14814, 147nfcxfr 2627 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x F
149148, 145nffv 5879 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( F `  z
)
150 nfcv 2629 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x  x.
151 nfmpt1 4542 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x
( x  e.  A  |->  C )
15229, 151nfcxfr 2627 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x G
153152, 145nffv 5879 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( G `  z
)
154149, 150, 153nfov 6318 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( ( F `  z )  x.  ( G `  z )
)
155146, 154nfeq 2640 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( H `  z
)  =  ( ( F `  z )  x.  ( G `  z ) )
156141, 155nfim 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 ) )
158157anbi2d 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 ) )
162160, 161oveq12d 6313 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  (
( F `  x
)  x.  ( G `
 x ) )  =  ( ( F `
 z )  x.  ( G `  z
) ) )
163159, 162eqeq12d 2489 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
( H `  x
)  =  ( ( F `  x )  x.  ( G `  x ) )  <->  ( H `  z )  =  ( ( F `  z
)  x.  ( G `
 z ) ) ) )
164158, 163imbi12d 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 )
16613, 28mulcld 9628 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( B  x.  C )  e.  CC )
167142fvmpt2 5964 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  A  /\  ( B  x.  C
)  e.  CC )  ->  ( H `  x )  =  ( B  x.  C ) )
168165, 166, 167syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( B  x.  C ) )
16914fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  A  /\  B  e.  CC )  ->  ( F `  x
)  =  B )
170165, 13, 169syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  B )
171170eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  B  =  ( F `  x ) )
17229fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  A  /\  C  e.  CC )  ->  ( G `  x
)  =  C )
173165, 28, 172syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  ( G `  x )  =  C )
174173eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  C  =  ( G `  x ) )
175171, 174oveq12d 6313 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( B  x.  C )  =  ( ( F `
 x )  x.  ( G `  x
) ) )
176168, 175eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( ( F `
 x )  x.  ( G `  x
) ) )
177156, 164, 176chvar 1982 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  A )  ->  ( H `  z )  =  ( ( F `
 z )  x.  ( G `  z
) ) )
178177oveq1d 6310 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  A )  ->  (
( H `  z
)  -  ( X  x.  Y ) )  =  ( ( ( F `  z )  x.  ( G `  z ) )  -  ( X  x.  Y
) ) )
179178fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  A )  ->  ( abs `  ( ( H `
 z )  -  ( X  x.  Y
) ) )  =  ( abs `  (
( ( F `  z )  x.  ( G `  z )
)  -  ( X  x.  Y ) ) ) )
180139, 140, 179syl2anc 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
182149, 181nfel 2642 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( F `  z
)  e.  CC
183141, 182nfim 1867 . . . . . . . . . . . . . . . . 17  |-  F/ x
( ( ph  /\  z  e.  A )  ->  ( F `  z
)  e.  CC )
184160eleq1d 2536 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
( F `  x
)  e.  CC  <->  ( F `  z )  e.  CC ) )
185158, 184imbi12d 320 . . . . . . . . . . . . . . . . 17  |-  ( x  =  z  ->  (
( ( ph  /\  x  e.  A )  ->  ( F `  x
)  e.  CC )  <-> 
( ( ph  /\  z  e.  A )  ->  ( F `  z
)  e.  CC ) ) )
18615ffvelrnda 6032 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  e.  CC )
187183, 185, 186chvar 1982 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  e.  CC )
18830ffvelrnda 6032 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  z  e.  A )  ->  ( G `  z )  e.  CC )
189187, 188jca 532 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  A )  ->  (
( F `  z
)  e.  CC  /\  ( G `  z )  e.  CC ) )
190139, 140, 189syl2anc 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 ) )
1921913ad2ant1 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 ) ) ) )
194193imp 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 ) ) )
1951943adant3 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 ) ) )
1971963ad2ant3 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 ) ) )
198195, 197mpd 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 ) )
1991983adant1l 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 ) )
201200fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ( F `  z )  ->  ( abs `  ( c  -  X ) )  =  ( abs `  (
( F `  z
)  -  X ) ) )
202201breq1d 4463 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ( F `  z )  ->  (
( abs `  (
c  -  X ) )  <  a  <->  ( abs `  ( ( F `  z )  -  X
) )  <  a
) )
203202anbi1d 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 ) )
205204oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( c  =  ( F `  z )  ->  (
( c  x.  d
)  -  ( X  x.  Y ) )  =  ( ( ( F `  z )  x.  d )  -  ( X  x.  Y
) ) )
206205fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( c  =  ( F `  z )  ->  ( abs `  ( ( c  x.  d )  -  ( X  x.  Y
) ) )  =  ( abs `  (
( ( F `  z )  x.  d
)  -  ( X  x.  Y ) ) ) )
207206breq1d 4463 . . . . . . . . . . . . . . . 16  |-  ( c  =  ( F `  z )  ->  (
( abs `  (
( c  x.  d
)  -  ( X  x.  Y ) ) )  <  w  <->  ( abs `  ( ( ( F `
 z )  x.  d )  -  ( X  x.  Y )
) )  <  w
) )
208203, 207imbi12d 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 ) )
210209fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  ( G `  z )  ->  ( abs `  ( d  -  Y ) )  =  ( abs `  (
( G `  z
)  -  Y ) ) )
211210breq1d 4463 . . . . . . . . . . . . . . . . 17  |-  ( d  =  ( G `  z )  ->  (
( abs `  (
d  -  Y ) )  <  b  <->  ( abs `  ( ( G `  z )  -  Y
) )  <  b
) )
212211anbi2d 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
) ) )
214213oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  ( G `  z )  ->  (
( ( F `  z )  x.  d
)  -  ( X  x.  Y ) )  =  ( ( ( F `  z )  x.  ( G `  z ) )  -  ( X  x.  Y
) ) )
215214fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( d  =  ( G `  z )  ->  ( abs `  ( ( ( F `  z )  x.  d )  -  ( X  x.  Y
) ) )  =  ( abs `  (
( ( F `  z )  x.  ( G `  z )
)  -  ( X  x.  Y ) ) ) )
216215breq1d 4463 . . . . . . . . . . . . . . . 16  |-  ( d  =  ( G `  z )  ->  (
( abs `  (
( ( F `  z )  x.  d
)  -  ( X  x.  Y ) ) )  <  w  <->  ( abs `  ( ( ( F `
 z )  x.  ( G `  z
) )  -  ( X  x.  Y )
) )  <  w
) )
217212, 216imbi12d 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 ) ) )
218208, 217rspc2v 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 ) ) )
219190, 192, 199, 218syl3c 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 )
220180, 219eqbrtrd 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 )
2212203exp 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 ) ) )
222136, 221ralrimi 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 ) )
223222ex 434 . . . . . . . . 9  |-  ( ( ( ( ph  /\  w  e.  RR+ )  /\  ( a  e.