Metamath Proof Explorer

Theorem pntpbnd1

Description: Lemma for pntpbnd . (Contributed by Mario Carneiro, 11-Apr-2016)

Ref Expression
Hypotheses pntpbnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntpbnd1.e 
|- ( ph -> E e. ( 0 (,) 1 ) )
pntpbnd1.x 
|- X = ( exp ` ( 2 / E ) )
pntpbnd1.y 
|- ( ph -> Y e. ( X (,) +oo ) )
pntpbnd1.1 
|- ( ph -> A e. RR+ )
pntpbnd1.2 
|- ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )
pntpbnd1.c 
|- C = ( A + 2 )
pntpbnd1.k 
|- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )
pntpbnd1.3 
|- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
Assertion pntpbnd1 
|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )

Proof

Step Hyp Ref Expression
1 pntpbnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntpbnd1.e 
 |-  ( ph -> E e. ( 0 (,) 1 ) )
3 pntpbnd1.x 
 |-  X = ( exp ` ( 2 / E ) )
4 pntpbnd1.y 
 |-  ( ph -> Y e. ( X (,) +oo ) )
5 pntpbnd1.1 
 |-  ( ph -> A e. RR+ )
6 pntpbnd1.2 
 |-  ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )
7 pntpbnd1.c 
 |-  C = ( A + 2 )
8 pntpbnd1.k 
 |-  ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )
9 pntpbnd1.3 
 |-  ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
10 fzfid 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) e. Fin )
11 ioossre 
 |-  ( X (,) +oo ) C_ RR
12 11 4 sselid 
 |-  ( ph -> Y e. RR )
13 0red 
 |-  ( ph -> 0 e. RR )
14 2re 
 |-  2 e. RR
15 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
16 15 2 sselid 
 |-  ( ph -> E e. RR )
17 eliooord 
 |-  ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
18 2 17 syl 
 |-  ( ph -> ( 0 < E /\ E < 1 ) )
19 18 simpld 
 |-  ( ph -> 0 < E )
20 16 19 elrpd 
 |-  ( ph -> E e. RR+ )
21 rerpdivcl 
 |-  ( ( 2 e. RR /\ E e. RR+ ) -> ( 2 / E ) e. RR )
22 14 20 21 sylancr 
 |-  ( ph -> ( 2 / E ) e. RR )
23 22 reefcld 
 |-  ( ph -> ( exp ` ( 2 / E ) ) e. RR )
24 3 23 eqeltrid 
 |-  ( ph -> X e. RR )
25 efgt0 
 |-  ( ( 2 / E ) e. RR -> 0 < ( exp ` ( 2 / E ) ) )
26 22 25 syl 
 |-  ( ph -> 0 < ( exp ` ( 2 / E ) ) )
27 26 3 breqtrrdi 
 |-  ( ph -> 0 < X )
28 eliooord 
 |-  ( Y e. ( X (,) +oo ) -> ( X < Y /\ Y < +oo ) )
29 4 28 syl 
 |-  ( ph -> ( X < Y /\ Y < +oo ) )
30 29 simpld 
 |-  ( ph -> X < Y )
31 13 24 12 27 30 lttrd 
 |-  ( ph -> 0 < Y )
32 13 12 31 ltled 
 |-  ( ph -> 0 <_ Y )
33 flge0nn0 
 |-  ( ( Y e. RR /\ 0 <_ Y ) -> ( |_ ` Y ) e. NN0 )
34 12 32 33 syl2anc 
 |-  ( ph -> ( |_ ` Y ) e. NN0 )
35 nn0p1nn 
 |-  ( ( |_ ` Y ) e. NN0 -> ( ( |_ ` Y ) + 1 ) e. NN )
36 34 35 syl 
 |-  ( ph -> ( ( |_ ` Y ) + 1 ) e. NN )
37 elfzuz 
 |-  ( n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
38 eluznn 
 |-  ( ( ( ( |_ ` Y ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) ) -> n e. NN )
39 36 37 38 syl2an 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. NN )
40 39 nnrpd 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. RR+ )
41 1 pntrf 
 |-  R : RR+ --> RR
42 41 ffvelcdmi 
 |-  ( n e. RR+ -> ( R ` n ) e. RR )
43 40 42 syl 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
44 39 peano2nnd 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) e. NN )
45 39 44 nnmulcld 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
46 43 45 nndivred 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
47 46 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
48 10 47 fsumrecl 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
49 43 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
50 fveq2 
 |-  ( i = n -> ( R ` i ) = ( R ` n ) )
51 50 breq2d 
 |-  ( i = n -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` n ) ) )
52 51 rspccva 
 |-  ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( R ` n ) )
53 52 adantll 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( R ` n ) )
54 45 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
55 54 nnred 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. RR )
56 54 nngt0d 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 < ( n x. ( n + 1 ) ) )
57 divge0 
 |-  ( ( ( ( R ` n ) e. RR /\ 0 <_ ( R ` n ) ) /\ ( ( n x. ( n + 1 ) ) e. RR /\ 0 < ( n x. ( n + 1 ) ) ) ) -> 0 <_ ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
58 49 53 55 56 57 syl22anc 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
59 10 47 58 fsumge0 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> 0 <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
60 48 59 absidd 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
61 47 58 absidd 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
62 61 sumeq2dv 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
63 60 62 eqtr4d 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
64 fzfid 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) e. Fin )
65 46 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
66 65 recnd 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
67 64 66 fsumneg 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
68 43 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
69 68 renegcld 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( R ` n ) e. RR )
70 50 breq1d 
 |-  ( i = n -> ( ( R ` i ) <_ 0 <-> ( R ` n ) <_ 0 ) )
71 70 rspccva 
 |-  ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) <_ 0 )
72 71 adantll 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) <_ 0 )
73 68 le0neg1d 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) <_ 0 <-> 0 <_ -u ( R ` n ) ) )
74 72 73 mpbid 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ -u ( R ` n ) )
75 45 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
76 75 nnred 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. RR )
77 75 nngt0d 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 < ( n x. ( n + 1 ) ) )
78 divge0 
 |-  ( ( ( -u ( R ` n ) e. RR /\ 0 <_ -u ( R ` n ) ) /\ ( ( n x. ( n + 1 ) ) e. RR /\ 0 < ( n x. ( n + 1 ) ) ) ) -> 0 <_ ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
79 69 74 76 77 78 syl22anc 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
80 43 recnd 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. CC )
81 45 nncnd 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. CC )
82 45 nnne0d 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) =/= 0 )
83 80 81 82 divnegd 
 |-  ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
84 83 adantlr 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
85 79 84 breqtrrd 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
86 65 le0neg1d 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 <-> 0 <_ -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
87 85 86 mpbird 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 )
88 65 87 absnidd 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
89 88 sumeq2dv 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
90 64 65 fsumrecl 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
91 65 renegcld 
 |-  ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
92 64 91 85 fsumge0 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> 0 <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
93 92 67 breqtrd 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> 0 <_ -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
94 90 le0neg1d 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 <-> 0 <_ -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
95 93 94 mpbird 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 )
96 90 95 absnidd 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
97 67 89 96 3eqtr4rd 
 |-  ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
98 2rp 
 |-  2 e. RR+
99 rpaddcl 
 |-  ( ( A e. RR+ /\ 2 e. RR+ ) -> ( A + 2 ) e. RR+ )
100 5 98 99 sylancl 
 |-  ( ph -> ( A + 2 ) e. RR+ )
101 7 100 eqeltrid 
 |-  ( ph -> C e. RR+ )
102 101 20 rpdivcld 
 |-  ( ph -> ( C / E ) e. RR+ )
103 102 rpred 
 |-  ( ph -> ( C / E ) e. RR )
104 103 reefcld 
 |-  ( ph -> ( exp ` ( C / E ) ) e. RR )
105 pnfxr 
 |-  +oo e. RR*
106 icossre 
 |-  ( ( ( exp ` ( C / E ) ) e. RR /\ +oo e. RR* ) -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
107 104 105 106 sylancl 
 |-  ( ph -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
108 107 8 sseldd 
 |-  ( ph -> K e. RR )
109 108 12 remulcld 
 |-  ( ph -> ( K x. Y ) e. RR )
110 12 recnd 
 |-  ( ph -> Y e. CC )
111 110 mullidd 
 |-  ( ph -> ( 1 x. Y ) = Y )
112 1red 
 |-  ( ph -> 1 e. RR )
113 efgt1 
 |-  ( ( C / E ) e. RR+ -> 1 < ( exp ` ( C / E ) ) )
114 102 113 syl 
 |-  ( ph -> 1 < ( exp ` ( C / E ) ) )
115 elicopnf 
 |-  ( ( exp ` ( C / E ) ) e. RR -> ( K e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) ) )
116 104 115 syl 
 |-  ( ph -> ( K e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) ) )
117 116 simplbda 
 |-  ( ( ph /\ K e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( exp ` ( C / E ) ) <_ K )
118 8 117 mpdan 
 |-  ( ph -> ( exp ` ( C / E ) ) <_ K )
119 112 104 108 114 118 ltletrd 
 |-  ( ph -> 1 < K )
120 ltmul1 
 |-  ( ( 1 e. RR /\ K e. RR /\ ( Y e. RR /\ 0 < Y ) ) -> ( 1 < K <-> ( 1 x. Y ) < ( K x. Y ) ) )
121 112 108 12 31 120 syl112anc 
 |-  ( ph -> ( 1 < K <-> ( 1 x. Y ) < ( K x. Y ) ) )
122 119 121 mpbid 
 |-  ( ph -> ( 1 x. Y ) < ( K x. Y ) )
123 111 122 eqbrtrrd 
 |-  ( ph -> Y < ( K x. Y ) )
124 12 109 123 ltled 
 |-  ( ph -> Y <_ ( K x. Y ) )
125 flword2 
 |-  ( ( Y e. RR /\ ( K x. Y ) e. RR /\ Y <_ ( K x. Y ) ) -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) )
126 12 109 124 125 syl3anc 
 |-  ( ph -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) )
127 109 flcld 
 |-  ( ph -> ( |_ ` ( K x. Y ) ) e. ZZ )
128 uzid 
 |-  ( ( |_ ` ( K x. Y ) ) e. ZZ -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` ( K x. Y ) ) ) )
129 127 128 syl 
 |-  ( ph -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` ( K x. Y ) ) ) )
130 elfzuzb 
 |-  ( ( |_ ` ( K x. Y ) ) e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) <-> ( ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) /\ ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` ( K x. Y ) ) ) ) )
131 126 129 130 sylanbrc 
 |-  ( ph -> ( |_ ` ( K x. Y ) ) e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) )
132 oveq2 
 |-  ( x = ( |_ ` Y ) -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) )
133 132 raleqdv 
 |-  ( x = ( |_ ` Y ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) ) )
134 132 raleqdv 
 |-  ( x = ( |_ ` Y ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) )
135 133 134 orbi12d 
 |-  ( x = ( |_ ` Y ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) ) )
136 135 imbi2d 
 |-  ( x = ( |_ ` Y ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) ) ) )
137 oveq2 
 |-  ( x = m -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... m ) )
138 137 raleqdv 
 |-  ( x = m -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) ) )
139 137 raleqdv 
 |-  ( x = m -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) )
140 138 139 orbi12d 
 |-  ( x = m -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) ) )
141 140 imbi2d 
 |-  ( x = m -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) ) ) )
142 oveq2 
 |-  ( x = ( m + 1 ) -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) )
143 142 raleqdv 
 |-  ( x = ( m + 1 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) ) )
144 142 raleqdv 
 |-  ( x = ( m + 1 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) )
145 143 144 orbi12d 
 |-  ( x = ( m + 1 ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
146 145 imbi2d 
 |-  ( x = ( m + 1 ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) ) )
147 oveq2 
 |-  ( x = ( |_ ` ( K x. Y ) ) -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) )
148 147 raleqdv 
 |-  ( x = ( |_ ` ( K x. Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) )
149 147 raleqdv 
 |-  ( x = ( |_ ` ( K x. Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) )
150 148 149 orbi12d 
 |-  ( x = ( |_ ` ( K x. Y ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) ) )
151 150 imbi2d 
 |-  ( x = ( |_ ` ( K x. Y ) ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) ) ) )
152 elfzle3 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` Y ) + 1 ) <_ ( |_ ` Y ) )
153 elfzel2 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( |_ ` Y ) e. ZZ )
154 153 zred 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( |_ ` Y ) e. RR )
155 154 ltp1d 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( |_ ` Y ) < ( ( |_ ` Y ) + 1 ) )
156 peano2re 
 |-  ( ( |_ ` Y ) e. RR -> ( ( |_ ` Y ) + 1 ) e. RR )
157 154 156 syl 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` Y ) + 1 ) e. RR )
158 154 157 ltnled 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` Y ) < ( ( |_ ` Y ) + 1 ) <-> -. ( ( |_ ` Y ) + 1 ) <_ ( |_ ` Y ) ) )
159 155 158 mpbid 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> -. ( ( |_ ` Y ) + 1 ) <_ ( |_ ` Y ) )
160 152 159 pm2.21dd 
 |-  ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( R ` i ) <_ 0 )
161 160 rgen 
 |-  A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0
162 161 olci 
 |-  ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 )
163 162 2a1i 
 |-  ( ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) -> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) ) )
164 elfzofz 
 |-  ( m e. ( ( |_ ` Y ) ..^ ( |_ ` ( K x. Y ) ) ) -> m e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) )
165 elfzp12 
 |-  ( ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) -> ( m e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) <-> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) )
166 126 165 syl 
 |-  ( ph -> ( m e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) <-> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) )
167 164 166 imbitrid 
 |-  ( ph -> ( m e. ( ( |_ ` Y ) ..^ ( |_ ` ( K x. Y ) ) ) -> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) )
168 167 imp 
 |-  ( ( ph /\ m e. ( ( |_ ` Y ) ..^ ( |_ ` ( K x. Y ) ) ) ) -> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) )
169 36 nnrpd 
 |-  ( ph -> ( ( |_ ` Y ) + 1 ) e. RR+ )
170 41 ffvelcdmi 
 |-  ( ( ( |_ ` Y ) + 1 ) e. RR+ -> ( R ` ( ( |_ ` Y ) + 1 ) ) e. RR )
171 169 170 syl 
 |-  ( ph -> ( R ` ( ( |_ ` Y ) + 1 ) ) e. RR )
172 13 171 letrid 
 |-  ( ph -> ( 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) \/ ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
173 172 adantr 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) \/ ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
174 oveq1 
 |-  ( m = ( |_ ` Y ) -> ( m + 1 ) = ( ( |_ ` Y ) + 1 ) )
175 174 oveq2d 
 |-  ( m = ( |_ ` Y ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = ( ( ( |_ ` Y ) + 1 ) ... ( ( |_ ` Y ) + 1 ) ) )
176 12 flcld 
 |-  ( ph -> ( |_ ` Y ) e. ZZ )
177 176 peano2zd 
 |-  ( ph -> ( ( |_ ` Y ) + 1 ) e. ZZ )
178 fzsn 
 |-  ( ( ( |_ ` Y ) + 1 ) e. ZZ -> ( ( ( |_ ` Y ) + 1 ) ... ( ( |_ ` Y ) + 1 ) ) = { ( ( |_ ` Y ) + 1 ) } )
179 177 178 syl 
 |-  ( ph -> ( ( ( |_ ` Y ) + 1 ) ... ( ( |_ ` Y ) + 1 ) ) = { ( ( |_ ` Y ) + 1 ) } )
180 175 179 sylan9eqr 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = { ( ( |_ ` Y ) + 1 ) } )
181 180 raleqdv 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> A. i e. { ( ( |_ ` Y ) + 1 ) } 0 <_ ( R ` i ) ) )
182 ovex 
 |-  ( ( |_ ` Y ) + 1 ) e. _V
183 fveq2 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> ( R ` i ) = ( R ` ( ( |_ ` Y ) + 1 ) ) )
184 183 breq2d 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) ) )
185 182 184 ralsn 
 |-  ( A. i e. { ( ( |_ ` Y ) + 1 ) } 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) )
186 181 185 bitrdi 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) ) )
187 180 raleqdv 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> A. i e. { ( ( |_ ` Y ) + 1 ) } ( R ` i ) <_ 0 ) )
188 183 breq1d 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> ( ( R ` i ) <_ 0 <-> ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
189 182 188 ralsn 
 |-  ( A. i e. { ( ( |_ ` Y ) + 1 ) } ( R ` i ) <_ 0 <-> ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 )
190 187 189 bitrdi 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
191 186 190 orbi12d 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) <-> ( 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) \/ ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) ) )
192 173 191 mpbird 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) )
193 192 a1d 
 |-  ( ( ph /\ m = ( |_ ` Y ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
194 elfzuz 
 |-  ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
195 194 adantl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
196 eluzfz2 
 |-  ( m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) -> m e. ( ( ( |_ ` Y ) + 1 ) ... m ) )
197 195 196 syl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. ( ( ( |_ ` Y ) + 1 ) ... m ) )
198 fveq2 
 |-  ( i = m -> ( R ` i ) = ( R ` m ) )
199 198 breq2d 
 |-  ( i = m -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` m ) ) )
200 199 rspcv 
 |-  ( m e. ( ( ( |_ ` Y ) + 1 ) ... m ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> 0 <_ ( R ` m ) ) )
201 197 200 syl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> 0 <_ ( R ` m ) ) )
202 9 adantr 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
203 eluznn 
 |-  ( ( ( ( |_ ` Y ) + 1 ) e. NN /\ m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) ) -> m e. NN )
204 36 194 203 syl2an 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. NN )
205 204 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> m e. NN )
206 elfzle1 
 |-  ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> ( ( |_ ` Y ) + 1 ) <_ m )
207 206 adantl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( |_ ` Y ) + 1 ) <_ m )
208 elfzelz 
 |-  ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> m e. ZZ )
209 zltp1le 
 |-  ( ( ( |_ ` Y ) e. ZZ /\ m e. ZZ ) -> ( ( |_ ` Y ) < m <-> ( ( |_ ` Y ) + 1 ) <_ m ) )
210 176 208 209 syl2an 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( |_ ` Y ) < m <-> ( ( |_ ` Y ) + 1 ) <_ m ) )
211 207 210 mpbird 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( |_ ` Y ) < m )
212 fllt 
 |-  ( ( Y e. RR /\ m e. ZZ ) -> ( Y < m <-> ( |_ ` Y ) < m ) )
213 12 208 212 syl2an 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( Y < m <-> ( |_ ` Y ) < m ) )
214 211 213 mpbird 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> Y < m )
215 elfzle2 
 |-  ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> m <_ ( |_ ` ( K x. Y ) ) )
216 215 adantl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m <_ ( |_ ` ( K x. Y ) ) )
217 flge 
 |-  ( ( ( K x. Y ) e. RR /\ m e. ZZ ) -> ( m <_ ( K x. Y ) <-> m <_ ( |_ ` ( K x. Y ) ) ) )
218 109 208 217 syl2an 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( m <_ ( K x. Y ) <-> m <_ ( |_ ` ( K x. Y ) ) ) )
219 216 218 mpbird 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m <_ ( K x. Y ) )
220 214 219 jca 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( Y < m /\ m <_ ( K x. Y ) ) )
221 220 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> ( Y < m /\ m <_ ( K x. Y ) ) )
222 2 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> E e. ( 0 (,) 1 ) )
223 4 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> Y e. ( X (,) +oo ) )
224 simpr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
225 1 222 3 223 205 221 224 pntpbnd1a 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> ( abs ` ( ( R ` m ) / m ) ) <_ E )
226 breq2 
 |-  ( y = m -> ( Y < y <-> Y < m ) )
227 breq1 
 |-  ( y = m -> ( y <_ ( K x. Y ) <-> m <_ ( K x. Y ) ) )
228 226 227 anbi12d 
 |-  ( y = m -> ( ( Y < y /\ y <_ ( K x. Y ) ) <-> ( Y < m /\ m <_ ( K x. Y ) ) ) )
229 fveq2 
 |-  ( y = m -> ( R ` y ) = ( R ` m ) )
230 id 
 |-  ( y = m -> y = m )
231 229 230 oveq12d 
 |-  ( y = m -> ( ( R ` y ) / y ) = ( ( R ` m ) / m ) )
232 231 fveq2d 
 |-  ( y = m -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` m ) / m ) ) )
233 232 breq1d 
 |-  ( y = m -> ( ( abs ` ( ( R ` y ) / y ) ) <_ E <-> ( abs ` ( ( R ` m ) / m ) ) <_ E ) )
234 228 233 anbi12d 
 |-  ( y = m -> ( ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) <-> ( ( Y < m /\ m <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` m ) / m ) ) <_ E ) ) )
235 234 rspcev 
 |-  ( ( m e. NN /\ ( ( Y < m /\ m <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` m ) / m ) ) <_ E ) ) -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
236 205 221 225 235 syl12anc 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
237 202 236 mtand 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -. ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
238 237 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ 0 <_ ( R ` m ) ) -> -. ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
239 204 nnrpd 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. RR+ )
240 41 ffvelcdmi 
 |-  ( m e. RR+ -> ( R ` m ) e. RR )
241 239 240 syl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` m ) e. RR )
242 241 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` m ) e. RR )
243 242 recnd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` m ) e. CC )
244 243 subid1d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( ( R ` m ) - 0 ) = ( R ` m ) )
245 204 peano2nnd 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( m + 1 ) e. NN )
246 245 nnrpd 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( m + 1 ) e. RR+ )
247 41 ffvelcdmi 
 |-  ( ( m + 1 ) e. RR+ -> ( R ` ( m + 1 ) ) e. RR )
248 246 247 syl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` ( m + 1 ) ) e. RR )
249 248 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` ( m + 1 ) ) e. RR )
250 0red 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> 0 e. RR )
251 0re 
 |-  0 e. RR
252 letric 
 |-  ( ( 0 e. RR /\ ( R ` ( m + 1 ) ) e. RR ) -> ( 0 <_ ( R ` ( m + 1 ) ) \/ ( R ` ( m + 1 ) ) <_ 0 ) )
253 251 248 252 sylancr 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( 0 <_ ( R ` ( m + 1 ) ) \/ ( R ` ( m + 1 ) ) <_ 0 ) )
254 253 ord 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( -. 0 <_ ( R ` ( m + 1 ) ) -> ( R ` ( m + 1 ) ) <_ 0 ) )
255 254 imp 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) -> ( R ` ( m + 1 ) ) <_ 0 )
256 255 adantrl 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` ( m + 1 ) ) <_ 0 )
257 249 250 242 256 lesub2dd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( ( R ` m ) - 0 ) <_ ( ( R ` m ) - ( R ` ( m + 1 ) ) ) )
258 244 257 eqbrtrrd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` m ) <_ ( ( R ` m ) - ( R ` ( m + 1 ) ) ) )
259 simprl 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> 0 <_ ( R ` m ) )
260 242 259 absidd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( abs ` ( R ` m ) ) = ( R ` m ) )
261 249 250 242 256 259 letrd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` ( m + 1 ) ) <_ ( R ` m ) )
262 249 242 261 abssuble0d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) = ( ( R ` m ) - ( R ` ( m + 1 ) ) ) )
263 258 260 262 3brtr4d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
264 263 expr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ 0 <_ ( R ` m ) ) -> ( -. 0 <_ ( R ` ( m + 1 ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) )
265 238 264 mt3d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ 0 <_ ( R ` m ) ) -> 0 <_ ( R ` ( m + 1 ) ) )
266 265 ex 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( 0 <_ ( R ` m ) -> 0 <_ ( R ` ( m + 1 ) ) ) )
267 201 266 syld 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> 0 <_ ( R ` ( m + 1 ) ) ) )
268 ovex 
 |-  ( m + 1 ) e. _V
269 fveq2 
 |-  ( i = ( m + 1 ) -> ( R ` i ) = ( R ` ( m + 1 ) ) )
270 269 breq2d 
 |-  ( i = ( m + 1 ) -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( m + 1 ) ) ) )
271 268 270 ralsn 
 |-  ( A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( m + 1 ) ) )
272 267 271 imbitrrdi 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) )
273 272 ancld 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) /\ A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) ) )
274 fzsuc 
 |-  ( m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) )
275 195 274 syl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) )
276 275 raleqdv 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) 0 <_ ( R ` i ) ) )
277 ralunb 
 |-  ( A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) 0 <_ ( R ` i ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) /\ A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) )
278 276 277 bitrdi 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) /\ A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) ) )
279 273 278 sylibrd 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) ) )
280 198 breq1d 
 |-  ( i = m -> ( ( R ` i ) <_ 0 <-> ( R ` m ) <_ 0 ) )
281 280 rspcv 
 |-  ( m e. ( ( ( |_ ` Y ) + 1 ) ... m ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( R ` m ) <_ 0 ) )
282 197 281 syl 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( R ` m ) <_ 0 ) )
283 237 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( R ` m ) <_ 0 ) -> -. ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
284 254 con1d 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( -. ( R ` ( m + 1 ) ) <_ 0 -> 0 <_ ( R ` ( m + 1 ) ) ) )
285 284 imp 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ -. ( R ` ( m + 1 ) ) <_ 0 ) -> 0 <_ ( R ` ( m + 1 ) ) )
286 285 adantrl 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> 0 <_ ( R ` ( m + 1 ) ) )
287 241 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) e. RR )
288 287 renegcld 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> -u ( R ` m ) e. RR )
289 248 adantr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` ( m + 1 ) ) e. RR )
290 288 289 addge02d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( 0 <_ ( R ` ( m + 1 ) ) <-> -u ( R ` m ) <_ ( ( R ` ( m + 1 ) ) + -u ( R ` m ) ) ) )
291 286 290 mpbid 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> -u ( R ` m ) <_ ( ( R ` ( m + 1 ) ) + -u ( R ` m ) ) )
292 289 recnd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` ( m + 1 ) ) e. CC )
293 287 recnd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) e. CC )
294 292 293 negsubd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( ( R ` ( m + 1 ) ) + -u ( R ` m ) ) = ( ( R ` ( m + 1 ) ) - ( R ` m ) ) )
295 291 294 breqtrd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> -u ( R ` m ) <_ ( ( R ` ( m + 1 ) ) - ( R ` m ) ) )
296 simprl 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) <_ 0 )
297 287 296 absnidd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( abs ` ( R ` m ) ) = -u ( R ` m ) )
298 0red 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> 0 e. RR )
299 287 298 289 296 286 letrd 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) <_ ( R ` ( m + 1 ) ) )
300 287 289 299 abssubge0d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) = ( ( R ` ( m + 1 ) ) - ( R ` m ) ) )
301 295 297 300 3brtr4d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
302 301 expr 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( R ` m ) <_ 0 ) -> ( -. ( R ` ( m + 1 ) ) <_ 0 -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) )
303 283 302 mt3d 
 |-  ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( R ` m ) <_ 0 ) -> ( R ` ( m + 1 ) ) <_ 0 )
304 303 ex 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` m ) <_ 0 -> ( R ` ( m + 1 ) ) <_ 0 ) )
305 282 304 syld 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( R ` ( m + 1 ) ) <_ 0 ) )
306 269 breq1d 
 |-  ( i = ( m + 1 ) -> ( ( R ` i ) <_ 0 <-> ( R ` ( m + 1 ) ) <_ 0 ) )
307 268 306 ralsn 
 |-  ( A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 <-> ( R ` ( m + 1 ) ) <_ 0 )
308 305 307 imbitrrdi 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 ) )
309 308 ancld 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 /\ A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 ) ) )
310 275 raleqdv 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) ( R ` i ) <_ 0 ) )
311 ralunb 
 |-  ( A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) ( R ` i ) <_ 0 <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 /\ A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 ) )
312 310 311 bitrdi 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 /\ A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 ) ) )
313 309 312 sylibrd 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) )
314 279 313 orim12d 
 |-  ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
315 193 314 jaodan 
 |-  ( ( ph /\ ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
316 168 315 syldan 
 |-  ( ( ph /\ m e. ( ( |_ ` Y ) ..^ ( |_ ` ( K x. Y ) ) ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
317 316 expcom 
 |-  ( m e. ( ( |_ ` Y ) ..^ ( |_ ` ( K x. Y ) ) ) -> ( ph -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) ) )
318 317 a2d 
 |-  ( m e. ( ( |_ ` Y ) ..^ ( |_ ` ( K x. Y ) ) ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) ) -> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) ) )
319 136 141 146 151 163 318 fzind2 
 |-  ( ( |_ ` ( K x. Y ) ) e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) -> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) ) )
320 131 319 mpcom 
 |-  ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) )
321 63 97 320 mpjaodan 
 |-  ( ph -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
322 fveq2 
 |-  ( y = n -> ( R ` y ) = ( R ` n ) )
323 id 
 |-  ( y = n -> y = n )
324 oveq1 
 |-  ( y = n -> ( y + 1 ) = ( n + 1 ) )
325 323 324 oveq12d 
 |-  ( y = n -> ( y x. ( y + 1 ) ) = ( n x. ( n + 1 ) ) )
326 322 325 oveq12d 
 |-  ( y = n -> ( ( R ` y ) / ( y x. ( y + 1 ) ) ) = ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
327 326 cbvsumv 
 |-  sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) = sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) )
328 oveq1 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> ( i ... j ) = ( ( ( |_ ` Y ) + 1 ) ... j ) )
329 328 sumeq1d 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
330 327 329 eqtrid 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
331 330 fveq2d 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) = ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
332 331 breq1d 
 |-  ( i = ( ( |_ ` Y ) + 1 ) -> ( ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A <-> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A ) )
333 oveq2 
 |-  ( j = ( |_ ` ( K x. Y ) ) -> ( ( ( |_ ` Y ) + 1 ) ... j ) = ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) )
334 333 sumeq1d 
 |-  ( j = ( |_ ` ( K x. Y ) ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
335 334 fveq2d 
 |-  ( j = ( |_ ` ( K x. Y ) ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
336 335 breq1d 
 |-  ( j = ( |_ ` ( K x. Y ) ) -> ( ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A <-> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A ) )
337 332 336 rspc2va 
 |-  ( ( ( ( ( |_ ` Y ) + 1 ) e. NN /\ ( |_ ` ( K x. Y ) ) e. ZZ ) /\ A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )
338 36 127 6 337 syl21anc 
 |-  ( ph -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )
339 321 338 eqbrtrrd 
 |-  ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )