Metamath Proof Explorer

Theorem stirlinglem5

Description: If T is between 0 and 1 , then a series (without alternating negative and positive terms) is given that converges to log((1+T)/(1-T)). (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem5.1 ⊢ 𝐷 = ( 𝑗 ∈ ℕ ↦ ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) )
stirlinglem5.2 ⊢ 𝐸 = ( 𝑗 ∈ ℕ ↦ ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) )
stirlinglem5.3 ⊢ 𝐹 = ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) + ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) )
stirlinglem5.4 ⊢ 𝐻 = ( 𝑗 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) )
stirlinglem5.5 ⊢ 𝐺 = ( 𝑗 ∈ ℕ0 ↦ ( ( 2 · 𝑗 ) + 1 ) )
stirlinglem5.6 ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
stirlinglem5.7 ⊢ ( 𝜑 → ( abs ‘ 𝑇 ) < 1 )
Assertion stirlinglem5 ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( log ‘ ( ( 1 + 𝑇 ) / ( 1 − 𝑇 ) ) ) )

Proof

Step Hyp Ref Expression
1 stirlinglem5.1 ⊢ 𝐷 = ( 𝑗 ∈ ℕ ↦ ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) )
2 stirlinglem5.2 ⊢ 𝐸 = ( 𝑗 ∈ ℕ ↦ ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) )
3 stirlinglem5.3 ⊢ 𝐹 = ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) + ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) )
4 stirlinglem5.4 ⊢ 𝐻 = ( 𝑗 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) )
5 stirlinglem5.5 ⊢ 𝐺 = ( 𝑗 ∈ ℕ0 ↦ ( ( 2 · 𝑗 ) + 1 ) )
6 stirlinglem5.6 ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
7 stirlinglem5.7 ⊢ ( 𝜑 → ( abs ‘ 𝑇 ) < 1 )
8 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
9 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
10 1 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑗 ∈ ℕ ↦ ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) ) )
11 1cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℂ )
12 11 negcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → - 1 ∈ ℂ )
13 nnm1nn0 ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑗 − 1 ) ∈ ℕ0 )
15 12 14 expcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( - 1 ↑ ( 𝑗 − 1 ) ) ∈ ℂ )
16 nncn ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℂ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℂ )
18 6 rpred ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑇 ∈ ℂ )
21 nnnn0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
23 20 22 expcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ↑ 𝑗 ) ∈ ℂ )
24 nnne0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ≠ 0 )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ≠ 0 )
26 15 17 23 25 div32d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( 𝑇 ↑ 𝑗 ) ) = ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) )
27 11 20 pncan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 1 + 𝑇 ) − 1 ) = 𝑇 )
28 27 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑇 = ( ( 1 + 𝑇 ) − 1 ) )
29 28 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑇 ↑ 𝑗 ) = ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( 𝑇 ↑ 𝑗 ) ) = ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) )
31 26 30 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) = ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) )
32 31 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) ) )
33 10 32 eqtrd ⊢ ( 𝜑 → 𝐷 = ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) ) )
34 33 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , 𝐷 ) = seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) ) ) )
35 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
36 35 19 addcld ⊢ ( 𝜑 → ( 1 + 𝑇 ) ∈ ℂ )
37 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
38 37 cnmetdval ⊢ ( ( 1 ∈ ℂ ∧ ( 1 + 𝑇 ) ∈ ℂ ) → ( 1 ( abs ∘ − ) ( 1 + 𝑇 ) ) = ( abs ‘ ( 1 − ( 1 + 𝑇 ) ) ) )
39 35 36 38 syl2anc ⊢ ( 𝜑 → ( 1 ( abs ∘ − ) ( 1 + 𝑇 ) ) = ( abs ‘ ( 1 − ( 1 + 𝑇 ) ) ) )
40 1m1e0 ⊢ ( 1 − 1 ) = 0
41 40 a1i ⊢ ( 𝜑 → ( 1 − 1 ) = 0 )
42 41 oveq1d ⊢ ( 𝜑 → ( ( 1 − 1 ) − 𝑇 ) = ( 0 − 𝑇 ) )
43 35 35 19 subsub4d ⊢ ( 𝜑 → ( ( 1 − 1 ) − 𝑇 ) = ( 1 − ( 1 + 𝑇 ) ) )
44 df-neg ⊢ - 𝑇 = ( 0 − 𝑇 )
45 44 eqcomi ⊢ ( 0 − 𝑇 ) = - 𝑇
46 45 a1i ⊢ ( 𝜑 → ( 0 − 𝑇 ) = - 𝑇 )
47 42 43 46 3eqtr3d ⊢ ( 𝜑 → ( 1 − ( 1 + 𝑇 ) ) = - 𝑇 )
48 47 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 1 − ( 1 + 𝑇 ) ) ) = ( abs ‘ - 𝑇 ) )
49 19 absnegd ⊢ ( 𝜑 → ( abs ‘ - 𝑇 ) = ( abs ‘ 𝑇 ) )
50 49 7 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ - 𝑇 ) < 1 )
51 48 50 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( 1 − ( 1 + 𝑇 ) ) ) < 1 )
52 39 51 eqbrtrd ⊢ ( 𝜑 → ( 1 ( abs ∘ − ) ( 1 + 𝑇 ) ) < 1 )
53 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
54 53 a1i ⊢ ( 𝜑 → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
55 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
56 55 rexrd ⊢ ( 𝜑 → 1 ∈ ℝ* )
57 elbl2 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 1 ∈ ℂ ∧ ( 1 + 𝑇 ) ∈ ℂ ) ) → ( ( 1 + 𝑇 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 1 ( abs ∘ − ) ( 1 + 𝑇 ) ) < 1 ) )
58 54 56 35 36 57 syl22anc ⊢ ( 𝜑 → ( ( 1 + 𝑇 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 1 ( abs ∘ − ) ( 1 + 𝑇 ) ) < 1 ) )
59 52 58 mpbird ⊢ ( 𝜑 → ( 1 + 𝑇 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) )
60 eqid ⊢ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) = ( 1 ( ball ‘ ( abs ∘ − ) ) 1 )
61 60 logtayl2 ⊢ ( ( 1 + 𝑇 ) ∈ ( 1 ( ball ‘ ( abs ∘ − ) ) 1 ) → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) ) ) ⇝ ( log ‘ ( 1 + 𝑇 ) ) )
62 59 61 syl ⊢ ( 𝜑 → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) / 𝑗 ) · ( ( ( 1 + 𝑇 ) − 1 ) ↑ 𝑗 ) ) ) ) ⇝ ( log ‘ ( 1 + 𝑇 ) ) )
63 34 62 eqbrtrd ⊢ ( 𝜑 → seq 1 ( + , 𝐷 ) ⇝ ( log ‘ ( 1 + 𝑇 ) ) )
64 seqex ⊢ seq 1 ( + , 𝐹 ) ∈ V
65 64 a1i ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ V )
66 2 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑗 ∈ ℕ ↦ ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) )
67 66 seqeq3d ⊢ ( 𝜑 → seq 1 ( + , 𝐸 ) = seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) ) )
68 logtayl ⊢ ( ( 𝑇 ∈ ℂ ∧ ( abs ‘ 𝑇 ) < 1 ) → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) ) ⇝ - ( log ‘ ( 1 − 𝑇 ) ) )
69 19 7 68 syl2anc ⊢ ( 𝜑 → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) ) ⇝ - ( log ‘ ( 1 − 𝑇 ) ) )
70 67 69 eqbrtrd ⊢ ( 𝜑 → seq 1 ( + , 𝐸 ) ⇝ - ( log ‘ ( 1 − 𝑇 ) ) )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
72 71 8 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
73 oveq1 ⊢ ( 𝑗 = 𝑛 → ( 𝑗 − 1 ) = ( 𝑛 − 1 ) )
74 73 oveq2d ⊢ ( 𝑗 = 𝑛 → ( - 1 ↑ ( 𝑗 − 1 ) ) = ( - 1 ↑ ( 𝑛 − 1 ) ) )
75 oveq2 ⊢ ( 𝑗 = 𝑛 → ( 𝑇 ↑ 𝑗 ) = ( 𝑇 ↑ 𝑛 ) )
76 id ⊢ ( 𝑗 = 𝑛 → 𝑗 = 𝑛 )
77 75 76 oveq12d ⊢ ( 𝑗 = 𝑛 → ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) = ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) )
78 74 77 oveq12d ⊢ ( 𝑗 = 𝑛 → ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) = ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
79 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑘 ) → 𝑛 ∈ ℕ )
80 79 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℕ )
81 1cnd ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℂ )
82 81 negcld ⊢ ( 𝑛 ∈ ℕ → - 1 ∈ ℂ )
83 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
84 82 83 expcld ⊢ ( 𝑛 ∈ ℕ → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
85 80 84 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
86 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑇 ∈ ℂ )
87 80 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℕ0 )
88 86 87 expcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝑇 ↑ 𝑛 ) ∈ ℂ )
89 80 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ∈ ℂ )
90 80 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝑛 ≠ 0 )
91 88 89 90 divcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ∈ ℂ )
92 85 91 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
93 1 78 80 92 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐷 ‘ 𝑛 ) = ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
94 93 92 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐷 ‘ 𝑛 ) ∈ ℂ )
95 addcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) → ( 𝑛 + 𝑖 ) ∈ ℂ )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ ) ) → ( 𝑛 + 𝑖 ) ∈ ℂ )
97 72 94 96 seqcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐷 ) ‘ 𝑘 ) ∈ ℂ )
98 2 77 80 91 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐸 ‘ 𝑛 ) = ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) )
99 98 91 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐸 ‘ 𝑛 ) ∈ ℂ )
100 72 99 96 seqcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐸 ) ‘ 𝑘 ) ∈ ℂ )
101 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → 𝜑 )
102 78 77 oveq12d ⊢ ( 𝑗 = 𝑛 → ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) + ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) = ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
103 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
104 84 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
105 19 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑇 ∈ ℂ )
106 103 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
107 105 106 expcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑇 ↑ 𝑛 ) ∈ ℂ )
108 103 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
109 103 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
110 107 108 109 divcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ∈ ℂ )
111 104 110 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
112 111 110 addcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
113 3 102 103 112 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
114 1 78 103 111 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐷 ‘ 𝑛 ) = ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
115 114 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = ( 𝐷 ‘ 𝑛 ) )
116 2 77 103 110 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ‘ 𝑛 ) = ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) )
117 116 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) = ( 𝐸 ‘ 𝑛 ) )
118 115 117 oveq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = ( ( 𝐷 ‘ 𝑛 ) + ( 𝐸 ‘ 𝑛 ) ) )
119 113 118 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐷 ‘ 𝑛 ) + ( 𝐸 ‘ 𝑛 ) ) )
120 101 80 119 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐷 ‘ 𝑛 ) + ( 𝐸 ‘ 𝑛 ) ) )
121 72 94 99 120 seradd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) = ( ( seq 1 ( + , 𝐷 ) ‘ 𝑘 ) + ( seq 1 ( + , 𝐸 ) ‘ 𝑘 ) ) )
122 8 9 63 65 70 97 100 121 climadd ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ ( ( log ‘ ( 1 + 𝑇 ) ) + - ( log ‘ ( 1 − 𝑇 ) ) ) )
123 1rp ⊢ 1 ∈ ℝ+
124 123 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
125 124 6 rpaddcld ⊢ ( 𝜑 → ( 1 + 𝑇 ) ∈ ℝ+ )
126 125 rpne0d ⊢ ( 𝜑 → ( 1 + 𝑇 ) ≠ 0 )
127 36 126 logcld ⊢ ( 𝜑 → ( log ‘ ( 1 + 𝑇 ) ) ∈ ℂ )
128 35 19 subcld ⊢ ( 𝜑 → ( 1 − 𝑇 ) ∈ ℂ )
129 18 55 absltd ⊢ ( 𝜑 → ( ( abs ‘ 𝑇 ) < 1 ↔ ( - 1 < 𝑇 ∧ 𝑇 < 1 ) ) )
130 7 129 mpbid ⊢ ( 𝜑 → ( - 1 < 𝑇 ∧ 𝑇 < 1 ) )
131 130 simprd ⊢ ( 𝜑 → 𝑇 < 1 )
132 18 131 gtned ⊢ ( 𝜑 → 1 ≠ 𝑇 )
133 35 19 132 subne0d ⊢ ( 𝜑 → ( 1 − 𝑇 ) ≠ 0 )
134 128 133 logcld ⊢ ( 𝜑 → ( log ‘ ( 1 − 𝑇 ) ) ∈ ℂ )
135 127 134 negsubd ⊢ ( 𝜑 → ( ( log ‘ ( 1 + 𝑇 ) ) + - ( log ‘ ( 1 − 𝑇 ) ) ) = ( ( log ‘ ( 1 + 𝑇 ) ) − ( log ‘ ( 1 − 𝑇 ) ) ) )
136 122 135 breqtrd ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ ( ( log ‘ ( 1 + 𝑇 ) ) − ( log ‘ ( 1 − 𝑇 ) ) ) )
137 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
138 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
139 2nn0 ⊢ 2 ∈ ℕ0
140 139 a1i ⊢ ( 𝑗 ∈ ℕ0 → 2 ∈ ℕ0 )
141 id ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℕ0 )
142 140 141 nn0mulcld ⊢ ( 𝑗 ∈ ℕ0 → ( 2 · 𝑗 ) ∈ ℕ0 )
143 nn0p1nn ⊢ ( ( 2 · 𝑗 ) ∈ ℕ0 → ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ )
144 142 143 syl ⊢ ( 𝑗 ∈ ℕ0 → ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ )
145 5 144 fmpti ⊢ 𝐺 : ℕ0 ⟶ ℕ
146 145 a1i ⊢ ( 𝜑 → 𝐺 : ℕ0 ⟶ ℕ )
147 2re ⊢ 2 ∈ ℝ
148 147 a1i ⊢ ( 𝑘 ∈ ℕ0 → 2 ∈ ℝ )
149 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
150 148 149 remulcld ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 𝑘 ) ∈ ℝ )
151 1red ⊢ ( 𝑘 ∈ ℕ0 → 1 ∈ ℝ )
152 149 151 readdcld ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℝ )
153 148 152 remulcld ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · ( 𝑘 + 1 ) ) ∈ ℝ )
154 2rp ⊢ 2 ∈ ℝ+
155 154 a1i ⊢ ( 𝑘 ∈ ℕ0 → 2 ∈ ℝ+ )
156 149 ltp1d ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 < ( 𝑘 + 1 ) )
157 149 152 155 156 ltmul2dd ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 𝑘 ) < ( 2 · ( 𝑘 + 1 ) ) )
158 150 153 151 157 ltadd1dd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 1 ) < ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) )
159 5 a1i ⊢ ( 𝑘 ∈ ℕ0 → 𝐺 = ( 𝑗 ∈ ℕ0 ↦ ( ( 2 · 𝑗 ) + 1 ) ) )
160 simpr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 = 𝑘 ) → 𝑗 = 𝑘 )
161 160 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 = 𝑘 ) → ( 2 · 𝑗 ) = ( 2 · 𝑘 ) )
162 161 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 = 𝑘 ) → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) )
163 id ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0 )
164 2cnd ⊢ ( 𝑘 ∈ ℕ0 → 2 ∈ ℂ )
165 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
166 164 165 mulcld ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 𝑘 ) ∈ ℂ )
167 1cnd ⊢ ( 𝑘 ∈ ℕ0 → 1 ∈ ℂ )
168 166 167 addcld ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
169 159 162 163 168 fvmptd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐺 ‘ 𝑘 ) = ( ( 2 · 𝑘 ) + 1 ) )
170 simpr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 = ( 𝑘 + 1 ) ) → 𝑗 = ( 𝑘 + 1 ) )
171 170 oveq2d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 = ( 𝑘 + 1 ) ) → ( 2 · 𝑗 ) = ( 2 · ( 𝑘 + 1 ) ) )
172 171 oveq1d ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑗 = ( 𝑘 + 1 ) ) → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) )
173 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
174 165 167 addcld ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℂ )
175 164 174 mulcld ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · ( 𝑘 + 1 ) ) ∈ ℂ )
176 175 167 addcld ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) ∈ ℂ )
177 159 172 173 176 fvmptd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐺 ‘ ( 𝑘 + 1 ) ) = ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) )
178 158 169 177 3brtr4d ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
179 178 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
180 eldifi ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → 𝑛 ∈ ℕ )
181 180 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → 𝑛 ∈ ℕ )
182 1cnd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → 1 ∈ ℂ )
183 182 negcld ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → - 1 ∈ ℂ )
184 180 83 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 𝑛 − 1 ) ∈ ℕ0 )
185 183 184 expcld ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
186 185 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( - 1 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
187 19 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → 𝑇 ∈ ℂ )
188 181 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → 𝑛 ∈ ℕ0 )
189 187 188 expcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( 𝑇 ↑ 𝑛 ) ∈ ℂ )
190 181 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → 𝑛 ∈ ℂ )
191 181 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → 𝑛 ≠ 0 )
192 189 190 191 divcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ∈ ℂ )
193 186 192 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
194 193 192 addcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
195 3 102 181 194 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
196 eldifn ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ¬ 𝑛 ∈ ran 𝐺 )
197 0nn0 ⊢ 0 ∈ ℕ0
198 1nn0 ⊢ 1 ∈ ℕ0
199 139 198 num0h ⊢ 1 = ( ( 2 · 0 ) + 1 )
200 oveq2 ⊢ ( 𝑗 = 0 → ( 2 · 𝑗 ) = ( 2 · 0 ) )
201 200 oveq1d ⊢ ( 𝑗 = 0 → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · 0 ) + 1 ) )
202 201 eqeq2d ⊢ ( 𝑗 = 0 → ( 1 = ( ( 2 · 𝑗 ) + 1 ) ↔ 1 = ( ( 2 · 0 ) + 1 ) ) )
203 202 rspcev ⊢ ( ( 0 ∈ ℕ0 ∧ 1 = ( ( 2 · 0 ) + 1 ) ) → ∃ 𝑗 ∈ ℕ0 1 = ( ( 2 · 𝑗 ) + 1 ) )
204 197 199 203 mp2an ⊢ ∃ 𝑗 ∈ ℕ0 1 = ( ( 2 · 𝑗 ) + 1 )
205 ax-1cn ⊢ 1 ∈ ℂ
206 5 elrnmpt ⊢ ( 1 ∈ ℂ → ( 1 ∈ ran 𝐺 ↔ ∃ 𝑗 ∈ ℕ0 1 = ( ( 2 · 𝑗 ) + 1 ) ) )
207 205 206 ax-mp ⊢ ( 1 ∈ ran 𝐺 ↔ ∃ 𝑗 ∈ ℕ0 1 = ( ( 2 · 𝑗 ) + 1 ) )
208 204 207 mpbir ⊢ 1 ∈ ran 𝐺
209 208 a1i ⊢ ( 𝑛 = 1 → 1 ∈ ran 𝐺 )
210 eleq1 ⊢ ( 𝑛 = 1 → ( 𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺 ) )
211 209 210 mpbird ⊢ ( 𝑛 = 1 → 𝑛 ∈ ran 𝐺 )
212 196 211 nsyl ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ¬ 𝑛 = 1 )
213 nn1m1nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 = 1 ∨ ( 𝑛 − 1 ) ∈ ℕ ) )
214 180 213 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 𝑛 = 1 ∨ ( 𝑛 − 1 ) ∈ ℕ ) )
215 214 ord ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( ¬ 𝑛 = 1 → ( 𝑛 − 1 ) ∈ ℕ ) )
216 212 215 mpd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 𝑛 − 1 ) ∈ ℕ )
217 nfcv ⊢ Ⅎ 𝑗 ℕ
218 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ℕ0 ↦ ( ( 2 · 𝑗 ) + 1 ) )
219 5 218 nfcxfr ⊢ Ⅎ 𝑗 𝐺
220 219 nfrn ⊢ Ⅎ 𝑗 ran 𝐺
221 217 220 nfdif ⊢ Ⅎ 𝑗 ( ℕ ∖ ran 𝐺 )
222 221 nfcri ⊢ Ⅎ 𝑗 𝑛 ∈ ( ℕ ∖ ran 𝐺 )
223 5 elrnmpt ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 𝑛 ∈ ran 𝐺 ↔ ∃ 𝑗 ∈ ℕ0 𝑛 = ( ( 2 · 𝑗 ) + 1 ) ) )
224 196 223 mtbid ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ¬ ∃ 𝑗 ∈ ℕ0 𝑛 = ( ( 2 · 𝑗 ) + 1 ) )
225 ralnex ⊢ ( ∀ 𝑗 ∈ ℕ0 ¬ 𝑛 = ( ( 2 · 𝑗 ) + 1 ) ↔ ¬ ∃ 𝑗 ∈ ℕ0 𝑛 = ( ( 2 · 𝑗 ) + 1 ) )
226 224 225 sylibr ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ∀ 𝑗 ∈ ℕ0 ¬ 𝑛 = ( ( 2 · 𝑗 ) + 1 ) )
227 226 r19.21bi ⊢ ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℕ0 ) → ¬ 𝑛 = ( ( 2 · 𝑗 ) + 1 ) )
228 227 neqned ⊢ ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℕ0 ) → 𝑛 ≠ ( ( 2 · 𝑗 ) + 1 ) )
229 228 necomd ⊢ ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 𝑛 )
230 229 adantlr ⊢ ( ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 𝑛 )
231 simplr ⊢ ( ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) ∧ ¬ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℤ )
232 simpr ⊢ ( ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ 𝑗 ∈ ℕ0 )
233 180 ad2antrr ⊢ ( ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) ∧ ¬ 𝑗 ∈ ℕ0 ) → 𝑛 ∈ ℕ )
234 147 a1i ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 2 ∈ ℝ )
235 simpl ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℤ )
236 235 zred ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℝ )
237 234 236 remulcld ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 2 · 𝑗 ) ∈ ℝ )
238 0red ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 0 ∈ ℝ )
239 1red ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 1 ∈ ℝ )
240 2cnd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 2 ∈ ℂ )
241 236 recnd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℂ )
242 240 241 mulcomd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 2 · 𝑗 ) = ( 𝑗 · 2 ) )
243 simpr ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ 𝑗 ∈ ℕ0 )
244 elnn0z ⊢ ( 𝑗 ∈ ℕ0 ↔ ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) )
245 243 244 sylnib ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) )
246 nan ⊢ ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ ( 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) ) ↔ ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) ∧ 𝑗 ∈ ℤ ) → ¬ 0 ≤ 𝑗 ) )
247 245 246 mpbi ⊢ ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) ∧ 𝑗 ∈ ℤ ) → ¬ 0 ≤ 𝑗 )
248 247 anabss1 ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ 0 ≤ 𝑗 )
249 236 238 ltnled ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 𝑗 < 0 ↔ ¬ 0 ≤ 𝑗 ) )
250 248 249 mpbird ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 𝑗 < 0 )
251 154 a1i ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 2 ∈ ℝ+ )
252 251 rpregt0d ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
253 mulltgt0 ⊢ ( ( ( 𝑗 ∈ ℝ ∧ 𝑗 < 0 ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝑗 · 2 ) < 0 )
254 236 250 252 253 syl21anc ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 𝑗 · 2 ) < 0 )
255 242 254 eqbrtrd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 2 · 𝑗 ) < 0 )
256 237 238 239 255 ltadd1dd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) < ( 0 + 1 ) )
257 1cnd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → 1 ∈ ℂ )
258 257 addid2d ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( 0 + 1 ) = 1 )
259 256 258 breqtrd ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) < 1 )
260 237 239 readdcld ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℝ )
261 260 239 ltnled ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ( ( ( 2 · 𝑗 ) + 1 ) < 1 ↔ ¬ 1 ≤ ( ( 2 · 𝑗 ) + 1 ) ) )
262 259 261 mpbid ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ 1 ≤ ( ( 2 · 𝑗 ) + 1 ) )
263 nnge1 ⊢ ( ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ → 1 ≤ ( ( 2 · 𝑗 ) + 1 ) )
264 262 263 nsyl ⊢ ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) → ¬ ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ )
265 264 adantr ⊢ ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ¬ ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ )
266 simpr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) → ( ( 2 · 𝑗 ) + 1 ) = 𝑛 )
267 simpl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) → 𝑛 ∈ ℕ )
268 266 267 eqeltrd ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ )
269 268 adantll ⊢ ( ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) → ( ( 2 · 𝑗 ) + 1 ) ∈ ℕ )
270 265 269 mtand ⊢ ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ¬ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 )
271 270 neqned ⊢ ( ( ( 𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 𝑛 )
272 231 232 233 271 syl21anc ⊢ ( ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) ∧ ¬ 𝑗 ∈ ℕ0 ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 𝑛 )
273 230 272 pm2.61dan ⊢ ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) → ( ( 2 · 𝑗 ) + 1 ) ≠ 𝑛 )
274 273 neneqd ⊢ ( ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ∧ 𝑗 ∈ ℤ ) → ¬ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 )
275 274 ex ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 𝑗 ∈ ℤ → ¬ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) )
276 222 275 ralrimi ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ∀ 𝑗 ∈ ℤ ¬ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 )
277 ralnex ⊢ ( ∀ 𝑗 ∈ ℤ ¬ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ↔ ¬ ∃ 𝑗 ∈ ℤ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 )
278 276 277 sylib ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ¬ ∃ 𝑗 ∈ ℤ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 )
279 180 nnzd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → 𝑛 ∈ ℤ )
280 odd2np1 ⊢ ( 𝑛 ∈ ℤ → ( ¬ 2 ∥ 𝑛 ↔ ∃ 𝑗 ∈ ℤ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) )
281 279 280 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( ¬ 2 ∥ 𝑛 ↔ ∃ 𝑗 ∈ ℤ ( ( 2 · 𝑗 ) + 1 ) = 𝑛 ) )
282 278 281 mtbird ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ¬ ¬ 2 ∥ 𝑛 )
283 282 notnotrd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → 2 ∥ 𝑛 )
284 180 nncnd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → 𝑛 ∈ ℂ )
285 284 182 npcand ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
286 283 285 breqtrrd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → 2 ∥ ( ( 𝑛 − 1 ) + 1 ) )
287 184 nn0zd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 𝑛 − 1 ) ∈ ℤ )
288 oddp1even ⊢ ( ( 𝑛 − 1 ) ∈ ℤ → ( ¬ 2 ∥ ( 𝑛 − 1 ) ↔ 2 ∥ ( ( 𝑛 − 1 ) + 1 ) ) )
289 287 288 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( ¬ 2 ∥ ( 𝑛 − 1 ) ↔ 2 ∥ ( ( 𝑛 − 1 ) + 1 ) ) )
290 286 289 mpbird ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ¬ 2 ∥ ( 𝑛 − 1 ) )
291 oexpneg ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑛 − 1 ) ∈ ℕ ∧ ¬ 2 ∥ ( 𝑛 − 1 ) ) → ( - 1 ↑ ( 𝑛 − 1 ) ) = - ( 1 ↑ ( 𝑛 − 1 ) ) )
292 182 216 290 291 syl3anc ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( - 1 ↑ ( 𝑛 − 1 ) ) = - ( 1 ↑ ( 𝑛 − 1 ) ) )
293 1exp ⊢ ( ( 𝑛 − 1 ) ∈ ℤ → ( 1 ↑ ( 𝑛 − 1 ) ) = 1 )
294 287 293 syl ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( 1 ↑ ( 𝑛 − 1 ) ) = 1 )
295 294 negeqd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → - ( 1 ↑ ( 𝑛 − 1 ) ) = - 1 )
296 292 295 eqtrd ⊢ ( 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) → ( - 1 ↑ ( 𝑛 − 1 ) ) = - 1 )
297 296 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( - 1 ↑ ( 𝑛 − 1 ) ) = - 1 )
298 297 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = ( - 1 · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
299 298 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( ( - 1 ↑ ( 𝑛 − 1 ) ) · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = ( ( - 1 · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
300 192 mulm1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( - 1 · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = - ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) )
301 300 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( - 1 · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = ( - ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
302 192 negcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → - ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ∈ ℂ )
303 302 192 addcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( - ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = ( ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) + - ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) )
304 192 negidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) + - ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = 0 )
305 301 303 304 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( ( - 1 · ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) + ( ( 𝑇 ↑ 𝑛 ) / 𝑛 ) ) = 0 )
306 195 299 305 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
307 113 112 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
308 3 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐹 = ( 𝑗 ∈ ℕ ↦ ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) + ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) ) )
309 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → 𝑗 = ( ( 2 · 𝑘 ) + 1 ) )
310 309 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → ( 𝑗 − 1 ) = ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) )
311 310 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → ( - 1 ↑ ( 𝑗 − 1 ) ) = ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) )
312 309 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → ( 𝑇 ↑ 𝑗 ) = ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
313 312 309 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) = ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) )
314 311 313 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) = ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
315 314 313 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( ( 2 · 𝑘 ) + 1 ) ) → ( ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) + ( ( 𝑇 ↑ 𝑗 ) / 𝑗 ) ) = ( ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
316 139 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 2 ∈ ℕ0 )
317 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
318 316 317 nn0mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · 𝑘 ) ∈ ℕ0 )
319 nn0p1nn ⊢ ( ( 2 · 𝑘 ) ∈ ℕ0 → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ )
320 318 319 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ )
321 167 negcld ⊢ ( 𝑘 ∈ ℕ0 → - 1 ∈ ℂ )
322 166 167 pncand ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) = ( 2 · 𝑘 ) )
323 139 a1i ⊢ ( 𝑘 ∈ ℕ0 → 2 ∈ ℕ0 )
324 323 163 nn0mulcld ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 𝑘 ) ∈ ℕ0 )
325 322 324 eqeltrd ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ∈ ℕ0 )
326 321 325 expcld ⊢ ( 𝑘 ∈ ℕ0 → ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) ∈ ℂ )
327 326 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) ∈ ℂ )
328 19 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑇 ∈ ℂ )
329 198 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℕ0 )
330 318 329 nn0addcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 )
331 328 330 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
332 2cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 2 ∈ ℂ )
333 165 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
334 332 333 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · 𝑘 ) ∈ ℂ )
335 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
336 334 335 addcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℂ )
337 0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ∈ ℝ )
338 147 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 2 ∈ ℝ )
339 149 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ )
340 338 339 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · 𝑘 ) ∈ ℝ )
341 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℝ )
342 0le2 ⊢ 0 ≤ 2
343 342 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 2 )
344 317 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 𝑘 )
345 338 339 343 344 mulge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( 2 · 𝑘 ) )
346 0lt1 ⊢ 0 < 1
347 346 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 < 1 )
348 340 341 345 347 addgegt0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 < ( ( 2 · 𝑘 ) + 1 ) )
349 337 348 gtned ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 2 · 𝑘 ) + 1 ) ≠ 0 )
350 331 336 349 divcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
351 327 350 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ∈ ℂ )
352 351 350 addcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ∈ ℂ )
353 308 315 320 352 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 2 · 𝑘 ) + 1 ) ) = ( ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
354 322 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) = ( 2 · 𝑘 ) )
355 354 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) = ( - 1 ↑ ( 2 · 𝑘 ) ) )
356 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
357 m1expeven ⊢ ( 𝑘 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑘 ) ) = 1 )
358 356 357 syl ⊢ ( 𝑘 ∈ ℕ0 → ( - 1 ↑ ( 2 · 𝑘 ) ) = 1 )
359 358 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · 𝑘 ) ) = 1 )
360 355 359 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) = 1 )
361 360 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
362 350 mulid2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) )
363 361 362 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) )
364 363 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
365 350 2timesd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) )
366 331 336 349 divrec2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) = ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) )
367 366 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
368 364 365 367 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( - 1 ↑ ( ( ( 2 · 𝑘 ) + 1 ) − 1 ) ) · ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) + ( ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) / ( ( 2 · 𝑘 ) + 1 ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
369 353 368 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) + 1 ) ) )
370 4 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐻 = ( 𝑗 ∈ ℕ0 ↦ ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) ) )
371 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → 𝑗 = 𝑘 )
372 371 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 2 · 𝑗 ) = ( 2 · 𝑘 ) )
373 372 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) )
374 373 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) = ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) )
375 373 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝑇 ↑ ( ( 2 · 𝑗 ) + 1 ) ) = ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
376 374 375 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) = ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) )
377 376 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 2 · ( ( 1 / ( ( 2 · 𝑗 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑗 ) + 1 ) ) ) ) = ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
378 336 349 reccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
379 378 331 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ∈ ℂ )
380 332 379 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) ∈ ℂ )
381 370 377 317 380 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = ( 2 · ( ( 1 / ( ( 2 · 𝑘 ) + 1 ) ) · ( 𝑇 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) ) )
382 198 a1i ⊢ ( 𝑘 ∈ ℕ0 → 1 ∈ ℕ0 )
383 324 382 nn0addcld ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 )
384 159 162 163 383 fvmptd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐺 ‘ 𝑘 ) = ( ( 2 · 𝑘 ) + 1 ) )
385 384 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 2 · 𝑘 ) + 1 ) )
386 385 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ( 2 · 𝑘 ) + 1 ) ) )
387 369 381 386 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
388 137 8 138 9 146 179 306 307 387 isercoll2 ⊢ ( 𝜑 → ( seq 0 ( + , 𝐻 ) ⇝ ( ( log ‘ ( 1 + 𝑇 ) ) − ( log ‘ ( 1 − 𝑇 ) ) ) ↔ seq 1 ( + , 𝐹 ) ⇝ ( ( log ‘ ( 1 + 𝑇 ) ) − ( log ‘ ( 1 − 𝑇 ) ) ) ) )
389 136 388 mpbird ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( ( log ‘ ( 1 + 𝑇 ) ) − ( log ‘ ( 1 − 𝑇 ) ) ) )
390 55 18 resubcld ⊢ ( 𝜑 → ( 1 − 𝑇 ) ∈ ℝ )
391 19 subidd ⊢ ( 𝜑 → ( 𝑇 − 𝑇 ) = 0 )
392 391 eqcomd ⊢ ( 𝜑 → 0 = ( 𝑇 − 𝑇 ) )
393 18 55 18 131 ltsub1dd ⊢ ( 𝜑 → ( 𝑇 − 𝑇 ) < ( 1 − 𝑇 ) )
394 392 393 eqbrtrd ⊢ ( 𝜑 → 0 < ( 1 − 𝑇 ) )
395 390 394 elrpd ⊢ ( 𝜑 → ( 1 − 𝑇 ) ∈ ℝ+ )
396 125 395 relogdivd ⊢ ( 𝜑 → ( log ‘ ( ( 1 + 𝑇 ) / ( 1 − 𝑇 ) ) ) = ( ( log ‘ ( 1 + 𝑇 ) ) − ( log ‘ ( 1 − 𝑇 ) ) ) )
397 389 396 breqtrrd ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( log ‘ ( ( 1 + 𝑇 ) / ( 1 − 𝑇 ) ) ) )