Metamath Proof Explorer

Theorem 0ellimcdiv

Description: If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 limCC E ) )
0ellimcdiv.d 
|- ( ph -> D e. ( G limCC E ) )
0ellimcdiv.dne0 
|- ( ph -> D =/= 0 )
Assertion 0ellimcdiv 
|- ( ph -> 0 e. ( H limCC E ) )

Proof

Step Hyp Ref Expression
1 0ellimcdiv.f 
 |-  F = ( x e. A |-> B )
2 0ellimcdiv.g 
 |-  G = ( x e. A |-> C )
3 0ellimcdiv.h 
 |-  H = ( x e. A |-> ( B / C ) )
4 0ellimcdiv.b 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 0ellimcdiv.c 
 |-  ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )
6 0ellimcdiv.0limf 
 |-  ( ph -> 0 e. ( F limCC E ) )
7 0ellimcdiv.d 
 |-  ( ph -> D e. ( G limCC E ) )
8 0ellimcdiv.dne0 
 |-  ( ph -> D =/= 0 )
9 0cnd 
 |-  ( ph -> 0 e. CC )
10 5 eldifad 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
11 10 2 fmptd 
 |-  ( ph -> G : A --> CC )
12 1 4 6 limcmptdm 
 |-  ( ph -> A C_ CC )
13 limcrcl 
 |-  ( D e. ( G limCC E ) -> ( G : dom G --> CC /\ dom G C_ CC /\ E e. CC ) )
14 7 13 syl 
 |-  ( ph -> ( G : dom G --> CC /\ dom G C_ CC /\ E e. CC ) )
15 14 simp3d 
 |-  ( ph -> E e. CC )
16 11 12 15 ellimc3 
 |-  ( ph -> ( D e. ( G limCC 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 ) ) ) )
17 7 16 mpbid 
 |-  ( 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 ) ) )
18 17 simprd 
 |-  ( ph -> A. y e. RR+ E. z e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( abs ` ( ( G ` v ) - D ) ) < y ) )
19 17 simpld 
 |-  ( ph -> D e. CC )
20 19 8 absrpcld 
 |-  ( ph -> ( abs ` D ) e. RR+ )
21 20 rphalfcld 
 |-  ( ph -> ( ( abs ` D ) / 2 ) e. RR+ )
22 breq2 
 |-  ( y = ( ( abs ` D ) / 2 ) -> ( ( abs ` ( ( G ` v ) - D ) ) < y <-> ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) )
23 22 imbi2d 
 |-  ( 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 ) ) ) )
24 23 rexralbidv 
 |-  ( 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 ) ) ) )
25 24 rspccva 
 |-  ( ( 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 ) ) )
26 18 21 25 syl2anc 
 |-  ( ph -> E. z e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) )
27 simpl1l 
 |-  ( ( ( ( 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 )
28 simpl3 
 |-  ( ( ( ( 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 )
29 simpr 
 |-  ( ( ( ( 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 ) )
30 simpl2 
 |-  ( ( ( ( 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 ) ) ) )
31 28 29 30 mp2d 
 |-  ( ( ( ( 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 ) )
32 20 rpcnd 
 |-  ( ph -> ( abs ` D ) e. CC )
33 32 2halvesd 
 |-  ( ph -> ( ( ( abs ` D ) / 2 ) + ( ( abs ` D ) / 2 ) ) = ( abs ` D ) )
34 33 eqcomd 
 |-  ( ph -> ( abs ` D ) = ( ( ( abs ` D ) / 2 ) + ( ( abs ` D ) / 2 ) ) )
35 34 oveq1d 
 |-  ( ph -> ( ( abs ` D ) - ( ( abs ` D ) / 2 ) ) = ( ( ( ( abs ` D ) / 2 ) + ( ( abs ` D ) / 2 ) ) - ( ( abs ` D ) / 2 ) ) )
36 2cnd 
 |-  ( ph -> 2 e. CC )
37 2ne0 
 |-  2 =/= 0
38 37 a1i 
 |-  ( ph -> 2 =/= 0 )
39 19 36 38 absdivd 
 |-  ( ph -> ( abs ` ( D / 2 ) ) = ( ( abs ` D ) / ( abs ` 2 ) ) )
40 2re 
 |-  2 e. RR
41 40 a1i 
 |-  ( ph -> 2 e. RR )
42 0le2 
 |-  0 <_ 2
43 42 a1i 
 |-  ( ph -> 0 <_ 2 )
44 41 43 absidd 
 |-  ( ph -> ( abs ` 2 ) = 2 )
45 44 oveq2d 
 |-  ( ph -> ( ( abs ` D ) / ( abs ` 2 ) ) = ( ( abs ` D ) / 2 ) )
46 39 45 eqtr2d 
 |-  ( ph -> ( ( abs ` D ) / 2 ) = ( abs ` ( D / 2 ) ) )
47 46 oveq2d 
 |-  ( ph -> ( ( abs ` D ) - ( ( abs ` D ) / 2 ) ) = ( ( abs ` D ) - ( abs ` ( D / 2 ) ) ) )
48 21 rpcnd 
 |-  ( ph -> ( ( abs ` D ) / 2 ) e. CC )
49 48 48 pncand 
 |-  ( ph -> ( ( ( ( abs ` D ) / 2 ) + ( ( abs ` D ) / 2 ) ) - ( ( abs ` D ) / 2 ) ) = ( ( abs ` D ) / 2 ) )
50 35 47 49 3eqtr3rd 
 |-  ( ph -> ( ( abs ` D ) / 2 ) = ( ( abs ` D ) - ( abs ` ( D / 2 ) ) ) )
51 50 3ad2ant1 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` D ) / 2 ) = ( ( abs ` D ) - ( abs ` ( D / 2 ) ) ) )
52 46 eqcomd 
 |-  ( ph -> ( abs ` ( D / 2 ) ) = ( ( abs ` D ) / 2 ) )
53 52 3ad2ant1 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( D / 2 ) ) = ( ( abs ` D ) / 2 ) )
54 53 oveq2d 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` D ) - ( abs ` ( D / 2 ) ) ) = ( ( abs ` D ) - ( ( abs ` D ) / 2 ) ) )
55 19 adantr 
 |-  ( ( ph /\ v e. A ) -> D e. CC )
56 55 abscld 
 |-  ( ( ph /\ v e. A ) -> ( abs ` D ) e. RR )
57 56 3adant3 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` D ) e. RR )
58 11 ffvelcdmda 
 |-  ( ( ph /\ v e. A ) -> ( G ` v ) e. CC )
59 58 3adant3 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( G ` v ) e. CC )
60 59 abscld 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( G ` v ) ) e. RR )
61 19 3ad2ant1 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> D e. CC )
62 61 59 subcld 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( D - ( G ` v ) ) e. CC )
63 62 abscld 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( D - ( G ` v ) ) ) e. RR )
64 60 63 readdcld 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` ( G ` v ) ) + ( abs ` ( D - ( G ` v ) ) ) ) e. RR )
65 57 rehalfcld 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` D ) / 2 ) e. RR )
66 60 65 readdcld 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` ( G ` v ) ) + ( ( abs ` D ) / 2 ) ) e. RR )
67 58 55 pncan3d 
 |-  ( ( ph /\ v e. A ) -> ( ( G ` v ) + ( D - ( G ` v ) ) ) = D )
68 67 eqcomd 
 |-  ( ( ph /\ v e. A ) -> D = ( ( G ` v ) + ( D - ( G ` v ) ) ) )
69 68 fveq2d 
 |-  ( ( ph /\ v e. A ) -> ( abs ` D ) = ( abs ` ( ( G ` v ) + ( D - ( G ` v ) ) ) ) )
70 55 58 subcld 
 |-  ( ( ph /\ v e. A ) -> ( D - ( G ` v ) ) e. CC )
71 58 70 abstrid 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( G ` v ) + ( D - ( G ` v ) ) ) ) <_ ( ( abs ` ( G ` v ) ) + ( abs ` ( D - ( G ` v ) ) ) ) )
72 69 71 eqbrtrd 
 |-  ( ( ph /\ v e. A ) -> ( abs ` D ) <_ ( ( abs ` ( G ` v ) ) + ( abs ` ( D - ( G ` v ) ) ) ) )
73 72 3adant3 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` D ) <_ ( ( abs ` ( G ` v ) ) + ( abs ` ( D - ( G ` v ) ) ) ) )
74 61 59 abssubd 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( D - ( G ` v ) ) ) = ( abs ` ( ( G ` v ) - D ) ) )
75 simp3 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) )
76 74 75 eqbrtrd 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( D - ( G ` v ) ) ) < ( ( abs ` D ) / 2 ) )
77 63 65 60 76 ltadd2dd 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` ( G ` v ) ) + ( abs ` ( D - ( G ` v ) ) ) ) < ( ( abs ` ( G ` v ) ) + ( ( abs ` D ) / 2 ) ) )
78 57 64 66 73 77 lelttrd 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` D ) < ( ( abs ` ( G ` v ) ) + ( ( abs ` D ) / 2 ) ) )
79 58 abscld 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( G ` v ) ) e. RR )
80 79 3adant3 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( abs ` ( G ` v ) ) e. RR )
81 57 65 80 ltsubaddd 
 |-  ( ( 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 ) ) ) )
82 78 81 mpbird 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` D ) - ( ( abs ` D ) / 2 ) ) < ( abs ` ( G ` v ) ) )
83 54 82 eqbrtrd 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` D ) - ( abs ` ( D / 2 ) ) ) < ( abs ` ( G ` v ) ) )
84 51 83 eqbrtrd 
 |-  ( ( ph /\ v e. A /\ ( abs ` ( ( G ` v ) - D ) ) < ( ( abs ` D ) / 2 ) ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) )
85 27 28 31 84 syl3anc 
 |-  ( ( ( ( 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 ) ) )
86 85 3exp1 
 |-  ( ( 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 ) ) ) ) ) )
87 86 ralimdv2 
 |-  ( ( 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 ) ) ) ) )
88 87 reximdva 
 |-  ( 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 ) ) ) ) )
89 26 88 mpd 
 |-  ( ph -> E. z e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) )
90 89 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> E. z e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) )
91 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
92 19 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> D e. CC )
93 8 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> D =/= 0 )
94 92 93 absrpcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` D ) e. RR+ )
95 94 rphalfcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( abs ` D ) / 2 ) e. RR+ )
96 91 95 rpmulcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( y x. ( ( abs ` D ) / 2 ) ) e. RR+ )
97 96 ex 
 |-  ( ph -> ( y e. RR+ -> ( y x. ( ( abs ` D ) / 2 ) ) e. RR+ ) )
98 97 imdistani 
 |-  ( ( ph /\ y e. RR+ ) -> ( ph /\ ( y x. ( ( abs ` D ) / 2 ) ) e. RR+ ) )
99 eleq1 
 |-  ( w = ( y x. ( ( abs ` D ) / 2 ) ) -> ( w e. RR+ <-> ( y x. ( ( abs ` D ) / 2 ) ) e. RR+ ) )
100 99 anbi2d 
 |-  ( w = ( y x. ( ( abs ` D ) / 2 ) ) -> ( ( ph /\ w e. RR+ ) <-> ( ph /\ ( y x. ( ( abs ` D ) / 2 ) ) e. RR+ ) ) )
101 breq2 
 |-  ( w = ( y x. ( ( abs ` D ) / 2 ) ) -> ( ( abs ` ( ( F ` v ) - 0 ) ) < w <-> ( abs ` ( ( F ` v ) - 0 ) ) < ( y x. ( ( abs ` D ) / 2 ) ) ) )
102 101 imbi2d 
 |-  ( 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 ) ) ) ) )
103 102 rexralbidv 
 |-  ( 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 ) ) ) ) )
104 100 103 imbi12d 
 |-  ( 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 ) ) ) ) ) )
105 4 1 fmptd 
 |-  ( ph -> F : A --> CC )
106 105 12 15 ellimc3 
 |-  ( ph -> ( 0 e. ( F limCC 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 ) ) ) )
107 6 106 mpbid 
 |-  ( 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 ) ) )
108 107 simprd 
 |-  ( ph -> A. w e. RR+ E. u e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < u ) -> ( abs ` ( ( F ` v ) - 0 ) ) < w ) )
109 108 r19.21bi 
 |-  ( ( ph /\ w e. RR+ ) -> E. u e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < u ) -> ( abs ` ( ( F ` v ) - 0 ) ) < w ) )
110 104 109 vtoclg 
 |-  ( ( 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 ) ) ) ) )
111 96 98 110 sylc 
 |-  ( ( 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 ) ) ) )
112 111 3ad2ant1 
 |-  ( ( ( 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 ) ) ) )
113 simp12 
 |-  ( ( ( ( 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+ )
114 simp2 
 |-  ( ( ( ( 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+ )
115 113 114 ifcld 
 |-  ( ( ( ( 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+ )
116 nfv 
 |-  F/ v ( ph /\ y e. RR+ )
117 nfv 
 |-  F/ v z e. RR+
118 nfra1 
 |-  F/ v A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) )
119 116 117 118 nf3an 
 |-  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 ) ) ) )
120 nfv 
 |-  F/ v u e. RR+
121 nfra1 
 |-  F/ v A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < u ) -> ( abs ` ( ( F ` v ) - 0 ) ) < ( y x. ( ( abs ` D ) / 2 ) ) )
122 119 120 121 nf3an 
 |-  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 ) ) ) )
123 simp111 
 |-  ( ( ( ( ( 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+ ) )
124 simp112 
 |-  ( ( ( ( ( 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+ )
125 simp12 
 |-  ( ( ( ( ( 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+ )
126 123 124 125 jca31 
 |-  ( ( ( ( ( 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+ ) )
127 simp2 
 |-  ( ( ( ( ( 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 )
128 simp3l 
 |-  ( ( ( ( ( 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 )
129 126 127 128 jca31 
 |-  ( ( ( ( ( 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 ) )
130 12 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> A C_ CC )
131 130 3ad2ant1 
 |-  ( ( ( 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 )
132 131 3ad2ant1 
 |-  ( ( ( ( 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 )
133 132 3ad2ant1 
 |-  ( ( ( ( ( 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 )
134 133 127 sseldd 
 |-  ( ( ( ( ( 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 )
135 15 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> E e. CC )
136 135 3ad2ant1 
 |-  ( ( ( 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 )
137 136 3ad2ant1 
 |-  ( ( ( ( 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 )
138 137 3ad2ant1 
 |-  ( ( ( ( ( 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 )
139 134 138 subcld 
 |-  ( ( ( ( ( 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 )
140 139 abscld 
 |-  ( ( ( ( ( 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 )
141 124 rpred 
 |-  ( ( ( ( ( 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 )
142 125 rpred 
 |-  ( ( ( ( ( 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 )
143 141 142 ifcld 
 |-  ( ( ( ( ( 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 )
144 simp3r 
 |-  ( ( ( ( ( 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 ) )
145 min1 
 |-  ( ( z e. RR /\ u e. RR ) -> if ( z <_ u , z , u ) <_ z )
146 141 142 145 syl2anc 
 |-  ( ( ( ( ( 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 )
147 140 143 141 144 146 ltletrd 
 |-  ( ( ( ( ( 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 )
148 simp113 
 |-  ( ( ( ( ( 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 ) ) ) )
149 rspa 
 |-  ( ( 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 ) ) ) )
150 148 127 149 syl2anc 
 |-  ( ( ( ( ( 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 ) ) ) )
151 128 147 150 mp2and 
 |-  ( ( ( ( ( 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 ) ) )
152 simp13 
 |-  ( ( ( ( ( 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 ) ) ) )
153 rspa 
 |-  ( ( 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 ) ) ) )
154 152 127 153 syl2anc 
 |-  ( ( ( ( ( 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 ) ) ) )
155 min2 
 |-  ( ( z e. RR /\ u e. RR ) -> if ( z <_ u , z , u ) <_ u )
156 141 142 155 syl2anc 
 |-  ( ( ( ( ( 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 )
157 140 143 142 144 156 ltletrd 
 |-  ( ( ( ( ( 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 )
158 128 157 jca 
 |-  ( ( ( ( ( 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 ) )
159 123 simpld 
 |-  ( ( ( ( ( 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 )
160 159 3ad2ant1 
 |-  ( ( ( ( ( ( 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 )
161 simp12 
 |-  ( ( ( ( ( ( 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 )
162 nfv 
 |-  F/ x ( ph /\ v e. A )
163 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
164 1 163 nfcxfr 
 |-  F/_ x F
165 nfcv 
 |-  F/_ x v
166 164 165 nffv 
 |-  F/_ x ( F ` v )
167 166 nfel1 
 |-  F/ x ( F ` v ) e. CC
168 162 167 nfim 
 |-  F/ x ( ( ph /\ v e. A ) -> ( F ` v ) e. CC )
169 eleq1 
 |-  ( x = v -> ( x e. A <-> v e. A ) )
170 169 anbi2d 
 |-  ( x = v -> ( ( ph /\ x e. A ) <-> ( ph /\ v e. A ) ) )
171 fveq2 
 |-  ( x = v -> ( F ` x ) = ( F ` v ) )
172 171 eleq1d 
 |-  ( x = v -> ( ( F ` x ) e. CC <-> ( F ` v ) e. CC ) )
173 170 172 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. A ) -> ( F ` x ) e. CC ) <-> ( ( ph /\ v e. A ) -> ( F ` v ) e. CC ) ) )
174 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
175 1 fvmpt2 
 |-  ( ( x e. A /\ B e. CC ) -> ( F ` x ) = B )
176 174 4 175 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
177 176 4 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. CC )
178 168 173 177 chvarfv 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) e. CC )
179 178 subid1d 
 |-  ( ( ph /\ v e. A ) -> ( ( F ` v ) - 0 ) = ( F ` v ) )
180 179 eqcomd 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) = ( ( F ` v ) - 0 ) )
181 180 fveq2d 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( F ` v ) ) = ( abs ` ( ( F ` v ) - 0 ) ) )
182 160 161 181 syl2anc 
 |-  ( ( ( ( ( ( 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 ) ) )
183 simp3 
 |-  ( ( ( ( ( ( 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 ) )
184 simp2 
 |-  ( ( ( ( ( ( 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 ) ) ) )
185 183 184 mpd 
 |-  ( ( ( ( ( ( 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 ) ) )
186 182 185 eqbrtrd 
 |-  ( ( ( ( ( ( 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 ) ) )
187 154 158 186 mpd3an23 
 |-  ( ( ( ( ( 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 ) ) )
188 simp-7l 
 |-  ( ( ( ( ( ( ( ( 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 )
189 simp-4r 
 |-  ( ( ( ( ( ( ( ( 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 )
190 eldifsni 
 |-  ( C e. ( CC \ { 0 } ) -> C =/= 0 )
191 5 190 syl 
 |-  ( ( ph /\ x e. A ) -> C =/= 0 )
192 4 10 191 divcld 
 |-  ( ( ph /\ x e. A ) -> ( B / C ) e. CC )
193 192 3 fmptd 
 |-  ( ph -> H : A --> CC )
194 193 ffvelcdmda 
 |-  ( ( ph /\ v e. A ) -> ( H ` v ) e. CC )
195 194 subid1d 
 |-  ( ( ph /\ v e. A ) -> ( ( H ` v ) - 0 ) = ( H ` v ) )
196 nfmpt1 
 |-  F/_ x ( x e. A |-> ( B / C ) )
197 3 196 nfcxfr 
 |-  F/_ x H
198 197 165 nffv 
 |-  F/_ x ( H ` v )
199 nfcv 
 |-  F/_ x /
200 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
201 2 200 nfcxfr 
 |-  F/_ x G
202 201 165 nffv 
 |-  F/_ x ( G ` v )
203 166 199 202 nfov 
 |-  F/_ x ( ( F ` v ) / ( G ` v ) )
204 198 203 nfeq 
 |-  F/ x ( H ` v ) = ( ( F ` v ) / ( G ` v ) )
205 162 204 nfim 
 |-  F/ x ( ( ph /\ v e. A ) -> ( H ` v ) = ( ( F ` v ) / ( G ` v ) ) )
206 fveq2 
 |-  ( x = v -> ( H ` x ) = ( H ` v ) )
207 fveq2 
 |-  ( x = v -> ( G ` x ) = ( G ` v ) )
208 171 207 oveq12d 
 |-  ( x = v -> ( ( F ` x ) / ( G ` x ) ) = ( ( F ` v ) / ( G ` v ) ) )
209 206 208 eqeq12d 
 |-  ( x = v -> ( ( H ` x ) = ( ( F ` x ) / ( G ` x ) ) <-> ( H ` v ) = ( ( F ` v ) / ( G ` v ) ) ) )
210 170 209 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) / ( G ` x ) ) ) <-> ( ( ph /\ v e. A ) -> ( H ` v ) = ( ( F ` v ) / ( G ` v ) ) ) ) )
211 3 fvmpt2 
 |-  ( ( x e. A /\ ( B / C ) e. CC ) -> ( H ` x ) = ( B / C ) )
212 174 192 211 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = ( B / C ) )
213 176 eqcomd 
 |-  ( ( ph /\ x e. A ) -> B = ( F ` x ) )
214 2 fvmpt2 
 |-  ( ( x e. A /\ C e. ( CC \ { 0 } ) ) -> ( G ` x ) = C )
215 174 5 214 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = C )
216 215 eqcomd 
 |-  ( ( ph /\ x e. A ) -> C = ( G ` x ) )
217 213 216 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( B / C ) = ( ( F ` x ) / ( G ` x ) ) )
218 212 217 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) / ( G ` x ) ) )
219 205 210 218 chvarfv 
 |-  ( ( ph /\ v e. A ) -> ( H ` v ) = ( ( F ` v ) / ( G ` v ) ) )
220 195 219 eqtrd 
 |-  ( ( ph /\ v e. A ) -> ( ( H ` v ) - 0 ) = ( ( F ` v ) / ( G ` v ) ) )
221 220 fveq2d 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( H ` v ) - 0 ) ) = ( abs ` ( ( F ` v ) / ( G ` v ) ) ) )
222 188 189 221 syl2anc 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( 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+ ) )
224 223 189 jca 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( ( 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 
 |-  F/_ x 0
228 202 227 nfne 
 |-  F/ x ( G ` v ) =/= 0
229 162 228 nfim 
 |-  F/ x ( ( ph /\ v e. A ) -> ( G ` v ) =/= 0 )
230 207 neeq1d 
 |-  ( x = v -> ( ( G ` x ) =/= 0 <-> ( G ` v ) =/= 0 ) )
231 170 230 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. A ) -> ( G ` x ) =/= 0 ) <-> ( ( ph /\ v e. A ) -> ( G ` v ) =/= 0 ) ) )
232 215 191 eqnetrd 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) =/= 0 )
233 229 231 232 chvarfv 
 |-  ( ( ph /\ v e. A ) -> ( G ` v ) =/= 0 )
234 178 58 233 absdivd 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( F ` v ) / ( G ` v ) ) ) = ( ( abs ` ( F ` v ) ) / ( abs ` ( G ` v ) ) ) )
235 234 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( abs ` ( ( F ` v ) / ( G ` v ) ) ) = ( ( abs ` ( F ` v ) ) / ( abs ` ( G ` v ) ) ) )
236 235 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) ) )
237 178 abscld 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( F ` v ) ) e. RR )
238 58 233 absne0d 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( G ` v ) ) =/= 0 )
239 237 79 238 redivcld 
 |-  ( ( ph /\ v e. A ) -> ( ( abs ` ( F ` v ) ) / ( abs ` ( G ` v ) ) ) e. RR )
240 239 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( ( abs ` ( F ` v ) ) / ( abs ` ( G ` v ) ) ) e. RR )
241 240 ad2antrr 
 |-  ( ( ( ( ( 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 
 |-  ( y e. RR+ -> y e. RR )
243 242 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> y e. RR )
244 21 rpred 
 |-  ( ph -> ( ( abs ` D ) / 2 ) e. RR )
245 244 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( ( abs ` D ) / 2 ) e. RR )
246 243 245 remulcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( y x. ( ( abs ` D ) / 2 ) ) e. RR )
247 246 ad2antrr 
 |-  ( ( ( ( ( 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 )
248 58 233 absrpcld 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( G ` v ) ) e. RR+ )
249 248 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( abs ` ( G ` v ) ) e. RR+ )
250 249 ad2antrr 
 |-  ( ( ( ( ( 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+ )
251 247 250 rerpdivcld 
 |-  ( ( ( ( ( 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 )
252 243 ad2antrr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) /\ ( abs ` ( F ` v ) ) < ( y x. ( ( abs ` D ) / 2 ) ) ) -> ph )
254 simpllr 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) /\ ( abs ` ( F ` v ) ) < ( y x. ( ( abs ` D ) / 2 ) ) ) -> v e. A )
255 253 254 237 syl2anc 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 ) ) )
257 255 247 250 256 ltdiv1dd 
 |-  ( ( ( ( ( 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 ) ) ) )
258 243 recnd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> y e. CC )
259 48 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( ( abs ` D ) / 2 ) e. CC )
260 249 rpcnd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( abs ` ( G ` v ) ) e. CC )
261 238 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( abs ` ( G ` v ) ) =/= 0 )
262 258 259 260 261 divassd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( ( y x. ( ( abs ` D ) / 2 ) ) / ( abs ` ( G ` v ) ) ) = ( y x. ( ( ( abs ` D ) / 2 ) / ( abs ` ( G ` v ) ) ) ) )
263 262 adantr 
 |-  ( ( ( ( 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 ) ) ) ) )
264 245 249 rerpdivcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( ( ( abs ` D ) / 2 ) / ( abs ` ( G ` v ) ) ) e. RR )
265 264 adantr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( ( abs ` D ) / 2 ) / ( abs ` ( G ` v ) ) ) e. RR )
266 1red 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> 1 e. RR )
267 simpllr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> y e. RR+ )
268 244 ad2antrr 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( abs ` D ) / 2 ) e. RR )
269 1rp 
 |-  1 e. RR+
270 269 a1i 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> 1 e. RR+ )
271 248 adantr 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( abs ` ( G ` v ) ) e. RR+ )
272 48 div1d 
 |-  ( ph -> ( ( ( abs ` D ) / 2 ) / 1 ) = ( ( abs ` D ) / 2 ) )
273 272 ad2antrr 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( ( abs ` D ) / 2 ) / 1 ) = ( ( abs ` D ) / 2 ) )
274 simpr 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) )
275 273 274 eqbrtrd 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( ( abs ` D ) / 2 ) / 1 ) < ( abs ` ( G ` v ) ) )
276 268 270 271 275 ltdiv23d 
 |-  ( ( ( ph /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( ( abs ` D ) / 2 ) / ( abs ` ( G ` v ) ) ) < 1 )
277 276 adantllr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( ( abs ` D ) / 2 ) / ( abs ` ( G ` v ) ) ) < 1 )
278 265 266 267 277 ltmul2dd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( y x. ( ( ( abs ` D ) / 2 ) / ( abs ` ( G ` v ) ) ) ) < ( y x. 1 ) )
279 263 278 eqbrtrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( y x. ( ( abs ` D ) / 2 ) ) / ( abs ` ( G ` v ) ) ) < ( y x. 1 ) )
280 258 mulridd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( y x. 1 ) = y )
281 280 adantr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( y x. 1 ) = y )
282 279 281 breqtrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ v e. A ) /\ ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> ( ( y x. ( ( abs ` D ) / 2 ) ) / ( abs ` ( G ` v ) ) ) < y )
283 282 adantr 
 |-  ( ( ( ( ( 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 ) ) ) < y )
284 241 251 252 257 283 lttrd 
 |-  ( ( ( ( ( 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 )
285 236 284 eqbrtrd 
 |-  ( ( ( ( ( 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 ) ) ) < y )
286 224 225 226 285 syl21anc 
 |-  ( ( ( ( ( ( ( ( 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 ) / ( G ` v ) ) ) < y )
287 222 286 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) < y )
288 129 151 187 287 syl21anc 
 |-  ( ( ( ( ( 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 ` ( ( H ` v ) - 0 ) ) < y )
289 288 3exp 
 |-  ( ( ( ( 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 ` ( ( H ` v ) - 0 ) ) < y ) ) )
290 122 289 ralrimi 
 |-  ( ( ( ( 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. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < if ( z <_ u , z , u ) ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) )
291 brimralrspcev 
 |-  ( ( if ( z <_ u , z , u ) e. RR+ /\ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < if ( z <_ u , z , u ) ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) ) -> E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) )
292 115 290 291 syl2anc 
 |-  ( ( ( ( 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. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) )
293 292 rexlimdv3a 
 |-  ( ( ( 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 ) ) ) -> E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) ) )
294 112 293 mpd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ z e. RR+ /\ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) ) -> E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) )
295 294 rexlimdv3a 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. z e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < z ) -> ( ( abs ` D ) / 2 ) < ( abs ` ( G ` v ) ) ) -> E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) ) )
296 90 295 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) )
297 296 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) )
298 193 12 15 ellimc3 
 |-  ( ph -> ( 0 e. ( H limCC E ) <-> ( 0 e. CC /\ A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= E /\ ( abs ` ( v - E ) ) < w ) -> ( abs ` ( ( H ` v ) - 0 ) ) < y ) ) ) )
299 9 297 298 mpbir2and 
 |-  ( ph -> 0 e. ( H limCC E ) )