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

Theorem 0ellimcdiv 31514
Description: If the numerator converges to 0 and the denominator converges to non zero then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
0ellimcdiv.f  |-  F  =  ( x  e.  A  |->  B )
0ellimcdiv.g  |-  G  =  ( x  e.  A  |->  C )
0ellimcdiv.h  |-  H  =  ( x  e.  A  |->  ( B  /  C
) )
0ellimcdiv.b  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  CC )
0ellimcdiv.c  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  ( CC  \  {
0 } ) )
0ellimcdiv.0limf  |-  ( ph  ->  0  e.  ( F lim
CC  E ) )
0ellimcdiv.d  |-  ( ph  ->  D  e.  ( G lim
CC  E ) )
0ellimcdiv.dne0  |-  ( ph  ->  D  =/=  0 )
Assertion
Ref Expression
0ellimcdiv  |-  ( ph  ->  0  e.  ( H lim
CC  E ) )
Distinct variable groups:    x, A    ph, x
Allowed substitution hints:    B( x)    C( x)    D( x)    E( x)    F( x)    G( x)    H( x)

Proof of Theorem 0ellimcdiv
Dummy variables  u  v  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 9600 . . . 4  |-  0  e.  CC
21a1i 11 . . 3  |-  ( ph  ->  0  e.  CC )
3 0ellimcdiv.d . . . . . . . . . 10  |-  ( ph  ->  D  e.  ( G lim
CC  E ) )
4 0ellimcdiv.c . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  ( CC  \  {
0 } ) )
54eldifad 3493 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  CC )
6 0ellimcdiv.g . . . . . . . . . . . 12  |-  G  =  ( x  e.  A  |->  C )
75, 6fmptd 6056 . . . . . . . . . . 11  |-  ( ph  ->  G : A --> CC )
8 0ellimcdiv.f . . . . . . . . . . . 12  |-  F  =  ( x  e.  A  |->  B )
9 0ellimcdiv.b . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  CC )
10 0ellimcdiv.0limf . . . . . . . . . . . 12  |-  ( ph  ->  0  e.  ( F lim
CC  E ) )
118, 9, 10limcmptdm 31500 . . . . . . . . . . 11  |-  ( ph  ->  A  C_  CC )
12 limcrcl 22146 . . . . . . . . . . . . 13  |-  ( D  e.  ( G lim CC  E )  ->  ( G : dom  G --> CC  /\  dom  G  C_  CC  /\  E  e.  CC ) )
133, 12syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( G : dom  G --> CC  /\  dom  G  C_  CC  /\  E  e.  CC ) )
1413simp3d 1010 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  CC )
157, 11, 14ellimc3 22151 . . . . . . . . . 10  |-  ( ph  ->  ( D  e.  ( G lim CC  E )  <-> 
( D  e.  CC  /\ 
A. y  e.  RR+  E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  y ) ) ) )
163, 15mpbid 210 . . . . . . . . 9  |-  ( ph  ->  ( D  e.  CC  /\ 
A. y  e.  RR+  E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  y ) ) )
1716simprd 463 . . . . . . . 8  |-  ( ph  ->  A. y  e.  RR+  E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  y ) )
1816simpld 459 . . . . . . . . . 10  |-  ( ph  ->  D  e.  CC )
19 0ellimcdiv.dne0 . . . . . . . . . 10  |-  ( ph  ->  D  =/=  0 )
2018, 19absrpcld 13259 . . . . . . . . 9  |-  ( ph  ->  ( abs `  D
)  e.  RR+ )
2120rphalfcld 11280 . . . . . . . 8  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  RR+ )
22 breq2 4457 . . . . . . . . . . . 12  |-  ( y  =  ( ( abs `  D )  /  2
)  ->  ( ( abs `  ( ( G `
 v )  -  D ) )  < 
y  <->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) )
2322imbi2d 316 . . . . . . . . . . 11  |-  ( y  =  ( ( abs `  D )  /  2
)  ->  ( (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  y )  <-> 
( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) ) )
2423ralbidv 2906 . . . . . . . . . 10  |-  ( y  =  ( ( abs `  D )  /  2
)  ->  ( A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  y )  <->  A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) ) )
2524rexbidv 2978 . . . . . . . . 9  |-  ( y  =  ( ( abs `  D )  /  2
)  ->  ( E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  y )  <->  E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) ) )
2625rspccva 3218 . . . . . . . 8  |-  ( ( A. y  e.  RR+  E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  y )  /\  ( ( abs `  D )  /  2
)  e.  RR+ )  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) )
2717, 21, 26syl2anc 661 . . . . . . 7  |-  ( ph  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) )
28 nfv 1683 . . . . . . . 8  |-  F/ z
ph
29 simpl1l 1047 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  ph )
30 simpl3 1001 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  v  e.  A
)
31 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
) )
32 simpl2 1000 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  ( v  e.  A  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) ) )
3330, 32mpd 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  ( abs `  ( ( G `
 v )  -  D ) )  < 
( ( abs `  D
)  /  2 ) ) )
3431, 33mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )
3520rpcnd 11270 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( abs `  D
)  e.  CC )
36352halvesd 10796 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( abs `  D )  /  2
)  +  ( ( abs `  D )  /  2 ) )  =  ( abs `  D
) )
3736eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  D
)  =  ( ( ( abs `  D
)  /  2 )  +  ( ( abs `  D )  /  2
) ) )
3837oveq1d 6310 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( ( ( abs `  D
)  /  2 )  +  ( ( abs `  D )  /  2
) )  -  (
( abs `  D
)  /  2 ) ) )
3921rpcnd 11270 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  CC )
4039, 39pncand 9943 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( abs `  D )  /  2 )  +  ( ( abs `  D
)  /  2 ) )  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  /  2
) )
4138, 40eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  /  2
) )
4241eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) ) )
43 2cn 10618 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  CC
4443a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  2  e.  CC )
45 2ne0 10640 . . . . . . . . . . . . . . . . . . . 20  |-  2  =/=  0
4645a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  2  =/=  0 )
4718, 44, 46absdivd 13266 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  ( abs `  2 ) ) )
48 2re 10617 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
4948a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  2  e.  RR )
50 2pos 10639 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  <  2
51 0re 9608 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR
5251, 48ltlei 9718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  <  2  ->  0  <_  2 )
5350, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  2
5453a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  2 )
5549, 54absidd 13234 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  2
)  =  2 )
5655oveq2d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( abs `  D
)  /  ( abs `  2 ) )  =  ( ( abs `  D )  /  2
) )
5747, 56eqtr2d 2509 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( abs `  ( D  /  2 ) ) )
5857oveq2d 6311 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) ) )
5942, 58eqtrd 2508 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) ) )
60593ad2ant1 1017 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  =  ( ( abs `  D )  -  ( abs `  ( D  /  2 ) ) ) )
6157eqcomd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  2
) )
62613ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  2
) )
6362oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) )  =  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) ) )
6418adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A )  ->  D  e.  CC )
6564abscld 13247 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  e.  RR )
66653adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  e.  RR )
677ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  v  e.  A )  ->  ( G `  v )  e.  CC )
68673adant3 1016 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( G `  v )  e.  CC )
6968abscld 13247 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( G `  v )
)  e.  RR )
70643adant3 1016 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  D  e.  CC )
7170, 68subcld 9942 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( D  -  ( G `  v ) )  e.  CC )
7271abscld 13247 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  e.  RR )
7369, 72readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( abs `  ( D  -  ( G `  v ) ) ) )  e.  RR )
7466rehalfcld 10797 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  e.  RR )
7569, 74readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( ( abs `  D
)  /  2 ) )  e.  RR )
7667, 64pncan3d 9945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  v  e.  A )  ->  (
( G `  v
)  +  ( D  -  ( G `  v ) ) )  =  D )
7776eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  v  e.  A )  ->  D  =  ( ( G `
 v )  +  ( D  -  ( G `  v )
) ) )
7877fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  =  ( abs `  (
( G `  v
)  +  ( D  -  ( G `  v ) ) ) ) )
7964, 67subcld 9942 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  v  e.  A )  ->  ( D  -  ( G `  v ) )  e.  CC )
8067, 79abstrid 13267 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( G `
 v )  +  ( D  -  ( G `  v )
) ) )  <_ 
( ( abs `  ( G `  v )
)  +  ( abs `  ( D  -  ( G `  v )
) ) ) )
8178, 80eqbrtrd 4473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  <_ 
( ( abs `  ( G `  v )
)  +  ( abs `  ( D  -  ( G `  v )
) ) ) )
82813adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  <_  ( ( abs `  ( G `  v ) )  +  ( abs `  ( D  -  ( G `  v ) ) ) ) )
8370, 68abssubd 13264 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  =  ( abs `  (
( G `  v
)  -  D ) ) )
84 simp3 998 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )
8583, 84eqbrtrd 4473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  <  ( ( abs `  D )  /  2
) )
8672, 74, 69, 85ltadd2dd 9752 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( abs `  ( D  -  ( G `  v ) ) ) )  <  ( ( abs `  ( G `
 v ) )  +  ( ( abs `  D )  /  2
) ) )
8766, 73, 75, 82, 86lelttrd 9751 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  <  ( ( abs `  ( G `  v ) )  +  ( ( abs `  D
)  /  2 ) ) )
8867abscld 13247 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR )
89883adant3 1016 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( G `  v )
)  e.  RR )
9066, 74, 89ltsubaddd 10160 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( ( abs `  D )  -  ( ( abs `  D )  /  2
) )  <  ( abs `  ( G `  v ) )  <->  ( abs `  D )  <  (
( abs `  ( G `  v )
)  +  ( ( abs `  D )  /  2 ) ) ) )
9187, 90mpbird 232 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) )  <  ( abs `  ( G `  v
) ) )
9263, 91eqbrtrd 4473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) )  <  ( abs `  ( G `  v )
) )
9360, 92eqbrtrd 4473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) )
9429, 30, 34, 93syl3anc 1228 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  z  e.  RR+ )  /\  ( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) )
9594ex 434 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  RR+ )  /\  (
v  e.  A  -> 
( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  /\  v  e.  A )  ->  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )
96953exp 1195 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  RR+ )  ->  ( (
v  e.  A  -> 
( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) ) )  ->  (
v  e.  A  -> 
( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) ) ) ) )
9796ralimdv2 2874 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  RR+ )  ->  ( A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) ) ) )
9897ex 434 . . . . . . . 8  |-  ( ph  ->  ( z  e.  RR+  ->  ( A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  ( abs `  ( ( G `
 v )  -  D ) )  < 
( ( abs `  D
)  /  2 ) )  ->  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) ) ) )
9928, 98reximdai 2936 . . . . . . 7  |-  ( ph  ->  ( E. z  e.  RR+  A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( abs `  ( ( G `  v )  -  D
) )  <  (
( abs `  D
)  /  2 ) )  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) ) )
10027, 99mpd 15 . . . . . 6  |-  ( ph  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )
101100adantr 465 . . . . 5  |-  ( (
ph  /\  y  e.  RR+ )  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )
102 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR+ )  ->  y  e.  RR+ )
10318adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR+ )  ->  D  e.  CC )
10419adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR+ )  ->  D  =/=  0 )
105103, 104absrpcld 13259 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( abs `  D )  e.  RR+ )
106105rphalfcld 11280 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( ( abs `  D )  / 
2 )  e.  RR+ )
107102, 106rpmulcld 11284 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )
108107ex 434 . . . . . . . . . . 11  |-  ( ph  ->  ( y  e.  RR+  ->  ( y  x.  (
( abs `  D
)  /  2 ) )  e.  RR+ )
)
109108imdistani 690 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( ph  /\  ( y  x.  (
( abs `  D
)  /  2 ) )  e.  RR+ )
)
110 eleq1 2539 . . . . . . . . . . . . 13  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( w  e.  RR+  <->  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )
)
111110anbi2d 703 . . . . . . . . . . . 12  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( ( ph  /\  w  e.  RR+ ) 
<->  ( ph  /\  (
y  x.  ( ( abs `  D )  /  2 ) )  e.  RR+ ) ) )
112 breq2 4457 . . . . . . . . . . . . . 14  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( ( abs `  ( ( F `
 v )  - 
0 ) )  < 
w  <->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
113112imbi2d 316 . . . . . . . . . . . . 13  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  w )  <-> 
( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) ) )
114113rexralbidv 2986 . . . . . . . . . . . 12  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  w )  <->  E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) ) )
115111, 114imbi12d 320 . . . . . . . . . . 11  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( (
( ph  /\  w  e.  RR+ )  ->  E. u  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
u )  ->  ( abs `  ( ( F `
 v )  - 
0 ) )  < 
w ) )  <->  ( ( ph  /\  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )  ->  E. u  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) ) ) )
1169, 8fmptd 6056 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> CC )
117116, 11, 14ellimc3 22151 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  e.  ( F lim CC  E )  <-> 
( 0  e.  CC  /\ 
A. w  e.  RR+  E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  w ) ) ) )
11810, 117mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  e.  CC  /\ 
A. w  e.  RR+  E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  w ) ) )
119118simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  A. w  e.  RR+  E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  w ) )
120119r19.21bi 2836 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  RR+ )  ->  E. u  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
u )  ->  ( abs `  ( ( F `
 v )  - 
0 ) )  < 
w ) )
121115, 120vtoclg 3176 . . . . . . . . . 10  |-  ( ( y  x.  ( ( abs `  D )  /  2 ) )  e.  RR+  ->  ( (
ph  /\  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )  ->  E. u  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) ) )
122107, 109, 121sylc 60 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR+ )  ->  E. u  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
u )  ->  ( abs `  ( ( F `
 v )  - 
0 ) )  < 
( y  x.  (
( abs `  D
)  /  2 ) ) ) )
1231223ad2ant1 1017 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  ->  E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
124 simp12 1027 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  ->  z  e.  RR+ )
125 simp2 997 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  ->  u  e.  RR+ )
126 ifcl 3987 . . . . . . . . . . . 12  |-  ( ( z  e.  RR+  /\  u  e.  RR+ )  ->  if ( z  <_  u ,  z ,  u
)  e.  RR+ )
127124, 125, 126syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  ->  if ( z  <_  u ,  z ,  u
)  e.  RR+ )
128 nfv 1683 . . . . . . . . . . . . . 14  |-  F/ v ( ph  /\  y  e.  RR+ )
129 nfv 1683 . . . . . . . . . . . . . 14  |-  F/ v  z  e.  RR+
130 nfra1 2848 . . . . . . . . . . . . . 14  |-  F/ v A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )
131128, 129, 130nf3an 1877 . . . . . . . . . . . . 13  |-  F/ v ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )
132 nfv 1683 . . . . . . . . . . . . 13  |-  F/ v  u  e.  RR+
133 nfra1 2848 . . . . . . . . . . . . 13  |-  F/ v A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )
134131, 132, 133nf3an 1877 . . . . . . . . . . . 12  |-  F/ v ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )
135 simp111 1125 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( ph  /\  y  e.  RR+ )
)
136 simp112 1126 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  z  e.  RR+ )
137 simp12 1027 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  u  e.  RR+ )
138135, 136, 137jca31 534 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ ) )
139 simp2 997 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  v  e.  A )
140 simp3l 1024 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  v  =/=  E )
141138, 139, 140jca31 534 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A
)  /\  v  =/=  E ) )
142 simp113 1127 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )
143 rsp 2833 . . . . . . . . . . . . . . . . . 18  |-  ( A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) )  -> 
( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) ) ) )
144143imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  v  e.  A
)  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )
145142, 139, 144syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )
14611adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  RR+ )  ->  A  C_  CC )
1471463ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  ->  A  C_  CC )
1481473ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  ->  A  C_  CC )
1491483ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  A  C_  CC )
150149, 139sseldd 3510 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  v  e.  CC )
15114adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  RR+ )  ->  E  e.  CC )
1521513ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  ->  E  e.  CC )
1531523ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  ->  E  e.  CC )
1541533ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  E  e.  CC )
155150, 154subcld 9942 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( v  -  E )  e.  CC )
156155abscld 13247 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( v  -  E
) )  e.  RR )
157136rpred 11268 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  z  e.  RR )
158137rpred 11268 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  u  e.  RR )
159157, 158ifcld 3988 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  if (
z  <_  u , 
z ,  u )  e.  RR )
160 simp3r 1025 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( v  -  E
) )  <  if ( z  <_  u ,  z ,  u
) )
161 min1 11401 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  RR  /\  u  e.  RR )  ->  if ( z  <_  u ,  z ,  u )  <_  z
)
162157, 158, 161syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  if (
z  <_  u , 
z ,  u )  <_  z )
163156, 159, 157, 160, 162ltletrd 9753 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( v  -  E
) )  <  z
)
164140, 163jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( v  =/=  E  /\  ( abs `  ( v  -  E
) )  <  z
) )
165 simpl 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
) )  ->  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )
166 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
) )  ->  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z ) )
167166, 165mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
) )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) )
168165, 166, 167syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
) )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) )
169145, 164, 168syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )
170 min2 11402 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  RR  /\  u  e.  RR )  ->  if ( z  <_  u ,  z ,  u )  <_  u
)
171157, 158, 170syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  if (
z  <_  u , 
z ,  u )  <_  u )
172156, 159, 158, 160, 171ltletrd 9753 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( v  -  E
) )  <  u
)
173140, 172jca 532 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( v  =/=  E  /\  ( abs `  ( v  -  E
) )  <  u
) )
174 simp13 1028 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
175 rsp 2833 . . . . . . . . . . . . . . . . . . 19  |-  ( A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  -> 
( v  e.  A  ->  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) ) )
176175imp 429 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )  /\  v  e.  A )  ->  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
177174, 139, 176syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
178135simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ph )
1791783ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ph )
1801393ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  v  e.  A )
181 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ x
( ph  /\  v  e.  A )
182 nfmpt1 4542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/_ x
( x  e.  A  |->  B )
1838, 182nfcxfr 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ x F
184 nfcv 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ x
v
185183, 184nffv 5879 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ x
( F `  v
)
186185nfel1 2645 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ x
( F `  v
)  e.  CC
187181, 186nfim 1867 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( F `  v
)  e.  CC )
188 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  v  ->  (
x  e.  A  <->  v  e.  A ) )
189188anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  v  ->  (
( ph  /\  x  e.  A )  <->  ( ph  /\  v  e.  A ) ) )
190 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  v  ->  ( F `  x )  =  ( F `  v ) )
191190eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  v  ->  (
( F `  x
)  e.  CC  <->  ( F `  v )  e.  CC ) )
192189, 191imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( F `  x
)  e.  CC )  <-> 
( ( ph  /\  v  e.  A )  ->  ( F `  v
)  e.  CC ) ) )
193 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
1948fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  A  /\  B  e.  CC )  ->  ( F `  x
)  =  B )
195193, 9, 194syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  B )
196195, 9eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  e.  CC )
197187, 192, 196chvar 1982 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  v  e.  A )  ->  ( F `  v )  e.  CC )
198197subid1d 9931 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  v  e.  A )  ->  (
( F `  v
)  -  0 )  =  ( F `  v ) )
199198eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  v  e.  A )  ->  ( F `  v )  =  ( ( F `
 v )  - 
0 ) )
200199fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( F `  v ) )  =  ( abs `  (
( F `  v
)  -  0 ) ) )
201179, 180, 200syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ( abs `  ( F `  v
) )  =  ( abs `  ( ( F `  v )  -  0 ) ) )
202 simp3 998 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ( v  =/=  E  /\  ( abs `  ( v  -  E
) )  <  u
) )
203 simp2 997 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
204202, 203mpd 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )
205201, 204eqbrtrd 4473 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )  /\  u  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )  /\  v  e.  A  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  if ( z  <_  u , 
z ,  u ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ( abs `  ( F `  v
) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )
2062053exp 1195 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  -> 
( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( F `  v
) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) ) )
207177, 206mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) ) )
208173, 207mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( F `  v
) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )
209141, 169, 208jca31 534 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+  /\  A. v  e.  A  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )  /\  u  e.  RR+  /\ 
A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E )  /\  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) )  /\  ( abs `  ( F `  v ) )  < 
( y  x.  (
( abs `  D
)  /  2 ) ) ) )
210 simp-7l 771 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ph )
211 simp-4r 766 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  v  e.  A )
212 eldifsni 4159 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( C  e.  ( CC  \  { 0 } )  ->  C  =/=  0
)
2134, 212syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  A )  ->  C  =/=  0 )
2149, 5, 213divcld 10332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  A )  ->  ( B  /  C )  e.  CC )
215 0ellimcdiv.h . . . . . . . . . . . . . . . . . . . . 21  |-  H  =  ( x  e.  A  |->  ( B  /  C
) )
216214, 215fmptd 6056 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  H : A --> CC )
217216ffvelrnda 6032 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  v  e.  A )  ->  ( H `  v )  e.  CC )
218217subid1d 9931 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  (
( H `  v
)  -  0 )  =  ( H `  v ) )
219 nfmpt1 4542 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ x
( x  e.  A  |->  ( B  /  C
) )
220215, 219nfcxfr 2627 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x H
221220, 184nffv 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x
( H `  v
)
222 nfcv 2629 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x  /
223 nfmpt1 4542 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ x
( x  e.  A  |->  C )
2246, 223nfcxfr 2627 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ x G
225224, 184nffv 5879 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x
( G `  v
)
226185, 222, 225nfov 6318 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x
( ( F `  v )  /  ( G `  v )
)
227221, 226nfeq 2640 . . . . . . . . . . . . . . . . . . . 20  |-  F/ x
( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) )
228181, 227nfim 1867 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) ) )
229 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  v  ->  ( H `  x )  =  ( H `  v ) )
230 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  v  ->  ( G `  x )  =  ( G `  v ) )
231190, 230oveq12d 6313 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  v  ->  (
( F `  x
)  /  ( G `
 x ) )  =  ( ( F `
 v )  / 
( G `  v
) ) )
232229, 231eqeq12d 2489 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  v  ->  (
( H `  x
)  =  ( ( F `  x )  /  ( G `  x ) )  <->  ( H `  v )  =  ( ( F `  v
)  /  ( G `
 v ) ) ) )
233189, 232imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( H `  x
)  =  ( ( F `  x )  /  ( G `  x ) ) )  <-> 
( ( ph  /\  v  e.  A )  ->  ( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) ) ) ) )
234215fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  A  /\  ( B  /  C
)  e.  CC )  ->  ( H `  x )  =  ( B  /  C ) )
235193, 214, 234syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( B  /  C ) )
236195eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  A )  ->  B  =  ( F `  x ) )
2376fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  A  /\  C  e.  ( CC  \  { 0 } ) )  ->  ( G `  x )  =  C )
238193, 4, 237syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  A )  ->  ( G `  x )  =  C )
239238eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  A )  ->  C  =  ( G `  x ) )
240236, 239oveq12d 6313 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  ( B  /  C )  =  ( ( F `  x )  /  ( G `  x )
) )
241235, 240eqtrd 2508 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( ( F `
 x )  / 
( G `  x
) ) )
242228, 233, 241chvar 1982 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( H `  v )  =  ( ( F `
 v )  / 
( G `  v
) ) )
243218, 242eqtrd 2508 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  (
( H `  v
)  -  0 )  =  ( ( F `
 v )  / 
( G `  v
) ) )
244243fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( H `
 v )  - 
0 ) )  =  ( abs `  (
( F `  v
)  /  ( G `
 v ) ) ) )
245210, 211, 244syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ( abs `  ( ( H `
 v )  - 
0 ) )  =  ( abs `  (
( F `  v
)  /  ( G `
 v ) ) ) )
246 simp-6l 769 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ( ph  /\  y  e.  RR+ ) )
247246, 211jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  (
( ph  /\  y  e.  RR+ )  /\  v  e.  A ) )
248 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ )  /\  v  e.  A )  /\  v  =/=  E
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `