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

Theorem 0ellimcdiv 31837
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 0cnd 9606 . 2  |-  ( ph  ->  0  e.  CC )
2 0ellimcdiv.d . . . . . . . . 9  |-  ( ph  ->  D  e.  ( G lim
CC  E ) )
3 0ellimcdiv.c . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  ( CC  \  {
0 } ) )
43eldifad 3483 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  CC )
5 0ellimcdiv.g . . . . . . . . . . 11  |-  G  =  ( x  e.  A  |->  C )
64, 5fmptd 6056 . . . . . . . . . 10  |-  ( ph  ->  G : A --> CC )
7 0ellimcdiv.f . . . . . . . . . . 11  |-  F  =  ( x  e.  A  |->  B )
8 0ellimcdiv.b . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  CC )
9 0ellimcdiv.0limf . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( F lim
CC  E ) )
107, 8, 9limcmptdm 31823 . . . . . . . . . 10  |-  ( ph  ->  A  C_  CC )
11 limcrcl 22404 . . . . . . . . . . . 12  |-  ( D  e.  ( G lim CC  E )  ->  ( G : dom  G --> CC  /\  dom  G  C_  CC  /\  E  e.  CC ) )
122, 11syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( G : dom  G --> CC  /\  dom  G  C_  CC  /\  E  e.  CC ) )
1312simp3d 1010 . . . . . . . . . 10  |-  ( ph  ->  E  e.  CC )
146, 10, 13ellimc3 22409 . . . . . . . . 9  |-  ( 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 ) ) ) )
152, 14mpbid 210 . . . . . . . 8  |-  ( 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 ) ) )
1615simprd 463 . . . . . . 7  |-  ( ph  ->  A. y  e.  RR+  E. z  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  y ) )
1715simpld 459 . . . . . . . . 9  |-  ( ph  ->  D  e.  CC )
18 0ellimcdiv.dne0 . . . . . . . . 9  |-  ( ph  ->  D  =/=  0 )
1917, 18absrpcld 13291 . . . . . . . 8  |-  ( ph  ->  ( abs `  D
)  e.  RR+ )
2019rphalfcld 11293 . . . . . . 7  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  RR+ )
21 breq2 4460 . . . . . . . . . 10  |-  ( y  =  ( ( abs `  D )  /  2
)  ->  ( ( abs `  ( ( G `
 v )  -  D ) )  < 
y  <->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) )
2221imbi2d 316 . . . . . . . . 9  |-  ( 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 ) ) ) )
2322rexralbidv 2976 . . . . . . . 8  |-  ( 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 ) ) ) )
2423rspccva 3209 . . . . . . 7  |-  ( ( 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 ) ) )
2516, 20, 24syl2anc 661 . . . . . 6  |-  ( ph  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) )
26 simpl1l 1047 . . . . . . . . . 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 ) )  ->  ph )
27 simpl3 1001 . . . . . . . . . 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 ) )  ->  v  e.  A
)
28 simpr 461 . . . . . . . . . . 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 ) )  ->  ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
) )
29 simpl2 1000 . . . . . . . . . . 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 ) )  ->  ( v  e.  A  ->  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  z )  -> 
( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) ) )
3027, 28, 29mp2d 45 . . . . . . . . . 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 `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )
3119rpcnd 11283 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  D
)  e.  CC )
32312halvesd 10805 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( abs `  D )  /  2
)  +  ( ( abs `  D )  /  2 ) )  =  ( abs `  D
) )
3332eqcomd 2465 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( abs `  D
)  =  ( ( ( abs `  D
)  /  2 )  +  ( ( abs `  D )  /  2
) ) )
3433oveq1d 6311 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( ( ( abs `  D
)  /  2 )  +  ( ( abs `  D )  /  2
) )  -  (
( abs `  D
)  /  2 ) ) )
35 2cnd 10629 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  2  e.  CC )
36 2ne0 10649 . . . . . . . . . . . . . . . . 17  |-  2  =/=  0
3736a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  2  =/=  0 )
3817, 35, 37absdivd 13298 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  ( abs `  2 ) ) )
39 2re 10626 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
4039a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  2  e.  RR )
41 0le2 10647 . . . . . . . . . . . . . . . . . 18  |-  0  <_  2
4241a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <_  2 )
4340, 42absidd 13266 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  2
)  =  2 )
4443oveq2d 6312 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  D
)  /  ( abs `  2 ) )  =  ( ( abs `  D )  /  2
) )
4538, 44eqtr2d 2499 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( abs `  ( D  /  2 ) ) )
4645oveq2d 6312 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) ) )
4720rpcnd 11283 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  CC )
4847, 47pncand 9951 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( abs `  D )  /  2 )  +  ( ( abs `  D
)  /  2 ) )  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  /  2
) )
4934, 46, 483eqtr3rd 2507 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) ) )
50493ad2ant1 1017 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  =  ( ( abs `  D )  -  ( abs `  ( D  /  2 ) ) ) )
5145eqcomd 2465 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  2
) )
52513ad2ant1 1017 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  2
) )
5352oveq2d 6312 . . . . . . . . . . . 12  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) )  =  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) ) )
5417adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  D  e.  CC )
5554abscld 13279 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  e.  RR )
56553adant3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  e.  RR )
576ffvelrnda 6032 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( G `  v )  e.  CC )
58573adant3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( G `  v )  e.  CC )
5958abscld 13279 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( G `  v )
)  e.  RR )
60173ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  D  e.  CC )
6160, 58subcld 9950 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( D  -  ( G `  v ) )  e.  CC )
6261abscld 13279 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  e.  RR )
6359, 62readdcld 9640 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( abs `  ( D  -  ( G `  v ) ) ) )  e.  RR )
6456rehalfcld 10806 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  e.  RR )
6559, 64readdcld 9640 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( ( abs `  D
)  /  2 ) )  e.  RR )
6657, 54pncan3d 9953 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  (
( G `  v
)  +  ( D  -  ( G `  v ) ) )  =  D )
6766eqcomd 2465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  D  =  ( ( G `
 v )  +  ( D  -  ( G `  v )
) ) )
6867fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  =  ( abs `  (
( G `  v
)  +  ( D  -  ( G `  v ) ) ) ) )
6954, 57subcld 9950 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( D  -  ( G `  v ) )  e.  CC )
7057, 69abstrid 13299 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( G `
 v )  +  ( D  -  ( G `  v )
) ) )  <_ 
( ( abs `  ( G `  v )
)  +  ( abs `  ( D  -  ( G `  v )
) ) ) )
7168, 70eqbrtrd 4476 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  <_ 
( ( abs `  ( G `  v )
)  +  ( abs `  ( D  -  ( G `  v )
) ) ) )
72713adant3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  <_  ( ( abs `  ( G `  v ) )  +  ( abs `  ( D  -  ( G `  v ) ) ) ) )
7360, 58abssubd 13296 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  =  ( abs `  (
( G `  v
)  -  D ) ) )
74 simp3 998 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )
7573, 74eqbrtrd 4476 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  <  ( ( abs `  D )  /  2
) )
7662, 64, 59, 75ltadd2dd 9758 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( abs `  ( D  -  ( G `  v ) ) ) )  <  ( ( abs `  ( G `
 v ) )  +  ( ( abs `  D )  /  2
) ) )
7756, 63, 65, 72, 76lelttrd 9757 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  <  ( ( abs `  ( G `  v ) )  +  ( ( abs `  D
)  /  2 ) ) )
7857abscld 13279 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR )
79783adant3 1016 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( G `  v )
)  e.  RR )
8056, 64, 79ltsubaddd 10169 . . . . . . . . . . . . 13  |-  ( (
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 ) ) ) )
8177, 80mpbird 232 . . . . . . . . . . . 12  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) )  <  ( abs `  ( G `  v
) ) )
8253, 81eqbrtrd 4476 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) )  <  ( abs `  ( G `  v )
) )
8350, 82eqbrtrd 4476 . . . . . . . . . 10  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) )
8426, 27, 30, 83syl3anc 1228 . . . . . . . . 9  |-  ( ( ( ( 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
) ) )
85843exp1 1212 . . . . . . . 8  |-  ( (
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 ) ) ) ) ) )
8685ralimdv2 2864 . . . . . . 7  |-  ( (
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 ) ) ) ) )
8786reximdva 2932 . . . . . 6  |-  ( 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 )
) ) ) )
8825, 87mpd 15 . . . . 5  |-  ( ph  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  z )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) ) )
8988adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  RR+ )  ->  E. z  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
z )  ->  (
( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) ) )
90 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR+ )  ->  y  e.  RR+ )
9117adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR+ )  ->  D  e.  CC )
9218adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR+ )  ->  D  =/=  0 )
9391, 92absrpcld 13291 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( abs `  D )  e.  RR+ )
9493rphalfcld 11293 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( ( abs `  D )  / 
2 )  e.  RR+ )
9590, 94rpmulcld 11297 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )
9695ex 434 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  RR+  ->  ( y  x.  (
( abs `  D
)  /  2 ) )  e.  RR+ )
)
9796imdistani 690 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( ph  /\  ( y  x.  (
( abs `  D
)  /  2 ) )  e.  RR+ )
)
98 eleq1 2529 . . . . . . . . . . 11  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( w  e.  RR+  <->  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )
)
9998anbi2d 703 . . . . . . . . . 10  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( ( ph  /\  w  e.  RR+ ) 
<->  ( ph  /\  (
y  x.  ( ( abs `  D )  /  2 ) )  e.  RR+ ) ) )
100 breq2 4460 . . . . . . . . . . . 12  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( ( abs `  ( ( F `
 v )  - 
0 ) )  < 
w  <->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
101100imbi2d 316 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
102101rexralbidv 2976 . . . . . . . . . 10  |-  ( 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
) ) ) ) )
10399, 102imbi12d 320 . . . . . . . . 9  |-  ( 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
) ) ) ) ) )
1048, 7fmptd 6056 . . . . . . . . . . . . 13  |-  ( ph  ->  F : A --> CC )
105104, 10, 13ellimc3 22409 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
1069, 105mpbid 210 . . . . . . . . . . 11  |-  ( 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 ) ) )
107106simprd 463 . . . . . . . . . 10  |-  ( ph  ->  A. w  e.  RR+  E. u  e.  RR+  A. v  e.  A  ( (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  u )  -> 
( abs `  (
( F `  v
)  -  0 ) )  <  w ) )
108107r19.21bi 2826 . . . . . . . . 9  |-  ( (
ph  /\  w  e.  RR+ )  ->  E. u  e.  RR+  A. v  e.  A  ( ( v  =/=  E  /\  ( abs `  ( v  -  E ) )  < 
u )  ->  ( abs `  ( ( F `
 v )  - 
0 ) )  < 
w ) )
109103, 108vtoclg 3167 . . . . . . . 8  |-  ( ( 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
) ) ) ) )
11095, 97, 109sylc 60 . . . . . . 7  |-  ( (
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 ) ) ) )
1111103ad2ant1 1017 . . . . . 6  |-  ( ( ( 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
) ) ) )
112 simp12 1027 . . . . . . . . 9  |-  ( ( ( ( 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+ )
113 simp2 997 . . . . . . . . 9  |-  ( ( ( ( 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+ )
114112, 113ifcld 3987 . . . . . . . 8  |-  ( ( ( ( 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+ )
115 nfv 1708 . . . . . . . . . . 11  |-  F/ v ( ph  /\  y  e.  RR+ )
116 nfv 1708 . . . . . . . . . . 11  |-  F/ v  z  e.  RR+
117 nfra1 2838 . . . . . . . . . . 11  |-  F/ v A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )
118115, 116, 117nf3an 1931 . . . . . . . . . 10  |-  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
) ) ) )
119 nfv 1708 . . . . . . . . . 10  |-  F/ v  u  e.  RR+
120 nfra1 2838 . . . . . . . . . 10  |-  F/ v A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  u
)  ->  ( abs `  ( ( F `  v )  -  0 ) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )
121118, 119, 120nf3an 1931 . . . . . . . . 9  |-  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 ) ) ) )
122 simp111 1125 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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+ )
)
123 simp112 1126 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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+ )
124 simp12 1027 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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+ )
125122, 123, 124jca31 534 . . . . . . . . . . . 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( (
( ph  /\  y  e.  RR+ )  /\  z  e.  RR+ )  /\  u  e.  RR+ ) )
126 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  v  e.  A )
127 simp3l 1024 . . . . . . . . . . . 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  v  =/=  E )
128125, 126, 127jca31 534 . . . . . . . . . . 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 ) ) ) )  /\  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 ) )
12910adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  RR+ )  ->  A  C_  CC )
1301293ad2ant1 1017 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 )
1311303ad2ant1 1017 . . . . . . . . . . . . . . . . 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 ) ) ) )  ->  A  C_  CC )
1321313ad2ant1 1017 . . . . . . . . . . . . . . . 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 ) ) )  ->  A  C_  CC )
133132, 126sseldd 3500 . . . . . . . . . . . . . . 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 ) ) )  ->  v  e.  CC )
13413adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  RR+ )  ->  E  e.  CC )
1351343ad2ant1 1017 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 )
1361353ad2ant1 1017 . . . . . . . . . . . . . . . 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 ) ) ) )  ->  E  e.  CC )
1371363ad2ant1 1017 . . . . . . . . . . . . . . 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 ) ) )  ->  E  e.  CC )
138133, 137subcld 9950 . . . . . . . . . . . . . 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 ) ) )  ->  ( v  -  E )  e.  CC )
139138abscld 13279 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
140123rpred 11281 . . . . . . . . . . . . . 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 ) ) )  ->  z  e.  RR )
141124rpred 11281 . . . . . . . . . . . . . 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 ) ) )  ->  u  e.  RR )
142140, 141ifcld 3987 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
143 simp3r 1025 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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
) )
144 min1 11414 . . . . . . . . . . . . . 14  |-  ( ( z  e.  RR  /\  u  e.  RR )  ->  if ( z  <_  u ,  z ,  u )  <_  z
)
145140, 141, 144syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
146139, 142, 140, 143, 145ltletrd 9759 . . . . . . . . . . . 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( v  -  E
) )  <  z
)
147 simp113 1127 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 )
) ) )
148 rspa 2824 . . . . . . . . . . . . 13  |-  ( ( 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 )
) ) )
149147, 126, 148syl2anc 661 . . . . . . . . . . . 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 ) ) ) )  /\  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 )
) ) )
150127, 146, 149mp2and 679 . . . . . . . . . . 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )
151 simp13 1028 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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
) ) ) )
152 rspa 2824 . . . . . . . . . . . . 13  |-  ( ( 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
) ) ) )
153151, 126, 152syl2anc 661 . . . . . . . . . . . 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 ) ) ) )  /\  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
) ) ) )
154 min2 11415 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  RR  /\  u  e.  RR )  ->  if ( z  <_  u ,  z ,  u )  <_  u
)
155140, 141, 154syl2anc 661 . . . . . . . . . . . . . 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 ) ) )  ->  if (
z  <_  u , 
z ,  u )  <_  u )
156139, 142, 141, 143, 155ltletrd 9759 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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
)
157127, 156jca 532 . . . . . . . . . . . 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( v  =/=  E  /\  ( abs `  ( v  -  E
) )  <  u
) )
158122simpld 459 . . . . . . . . . . . . . . 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 )
1591583ad2ant1 1017 . . . . . . . . . . . . . 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 ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  ph )
160 simp12 1027 . . . . . . . . . . . . . 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 ) ) )  /\  (
( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u )  ->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) )  /\  ( v  =/=  E  /\  ( abs `  (
v  -  E ) )  <  u ) )  ->  v  e.  A )
161 nfv 1708 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( ph  /\  v  e.  A )
162 nfmpt1 4546 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x
( x  e.  A  |->  B )
1637, 162nfcxfr 2617 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x F
164 nfcv 2619 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x
v
165163, 164nffv 5879 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( F `  v
)
166165nfel1 2635 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( F `  v
)  e.  CC
167161, 166nfim 1921 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( F `  v
)  e.  CC )
168 eleq1 2529 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  v  ->  (
x  e.  A  <->  v  e.  A ) )
169168anbi2d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( ph  /\  x  e.  A )  <->  ( ph  /\  v  e.  A ) ) )
170 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  v  ->  ( F `  x )  =  ( F `  v ) )
171170eleq1d 2526 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( F `  x
)  e.  CC  <->  ( F `  v )  e.  CC ) )
172169, 171imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( F `  x
)  e.  CC )  <-> 
( ( ph  /\  v  e.  A )  ->  ( F `  v
)  e.  CC ) ) )
173 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
1747fvmpt2 5964 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  A  /\  B  e.  CC )  ->  ( F `  x
)  =  B )
175173, 8, 174syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  B )
176175, 8eqeltrd 2545 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  e.  CC )
177167, 172, 176chvar 2014 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( F `  v )  e.  CC )
178177subid1d 9939 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  (
( F `  v
)  -  0 )  =  ( F `  v ) )
179178eqcomd 2465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( F `  v )  =  ( ( F `
 v )  - 
0 ) )
180179fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( F `  v ) )  =  ( abs `  (
( F `  v
)  -  0 ) ) )
181159, 160, 180syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
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 ) ) )
182 simp3 998 . . . . . . . . . . . . . 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 ) ) )  /\  (
( 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
) )
183 simp2 997 . . . . . . . . . . . . . 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 ) ) )  /\  (
( 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
) ) ) )
184182, 183mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
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 ) ) )
185181, 184eqbrtrd 4476 . . . . . . . . . . . 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
) ) ) )  /\  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 ) ) )
186153, 157, 185mpd3an23 1326 . . . . . . . . . . 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 ) ) ) )  /\  v  e.  A  /\  (
v  =/=  E  /\  ( abs `  ( v  -  E ) )  <  if ( z  <_  u ,  z ,  u ) ) )  ->  ( abs `  ( F `  v
) )  <  (
y  x.  ( ( abs `  D )  /  2 ) ) )
187 simp-7l 773 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( 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 )
188 simp-4r 768 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( 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 )
189 eldifsni 4158 . . . . . . . . . . . . . . . . . . . 20  |-  ( C  e.  ( CC  \  { 0 } )  ->  C  =/=  0
)
1903, 189syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  C  =/=  0 )
1918, 4, 190divcld 10341 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( B  /  C )  e.  CC )
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18  |-  H  =  ( x  e.  A  |->  ( B  /  C
) )
193191, 192fmptd 6056 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  H : A --> CC )
194193ffvelrnda 6032 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( H `  v )  e.  CC )
195194subid1d 9939 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  (
( H `  v
)  -  0 )  =  ( H `  v ) )
196 nfmpt1 4546 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( x  e.  A  |->  ( B  /  C
) )
197192, 196nfcxfr 2617 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x H
198197, 164nffv 5879 . . . . . . . . . . . . . . . . . 18  |-  F/_ x
( H `  v
)
199 nfcv 2619 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x  /
200 nfmpt1 4546 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x
( x  e.  A  |->  C )
2015, 200nfcxfr 2617 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x G
202201, 164nffv 5879 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( G `  v
)
203165, 199, 202nfov 6322 . . . . . . . . . . . . . . . . . 18  |-  F/_ x
( ( F `  v )  /  ( G `  v )
)
204198, 203nfeq 2630 . . . . . . . . . . . . . . . . 17  |-  F/ x
( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) )
205161, 204nfim 1921 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) ) )
206 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  ( H `  x )  =  ( H `  v ) )
207 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  ( G `  x )  =  ( G `  v ) )
208170, 207oveq12d 6314 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  (
( F `  x
)  /  ( G `
 x ) )  =  ( ( F `
 v )  / 
( G `  v
) ) )
209206, 208eqeq12d 2479 . . . . . . . . . . . . . . . . 17  |-  ( x  =  v  ->  (
( H `  x
)  =  ( ( F `  x )  /  ( G `  x ) )  <->  ( H `  v )  =  ( ( F `  v
)  /  ( G `
 v ) ) ) )
210169, 209imbi12d 320 . . . . . . . . . . . . . . . 16  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( H `  x
)  =  ( ( F `  x )  /  ( G `  x ) ) )  <-> 
( ( ph  /\  v  e.  A )  ->  ( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) ) ) ) )
211192fvmpt2 5964 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  A  /\  ( B  /  C
)  e.  CC )  ->  ( H `  x )  =  ( B  /  C ) )
212173, 191, 211syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( B  /  C ) )
213175eqcomd 2465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  B  =  ( F `  x ) )
2145fvmpt2 5964 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  A  /\  C  e.  ( CC  \  { 0 } ) )  ->  ( G `  x )  =  C )
215173, 3, 214syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( G `  x )  =  C )
216215eqcomd 2465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  C  =  ( G `  x ) )
217213, 216oveq12d 6314 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( B  /  C )  =  ( ( F `  x )  /  ( G `  x )
) )
218212, 217eqtrd 2498 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( ( F `
 x )  / 
( G `  x
) ) )
219205, 210, 218chvar 2014 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( H `  v )  =  ( ( F `
 v )  / 
( G `  v
) ) )
220195, 219eqtrd 2498 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A )  ->  (
( H `  v
)  -  0 )  =  ( ( F `
 v )  / 
( G `  v
) ) )
221220fveq2d 5876 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( H `
 v )  - 
0 ) )  =  ( abs `  (
( F `  v
)  /  ( G `
 v ) ) ) )
222187, 188, 221syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( 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 ) ) ) )
223 simp-6l 771 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( 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+ ) )
224223, 188jca 532 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( 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 ) )
225 simplr 755 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( 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 `  D
)  /  2 )  <  ( abs `  ( G `  v )
) )
226 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( 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 `  ( F `  v ) )  < 
( y  x.  (
( abs `  D
)  /  2 ) ) )
227 nfcv 2619 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
0
228202, 227nfne 2788 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( G `  v
)  =/=  0
229161, 228nfim 1921 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( G `  v
)  =/=  0 )
230207neeq1d 2734 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( G `  x
)  =/=  0  <->  ( G `  v )  =/=  0 ) )
231169, 230imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( G `  x
)  =/=  0 )  <-> 
( ( ph  /\  v  e.  A )  ->  ( G `  v
)  =/=  0 ) ) )
232215, 190eqnetrd 2750 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( G `  x )  =/=  0 )
233229, 231, 232chvar 2014 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( G `  v )  =/=  0 )
234177, 57, 233absdivd 13298 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( F `
 v )  / 
( G `  v
) ) )  =  ( ( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) ) )
235234adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( ( F `
 v )  / 
( G `  v
) ) )  =  ( ( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) ) )
236235ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ( abs `  ( ( F `
 v )  / 
( G `  v
) ) )  =  ( ( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) ) )
237177abscld 13279 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( F `  v ) )  e.  RR )
23857, 233absne0d 13290 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  =/=  0 )
239237, 78, 238redivcld 10393 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  (
( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) )  e.  RR )
240239adantlr 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) )  e.  RR )
241240ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  (
( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) )  e.  RR )
242 rpre 11251 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  RR+  ->  y  e.  RR )
243242ad2antlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  y  e.  RR )
24420rpred 11281 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  RR )
245244ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( abs `  D
)  /  2 )  e.  RR )
246243, 245remulcld 9641 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
y  x.  ( ( abs `  D )  /  2 ) )  e.  RR )
247246ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  (
y  x.  ( ( abs `  D )  /  2 ) )  e.  RR )
24857, 233absrpcld 13291 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR+ )
249248adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR+ )
250249ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ( abs `  ( G `  v ) )  e.  RR+ )
251247, 250rerpdivcld 11308 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  (
( y  x.  (
( abs `  D
)  /  2 ) )  /  ( abs `  ( G `  v
) ) )  e.  RR )
252243ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  y  e.  RR )
253 simp-4l 767 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ph )
254 simpllr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  v  e.  A )
255253, 254, 237syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ( abs `  ( F `  v ) )  e.  RR )
256 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  ( abs `  ( F `  v ) )  < 
( y  x.  (
( abs `  D
)  /  2 ) ) )
257255, 247, 250, 256ltdiv1dd 11334 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A
)  /\  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )  /\  ( abs `  ( F `  v )
)  <  ( y  x.  ( ( abs `  D
)  /  2 ) ) )  ->  (
( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) )  < 
( ( y  x.  ( ( abs `  D
)  /  2 ) )  /  ( abs `  ( G `  v
) ) ) )
258243recnd 9639 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  y  e.  CC )
25947ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( abs `  D
)  /  2 )  e.  CC )
260249rpcnd 11283 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  CC )
261238adantlr 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  =/=  0 )
262258, 259, 260, 261divassd 10376 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( y  x.  (
( abs `  D
)  /  2 ) )  /  ( abs `  ( G `  v
) ) )  =  ( y  x.  (
( ( abs `  D
)  /  2 )  /  ( abs `  ( G `  v )
) ) ) )
263262adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  /\  ( ( abs `  D
)  /  2 )  <  ( abs `  ( G `  v )
) )  ->  (
( y  x.  (
( abs `  D
)  /  2 ) )  /  ( abs `  ( G `  v
) ) )  =  ( y  x.  (
( ( abs `  D
)  /  2 )  /  ( abs `  ( G `  v )
) ) ) )
264245, 249rerpdivcld 11308 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )