Metamath Proof Explorer


Theorem zetacvg

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

Ref Expression
Hypotheses zetacvg.1 ( 𝜑𝑆 ∈ ℂ )
zetacvg.2 ( 𝜑 → 1 < ( ℜ ‘ 𝑆 ) )
zetacvg.3 ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) = ( 𝑘𝑐 - 𝑆 ) )
Assertion zetacvg ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

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