Metamath Proof Explorer

Theorem dchrisumlem3

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.g 
|- G = ( DChr ` N )
rpvmasum.d 
|- D = ( Base ` G )
rpvmasum.1 
|- .1. = ( 0g ` G )
dchrisum.b 
|- ( ph -> X e. D )
dchrisum.n1 
|- ( ph -> X =/= .1. )
dchrisum.2 
|- ( n = x -> A = B )
dchrisum.3 
|- ( ph -> M e. NN )
dchrisum.4 
|- ( ( ph /\ n e. RR+ ) -> A e. RR )
dchrisum.5 
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
dchrisum.6 
|- ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
dchrisum.7 
|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
dchrisum.9 
|- ( ph -> R e. RR )
dchrisum.10 
|- ( ph -> A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R )
Assertion dchrisumlem3 
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum.g 
 |-  G = ( DChr ` N )
5 rpvmasum.d 
 |-  D = ( Base ` G )
6 rpvmasum.1 
 |-  .1. = ( 0g ` G )
7 dchrisum.b 
 |-  ( ph -> X e. D )
8 dchrisum.n1 
 |-  ( ph -> X =/= .1. )
9 dchrisum.2 
 |-  ( n = x -> A = B )
10 dchrisum.3 
 |-  ( ph -> M e. NN )
11 dchrisum.4 
 |-  ( ( ph /\ n e. RR+ ) -> A e. RR )
12 dchrisum.5 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
13 dchrisum.6 
 |-  ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
14 dchrisum.7 
 |-  F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
15 dchrisum.9 
 |-  ( ph -> R e. RR )
16 dchrisum.10 
 |-  ( ph -> A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R )
17 nnuz 
 |-  NN = ( ZZ>= ` 1 )
18 1zzd 
 |-  ( ph -> 1 e. ZZ )
19 simpr 
 |-  ( ( ph /\ i e. NN ) -> i e. NN )
20 7 adantr 
 |-  ( ( ph /\ i e. NN ) -> X e. D )
21 19 nnzd 
 |-  ( ( ph /\ i e. NN ) -> i e. ZZ )
22 4 1 5 2 20 21 dchrzrhcl 
 |-  ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) e. CC )
23 11 ralrimiva 
 |-  ( ph -> A. n e. RR+ A e. RR )
24 nnrp 
 |-  ( i e. NN -> i e. RR+ )
25 nfcsb1v 
 |-  F/_ n [_ i / n ]_ A
26 25 nfel1 
 |-  F/ n [_ i / n ]_ A e. RR
27 csbeq1a 
 |-  ( n = i -> A = [_ i / n ]_ A )
28 27 eleq1d 
 |-  ( n = i -> ( A e. RR <-> [_ i / n ]_ A e. RR ) )
29 26 28 rspc 
 |-  ( i e. RR+ -> ( A. n e. RR+ A e. RR -> [_ i / n ]_ A e. RR ) )
30 29 impcom 
 |-  ( ( A. n e. RR+ A e. RR /\ i e. RR+ ) -> [_ i / n ]_ A e. RR )
31 23 24 30 syl2an 
 |-  ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
32 31 recnd 
 |-  ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
33 22 32 mulcld 
 |-  ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
34 nfcv 
 |-  F/_ n i
35 nfcv 
 |-  F/_ n ( X ` ( L ` i ) )
36 nfcv 
 |-  F/_ n x.
37 35 36 25 nfov 
 |-  F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
38 2fveq3 
 |-  ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
39 38 27 oveq12d 
 |-  ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
40 34 37 39 14 fvmptf 
 |-  ( ( i e. NN /\ ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
41 19 33 40 syl2anc 
 |-  ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
42 41 33 eqeltrd 
 |-  ( ( ph /\ i e. NN ) -> ( F ` i ) e. CC )
43 17 18 42 serf 
 |-  ( ph -> seq 1 ( + , F ) : NN --> CC )
44 43 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) e. CC )
45 11 recnd 
 |-  ( ( ph /\ n e. RR+ ) -> A e. CC )
46 45 ralrimiva 
 |-  ( ph -> A. n e. RR+ A e. CC )
47 46 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> A. n e. RR+ A e. CC )
48 id 
 |-  ( e e. RR+ -> e e. RR+ )
49 2re 
 |-  2 e. RR
50 remulcl 
 |-  ( ( 2 e. RR /\ R e. RR ) -> ( 2 x. R ) e. RR )
51 49 15 50 sylancr 
 |-  ( ph -> ( 2 x. R ) e. RR )
52 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
53 3 52 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ N ) )
54 oveq2 
 |-  ( u = 0 -> ( 0 ..^ u ) = ( 0 ..^ 0 ) )
55 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
56 54 55 eqtrdi 
 |-  ( u = 0 -> ( 0 ..^ u ) = (/) )
57 56 sumeq1d 
 |-  ( u = 0 -> sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) = sum_ n e. (/) ( X ` ( L ` n ) ) )
58 sum0 
 |-  sum_ n e. (/) ( X ` ( L ` n ) ) = 0
59 57 58 eqtrdi 
 |-  ( u = 0 -> sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) = 0 )
60 59 abs00bd 
 |-  ( u = 0 -> ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) = 0 )
61 60 breq1d 
 |-  ( u = 0 -> ( ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R <-> 0 <_ R ) )
62 61 rspcv 
 |-  ( 0 e. ( 0 ..^ N ) -> ( A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R -> 0 <_ R ) )
63 53 16 62 sylc 
 |-  ( ph -> 0 <_ R )
64 0le2 
 |-  0 <_ 2
65 mulge0 
 |-  ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( R e. RR /\ 0 <_ R ) ) -> 0 <_ ( 2 x. R ) )
66 49 64 65 mpanl12 
 |-  ( ( R e. RR /\ 0 <_ R ) -> 0 <_ ( 2 x. R ) )
67 15 63 66 syl2anc 
 |-  ( ph -> 0 <_ ( 2 x. R ) )
68 51 67 ge0p1rpd 
 |-  ( ph -> ( ( 2 x. R ) + 1 ) e. RR+ )
69 rpdivcl 
 |-  ( ( e e. RR+ /\ ( ( 2 x. R ) + 1 ) e. RR+ ) -> ( e / ( ( 2 x. R ) + 1 ) ) e. RR+ )
70 48 68 69 syl2anr 
 |-  ( ( ph /\ e e. RR+ ) -> ( e / ( ( 2 x. R ) + 1 ) ) e. RR+ )
71 13 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> ( n e. RR+ |-> A ) ~~>r 0 )
72 47 70 71 rlimi 
 |-  ( ( ph /\ e e. RR+ ) -> E. m e. RR A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) )
73 simpr 
 |-  ( ( ph /\ m e. RR ) -> m e. RR )
74 10 nnred 
 |-  ( ph -> M e. RR )
75 74 adantr 
 |-  ( ( ph /\ m e. RR ) -> M e. RR )
76 73 75 ifcld 
 |-  ( ( ph /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR )
77 0red 
 |-  ( ( ph /\ m e. RR ) -> 0 e. RR )
78 10 nngt0d 
 |-  ( ph -> 0 < M )
79 78 adantr 
 |-  ( ( ph /\ m e. RR ) -> 0 < M )
80 max1 
 |-  ( ( M e. RR /\ m e. RR ) -> M <_ if ( M <_ m , m , M ) )
81 74 80 sylan 
 |-  ( ( ph /\ m e. RR ) -> M <_ if ( M <_ m , m , M ) )
82 77 75 76 79 81 ltletrd 
 |-  ( ( ph /\ m e. RR ) -> 0 < if ( M <_ m , m , M ) )
83 76 82 elrpd 
 |-  ( ( ph /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR+ )
84 83 adantlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR+ )
85 nfv 
 |-  F/ n m <_ if ( M <_ m , m , M )
86 nfcv 
 |-  F/_ n abs
87 nfcsb1v 
 |-  F/_ n [_ if ( M <_ m , m , M ) / n ]_ A
88 nfcv 
 |-  F/_ n -
89 nfcv 
 |-  F/_ n 0
90 87 88 89 nfov 
 |-  F/_ n ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 )
91 86 90 nffv 
 |-  F/_ n ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) )
92 nfcv 
 |-  F/_ n <
93 nfcv 
 |-  F/_ n ( e / ( ( 2 x. R ) + 1 ) )
94 91 92 93 nfbr 
 |-  F/ n ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) )
95 85 94 nfim 
 |-  F/ n ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) )
96 breq2 
 |-  ( n = if ( M <_ m , m , M ) -> ( m <_ n <-> m <_ if ( M <_ m , m , M ) ) )
97 csbeq1a 
 |-  ( n = if ( M <_ m , m , M ) -> A = [_ if ( M <_ m , m , M ) / n ]_ A )
98 97 fvoveq1d 
 |-  ( n = if ( M <_ m , m , M ) -> ( abs ` ( A - 0 ) ) = ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) )
99 98 breq1d 
 |-  ( n = if ( M <_ m , m , M ) -> ( ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) <-> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) )
100 96 99 imbi12d 
 |-  ( n = if ( M <_ m , m , M ) -> ( ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) <-> ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) ) )
101 95 100 rspc 
 |-  ( if ( M <_ m , m , M ) e. RR+ -> ( A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) ) )
102 84 101 syl 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) ) )
103 74 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> M e. RR )
104 max2 
 |-  ( ( M e. RR /\ m e. RR ) -> m <_ if ( M <_ m , m , M ) )
105 103 104 sylancom 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> m <_ if ( M <_ m , m , M ) )
106 23 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> A. n e. RR+ A e. RR )
107 87 nfel1 
 |-  F/ n [_ if ( M <_ m , m , M ) / n ]_ A e. RR
108 97 eleq1d 
 |-  ( n = if ( M <_ m , m , M ) -> ( A e. RR <-> [_ if ( M <_ m , m , M ) / n ]_ A e. RR ) )
109 107 108 rspc 
 |-  ( if ( M <_ m , m , M ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ if ( M <_ m , m , M ) / n ]_ A e. RR ) )
110 84 106 109 sylc 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> [_ if ( M <_ m , m , M ) / n ]_ A e. RR )
111 110 recnd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> [_ if ( M <_ m , m , M ) / n ]_ A e. CC )
112 111 subid1d 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) = [_ if ( M <_ m , m , M ) / n ]_ A )
113 112 fveq2d 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) = ( abs ` [_ if ( M <_ m , m , M ) / n ]_ A ) )
114 76 adantlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR )
115 103 80 sylancom 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> M <_ if ( M <_ m , m , M ) )
116 elicopnf 
 |-  ( M e. RR -> ( if ( M <_ m , m , M ) e. ( M [,) +oo ) <-> ( if ( M <_ m , m , M ) e. RR /\ M <_ if ( M <_ m , m , M ) ) ) )
117 103 116 syl 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( if ( M <_ m , m , M ) e. ( M [,) +oo ) <-> ( if ( M <_ m , m , M ) e. RR /\ M <_ if ( M <_ m , m , M ) ) ) )
118 114 115 117 mpbir2and 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> if ( M <_ m , m , M ) e. ( M [,) +oo ) )
119 3 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> N e. NN )
120 7 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> X e. D )
121 8 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> X =/= .1. )
122 10 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> M e. NN )
123 11 ad4ant14 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ n e. RR+ ) -> A e. RR )
124 simpll 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ph )
125 124 12 syl3an1 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
126 13 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( n e. RR+ |-> A ) ~~>r 0 )
127 1 2 119 4 5 6 120 121 9 122 123 125 126 14 dchrisumlema 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( if ( M <_ m , m , M ) e. RR+ -> [_ if ( M <_ m , m , M ) / n ]_ A e. RR ) /\ ( if ( M <_ m , m , M ) e. ( M [,) +oo ) -> 0 <_ [_ if ( M <_ m , m , M ) / n ]_ A ) ) )
128 127 simprd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( if ( M <_ m , m , M ) e. ( M [,) +oo ) -> 0 <_ [_ if ( M <_ m , m , M ) / n ]_ A ) )
129 118 128 mpd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> 0 <_ [_ if ( M <_ m , m , M ) / n ]_ A )
130 110 129 absidd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( abs ` [_ if ( M <_ m , m , M ) / n ]_ A ) = [_ if ( M <_ m , m , M ) / n ]_ A )
131 113 130 eqtrd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) = [_ if ( M <_ m , m , M ) / n ]_ A )
132 131 breq1d 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) <-> [_ if ( M <_ m , m , M ) / n ]_ A < ( e / ( ( 2 x. R ) + 1 ) ) ) )
133 rpre 
 |-  ( e e. RR+ -> e e. RR )
134 133 ad2antlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> e e. RR )
135 68 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) + 1 ) e. RR+ )
136 110 134 135 ltmuldiv2d 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e <-> [_ if ( M <_ m , m , M ) / n ]_ A < ( e / ( ( 2 x. R ) + 1 ) ) ) )
137 132 136 bitr4d 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) <-> ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
138 51 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( 2 x. R ) e. RR )
139 135 rpred 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) + 1 ) e. RR )
140 138 lep1d 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( 2 x. R ) <_ ( ( 2 x. R ) + 1 ) )
141 138 139 110 129 140 lemul1ad 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) <_ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) )
142 138 110 remulcld 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR )
143 139 110 remulcld 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR )
144 lelttr 
 |-  ( ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR /\ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR /\ e e. RR ) -> ( ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) <_ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
145 142 143 134 144 syl3anc 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) <_ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
146 141 145 mpand 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
147 137 146 sylbid 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
148 1red 
 |-  ( ( ph /\ m e. RR ) -> 1 e. RR )
149 10 adantr 
 |-  ( ( ph /\ m e. RR ) -> M e. NN )
150 149 nnge1d 
 |-  ( ( ph /\ m e. RR ) -> 1 <_ M )
151 148 75 76 150 81 letrd 
 |-  ( ( ph /\ m e. RR ) -> 1 <_ if ( M <_ m , m , M ) )
152 flge1nn 
 |-  ( ( if ( M <_ m , m , M ) e. RR /\ 1 <_ if ( M <_ m , m , M ) ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
153 76 151 152 syl2anc 
 |-  ( ( ph /\ m e. RR ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
154 153 adantlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
155 3 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> N e. NN )
156 7 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> X e. D )
157 8 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> X =/= .1. )
158 10 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> M e. NN )
159 11 ad4ant14 
 |-  ( ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) /\ n e. RR+ ) -> A e. RR )
160 12 3adant1r 
 |-  ( ( ( ph /\ m e. RR ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
161 160 3adant1r 
 |-  ( ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
162 13 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( n e. RR+ |-> A ) ~~>r 0 )
163 15 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> R e. RR )
164 16 ad2antrr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R )
165 83 adantr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> if ( M <_ m , m , M ) e. RR+ )
166 81 adantr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> M <_ if ( M <_ m , m , M ) )
167 76 adantr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> if ( M <_ m , m , M ) e. RR )
168 fllep1 
 |-  ( if ( M <_ m , m , M ) e. RR -> if ( M <_ m , m , M ) <_ ( ( |_ ` if ( M <_ m , m , M ) ) + 1 ) )
169 167 168 syl 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> if ( M <_ m , m , M ) <_ ( ( |_ ` if ( M <_ m , m , M ) ) + 1 ) )
170 153 adantr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
171 simpr 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) )
172 1 2 155 4 5 6 156 157 9 158 159 161 162 14 163 164 165 166 169 170 171 dchrisumlem2 
 |-  ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) )
173 172 adantllr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) )
174 43 ad3antrrr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> seq 1 ( + , F ) : NN --> CC )
175 eluznn 
 |-  ( ( ( |_ ` if ( M <_ m , m , M ) ) e. NN /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> k e. NN )
176 154 175 sylan 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> k e. NN )
177 174 176 ffvelrnd 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( seq 1 ( + , F ) ` k ) e. CC )
178 154 adantr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
179 174 178 ffvelrnd 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) e. CC )
180 177 179 subcld 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) e. CC )
181 180 abscld 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) e. RR )
182 142 adantr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR )
183 134 adantr 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> e e. RR )
184 lelttr 
 |-  ( ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) e. RR /\ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR /\ e e. RR ) -> ( ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
185 181 182 183 184 syl3anc 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
186 173 185 mpand 
 |-  ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
187 186 ralrimdva 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> A. k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
188 fveq2 
 |-  ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) )
189 fveq2 
 |-  ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( seq 1 ( + , F ) ` j ) = ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) )
190 189 oveq2d 
 |-  ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) = ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) )
191 190 fveq2d 
 |-  ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) )
192 191 breq1d 
 |-  ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e <-> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
193 188 192 raleqbidv 
 |-  ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e <-> A. k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
194 193 rspcev 
 |-  ( ( ( |_ ` if ( M <_ m , m , M ) ) e. NN /\ A. k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e )
195 154 187 194 syl6an 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
196 147 195 syld 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
197 105 196 embantd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
198 102 197 syld 
 |-  ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
199 198 rexlimdva 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. m e. RR A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
200 72 199 mpd 
 |-  ( ( ph /\ e e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e )
201 200 ralrimiva 
 |-  ( ph -> A. e e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e )
202 seqex 
 |-  seq 1 ( + , F ) e. _V
203 202 a1i 
 |-  ( ph -> seq 1 ( + , F ) e. _V )
204 17 44 201 203 caucvg 
 |-  ( ph -> seq 1 ( + , F ) e. dom ~~> )
205 202 eldm 
 |-  ( seq 1 ( + , F ) e. dom ~~> <-> E. t seq 1 ( + , F ) ~~> t )
206 204 205 sylib 
 |-  ( ph -> E. t seq 1 ( + , F ) ~~> t )
207 simpr 
 |-  ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> seq 1 ( + , F ) ~~> t )
208 elrege0 
 |-  ( ( 2 x. R ) e. ( 0 [,) +oo ) <-> ( ( 2 x. R ) e. RR /\ 0 <_ ( 2 x. R ) ) )
209 51 67 208 sylanbrc 
 |-  ( ph -> ( 2 x. R ) e. ( 0 [,) +oo ) )
210 209 adantr 
 |-  ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> ( 2 x. R ) e. ( 0 [,) +oo ) )
211 eqid 
 |-  ( ZZ>= ` ( |_ ` m ) ) = ( ZZ>= ` ( |_ ` m ) )
212 pnfxr 
 |-  +oo e. RR*
213 icossre 
 |-  ( ( M e. RR /\ +oo e. RR* ) -> ( M [,) +oo ) C_ RR )
214 74 212 213 sylancl 
 |-  ( ph -> ( M [,) +oo ) C_ RR )
215 214 sselda 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> m e. RR )
216 215 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> m e. RR )
217 216 flcld 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( |_ ` m ) e. ZZ )
218 simplr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> seq 1 ( + , F ) ~~> t )
219 43 ad2antrr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> seq 1 ( + , F ) : NN --> CC )
220 1red 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> 1 e. RR )
221 74 ad2antrr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> M e. RR )
222 10 ad2antrr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> M e. NN )
223 222 nnge1d 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> 1 <_ M )
224 elicopnf 
 |-  ( M e. RR -> ( m e. ( M [,) +oo ) <-> ( m e. RR /\ M <_ m ) ) )
225 74 224 syl 
 |-  ( ph -> ( m e. ( M [,) +oo ) <-> ( m e. RR /\ M <_ m ) ) )
226 225 simplbda 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> M <_ m )
227 226 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> M <_ m )
228 220 221 216 223 227 letrd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> 1 <_ m )
229 flge1nn 
 |-  ( ( m e. RR /\ 1 <_ m ) -> ( |_ ` m ) e. NN )
230 216 228 229 syl2anc 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( |_ ` m ) e. NN )
231 219 230 ffvelrnd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( seq 1 ( + , F ) ` ( |_ ` m ) ) e. CC )
232 nnex 
 |-  NN e. _V
233 232 mptex 
 |-  ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) e. _V
234 233 a1i 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) e. _V )
235 219 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> seq 1 ( + , F ) : NN --> CC )
236 eluznn 
 |-  ( ( ( |_ ` m ) e. NN /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> i e. NN )
237 230 236 sylan 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> i e. NN )
238 235 237 ffvelrnd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( seq 1 ( + , F ) ` i ) e. CC )
239 fveq2 
 |-  ( k = i -> ( seq 1 ( + , F ) ` k ) = ( seq 1 ( + , F ) ` i ) )
240 239 oveq2d 
 |-  ( k = i -> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
241 eqid 
 |-  ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) = ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) )
242 ovex 
 |-  ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) e. _V
243 240 241 242 fvmpt3i 
 |-  ( i e. NN -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
244 237 243 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
245 211 217 218 231 234 238 244 climsubc2 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ~~> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) )
246 232 mptex 
 |-  ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) e. _V
247 246 a1i 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) e. _V )
248 fvex 
 |-  ( seq 1 ( + , F ) ` ( |_ ` m ) ) e. _V
249 248 fvconst2 
 |-  ( i e. NN -> ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) = ( seq 1 ( + , F ) ` ( |_ ` m ) ) )
250 237 249 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) = ( seq 1 ( + , F ) ` ( |_ ` m ) ) )
251 250 oveq1d 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) - ( seq 1 ( + , F ) ` i ) ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
252 244 251 eqtr4d 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) = ( ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) - ( seq 1 ( + , F ) ` i ) ) )
253 231 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` m ) ) e. CC )
254 250 253 eqeltrd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) e. CC )
255 254 238 subcld 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) - ( seq 1 ( + , F ) ` i ) ) e. CC )
256 252 255 eqeltrd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) e. CC )
257 240 fveq2d 
 |-  ( k = i -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
258 eqid 
 |-  ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) = ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) )
259 fvex 
 |-  ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) e. _V
260 257 258 259 fvmpt3i 
 |-  ( i e. NN -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
261 237 260 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
262 244 fveq2d 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
263 261 262 eqtr4d 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) ) )
264 211 245 247 217 256 263 climabs 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ~~> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) )
265 51 ad2antrr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( 2 x. R ) e. RR )
266 0red 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> 0 e. RR )
267 74 adantr 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> M e. RR )
268 78 adantr 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> 0 < M )
269 266 267 215 268 226 ltletrd 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> 0 < m )
270 215 269 elrpd 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> m e. RR+ )
271 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
272 271 nfel1 
 |-  F/ n [_ m / n ]_ A e. RR
273 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
274 273 eleq1d 
 |-  ( n = m -> ( A e. RR <-> [_ m / n ]_ A e. RR ) )
275 272 274 rspc 
 |-  ( m e. RR+ -> ( A. n e. RR+ A e. RR -> [_ m / n ]_ A e. RR ) )
276 23 275 mpan9 
 |-  ( ( ph /\ m e. RR+ ) -> [_ m / n ]_ A e. RR )
277 270 276 syldan 
 |-  ( ( ph /\ m e. ( M [,) +oo ) ) -> [_ m / n ]_ A e. RR )
278 277 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> [_ m / n ]_ A e. RR )
279 265 278 remulcld 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( ( 2 x. R ) x. [_ m / n ]_ A ) e. RR )
280 279 recnd 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( ( 2 x. R ) x. [_ m / n ]_ A ) e. CC )
281 1z 
 |-  1 e. ZZ
282 17 eqimss2i 
 |-  ( ZZ>= ` 1 ) C_ NN
283 282 232 climconst2 
 |-  ( ( ( ( 2 x. R ) x. [_ m / n ]_ A ) e. CC /\ 1 e. ZZ ) -> ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ~~> ( ( 2 x. R ) x. [_ m / n ]_ A ) )
284 280 281 283 sylancl 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ~~> ( ( 2 x. R ) x. [_ m / n ]_ A ) )
285 253 238 subcld 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) e. CC )
286 285 abscld 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) e. RR )
287 261 286 eqeltrd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) e. RR )
288 ovex 
 |-  ( ( 2 x. R ) x. [_ m / n ]_ A ) e. _V
289 288 fvconst2 
 |-  ( i e. NN -> ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) = ( ( 2 x. R ) x. [_ m / n ]_ A ) )
290 237 289 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) = ( ( 2 x. R ) x. [_ m / n ]_ A ) )
291 279 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( 2 x. R ) x. [_ m / n ]_ A ) e. RR )
292 290 291 eqeltrd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) e. RR )
293 simplll 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ph )
294 293 3 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> N e. NN )
295 293 7 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> X e. D )
296 293 8 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> X =/= .1. )
297 222 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> M e. NN )
298 293 11 sylan 
 |-  ( ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) /\ n e. RR+ ) -> A e. RR )
299 293 12 syl3an1 
 |-  ( ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
300 293 13 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( n e. RR+ |-> A ) ~~>r 0 )
301 293 15 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> R e. RR )
302 293 16 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R )
303 270 adantlr 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> m e. RR+ )
304 303 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m e. RR+ )
305 227 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> M <_ m )
306 216 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m e. RR )
307 reflcl 
 |-  ( m e. RR -> ( |_ ` m ) e. RR )
308 peano2re 
 |-  ( ( |_ ` m ) e. RR -> ( ( |_ ` m ) + 1 ) e. RR )
309 306 307 308 3syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( |_ ` m ) + 1 ) e. RR )
310 flltp1 
 |-  ( m e. RR -> m < ( ( |_ ` m ) + 1 ) )
311 306 310 syl 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m < ( ( |_ ` m ) + 1 ) )
312 306 309 311 ltled 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m <_ ( ( |_ ` m ) + 1 ) )
313 230 adantr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( |_ ` m ) e. NN )
314 simpr 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> i e. ( ZZ>= ` ( |_ ` m ) ) )
315 1 2 294 4 5 6 295 296 9 297 298 299 300 14 301 302 304 305 312 313 314 dchrisumlem2 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` i ) - ( seq 1 ( + , F ) ` ( |_ ` m ) ) ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) )
316 253 238 abssubd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` i ) - ( seq 1 ( + , F ) ` ( |_ ` m ) ) ) ) )
317 261 316 eqtrd 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( seq 1 ( + , F ) ` i ) - ( seq 1 ( + , F ) ` ( |_ ` m ) ) ) ) )
318 315 317 290 3brtr4d 
 |-  ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) <_ ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) )
319 211 217 264 284 287 292 318 climle 
 |-  ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) )
320 319 ralrimiva 
 |-  ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) )
321 oveq1 
 |-  ( c = ( 2 x. R ) -> ( c x. B ) = ( ( 2 x. R ) x. B ) )
322 321 breq2d 
 |-  ( c = ( 2 x. R ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) ) )
323 322 ralbidv 
 |-  ( c = ( 2 x. R ) -> ( A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) <-> A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) ) )
324 2fveq3 
 |-  ( m = x -> ( seq 1 ( + , F ) ` ( |_ ` m ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) )
325 324 fvoveq1d 
 |-  ( m = x -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) )
326 vex 
 |-  m e. _V
327 326 a1i 
 |-  ( m = x -> m e. _V )
328 equequ2 
 |-  ( m = x -> ( n = m <-> n = x ) )
329 328 biimpa 
 |-  ( ( m = x /\ n = m ) -> n = x )
330 329 9 syl 
 |-  ( ( m = x /\ n = m ) -> A = B )
331 327 330 csbied 
 |-  ( m = x -> [_ m / n ]_ A = B )
332 331 oveq2d 
 |-  ( m = x -> ( ( 2 x. R ) x. [_ m / n ]_ A ) = ( ( 2 x. R ) x. B ) )
333 325 332 breq12d 
 |-  ( m = x -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) ) )
334 333 cbvralvw 
 |-  ( A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) <-> A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) )
335 323 334 bitr4di 
 |-  ( c = ( 2 x. R ) -> ( A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) <-> A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) ) )
336 335 rspcev 
 |-  ( ( ( 2 x. R ) e. ( 0 [,) +oo ) /\ A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) ) -> E. c e. ( 0 [,) +oo ) A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) )
337 210 320 336 syl2anc 
 |-  ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> E. c e. ( 0 [,) +oo ) A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) )
338 r19.42v 
 |-  ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) <-> ( seq 1 ( + , F ) ~~> t /\ E. c e. ( 0 [,) +oo ) A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
339 207 337 338 sylanbrc 
 |-  ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
340 339 ex 
 |-  ( ph -> ( seq 1 ( + , F ) ~~> t -> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) ) )
341 340 eximdv 
 |-  ( ph -> ( E. t seq 1 ( + , F ) ~~> t -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) ) )
342 206 341 mpd 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )