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 addlidd ⊢ ( 𝜑 → ( 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 ⇝ )