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

Theorem 0ellimcdiv 37549
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 9636 . 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 3448 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  CC )
5 0ellimcdiv.g . . . . . . . . . . 11  |-  G  =  ( x  e.  A  |->  C )
64, 5fmptd 6057 . . . . . . . . . 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 37534 . . . . . . . . . 10  |-  ( ph  ->  A  C_  CC )
11 limcrcl 22815 . . . . . . . . . . . 12  |-  ( D  e.  ( G lim CC  E )  ->  ( G : dom  G --> CC  /\  dom  G  C_  CC  /\  E  e.  CC ) )
122, 11syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( G : dom  G --> CC  /\  dom  G  C_  CC  /\  E  e.  CC ) )
1312simp3d 1019 . . . . . . . . . 10  |-  ( ph  ->  E  e.  CC )
146, 10, 13ellimc3 22820 . . . . . . . . 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 213 . . . . . . . 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 464 . . . . . . 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 460 . . . . . . . . 9  |-  ( ph  ->  D  e.  CC )
18 0ellimcdiv.dne0 . . . . . . . . 9  |-  ( ph  ->  D  =/=  0 )
1917, 18absrpcld 13497 . . . . . . . 8  |-  ( ph  ->  ( abs `  D
)  e.  RR+ )
2019rphalfcld 11353 . . . . . . 7  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  RR+ )
21 breq2 4424 . . . . . . . . . 10  |-  ( y  =  ( ( abs `  D )  /  2
)  ->  ( ( abs `  ( ( G `
 v )  -  D ) )  < 
y  <->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) ) )
2221imbi2d 317 . . . . . . . . 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 2947 . . . . . . . 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 3181 . . . . . . 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 665 . . . . . 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 1056 . . . . . . . . . 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 1010 . . . . . . . . . 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 462 . . . . . . . . . . 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 1009 . . . . . . . . . . 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 46 . . . . . . . . . 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 11343 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  D
)  e.  CC )
32312halvesd 10858 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( abs `  D )  /  2
)  +  ( ( abs `  D )  /  2 ) )  =  ( abs `  D
) )
3332eqcomd 2430 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( abs `  D
)  =  ( ( ( abs `  D
)  /  2 )  +  ( ( abs `  D )  /  2
) ) )
3433oveq1d 6316 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( ( ( abs `  D
)  /  2 )  +  ( ( abs `  D )  /  2
) )  -  (
( abs `  D
)  /  2 ) ) )
35 2cnd 10682 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  2  e.  CC )
36 2ne0 10702 . . . . . . . . . . . . . . . . 17  |-  2  =/=  0
3736a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  2  =/=  0 )
3817, 35, 37absdivd 13504 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  ( abs `  2 ) ) )
39 2re 10679 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
4039a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  2  e.  RR )
41 0le2 10700 . . . . . . . . . . . . . . . . . 18  |-  0  <_  2
4241a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <_  2 )
4340, 42absidd 13472 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( abs `  2
)  =  2 )
4443oveq2d 6317 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  D
)  /  ( abs `  2 ) )  =  ( ( abs `  D )  /  2
) )
4538, 44eqtr2d 2464 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( abs `  ( D  /  2 ) ) )
4645oveq2d 6317 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  D
)  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) ) )
4720rpcnd 11343 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  CC )
4847, 47pncand 9987 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( abs `  D )  /  2 )  +  ( ( abs `  D
)  /  2 ) )  -  ( ( abs `  D )  /  2 ) )  =  ( ( abs `  D )  /  2
) )
4934, 46, 483eqtr3rd 2472 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  =  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) ) )
50493ad2ant1 1026 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  =  ( ( abs `  D )  -  ( abs `  ( D  /  2 ) ) ) )
5145eqcomd 2430 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  2
) )
52513ad2ant1 1026 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  /  2 ) )  =  ( ( abs `  D )  /  2
) )
5352oveq2d 6317 . . . . . . . . . . . 12  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) )  =  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) ) )
5417adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  D  e.  CC )
5554abscld 13485 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  e.  RR )
56553adant3 1025 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  e.  RR )
576ffvelrnda 6033 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( G `  v )  e.  CC )
58573adant3 1025 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( G `  v )  e.  CC )
5958abscld 13485 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( G `  v )
)  e.  RR )
60173ad2ant1 1026 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  D  e.  CC )
6160, 58subcld 9986 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( D  -  ( G `  v ) )  e.  CC )
6261abscld 13485 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  e.  RR )
6359, 62readdcld 9670 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( abs `  ( D  -  ( G `  v ) ) ) )  e.  RR )
6456rehalfcld 10859 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  e.  RR )
6559, 64readdcld 9670 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  ( G `  v
) )  +  ( ( abs `  D
)  /  2 ) )  e.  RR )
6657, 54pncan3d 9989 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  (
( G `  v
)  +  ( D  -  ( G `  v ) ) )  =  D )
6766eqcomd 2430 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  D  =  ( ( G `
 v )  +  ( D  -  ( G `  v )
) ) )
6867fveq2d 5881 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  =  ( abs `  (
( G `  v
)  +  ( D  -  ( G `  v ) ) ) ) )
6954, 57subcld 9986 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( D  -  ( G `  v ) )  e.  CC )
7057, 69abstrid 13505 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( G `
 v )  +  ( D  -  ( G `  v )
) ) )  <_ 
( ( abs `  ( G `  v )
)  +  ( abs `  ( D  -  ( G `  v )
) ) ) )
7168, 70eqbrtrd 4441 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  D )  <_ 
( ( abs `  ( G `  v )
)  +  ( abs `  ( D  -  ( G `  v )
) ) ) )
72713adant3 1025 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  <_  ( ( abs `  ( G `  v ) )  +  ( abs `  ( D  -  ( G `  v ) ) ) ) )
7360, 58abssubd 13502 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  =  ( abs `  (
( G `  v
)  -  D ) ) )
74 simp3 1007 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )
7573, 74eqbrtrd 4441 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( D  -  ( G `  v ) ) )  <  ( ( abs `  D )  /  2
) )
7662, 64, 59, 75ltadd2dd 9794 . . . . . . . . . . . . . 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 9793 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  D
)  <  ( ( abs `  ( G `  v ) )  +  ( ( abs `  D
)  /  2 ) ) )
7857abscld 13485 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR )
79783adant3 1025 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( abs `  ( G `  v )
)  e.  RR )
8056, 64, 79ltsubaddd 10209 . . . . . . . . . . . . 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 235 . . . . . . . . . . . 12  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  (
( abs `  D
)  /  2 ) )  <  ( abs `  ( G `  v
) ) )
8253, 81eqbrtrd 4441 . . . . . . . . . . 11  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  -  ( abs `  ( D  / 
2 ) ) )  <  ( abs `  ( G `  v )
) )
8350, 82eqbrtrd 4441 . . . . . . . . . 10  |-  ( (
ph  /\  v  e.  A  /\  ( abs `  (
( G `  v
)  -  D ) )  <  ( ( abs `  D )  /  2 ) )  ->  ( ( abs `  D )  /  2
)  <  ( abs `  ( G `  v
) ) )
8426, 27, 30, 83syl3anc 1264 . . . . . . . . 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 1221 . . . . . . . 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 2832 . . . . . . 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 2900 . . . . . 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 466 . . . 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 462 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR+ )  ->  y  e.  RR+ )
9117adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR+ )  ->  D  e.  CC )
9218adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  RR+ )  ->  D  =/=  0 )
9391, 92absrpcld 13497 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( abs `  D )  e.  RR+ )
9493rphalfcld 11353 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( ( abs `  D )  / 
2 )  e.  RR+ )
9590, 94rpmulcld 11357 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )
9695ex 435 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  RR+  ->  ( y  x.  (
( abs `  D
)  /  2 ) )  e.  RR+ )
)
9796imdistani 694 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR+ )  ->  ( ph  /\  ( y  x.  (
( abs `  D
)  /  2 ) )  e.  RR+ )
)
98 eleq1 2494 . . . . . . . . . . 11  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( w  e.  RR+  <->  ( y  x.  ( ( abs `  D
)  /  2 ) )  e.  RR+ )
)
9998anbi2d 708 . . . . . . . . . 10  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( ( ph  /\  w  e.  RR+ ) 
<->  ( ph  /\  (
y  x.  ( ( abs `  D )  /  2 ) )  e.  RR+ ) ) )
100 breq2 4424 . . . . . . . . . . . 12  |-  ( w  =  ( y  x.  ( ( abs `  D
)  /  2 ) )  ->  ( ( abs `  ( ( F `
 v )  - 
0 ) )  < 
w  <->  ( abs `  (
( F `  v
)  -  0 ) )  <  ( y  x.  ( ( abs `  D )  /  2
) ) ) )
101100imbi2d 317 . . . . . . . . . . 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 2947 . . . . . . . . . 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 321 . . . . . . . . 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 6057 . . . . . . . . . . . . 13  |-  ( ph  ->  F : A --> CC )
105104, 10, 13ellimc3 22820 . . . . . . . . . . . 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 213 . . . . . . . . . . 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 464 . . . . . . . . . 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 2794 . . . . . . . . 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 3139 . . . . . . . 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 62 . . . . . . 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 1026 . . . . . 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 1036 . . . . . . . . 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 1006 . . . . . . . . 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 3952 . . . . . . . 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 1751 . . . . . . . . . . 11  |-  F/ v ( ph  /\  y  e.  RR+ )
116 nfv 1751 . . . . . . . . . . 11  |-  F/ v  z  e.  RR+
117 nfra1 2806 . . . . . . . . . . 11  |-  F/ v A. v  e.  A  ( ( v  =/= 
E  /\  ( abs `  ( v  -  E
) )  <  z
)  ->  ( ( abs `  D )  / 
2 )  <  ( abs `  ( G `  v ) ) )
118115, 116, 117nf3an 1986 . . . . . . . . . 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 1751 . . . . . . . . . 10  |-  F/ v  u  e.  RR+
120 nfra1 2806 . . . . . . . . . 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 1986 . . . . . . . . 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 1134 . . . . . . . . . . . . 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 1135 . . . . . . . . . . . . 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 1036 . . . . . . . . . . . . 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 536 . . . . . . . . . . . 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 1006 . . . . . . . . . . . 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 1033 . . . . . . . . . . . 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 536 . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  RR+ )  ->  A  C_  CC )
1301293ad2ant1 1026 . . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  RR+ )  ->  E  e.  CC )
1351343ad2ant1 1026 . . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . 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 9986 . . . . . . . . . . . . . 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 13485 . . . . . . . . . . . . 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 11341 . . . . . . . . . . . . . 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 11341 . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . 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 1034 . . . . . . . . . . . . 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 11483 . . . . . . . . . . . . . 14  |-  ( ( z  e.  RR  /\  u  e.  RR )  ->  if ( z  <_  u ,  z ,  u )  <_  z
)
145140, 141, 144syl2anc 665 . . . . . . . . . . . . 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 9795 . . . . . . . . . . . 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 1136 . . . . . . . . . . . . 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 2792 . . . . . . . . . . . . 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 665 . . . . . . . . . . . 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 683 . . . . . . . . . . 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 1037 . . . . . . . . . . . . 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 2792 . . . . . . . . . . . . 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 665 . . . . . . . . . . . 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 11484 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  RR  /\  u  e.  RR )  ->  if ( z  <_  u ,  z ,  u )  <_  u
)
155140, 141, 154syl2anc 665 . . . . . . . . . . . . . 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 9795 . . . . . . . . . . . . 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 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 ) ) )  ->  ( v  =/=  E  /\  ( abs `  ( v  -  E
) )  <  u
) )
158122simpld 460 . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . 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 1036 . . . . . . . . . . . . . 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 1751 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( ph  /\  v  e.  A )
162 nfmpt1 4510 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ x
( x  e.  A  |->  B )
1637, 162nfcxfr 2582 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x F
164 nfcv 2584 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x
v
165163, 164nffv 5884 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( F `  v
)
166165nfel1 2600 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( F `  v
)  e.  CC
167161, 166nfim 1976 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( F `  v
)  e.  CC )
168 eleq1 2494 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  v  ->  (
x  e.  A  <->  v  e.  A ) )
169168anbi2d 708 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( ph  /\  x  e.  A )  <->  ( ph  /\  v  e.  A ) ) )
170 fveq2 5877 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  v  ->  ( F `  x )  =  ( F `  v ) )
171170eleq1d 2491 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( F `  x
)  e.  CC  <->  ( F `  v )  e.  CC ) )
172169, 171imbi12d 321 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( F `  x
)  e.  CC )  <-> 
( ( ph  /\  v  e.  A )  ->  ( F `  v
)  e.  CC ) ) )
173 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  A )
1747fvmpt2 5969 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  A  /\  B  e.  CC )  ->  ( F `  x
)  =  B )
175173, 8, 174syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  B )
176175, 8eqeltrd 2510 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  e.  CC )
177167, 172, 176chvar 2067 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( F `  v )  e.  CC )
178177subid1d 9975 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  (
( F `  v
)  -  0 )  =  ( F `  v ) )
179178eqcomd 2430 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( F `  v )  =  ( ( F `
 v )  - 
0 ) )
180179fveq2d 5881 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( F `  v ) )  =  ( abs `  (
( F `  v
)  -  0 ) ) )
181159, 160, 180syl2anc 665 . . . . . . . . . . . . 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 1007 . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . 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 4441 . . . . . . . . . . . 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 1362 . . . . . . . . . . 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 780 . . . . . . . . . . . . 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 775 . . . . . . . . . . . . 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 4123 . . . . . . . . . . . . . . . . . . . 20  |-  ( C  e.  ( CC  \  { 0 } )  ->  C  =/=  0
)
1903, 189syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  C  =/=  0 )
1918, 4, 190divcld 10383 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( B  /  C )  e.  CC )
192 0ellimcdiv.h . . . . . . . . . . . . . . . . . 18  |-  H  =  ( x  e.  A  |->  ( B  /  C
) )
193191, 192fmptd 6057 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  H : A --> CC )
194193ffvelrnda 6033 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( H `  v )  e.  CC )
195194subid1d 9975 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  (
( H `  v
)  -  0 )  =  ( H `  v ) )
196 nfmpt1 4510 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( x  e.  A  |->  ( B  /  C
) )
197192, 196nfcxfr 2582 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x H
198197, 164nffv 5884 . . . . . . . . . . . . . . . . . 18  |-  F/_ x
( H `  v
)
199 nfcv 2584 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x  /
200 nfmpt1 4510 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x
( x  e.  A  |->  C )
2015, 200nfcxfr 2582 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x G
202201, 164nffv 5884 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( G `  v
)
203165, 199, 202nfov 6327 . . . . . . . . . . . . . . . . . 18  |-  F/_ x
( ( F `  v )  /  ( G `  v )
)
204198, 203nfeq 2595 . . . . . . . . . . . . . . . . 17  |-  F/ x
( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) )
205161, 204nfim 1976 . . . . . . . . . . . . . . . 16  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) ) )
206 fveq2 5877 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  ( H `  x )  =  ( H `  v ) )
207 fveq2 5877 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  ( G `  x )  =  ( G `  v ) )
208170, 207oveq12d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  (
( F `  x
)  /  ( G `
 x ) )  =  ( ( F `
 v )  / 
( G `  v
) ) )
209206, 208eqeq12d 2444 . . . . . . . . . . . . . . . . 17  |-  ( x  =  v  ->  (
( H `  x
)  =  ( ( F `  x )  /  ( G `  x ) )  <->  ( H `  v )  =  ( ( F `  v
)  /  ( G `
 v ) ) ) )
210169, 209imbi12d 321 . . . . . . . . . . . . . . . 16  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( H `  x
)  =  ( ( F `  x )  /  ( G `  x ) ) )  <-> 
( ( ph  /\  v  e.  A )  ->  ( H `  v
)  =  ( ( F `  v )  /  ( G `  v ) ) ) ) )
211192fvmpt2 5969 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  A  /\  ( B  /  C
)  e.  CC )  ->  ( H `  x )  =  ( B  /  C ) )
212173, 191, 211syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( B  /  C ) )
213175eqcomd 2430 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  B  =  ( F `  x ) )
2145fvmpt2 5969 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  A  /\  C  e.  ( CC  \  { 0 } ) )  ->  ( G `  x )  =  C )
215173, 3, 214syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( G `  x )  =  C )
216215eqcomd 2430 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  C  =  ( G `  x ) )
217213, 216oveq12d 6319 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( B  /  C )  =  ( ( F `  x )  /  ( G `  x )
) )
218212, 217eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( H `  x )  =  ( ( F `
 x )  / 
( G `  x
) ) )
219205, 210, 218chvar 2067 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  A )  ->  ( H `  v )  =  ( ( F `
 v )  / 
( G `  v
) ) )
220195, 219eqtrd 2463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  v  e.  A )  ->  (
( H `  v
)  -  0 )  =  ( ( F `
 v )  / 
( G `  v
) ) )
221220fveq2d 5881 . . . . . . . . . . . . 13  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( H `
 v )  - 
0 ) )  =  ( abs `  (
( F `  v
)  /  ( G `
 v ) ) ) )
222187, 188, 221syl2anc 665 . . . . . . . . . . . 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 778 . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . 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 760 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 2584 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
0
228202, 227nfne 2756 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( G `  v
)  =/=  0
229161, 228nfim 1976 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( ( ph  /\  v  e.  A )  ->  ( G `  v
)  =/=  0 )
230207neeq1d 2701 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  v  ->  (
( G `  x
)  =/=  0  <->  ( G `  v )  =/=  0 ) )
231169, 230imbi12d 321 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  v  ->  (
( ( ph  /\  x  e.  A )  ->  ( G `  x
)  =/=  0 )  <-> 
( ( ph  /\  v  e.  A )  ->  ( G `  v
)  =/=  0 ) ) )
232215, 190eqnetrd 2717 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( G `  x )  =/=  0 )
233229, 231, 232chvar 2067 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  ( G `  v )  =/=  0 )
234177, 57, 233absdivd 13504 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( ( F `
 v )  / 
( G `  v
) ) )  =  ( ( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) ) )
235234adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( ( F `
 v )  / 
( G `  v
) ) )  =  ( ( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) ) )
236235ad2antrr 730 . . . . . . . . . . . . . 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 13485 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( F `  v ) )  e.  RR )
23857, 233absne0d 13496 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  =/=  0 )
239237, 78, 238redivcld 10435 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  v  e.  A )  ->  (
( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) )  e.  RR )
240239adantlr 719 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( abs `  ( F `  v )
)  /  ( abs `  ( G `  v
) ) )  e.  RR )
241240ad2antrr 730 . . . . . . . . . . . . . . 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 11308 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  RR+  ->  y  e.  RR )
243242ad2antlr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  y  e.  RR )
24420rpred 11341 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( abs `  D
)  /  2 )  e.  RR )
245244ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( abs `  D
)  /  2 )  e.  RR )
246243, 245remulcld 9671 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
y  x.  ( ( abs `  D )  /  2 ) )  e.  RR )
247246ad2antrr 730 . . . . . . . . . . . . . . . 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 13497 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR+ )
249248adantlr 719 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  RR+ )
250249ad2antrr 730 . . . . . . . . . . . . . . . 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 11369 . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 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 767 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . 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 11395 . . . . . . . . . . . . . . 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 9669 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  y  e.  CC )
25947ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  (
( abs `  D
)  /  2 )  e.  CC )
260249rpcnd 11343 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  e.  CC )
261238adantlr 719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->  ( abs `  ( G `  v ) )  =/=  0 )
262258, 259, 260, 261divassd 10418 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 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 11369 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  RR+ )  /\  v  e.  A )  ->