Step |
Hyp |
Ref |
Expression |
1 |
|
o1fsum.1 |
|- ( ( ph /\ k e. NN ) -> A e. V ) |
2 |
|
o1fsum.2 |
|- ( ph -> ( k e. NN |-> A ) e. O(1) ) |
3 |
|
nnssre |
|- NN C_ RR |
4 |
3
|
a1i |
|- ( ph -> NN C_ RR ) |
5 |
1 2
|
o1mptrcl |
|- ( ( ph /\ k e. NN ) -> A e. CC ) |
6 |
|
1red |
|- ( ph -> 1 e. RR ) |
7 |
4 5 6
|
elo1mpt2 |
|- ( ph -> ( ( k e. NN |-> A ) e. O(1) <-> E. c e. ( 1 [,) +oo ) E. m e. RR A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) ) |
8 |
2 7
|
mpbid |
|- ( ph -> E. c e. ( 1 [,) +oo ) E. m e. RR A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) |
9 |
|
rpssre |
|- RR+ C_ RR |
10 |
9
|
a1i |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> RR+ C_ RR ) |
11 |
|
nfcv |
|- F/_ n A |
12 |
|
nfcsb1v |
|- F/_ k [_ n / k ]_ A |
13 |
|
csbeq1a |
|- ( k = n -> A = [_ n / k ]_ A ) |
14 |
11 12 13
|
cbvsumi |
|- sum_ k e. ( 1 ... ( |_ ` x ) ) A = sum_ n e. ( 1 ... ( |_ ` x ) ) [_ n / k ]_ A |
15 |
|
fzfid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
16 |
|
o1f |
|- ( ( k e. NN |-> A ) e. O(1) -> ( k e. NN |-> A ) : dom ( k e. NN |-> A ) --> CC ) |
17 |
2 16
|
syl |
|- ( ph -> ( k e. NN |-> A ) : dom ( k e. NN |-> A ) --> CC ) |
18 |
1
|
ralrimiva |
|- ( ph -> A. k e. NN A e. V ) |
19 |
|
dmmptg |
|- ( A. k e. NN A e. V -> dom ( k e. NN |-> A ) = NN ) |
20 |
18 19
|
syl |
|- ( ph -> dom ( k e. NN |-> A ) = NN ) |
21 |
20
|
feq2d |
|- ( ph -> ( ( k e. NN |-> A ) : dom ( k e. NN |-> A ) --> CC <-> ( k e. NN |-> A ) : NN --> CC ) ) |
22 |
17 21
|
mpbid |
|- ( ph -> ( k e. NN |-> A ) : NN --> CC ) |
23 |
|
eqid |
|- ( k e. NN |-> A ) = ( k e. NN |-> A ) |
24 |
23
|
fmpt |
|- ( A. k e. NN A e. CC <-> ( k e. NN |-> A ) : NN --> CC ) |
25 |
22 24
|
sylibr |
|- ( ph -> A. k e. NN A e. CC ) |
26 |
25
|
ad3antrrr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> A. k e. NN A e. CC ) |
27 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN ) |
28 |
12
|
nfel1 |
|- F/ k [_ n / k ]_ A e. CC |
29 |
13
|
eleq1d |
|- ( k = n -> ( A e. CC <-> [_ n / k ]_ A e. CC ) ) |
30 |
28 29
|
rspc |
|- ( n e. NN -> ( A. k e. NN A e. CC -> [_ n / k ]_ A e. CC ) ) |
31 |
30
|
impcom |
|- ( ( A. k e. NN A e. CC /\ n e. NN ) -> [_ n / k ]_ A e. CC ) |
32 |
26 27 31
|
syl2an |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> [_ n / k ]_ A e. CC ) |
33 |
15 32
|
fsumcl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) [_ n / k ]_ A e. CC ) |
34 |
14 33
|
eqeltrid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) A e. CC ) |
35 |
|
rpcn |
|- ( x e. RR+ -> x e. CC ) |
36 |
35
|
adantl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> x e. CC ) |
37 |
|
rpne0 |
|- ( x e. RR+ -> x =/= 0 ) |
38 |
37
|
adantl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> x =/= 0 ) |
39 |
34 36 38
|
divcld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) e. CC ) |
40 |
|
simplrl |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> c e. ( 1 [,) +oo ) ) |
41 |
|
1re |
|- 1 e. RR |
42 |
|
elicopnf |
|- ( 1 e. RR -> ( c e. ( 1 [,) +oo ) <-> ( c e. RR /\ 1 <_ c ) ) ) |
43 |
41 42
|
ax-mp |
|- ( c e. ( 1 [,) +oo ) <-> ( c e. RR /\ 1 <_ c ) ) |
44 |
40 43
|
sylib |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> ( c e. RR /\ 1 <_ c ) ) |
45 |
44
|
simpld |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> c e. RR ) |
46 |
|
fzfid |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> ( 1 ... ( |_ ` c ) ) e. Fin ) |
47 |
25
|
ad2antrr |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> A. k e. NN A e. CC ) |
48 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` c ) ) -> n e. NN ) |
49 |
47 48 31
|
syl2an |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ n e. ( 1 ... ( |_ ` c ) ) ) -> [_ n / k ]_ A e. CC ) |
50 |
49
|
abscld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ n e. ( 1 ... ( |_ ` c ) ) ) -> ( abs ` [_ n / k ]_ A ) e. RR ) |
51 |
46 50
|
fsumrecl |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) e. RR ) |
52 |
|
simplrr |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> m e. RR ) |
53 |
51 52
|
readdcld |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) e. RR ) |
54 |
34 36 38
|
absdivd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ x e. RR+ ) -> ( abs ` ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) = ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / ( abs ` x ) ) ) |
55 |
54
|
adantrr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) = ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / ( abs ` x ) ) ) |
56 |
|
rprege0 |
|- ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) ) |
57 |
56
|
ad2antrl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( x e. RR /\ 0 <_ x ) ) |
58 |
|
absid |
|- ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x ) |
59 |
57 58
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` x ) = x ) |
60 |
59
|
oveq2d |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / ( abs ` x ) ) = ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / x ) ) |
61 |
55 60
|
eqtrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) = ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / x ) ) |
62 |
34
|
adantrr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) A e. CC ) |
63 |
62
|
abscld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) e. RR ) |
64 |
|
fzfid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
65 |
47 27 31
|
syl2an |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> [_ n / k ]_ A e. CC ) |
66 |
65
|
adantlr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> [_ n / k ]_ A e. CC ) |
67 |
66
|
abscld |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` [_ n / k ]_ A ) e. RR ) |
68 |
64 67
|
fsumrecl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) e. RR ) |
69 |
57
|
simpld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> x e. RR ) |
70 |
51
|
adantr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) e. RR ) |
71 |
52
|
adantr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> m e. RR ) |
72 |
70 71
|
readdcld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) e. RR ) |
73 |
69 72
|
remulcld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( x x. ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) e. RR ) |
74 |
14
|
fveq2i |
|- ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) = ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) [_ n / k ]_ A ) |
75 |
64 66
|
fsumabs |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) [_ n / k ]_ A ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) ) |
76 |
74 75
|
eqbrtrid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) ) |
77 |
|
fzfid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) e. Fin ) |
78 |
|
ssun2 |
|- ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) C_ ( ( 1 ... ( |_ ` c ) ) u. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) |
79 |
|
flge1nn |
|- ( ( c e. RR /\ 1 <_ c ) -> ( |_ ` c ) e. NN ) |
80 |
44 79
|
syl |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> ( |_ ` c ) e. NN ) |
81 |
80
|
adantr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` c ) e. NN ) |
82 |
81
|
nnred |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` c ) e. RR ) |
83 |
45
|
adantr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> c e. RR ) |
84 |
|
flle |
|- ( c e. RR -> ( |_ ` c ) <_ c ) |
85 |
83 84
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` c ) <_ c ) |
86 |
|
simprr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> c <_ x ) |
87 |
82 83 69 85 86
|
letrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` c ) <_ x ) |
88 |
|
fznnfl |
|- ( x e. RR -> ( ( |_ ` c ) e. ( 1 ... ( |_ ` x ) ) <-> ( ( |_ ` c ) e. NN /\ ( |_ ` c ) <_ x ) ) ) |
89 |
69 88
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( |_ ` c ) e. ( 1 ... ( |_ ` x ) ) <-> ( ( |_ ` c ) e. NN /\ ( |_ ` c ) <_ x ) ) ) |
90 |
81 87 89
|
mpbir2and |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` c ) e. ( 1 ... ( |_ ` x ) ) ) |
91 |
|
fzsplit |
|- ( ( |_ ` c ) e. ( 1 ... ( |_ ` x ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` c ) ) u. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) ) |
92 |
90 91
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` c ) ) u. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) ) |
93 |
78 92
|
sseqtrrid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` x ) ) ) |
94 |
93
|
sselda |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) -> n e. ( 1 ... ( |_ ` x ) ) ) |
95 |
65
|
abscld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` [_ n / k ]_ A ) e. RR ) |
96 |
95
|
adantlr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` [_ n / k ]_ A ) e. RR ) |
97 |
94 96
|
syldan |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` [_ n / k ]_ A ) e. RR ) |
98 |
77 97
|
fsumrecl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) e. RR ) |
99 |
69 70
|
remulcld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( x x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) e. RR ) |
100 |
69 71
|
remulcld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( x x. m ) e. RR ) |
101 |
70
|
recnd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) e. CC ) |
102 |
101
|
mulid2d |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( 1 x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) = sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) |
103 |
|
1red |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> 1 e. RR ) |
104 |
49
|
absge0d |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ n e. ( 1 ... ( |_ ` c ) ) ) -> 0 <_ ( abs ` [_ n / k ]_ A ) ) |
105 |
46 50 104
|
fsumge0 |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) |
106 |
51 105
|
jca |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) e. RR /\ 0 <_ sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) ) |
107 |
106
|
adantr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) e. RR /\ 0 <_ sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) ) |
108 |
44
|
simprd |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> 1 <_ c ) |
109 |
108
|
adantr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> 1 <_ c ) |
110 |
103 83 69 109 86
|
letrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> 1 <_ x ) |
111 |
|
lemul1a |
|- ( ( ( 1 e. RR /\ x e. RR /\ ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) e. RR /\ 0 <_ sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) ) /\ 1 <_ x ) -> ( 1 x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) <_ ( x x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) ) |
112 |
103 69 107 110 111
|
syl31anc |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( 1 x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) <_ ( x x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) ) |
113 |
102 112
|
eqbrtrrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) <_ ( x x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) ) |
114 |
|
hashcl |
|- ( ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) e. Fin -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) e. NN0 ) |
115 |
|
nn0re |
|- ( ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) e. NN0 -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) e. RR ) |
116 |
77 114 115
|
3syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) e. RR ) |
117 |
116 71
|
remulcld |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) x. m ) e. RR ) |
118 |
71
|
adantr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) -> m e. RR ) |
119 |
|
elfzuz |
|- ( n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) -> n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) |
120 |
81
|
peano2nnd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( |_ ` c ) + 1 ) e. NN ) |
121 |
|
eluznn |
|- ( ( ( ( |_ ` c ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> n e. NN ) |
122 |
120 121
|
sylan |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> n e. NN ) |
123 |
|
simpllr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) |
124 |
83
|
adantr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> c e. RR ) |
125 |
|
reflcl |
|- ( c e. RR -> ( |_ ` c ) e. RR ) |
126 |
|
peano2re |
|- ( ( |_ ` c ) e. RR -> ( ( |_ ` c ) + 1 ) e. RR ) |
127 |
124 125 126
|
3syl |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> ( ( |_ ` c ) + 1 ) e. RR ) |
128 |
122
|
nnred |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> n e. RR ) |
129 |
|
fllep1 |
|- ( c e. RR -> c <_ ( ( |_ ` c ) + 1 ) ) |
130 |
124 129
|
syl |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> c <_ ( ( |_ ` c ) + 1 ) ) |
131 |
|
eluzle |
|- ( n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) -> ( ( |_ ` c ) + 1 ) <_ n ) |
132 |
131
|
adantl |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> ( ( |_ ` c ) + 1 ) <_ n ) |
133 |
124 127 128 130 132
|
letrd |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> c <_ n ) |
134 |
|
nfv |
|- F/ k c <_ n |
135 |
|
nfcv |
|- F/_ k abs |
136 |
135 12
|
nffv |
|- F/_ k ( abs ` [_ n / k ]_ A ) |
137 |
|
nfcv |
|- F/_ k <_ |
138 |
|
nfcv |
|- F/_ k m |
139 |
136 137 138
|
nfbr |
|- F/ k ( abs ` [_ n / k ]_ A ) <_ m |
140 |
134 139
|
nfim |
|- F/ k ( c <_ n -> ( abs ` [_ n / k ]_ A ) <_ m ) |
141 |
|
breq2 |
|- ( k = n -> ( c <_ k <-> c <_ n ) ) |
142 |
13
|
fveq2d |
|- ( k = n -> ( abs ` A ) = ( abs ` [_ n / k ]_ A ) ) |
143 |
142
|
breq1d |
|- ( k = n -> ( ( abs ` A ) <_ m <-> ( abs ` [_ n / k ]_ A ) <_ m ) ) |
144 |
141 143
|
imbi12d |
|- ( k = n -> ( ( c <_ k -> ( abs ` A ) <_ m ) <-> ( c <_ n -> ( abs ` [_ n / k ]_ A ) <_ m ) ) ) |
145 |
140 144
|
rspc |
|- ( n e. NN -> ( A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) -> ( c <_ n -> ( abs ` [_ n / k ]_ A ) <_ m ) ) ) |
146 |
122 123 133 145
|
syl3c |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> ( abs ` [_ n / k ]_ A ) <_ m ) |
147 |
119 146
|
sylan2 |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) -> ( abs ` [_ n / k ]_ A ) <_ m ) |
148 |
77 97 118 147
|
fsumle |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) <_ sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) m ) |
149 |
71
|
recnd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> m e. CC ) |
150 |
|
fsumconst |
|- ( ( ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) e. Fin /\ m e. CC ) -> sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) m = ( ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) x. m ) ) |
151 |
77 149 150
|
syl2anc |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) m = ( ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) x. m ) ) |
152 |
148 151
|
breqtrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) <_ ( ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) x. m ) ) |
153 |
|
biidd |
|- ( n = ( ( |_ ` c ) + 1 ) -> ( 0 <_ m <-> 0 <_ m ) ) |
154 |
|
0red |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> 0 e. RR ) |
155 |
47 30
|
mpan9 |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ n e. NN ) -> [_ n / k ]_ A e. CC ) |
156 |
155
|
adantlr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. NN ) -> [_ n / k ]_ A e. CC ) |
157 |
122 156
|
syldan |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> [_ n / k ]_ A e. CC ) |
158 |
157
|
abscld |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> ( abs ` [_ n / k ]_ A ) e. RR ) |
159 |
71
|
adantr |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> m e. RR ) |
160 |
157
|
absge0d |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> 0 <_ ( abs ` [_ n / k ]_ A ) ) |
161 |
154 158 159 160 146
|
letrd |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) -> 0 <_ m ) |
162 |
161
|
ralrimiva |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> A. n e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) 0 <_ m ) |
163 |
120
|
nnzd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( |_ ` c ) + 1 ) e. ZZ ) |
164 |
|
uzid |
|- ( ( ( |_ ` c ) + 1 ) e. ZZ -> ( ( |_ ` c ) + 1 ) e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) |
165 |
163 164
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( |_ ` c ) + 1 ) e. ( ZZ>= ` ( ( |_ ` c ) + 1 ) ) ) |
166 |
153 162 165
|
rspcdva |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> 0 <_ m ) |
167 |
|
reflcl |
|- ( x e. RR -> ( |_ ` x ) e. RR ) |
168 |
69 167
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` x ) e. RR ) |
169 |
|
ssdomg |
|- ( ( 1 ... ( |_ ` x ) ) e. Fin -> ( ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` x ) ) -> ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ~<_ ( 1 ... ( |_ ` x ) ) ) ) |
170 |
64 93 169
|
sylc |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ~<_ ( 1 ... ( |_ ` x ) ) ) |
171 |
|
hashdomi |
|- ( ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ~<_ ( 1 ... ( |_ ` x ) ) -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) <_ ( # ` ( 1 ... ( |_ ` x ) ) ) ) |
172 |
170 171
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) <_ ( # ` ( 1 ... ( |_ ` x ) ) ) ) |
173 |
|
flge0nn0 |
|- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 ) |
174 |
|
hashfz1 |
|- ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) ) |
175 |
57 173 174
|
3syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) ) |
176 |
172 175
|
breqtrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) <_ ( |_ ` x ) ) |
177 |
|
flle |
|- ( x e. RR -> ( |_ ` x ) <_ x ) |
178 |
69 177
|
syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( |_ ` x ) <_ x ) |
179 |
116 168 69 176 178
|
letrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) <_ x ) |
180 |
116 69 71 166 179
|
lemul1ad |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( # ` ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) x. m ) <_ ( x x. m ) ) |
181 |
98 117 100 152 180
|
letrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) <_ ( x x. m ) ) |
182 |
70 98 99 100 113 181
|
le2addd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) ) <_ ( ( x x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) + ( x x. m ) ) ) |
183 |
|
ltp1 |
|- ( ( |_ ` c ) e. RR -> ( |_ ` c ) < ( ( |_ ` c ) + 1 ) ) |
184 |
|
fzdisj |
|- ( ( |_ ` c ) < ( ( |_ ` c ) + 1 ) -> ( ( 1 ... ( |_ ` c ) ) i^i ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) = (/) ) |
185 |
82 183 184
|
3syl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( 1 ... ( |_ ` c ) ) i^i ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ) = (/) ) |
186 |
96
|
recnd |
|- ( ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` [_ n / k ]_ A ) e. CC ) |
187 |
185 92 64 186
|
fsumsplit |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) = ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + sum_ n e. ( ( ( |_ ` c ) + 1 ) ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) ) ) |
188 |
36
|
adantrr |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> x e. CC ) |
189 |
188 101 149
|
adddid |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( x x. ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) = ( ( x x. sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) ) + ( x x. m ) ) ) |
190 |
182 187 189
|
3brtr4d |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` [_ n / k ]_ A ) <_ ( x x. ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) ) |
191 |
63 68 73 76 190
|
letrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) <_ ( x x. ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) ) |
192 |
|
rpregt0 |
|- ( x e. RR+ -> ( x e. RR /\ 0 < x ) ) |
193 |
192
|
ad2antrl |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( x e. RR /\ 0 < x ) ) |
194 |
|
ledivmul |
|- ( ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) e. RR /\ ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) <-> ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) <_ ( x x. ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) ) ) |
195 |
63 72 193 194
|
syl3anc |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) <-> ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) <_ ( x x. ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) ) ) |
196 |
191 195
|
mpbird |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) A ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) |
197 |
61 196
|
eqbrtrd |
|- ( ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) /\ ( x e. RR+ /\ c <_ x ) ) -> ( abs ` ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` c ) ) ( abs ` [_ n / k ]_ A ) + m ) ) |
198 |
10 39 45 53 197
|
elo1d |
|- ( ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) /\ A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) ) -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) e. O(1) ) |
199 |
198
|
ex |
|- ( ( ph /\ ( c e. ( 1 [,) +oo ) /\ m e. RR ) ) -> ( A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) e. O(1) ) ) |
200 |
199
|
rexlimdvva |
|- ( ph -> ( E. c e. ( 1 [,) +oo ) E. m e. RR A. k e. NN ( c <_ k -> ( abs ` A ) <_ m ) -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) e. O(1) ) ) |
201 |
8 200
|
mpd |
|- ( ph -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) A / x ) ) e. O(1) ) |