Metamath Proof Explorer

Theorem addlimc

Description: Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses addlimc.f 
|- F = ( x e. A |-> B )
addlimc.g 
|- G = ( x e. A |-> C )
addlimc.h 
|- H = ( x e. A |-> ( B + C ) )
addlimc.b 
|- ( ( ph /\ x e. A ) -> B e. CC )
addlimc.c 
|- ( ( ph /\ x e. A ) -> C e. CC )
addlimc.e 
|- ( ph -> E e. ( F limCC D ) )
addlimc.i 
|- ( ph -> I e. ( G limCC D ) )
Assertion addlimc 
|- ( ph -> ( E + I ) e. ( H limCC D ) )

Proof

Step Hyp Ref Expression
1 addlimc.f 
 |-  F = ( x e. A |-> B )
2 addlimc.g 
 |-  G = ( x e. A |-> C )
3 addlimc.h 
 |-  H = ( x e. A |-> ( B + C ) )
4 addlimc.b 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 addlimc.c 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
6 addlimc.e 
 |-  ( ph -> E e. ( F limCC D ) )
7 addlimc.i 
 |-  ( ph -> I e. ( G limCC D ) )
8 limccl 
 |-  ( F limCC D ) C_ CC
9 8 6 sseldi 
 |-  ( ph -> E e. CC )
10 limccl 
 |-  ( G limCC D ) C_ CC
11 10 7 sseldi 
 |-  ( ph -> I e. CC )
12 9 11 addcld 
 |-  ( ph -> ( E + I ) e. CC )
13 4 1 fmptd 
 |-  ( ph -> F : A --> CC )
14 1 4 6 limcmptdm 
 |-  ( ph -> A C_ CC )
15 limcrcl 
 |-  ( E e. ( F limCC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
16 6 15 syl 
 |-  ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
17 16 simp3d 
 |-  ( ph -> D e. CC )
18 13 14 17 ellimc3 
 |-  ( ph -> ( E e. ( F limCC D ) <-> ( E e. CC /\ A. z e. RR+ E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < z ) ) ) )
19 6 18 mpbid 
 |-  ( ph -> ( E e. CC /\ A. z e. RR+ E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < z ) ) )
20 19 simprd 
 |-  ( ph -> A. z e. RR+ E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < z ) )
21 rphalfcl 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR+ )
22 breq2 
 |-  ( z = ( y / 2 ) -> ( ( abs ` ( ( F ` v ) - E ) ) < z <-> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) )
23 22 imbi2d 
 |-  ( z = ( y / 2 ) -> ( ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < z ) <-> ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) ) )
24 23 rexralbidv 
 |-  ( z = ( y / 2 ) -> ( E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < z ) <-> E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) ) )
25 24 rspccva 
 |-  ( ( A. z e. RR+ E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < z ) /\ ( y / 2 ) e. RR+ ) -> E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) )
26 20 21 25 syl2an 
 |-  ( ( ph /\ y e. RR+ ) -> E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) )
27 5 2 fmptd 
 |-  ( ph -> G : A --> CC )
28 27 14 17 ellimc3 
 |-  ( ph -> ( I e. ( G limCC D ) <-> ( I e. CC /\ A. z e. RR+ E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < z ) ) ) )
29 7 28 mpbid 
 |-  ( ph -> ( I e. CC /\ A. z e. RR+ E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < z ) ) )
30 29 simprd 
 |-  ( ph -> A. z e. RR+ E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < z ) )
31 breq2 
 |-  ( z = ( y / 2 ) -> ( ( abs ` ( ( G ` v ) - I ) ) < z <-> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) )
32 31 imbi2d 
 |-  ( z = ( y / 2 ) -> ( ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < z ) <-> ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) )
33 32 rexralbidv 
 |-  ( z = ( y / 2 ) -> ( E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < z ) <-> E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) )
34 33 rspccva 
 |-  ( ( A. z e. RR+ E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < z ) /\ ( y / 2 ) e. RR+ ) -> E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) )
35 30 21 34 syl2an 
 |-  ( ( ph /\ y e. RR+ ) -> E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) )
36 reeanv 
 |-  ( E. a e. RR+ E. b e. RR+ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) <-> ( E. a e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ E. b e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) )
37 26 35 36 sylanbrc 
 |-  ( ( ph /\ y e. RR+ ) -> E. a e. RR+ E. b e. RR+ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) )
38 ifcl 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) e. RR+ )
39 38 3ad2ant2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> if ( a <_ b , a , b ) e. RR+ )
40 nfv 
 |-  F/ v ( ph /\ y e. RR+ )
41 nfv 
 |-  F/ v ( a e. RR+ /\ b e. RR+ )
42 nfra1 
 |-  F/ v A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) )
43 nfra1 
 |-  F/ v A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) )
44 42 43 nfan 
 |-  F/ v ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) )
45 40 41 44 nf3an 
 |-  F/ v ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) )
46 simp11l 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ph )
47 simp2 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> v e. A )
48 46 47 jca 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( ph /\ v e. A ) )
49 rpre 
 |-  ( y e. RR+ -> y e. RR )
50 49 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR )
51 50 3ad2ant1 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> y e. RR )
52 51 3ad2ant1 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> y e. RR )
53 simp13l 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) )
54 simp3l 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> v =/= D )
55 14 sselda 
 |-  ( ( ph /\ v e. A ) -> v e. CC )
56 46 47 55 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> v e. CC )
57 46 17 syl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> D e. CC )
58 56 57 subcld 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( v - D ) e. CC )
59 58 abscld 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( v - D ) ) e. RR )
60 39 rpred 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> if ( a <_ b , a , b ) e. RR )
61 60 3ad2ant1 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> if ( a <_ b , a , b ) e. RR )
62 simpl 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> a e. RR+ )
63 62 rpred 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> a e. RR )
64 63 3ad2ant2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> a e. RR )
65 64 3ad2ant1 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> a e. RR )
66 simp3r 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) )
67 simpr 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> b e. RR+ )
68 67 rpred 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> b e. RR )
69 min1 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , a , b ) <_ a )
70 63 68 69 syl2anc 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) <_ a )
71 70 3ad2ant2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> if ( a <_ b , a , b ) <_ a )
72 71 3ad2ant1 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> if ( a <_ b , a , b ) <_ a )
73 59 61 65 66 72 ltletrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( v - D ) ) < a )
74 54 73 jca 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( v =/= D /\ ( abs ` ( v - D ) ) < a ) )
75 rsp 
 |-  ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) -> ( v e. A -> ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) ) )
76 53 47 74 75 syl3c 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) )
77 48 52 76 jca31 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) )
78 simp13r 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) )
79 68 3ad2ant2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> b e. RR )
80 79 3ad2ant1 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> b e. RR )
81 min2 
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , a , b ) <_ b )
82 63 68 81 syl2anc 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> if ( a <_ b , a , b ) <_ b )
83 82 3ad2ant2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> if ( a <_ b , a , b ) <_ b )
84 83 3ad2ant1 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> if ( a <_ b , a , b ) <_ b )
85 59 61 80 66 84 ltletrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( v - D ) ) < b )
86 54 85 jca 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( v =/= D /\ ( abs ` ( v - D ) ) < b ) )
87 rsp 
 |-  ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( v e. A -> ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) )
88 78 47 86 87 syl3c 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) )
89 4 5 addcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. CC )
90 89 3 fmptd 
 |-  ( ph -> H : A --> CC )
91 90 ffvelrnda 
 |-  ( ( ph /\ v e. A ) -> ( H ` v ) e. CC )
92 91 ad3antrrr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( H ` v ) e. CC )
93 simp-4l 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ph )
94 93 12 syl 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( E + I ) e. CC )
95 92 94 subcld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( H ` v ) - ( E + I ) ) e. CC )
96 95 abscld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) e. RR )
97 13 ffvelrnda 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) e. CC )
98 97 ad3antrrr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( F ` v ) e. CC )
99 93 9 syl 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> E e. CC )
100 98 99 subcld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( F ` v ) - E ) e. CC )
101 100 abscld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( F ` v ) - E ) ) e. RR )
102 27 ffvelrnda 
 |-  ( ( ph /\ v e. A ) -> ( G ` v ) e. CC )
103 102 ad3antrrr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( G ` v ) e. CC )
104 93 11 syl 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> I e. CC )
105 103 104 subcld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( G ` v ) - I ) e. CC )
106 105 abscld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` v ) - I ) ) e. RR )
107 101 106 readdcld 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( abs ` ( ( F ` v ) - E ) ) + ( abs ` ( ( G ` v ) - I ) ) ) e. RR )
108 simpllr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> y e. RR )
109 nfv 
 |-  F/ x ( ph /\ v e. A )
110 nfmpt1 
 |-  F/_ x ( x e. A |-> ( B + C ) )
111 3 110 nfcxfr 
 |-  F/_ x H
112 nfcv 
 |-  F/_ x v
113 111 112 nffv 
 |-  F/_ x ( H ` v )
114 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
115 1 114 nfcxfr 
 |-  F/_ x F
116 115 112 nffv 
 |-  F/_ x ( F ` v )
117 nfcv 
 |-  F/_ x +
118 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
119 2 118 nfcxfr 
 |-  F/_ x G
120 119 112 nffv 
 |-  F/_ x ( G ` v )
121 116 117 120 nfov 
 |-  F/_ x ( ( F ` v ) + ( G ` v ) )
122 113 121 nfeq 
 |-  F/ x ( H ` v ) = ( ( F ` v ) + ( G ` v ) )
123 109 122 nfim 
 |-  F/ x ( ( ph /\ v e. A ) -> ( H ` v ) = ( ( F ` v ) + ( G ` v ) ) )
124 eleq1w 
 |-  ( x = v -> ( x e. A <-> v e. A ) )
125 124 anbi2d 
 |-  ( x = v -> ( ( ph /\ x e. A ) <-> ( ph /\ v e. A ) ) )
126 fveq2 
 |-  ( x = v -> ( H ` x ) = ( H ` v ) )
127 fveq2 
 |-  ( x = v -> ( F ` x ) = ( F ` v ) )
128 fveq2 
 |-  ( x = v -> ( G ` x ) = ( G ` v ) )
129 127 128 oveq12d 
 |-  ( x = v -> ( ( F ` x ) + ( G ` x ) ) = ( ( F ` v ) + ( G ` v ) ) )
130 126 129 eqeq12d 
 |-  ( x = v -> ( ( H ` x ) = ( ( F ` x ) + ( G ` x ) ) <-> ( H ` v ) = ( ( F ` v ) + ( G ` v ) ) ) )
131 125 130 imbi12d 
 |-  ( x = v -> ( ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) + ( G ` x ) ) ) <-> ( ( ph /\ v e. A ) -> ( H ` v ) = ( ( F ` v ) + ( G ` v ) ) ) ) )
132 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
133 3 fvmpt2 
 |-  ( ( x e. A /\ ( B + C ) e. CC ) -> ( H ` x ) = ( B + C ) )
134 132 89 133 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = ( B + C ) )
135 1 fvmpt2 
 |-  ( ( x e. A /\ B e. CC ) -> ( F ` x ) = B )
136 132 4 135 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
137 136 eqcomd 
 |-  ( ( ph /\ x e. A ) -> B = ( F ` x ) )
138 2 fvmpt2 
 |-  ( ( x e. A /\ C e. CC ) -> ( G ` x ) = C )
139 132 5 138 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = C )
140 139 eqcomd 
 |-  ( ( ph /\ x e. A ) -> C = ( G ` x ) )
141 137 140 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) = ( ( F ` x ) + ( G ` x ) ) )
142 134 141 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) = ( ( F ` x ) + ( G ` x ) ) )
143 123 131 142 chvarfv 
 |-  ( ( ph /\ v e. A ) -> ( H ` v ) = ( ( F ` v ) + ( G ` v ) ) )
144 143 ad3antrrr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( H ` v ) = ( ( F ` v ) + ( G ` v ) ) )
145 144 oveq1d 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( H ` v ) - ( E + I ) ) = ( ( ( F ` v ) + ( G ` v ) ) - ( E + I ) ) )
146 98 103 99 104 addsub4d 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( ( F ` v ) + ( G ` v ) ) - ( E + I ) ) = ( ( ( F ` v ) - E ) + ( ( G ` v ) - I ) ) )
147 145 146 eqtrd 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( H ` v ) - ( E + I ) ) = ( ( ( F ` v ) - E ) + ( ( G ` v ) - I ) ) )
148 147 fveq2d 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) = ( abs ` ( ( ( F ` v ) - E ) + ( ( G ` v ) - I ) ) ) )
149 100 105 abstrid 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( ( F ` v ) - E ) + ( ( G ` v ) - I ) ) ) <_ ( ( abs ` ( ( F ` v ) - E ) ) + ( abs ` ( ( G ` v ) - I ) ) ) )
150 148 149 eqbrtrd 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) <_ ( ( abs ` ( ( F ` v ) - E ) ) + ( abs ` ( ( G ` v ) - I ) ) ) )
151 simplr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) )
152 simpr 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) )
153 101 106 108 151 152 lt2halvesd 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( ( abs ` ( ( F ` v ) - E ) ) + ( abs ` ( ( G ` v ) - I ) ) ) < y )
154 96 107 108 150 153 lelttrd 
 |-  ( ( ( ( ( ph /\ v e. A ) /\ y e. RR ) /\ ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y )
155 77 88 154 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) /\ v e. A /\ ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y )
156 155 3exp 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> ( v e. A -> ( ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) ) )
157 45 156 ralrimi 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) )
158 brimralrspcev 
 |-  ( ( if ( a <_ b , a , b ) e. RR+ /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < if ( a <_ b , a , b ) ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) )
159 39 157 158 syl2anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( a e. RR+ /\ b e. RR+ ) /\ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) )
160 159 3exp 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( a e. RR+ /\ b e. RR+ ) -> ( ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) ) ) )
161 160 rexlimdvv 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. a e. RR+ E. b e. RR+ ( A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < a ) -> ( abs ` ( ( F ` v ) - E ) ) < ( y / 2 ) ) /\ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < b ) -> ( abs ` ( ( G ` v ) - I ) ) < ( y / 2 ) ) ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) ) )
162 37 161 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) )
163 162 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) )
164 90 14 17 ellimc3 
 |-  ( ph -> ( ( E + I ) e. ( H limCC D ) <-> ( ( E + I ) e. CC /\ A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= D /\ ( abs ` ( v - D ) ) < w ) -> ( abs ` ( ( H ` v ) - ( E + I ) ) ) < y ) ) ) )
165 12 163 164 mpbir2and 
 |-  ( ph -> ( E + I ) e. ( H limCC D ) )