Metamath Proof Explorer

Theorem zetacvg

Description: The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014)

Ref Expression
Hypotheses zetacvg.1 
|- ( ph -> S e. CC )
zetacvg.2 
|- ( ph -> 1 < ( Re ` S ) )
zetacvg.3 
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( k ^c -u S ) )
Assertion zetacvg 
|- ( ph -> seq 1 ( + , F ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 zetacvg.1 
 |-  ( ph -> S e. CC )
2 zetacvg.2 
 |-  ( ph -> 1 < ( Re ` S ) )
3 zetacvg.3 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( k ^c -u S ) )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( ph -> 1 e. ZZ )
6 oveq1 
 |-  ( n = k -> ( n ^c -u ( Re ` S ) ) = ( k ^c -u ( Re ` S ) ) )
7 eqid 
 |-  ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) = ( n e. NN |-> ( n ^c -u ( Re ` S ) ) )
8 ovex 
 |-  ( k ^c -u ( Re ` S ) ) e. _V
9 6 7 8 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) = ( k ^c -u ( Re ` S ) ) )
10 9 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) = ( k ^c -u ( Re ` S ) ) )
11 nncn 
 |-  ( k e. NN -> k e. CC )
12 11 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. CC )
13 nnne0 
 |-  ( k e. NN -> k =/= 0 )
14 13 adantl 
 |-  ( ( ph /\ k e. NN ) -> k =/= 0 )
15 1 negcld 
 |-  ( ph -> -u S e. CC )
16 15 adantr 
 |-  ( ( ph /\ k e. NN ) -> -u S e. CC )
17 12 14 16 cxpefd 
 |-  ( ( ph /\ k e. NN ) -> ( k ^c -u S ) = ( exp ` ( -u S x. ( log ` k ) ) ) )
18 3 17 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( exp ` ( -u S x. ( log ` k ) ) ) )
19 18 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( F ` k ) ) = ( abs ` ( exp ` ( -u S x. ( log ` k ) ) ) ) )
20 nnrp 
 |-  ( k e. NN -> k e. RR+ )
21 20 relogcld 
 |-  ( k e. NN -> ( log ` k ) e. RR )
22 21 recnd 
 |-  ( k e. NN -> ( log ` k ) e. CC )
23 mulcl 
 |-  ( ( -u S e. CC /\ ( log ` k ) e. CC ) -> ( -u S x. ( log ` k ) ) e. CC )
24 15 22 23 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( -u S x. ( log ` k ) ) e. CC )
25 absef 
 |-  ( ( -u S x. ( log ` k ) ) e. CC -> ( abs ` ( exp ` ( -u S x. ( log ` k ) ) ) ) = ( exp ` ( Re ` ( -u S x. ( log ` k ) ) ) ) )
26 24 25 syl 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( exp ` ( -u S x. ( log ` k ) ) ) ) = ( exp ` ( Re ` ( -u S x. ( log ` k ) ) ) ) )
27 remul 
 |-  ( ( -u S e. CC /\ ( log ` k ) e. CC ) -> ( Re ` ( -u S x. ( log ` k ) ) ) = ( ( ( Re ` -u S ) x. ( Re ` ( log ` k ) ) ) - ( ( Im ` -u S ) x. ( Im ` ( log ` k ) ) ) ) )
28 15 22 27 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( Re ` ( -u S x. ( log ` k ) ) ) = ( ( ( Re ` -u S ) x. ( Re ` ( log ` k ) ) ) - ( ( Im ` -u S ) x. ( Im ` ( log ` k ) ) ) ) )
29 1 renegd 
 |-  ( ph -> ( Re ` -u S ) = -u ( Re ` S ) )
30 21 rered 
 |-  ( k e. NN -> ( Re ` ( log ` k ) ) = ( log ` k ) )
31 29 30 oveqan12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( Re ` -u S ) x. ( Re ` ( log ` k ) ) ) = ( -u ( Re ` S ) x. ( log ` k ) ) )
32 21 reim0d 
 |-  ( k e. NN -> ( Im ` ( log ` k ) ) = 0 )
33 32 oveq2d 
 |-  ( k e. NN -> ( ( Im ` -u S ) x. ( Im ` ( log ` k ) ) ) = ( ( Im ` -u S ) x. 0 ) )
34 imcl 
 |-  ( -u S e. CC -> ( Im ` -u S ) e. RR )
35 34 recnd 
 |-  ( -u S e. CC -> ( Im ` -u S ) e. CC )
36 15 35 syl 
 |-  ( ph -> ( Im ` -u S ) e. CC )
37 36 mul01d 
 |-  ( ph -> ( ( Im ` -u S ) x. 0 ) = 0 )
38 33 37 sylan9eqr 
 |-  ( ( ph /\ k e. NN ) -> ( ( Im ` -u S ) x. ( Im ` ( log ` k ) ) ) = 0 )
39 31 38 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( Re ` -u S ) x. ( Re ` ( log ` k ) ) ) - ( ( Im ` -u S ) x. ( Im ` ( log ` k ) ) ) ) = ( ( -u ( Re ` S ) x. ( log ` k ) ) - 0 ) )
40 1 recld 
 |-  ( ph -> ( Re ` S ) e. RR )
41 40 renegcld 
 |-  ( ph -> -u ( Re ` S ) e. RR )
42 41 recnd 
 |-  ( ph -> -u ( Re ` S ) e. CC )
43 mulcl 
 |-  ( ( -u ( Re ` S ) e. CC /\ ( log ` k ) e. CC ) -> ( -u ( Re ` S ) x. ( log ` k ) ) e. CC )
44 42 22 43 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( -u ( Re ` S ) x. ( log ` k ) ) e. CC )
45 44 subid1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( -u ( Re ` S ) x. ( log ` k ) ) - 0 ) = ( -u ( Re ` S ) x. ( log ` k ) ) )
46 28 39 45 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( Re ` ( -u S x. ( log ` k ) ) ) = ( -u ( Re ` S ) x. ( log ` k ) ) )
47 46 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( Re ` ( -u S x. ( log ` k ) ) ) ) = ( exp ` ( -u ( Re ` S ) x. ( log ` k ) ) ) )
48 42 adantr 
 |-  ( ( ph /\ k e. NN ) -> -u ( Re ` S ) e. CC )
49 12 14 48 cxpefd 
 |-  ( ( ph /\ k e. NN ) -> ( k ^c -u ( Re ` S ) ) = ( exp ` ( -u ( Re ` S ) x. ( log ` k ) ) ) )
50 47 49 eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( Re ` ( -u S x. ( log ` k ) ) ) ) = ( k ^c -u ( Re ` S ) ) )
51 19 26 50 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( F ` k ) ) = ( k ^c -u ( Re ` S ) ) )
52 10 51 eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) = ( abs ` ( F ` k ) ) )
53 12 16 cxpcld 
 |-  ( ( ph /\ k e. NN ) -> ( k ^c -u S ) e. CC )
54 3 53 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. CC )
55 2rp 
 |-  2 e. RR+
56 1re 
 |-  1 e. RR
57 resubcl 
 |-  ( ( 1 e. RR /\ ( Re ` S ) e. RR ) -> ( 1 - ( Re ` S ) ) e. RR )
58 56 40 57 sylancr 
 |-  ( ph -> ( 1 - ( Re ` S ) ) e. RR )
59 rpcxpcl 
 |-  ( ( 2 e. RR+ /\ ( 1 - ( Re ` S ) ) e. RR ) -> ( 2 ^c ( 1 - ( Re ` S ) ) ) e. RR+ )
60 55 58 59 sylancr 
 |-  ( ph -> ( 2 ^c ( 1 - ( Re ` S ) ) ) e. RR+ )
61 60 rpcnd 
 |-  ( ph -> ( 2 ^c ( 1 - ( Re ` S ) ) ) e. CC )
62 recl 
 |-  ( S e. CC -> ( Re ` S ) e. RR )
63 62 recnd 
 |-  ( S e. CC -> ( Re ` S ) e. CC )
64 1 63 syl 
 |-  ( ph -> ( Re ` S ) e. CC )
65 64 addlidd 
 |-  ( ph -> ( 0 + ( Re ` S ) ) = ( Re ` S ) )
66 2 65 breqtrrd 
 |-  ( ph -> 1 < ( 0 + ( Re ` S ) ) )
67 0re 
 |-  0 e. RR
68 ltsubadd 
 |-  ( ( 1 e. RR /\ ( Re ` S ) e. RR /\ 0 e. RR ) -> ( ( 1 - ( Re ` S ) ) < 0 <-> 1 < ( 0 + ( Re ` S ) ) ) )
69 56 67 68 mp3an13 
 |-  ( ( Re ` S ) e. RR -> ( ( 1 - ( Re ` S ) ) < 0 <-> 1 < ( 0 + ( Re ` S ) ) ) )
70 40 69 syl 
 |-  ( ph -> ( ( 1 - ( Re ` S ) ) < 0 <-> 1 < ( 0 + ( Re ` S ) ) ) )
71 66 70 mpbird 
 |-  ( ph -> ( 1 - ( Re ` S ) ) < 0 )
72 2re 
 |-  2 e. RR
73 1lt2 
 |-  1 < 2
74 cxplt 
 |-  ( ( ( 2 e. RR /\ 1 < 2 ) /\ ( ( 1 - ( Re ` S ) ) e. RR /\ 0 e. RR ) ) -> ( ( 1 - ( Re ` S ) ) < 0 <-> ( 2 ^c ( 1 - ( Re ` S ) ) ) < ( 2 ^c 0 ) ) )
75 72 73 74 mpanl12 
 |-  ( ( ( 1 - ( Re ` S ) ) e. RR /\ 0 e. RR ) -> ( ( 1 - ( Re ` S ) ) < 0 <-> ( 2 ^c ( 1 - ( Re ` S ) ) ) < ( 2 ^c 0 ) ) )
76 58 67 75 sylancl 
 |-  ( ph -> ( ( 1 - ( Re ` S ) ) < 0 <-> ( 2 ^c ( 1 - ( Re ` S ) ) ) < ( 2 ^c 0 ) ) )
77 71 76 mpbid 
 |-  ( ph -> ( 2 ^c ( 1 - ( Re ` S ) ) ) < ( 2 ^c 0 ) )
78 60 rprege0d 
 |-  ( ph -> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) e. RR /\ 0 <_ ( 2 ^c ( 1 - ( Re ` S ) ) ) ) )
79 absid 
 |-  ( ( ( 2 ^c ( 1 - ( Re ` S ) ) ) e. RR /\ 0 <_ ( 2 ^c ( 1 - ( Re ` S ) ) ) ) -> ( abs ` ( 2 ^c ( 1 - ( Re ` S ) ) ) ) = ( 2 ^c ( 1 - ( Re ` S ) ) ) )
80 78 79 syl 
 |-  ( ph -> ( abs ` ( 2 ^c ( 1 - ( Re ` S ) ) ) ) = ( 2 ^c ( 1 - ( Re ` S ) ) ) )
81 2cn 
 |-  2 e. CC
82 cxp0 
 |-  ( 2 e. CC -> ( 2 ^c 0 ) = 1 )
83 81 82 ax-mp 
 |-  ( 2 ^c 0 ) = 1
84 83 eqcomi 
 |-  1 = ( 2 ^c 0 )
85 84 a1i 
 |-  ( ph -> 1 = ( 2 ^c 0 ) )
86 77 80 85 3brtr4d 
 |-  ( ph -> ( abs ` ( 2 ^c ( 1 - ( Re ` S ) ) ) ) < 1 )
87 oveq2 
 |-  ( n = m -> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) = ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) )
88 eqid 
 |-  ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) = ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) )
89 ovex 
 |-  ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) e. _V
90 87 88 89 fvmpt 
 |-  ( m e. NN0 -> ( ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ` m ) = ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) )
91 90 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ` m ) = ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) )
92 61 86 91 geolim 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( 2 ^c ( 1 - ( Re ` S ) ) ) ) ) )
93 seqex 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ) e. _V
94 ovex 
 |-  ( 1 / ( 1 - ( 2 ^c ( 1 - ( Re ` S ) ) ) ) ) e. _V
95 93 94 breldm 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( 2 ^c ( 1 - ( Re ` S ) ) ) ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ) e. dom ~~> )
96 92 95 syl 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ) e. dom ~~> )
97 rpcxpcl 
 |-  ( ( k e. RR+ /\ -u ( Re ` S ) e. RR ) -> ( k ^c -u ( Re ` S ) ) e. RR+ )
98 20 41 97 syl2anr 
 |-  ( ( ph /\ k e. NN ) -> ( k ^c -u ( Re ` S ) ) e. RR+ )
99 98 rpred 
 |-  ( ( ph /\ k e. NN ) -> ( k ^c -u ( Re ` S ) ) e. RR )
100 10 99 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) e. RR )
101 98 rpge0d 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( k ^c -u ( Re ` S ) ) )
102 101 10 breqtrrd 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) )
103 nnre 
 |-  ( k e. NN -> k e. RR )
104 103 lep1d 
 |-  ( k e. NN -> k <_ ( k + 1 ) )
105 20 reeflogd 
 |-  ( k e. NN -> ( exp ` ( log ` k ) ) = k )
106 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
107 106 nnrpd 
 |-  ( k e. NN -> ( k + 1 ) e. RR+ )
108 107 reeflogd 
 |-  ( k e. NN -> ( exp ` ( log ` ( k + 1 ) ) ) = ( k + 1 ) )
109 104 105 108 3brtr4d 
 |-  ( k e. NN -> ( exp ` ( log ` k ) ) <_ ( exp ` ( log ` ( k + 1 ) ) ) )
110 107 relogcld 
 |-  ( k e. NN -> ( log ` ( k + 1 ) ) e. RR )
111 efle 
 |-  ( ( ( log ` k ) e. RR /\ ( log ` ( k + 1 ) ) e. RR ) -> ( ( log ` k ) <_ ( log ` ( k + 1 ) ) <-> ( exp ` ( log ` k ) ) <_ ( exp ` ( log ` ( k + 1 ) ) ) ) )
112 21 110 111 syl2anc 
 |-  ( k e. NN -> ( ( log ` k ) <_ ( log ` ( k + 1 ) ) <-> ( exp ` ( log ` k ) ) <_ ( exp ` ( log ` ( k + 1 ) ) ) ) )
113 109 112 mpbird 
 |-  ( k e. NN -> ( log ` k ) <_ ( log ` ( k + 1 ) ) )
114 113 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( log ` k ) <_ ( log ` ( k + 1 ) ) )
115 21 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( log ` k ) e. RR )
116 106 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
117 116 nnrpd 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. RR+ )
118 117 relogcld 
 |-  ( ( ph /\ k e. NN ) -> ( log ` ( k + 1 ) ) e. RR )
119 40 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( Re ` S ) e. RR )
120 67 a1i 
 |-  ( ph -> 0 e. RR )
121 56 a1i 
 |-  ( ph -> 1 e. RR )
122 0lt1 
 |-  0 < 1
123 122 a1i 
 |-  ( ph -> 0 < 1 )
124 120 121 40 123 2 lttrd 
 |-  ( ph -> 0 < ( Re ` S ) )
125 124 adantr 
 |-  ( ( ph /\ k e. NN ) -> 0 < ( Re ` S ) )
126 lemul2 
 |-  ( ( ( log ` k ) e. RR /\ ( log ` ( k + 1 ) ) e. RR /\ ( ( Re ` S ) e. RR /\ 0 < ( Re ` S ) ) ) -> ( ( log ` k ) <_ ( log ` ( k + 1 ) ) <-> ( ( Re ` S ) x. ( log ` k ) ) <_ ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) )
127 115 118 119 125 126 syl112anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( log ` k ) <_ ( log ` ( k + 1 ) ) <-> ( ( Re ` S ) x. ( log ` k ) ) <_ ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) )
128 114 127 mpbid 
 |-  ( ( ph /\ k e. NN ) -> ( ( Re ` S ) x. ( log ` k ) ) <_ ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) )
129 remulcl 
 |-  ( ( ( Re ` S ) e. RR /\ ( log ` k ) e. RR ) -> ( ( Re ` S ) x. ( log ` k ) ) e. RR )
130 40 21 129 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( ( Re ` S ) x. ( log ` k ) ) e. RR )
131 remulcl 
 |-  ( ( ( Re ` S ) e. RR /\ ( log ` ( k + 1 ) ) e. RR ) -> ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) e. RR )
132 40 110 131 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) e. RR )
133 130 132 lenegd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( Re ` S ) x. ( log ` k ) ) <_ ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) <-> -u ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) <_ -u ( ( Re ` S ) x. ( log ` k ) ) ) )
134 128 133 mpbid 
 |-  ( ( ph /\ k e. NN ) -> -u ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) <_ -u ( ( Re ` S ) x. ( log ` k ) ) )
135 110 recnd 
 |-  ( k e. NN -> ( log ` ( k + 1 ) ) e. CC )
136 mulneg1 
 |-  ( ( ( Re ` S ) e. CC /\ ( log ` ( k + 1 ) ) e. CC ) -> ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) = -u ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) )
137 64 135 136 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) = -u ( ( Re ` S ) x. ( log ` ( k + 1 ) ) ) )
138 mulneg1 
 |-  ( ( ( Re ` S ) e. CC /\ ( log ` k ) e. CC ) -> ( -u ( Re ` S ) x. ( log ` k ) ) = -u ( ( Re ` S ) x. ( log ` k ) ) )
139 64 22 138 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( -u ( Re ` S ) x. ( log ` k ) ) = -u ( ( Re ` S ) x. ( log ` k ) ) )
140 134 137 139 3brtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) <_ ( -u ( Re ` S ) x. ( log ` k ) ) )
141 remulcl 
 |-  ( ( -u ( Re ` S ) e. RR /\ ( log ` ( k + 1 ) ) e. RR ) -> ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) e. RR )
142 41 110 141 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) e. RR )
143 remulcl 
 |-  ( ( -u ( Re ` S ) e. RR /\ ( log ` k ) e. RR ) -> ( -u ( Re ` S ) x. ( log ` k ) ) e. RR )
144 41 21 143 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( -u ( Re ` S ) x. ( log ` k ) ) e. RR )
145 efle 
 |-  ( ( ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) e. RR /\ ( -u ( Re ` S ) x. ( log ` k ) ) e. RR ) -> ( ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) <_ ( -u ( Re ` S ) x. ( log ` k ) ) <-> ( exp ` ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) <_ ( exp ` ( -u ( Re ` S ) x. ( log ` k ) ) ) ) )
146 142 144 145 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) <_ ( -u ( Re ` S ) x. ( log ` k ) ) <-> ( exp ` ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) <_ ( exp ` ( -u ( Re ` S ) x. ( log ` k ) ) ) ) )
147 140 146 mpbid 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) <_ ( exp ` ( -u ( Re ` S ) x. ( log ` k ) ) ) )
148 oveq1 
 |-  ( n = ( k + 1 ) -> ( n ^c -u ( Re ` S ) ) = ( ( k + 1 ) ^c -u ( Re ` S ) ) )
149 ovex 
 |-  ( ( k + 1 ) ^c -u ( Re ` S ) ) e. _V
150 148 7 149 fvmpt 
 |-  ( ( k + 1 ) e. NN -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( k + 1 ) ) = ( ( k + 1 ) ^c -u ( Re ` S ) ) )
151 116 150 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( k + 1 ) ) = ( ( k + 1 ) ^c -u ( Re ` S ) ) )
152 116 nncnd 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. CC )
153 116 nnne0d 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) =/= 0 )
154 152 153 48 cxpefd 
 |-  ( ( ph /\ k e. NN ) -> ( ( k + 1 ) ^c -u ( Re ` S ) ) = ( exp ` ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) )
155 151 154 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( k + 1 ) ) = ( exp ` ( -u ( Re ` S ) x. ( log ` ( k + 1 ) ) ) ) )
156 10 49 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) = ( exp ` ( -u ( Re ` S ) x. ( log ` k ) ) ) )
157 147 155 156 3brtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( k + 1 ) ) <_ ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` k ) )
158 58 recnd 
 |-  ( ph -> ( 1 - ( Re ` S ) ) e. CC )
159 158 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> ( 1 - ( Re ` S ) ) e. CC )
160 nn0re 
 |-  ( m e. NN0 -> m e. RR )
161 160 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> m e. RR )
162 161 recnd 
 |-  ( ( ph /\ m e. NN0 ) -> m e. CC )
163 159 162 mulcomd 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 1 - ( Re ` S ) ) x. m ) = ( m x. ( 1 - ( Re ` S ) ) ) )
164 163 oveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^c ( ( 1 - ( Re ` S ) ) x. m ) ) = ( 2 ^c ( m x. ( 1 - ( Re ` S ) ) ) ) )
165 55 a1i 
 |-  ( ( ph /\ m e. NN0 ) -> 2 e. RR+ )
166 165 161 159 cxpmuld 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^c ( m x. ( 1 - ( Re ` S ) ) ) ) = ( ( 2 ^c m ) ^c ( 1 - ( Re ` S ) ) ) )
167 simpr 
 |-  ( ( ph /\ m e. NN0 ) -> m e. NN0 )
168 cxpexp 
 |-  ( ( 2 e. CC /\ m e. NN0 ) -> ( 2 ^c m ) = ( 2 ^ m ) )
169 81 167 168 sylancr 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^c m ) = ( 2 ^ m ) )
170 ax-1cn 
 |-  1 e. CC
171 64 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> ( Re ` S ) e. CC )
172 negsub 
 |-  ( ( 1 e. CC /\ ( Re ` S ) e. CC ) -> ( 1 + -u ( Re ` S ) ) = ( 1 - ( Re ` S ) ) )
173 170 171 172 sylancr 
 |-  ( ( ph /\ m e. NN0 ) -> ( 1 + -u ( Re ` S ) ) = ( 1 - ( Re ` S ) ) )
174 173 eqcomd 
 |-  ( ( ph /\ m e. NN0 ) -> ( 1 - ( Re ` S ) ) = ( 1 + -u ( Re ` S ) ) )
175 169 174 oveq12d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^c m ) ^c ( 1 - ( Re ` S ) ) ) = ( ( 2 ^ m ) ^c ( 1 + -u ( Re ` S ) ) ) )
176 164 166 175 3eqtrd 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^c ( ( 1 - ( Re ` S ) ) x. m ) ) = ( ( 2 ^ m ) ^c ( 1 + -u ( Re ` S ) ) ) )
177 58 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> ( 1 - ( Re ` S ) ) e. RR )
178 165 177 162 cxpmuld 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^c ( ( 1 - ( Re ` S ) ) x. m ) ) = ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^c m ) )
179 2nn 
 |-  2 e. NN
180 nnexpcl 
 |-  ( ( 2 e. NN /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
181 179 180 mpan 
 |-  ( m e. NN0 -> ( 2 ^ m ) e. NN )
182 181 adantl 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
183 182 nncnd 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^ m ) e. CC )
184 182 nnne0d 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^ m ) =/= 0 )
185 1cnd 
 |-  ( ( ph /\ m e. NN0 ) -> 1 e. CC )
186 42 adantr 
 |-  ( ( ph /\ m e. NN0 ) -> -u ( Re ` S ) e. CC )
187 183 184 185 186 cxpaddd 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^ m ) ^c ( 1 + -u ( Re ` S ) ) ) = ( ( ( 2 ^ m ) ^c 1 ) x. ( ( 2 ^ m ) ^c -u ( Re ` S ) ) ) )
188 176 178 187 3eqtr3d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^c m ) = ( ( ( 2 ^ m ) ^c 1 ) x. ( ( 2 ^ m ) ^c -u ( Re ` S ) ) ) )
189 cxpexp 
 |-  ( ( ( 2 ^c ( 1 - ( Re ` S ) ) ) e. CC /\ m e. NN0 ) -> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^c m ) = ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) )
190 61 189 sylan 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^c m ) = ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) )
191 183 cxp1d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^ m ) ^c 1 ) = ( 2 ^ m ) )
192 191 oveq1d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( ( 2 ^ m ) ^c 1 ) x. ( ( 2 ^ m ) ^c -u ( Re ` S ) ) ) = ( ( 2 ^ m ) x. ( ( 2 ^ m ) ^c -u ( Re ` S ) ) ) )
193 188 190 192 3eqtr3d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ m ) = ( ( 2 ^ m ) x. ( ( 2 ^ m ) ^c -u ( Re ` S ) ) ) )
194 179 167 180 sylancr 
 |-  ( ( ph /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
195 oveq1 
 |-  ( n = ( 2 ^ m ) -> ( n ^c -u ( Re ` S ) ) = ( ( 2 ^ m ) ^c -u ( Re ` S ) ) )
196 ovex 
 |-  ( ( 2 ^ m ) ^c -u ( Re ` S ) ) e. _V
197 195 7 196 fvmpt 
 |-  ( ( 2 ^ m ) e. NN -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( 2 ^ m ) ) = ( ( 2 ^ m ) ^c -u ( Re ` S ) ) )
198 194 197 syl 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( 2 ^ m ) ) = ( ( 2 ^ m ) ^c -u ( Re ` S ) ) )
199 198 oveq2d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( 2 ^ m ) x. ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( 2 ^ m ) ) ) = ( ( 2 ^ m ) x. ( ( 2 ^ m ) ^c -u ( Re ` S ) ) ) )
200 193 91 199 3eqtr4d 
 |-  ( ( ph /\ m e. NN0 ) -> ( ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ` m ) = ( ( 2 ^ m ) x. ( ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ` ( 2 ^ m ) ) ) )
201 100 102 157 200 climcnds 
 |-  ( ph -> ( seq 1 ( + , ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ) e. dom ~~> <-> seq 0 ( + , ( n e. NN0 |-> ( ( 2 ^c ( 1 - ( Re ` S ) ) ) ^ n ) ) ) e. dom ~~> ) )
202 96 201 mpbird 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> ( n ^c -u ( Re ` S ) ) ) ) e. dom ~~> )
203 4 5 52 54 202 abscvgcvg 
 |-  ( ph -> seq 1 ( + , F ) e. dom ~~> )