Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stirlinglem5 Structured version   Visualization version   GIF version

Theorem stirlinglem5 40816
Description: If 𝑇 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.)
Hypotheses
Ref Expression
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
Ref Expression
stirlinglem5 (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇))))
Distinct variable groups:   𝜑,𝑗   𝑇,𝑗
Allowed substitution hints:   𝐷(𝑗)   𝐸(𝑗)   𝐹(𝑗)   𝐺(𝑗)   𝐻(𝑗)

Proof of Theorem stirlinglem5
Dummy variables 𝑖 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11936 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 11620 . . . . 5 (𝜑 → 1 ∈ ℤ)
3 stirlinglem5.1 . . . . . . . . 9 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)))
43a1i 11 . . . . . . . 8 (𝜑𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))))
5 1cnd 10268 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℂ)
65negcld 10591 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → -1 ∈ ℂ)
7 nnm1nn0 11546 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
87adantl 473 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℕ0)
96, 8expcld 13222 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (-1↑(𝑗 − 1)) ∈ ℂ)
10 nncn 11240 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
1110adantl 473 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℂ)
12 stirlinglem5.6 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℝ+)
1312rpred 12085 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ ℝ)
1413recnd 10280 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℂ)
1514adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
16 nnnn0 11511 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
1716adantl 473 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
1815, 17expcld 13222 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℂ)
19 nnne0 11265 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ≠ 0)
2019adantl 473 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ≠ 0)
219, 11, 18, 20div32d 11036 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇𝑗)) = ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)))
225, 15pncan2d 10606 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((1 + 𝑇) − 1) = 𝑇)
2322eqcomd 2766 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑇 = ((1 + 𝑇) − 1))
2423oveq1d 6829 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (((1 + 𝑇) − 1)↑𝑗))
2524oveq2d 6830 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))
2621, 25eqtr3d 2796 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))
2726mpteq2dva 4896 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))))
284, 27eqtrd 2794 . . . . . . 7 (𝜑𝐷 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))))
2928seqeq3d 13023 . . . . . 6 (𝜑 → seq1( + , 𝐷) = seq1( + , (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))))
30 1cnd 10268 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
3130, 14addcld 10271 . . . . . . . . . 10 (𝜑 → (1 + 𝑇) ∈ ℂ)
32 eqid 2760 . . . . . . . . . . 11 (abs ∘ − ) = (abs ∘ − )
3332cnmetdval 22795 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ) → (1(abs ∘ − )(1 + 𝑇)) = (abs‘(1 − (1 + 𝑇))))
3430, 31, 33syl2anc 696 . . . . . . . . 9 (𝜑 → (1(abs ∘ − )(1 + 𝑇)) = (abs‘(1 − (1 + 𝑇))))
35 1m1e0 11301 . . . . . . . . . . . . . 14 (1 − 1) = 0
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 − 1) = 0)
3736oveq1d 6829 . . . . . . . . . . . 12 (𝜑 → ((1 − 1) − 𝑇) = (0 − 𝑇))
3830, 30, 14subsub4d 10635 . . . . . . . . . . . 12 (𝜑 → ((1 − 1) − 𝑇) = (1 − (1 + 𝑇)))
39 df-neg 10481 . . . . . . . . . . . . . 14 -𝑇 = (0 − 𝑇)
4039eqcomi 2769 . . . . . . . . . . . . 13 (0 − 𝑇) = -𝑇
4140a1i 11 . . . . . . . . . . . 12 (𝜑 → (0 − 𝑇) = -𝑇)
4237, 38, 413eqtr3d 2802 . . . . . . . . . . 11 (𝜑 → (1 − (1 + 𝑇)) = -𝑇)
4342fveq2d 6357 . . . . . . . . . 10 (𝜑 → (abs‘(1 − (1 + 𝑇))) = (abs‘-𝑇))
4414absnegd 14407 . . . . . . . . . . 11 (𝜑 → (abs‘-𝑇) = (abs‘𝑇))
45 stirlinglem5.7 . . . . . . . . . . 11 (𝜑 → (abs‘𝑇) < 1)
4644, 45eqbrtrd 4826 . . . . . . . . . 10 (𝜑 → (abs‘-𝑇) < 1)
4743, 46eqbrtrd 4826 . . . . . . . . 9 (𝜑 → (abs‘(1 − (1 + 𝑇))) < 1)
4834, 47eqbrtrd 4826 . . . . . . . 8 (𝜑 → (1(abs ∘ − )(1 + 𝑇)) < 1)
49 cnxmet 22797 . . . . . . . . . 10 (abs ∘ − ) ∈ (∞Met‘ℂ)
5049a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51 1red 10267 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
5251rexrd 10301 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ*)
53 elbl2 22416 . . . . . . . . 9 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ)) → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1))
5450, 52, 30, 31, 53syl22anc 1478 . . . . . . . 8 (𝜑 → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1))
5548, 54mpbird 247 . . . . . . 7 (𝜑 → (1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1))
56 eqid 2760 . . . . . . . 8 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
5756logtayl2 24628 . . . . . . 7 ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) → seq1( + , (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) ⇝ (log‘(1 + 𝑇)))
5855, 57syl 17 . . . . . 6 (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) ⇝ (log‘(1 + 𝑇)))
5929, 58eqbrtrd 4826 . . . . 5 (𝜑 → seq1( + , 𝐷) ⇝ (log‘(1 + 𝑇)))
60 seqex 13017 . . . . . 6 seq1( + , 𝐹) ∈ V
6160a1i 11 . . . . 5 (𝜑 → seq1( + , 𝐹) ∈ V)
62 stirlinglem5.2 . . . . . . . 8 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))
6362a1i 11 . . . . . . 7 (𝜑𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗)))
6463seqeq3d 13023 . . . . . 6 (𝜑 → seq1( + , 𝐸) = seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))))
65 logtayl 24626 . . . . . . 7 ((𝑇 ∈ ℂ ∧ (abs‘𝑇) < 1) → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇)))
6614, 45, 65syl2anc 696 . . . . . 6 (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇)))
6764, 66eqbrtrd 4826 . . . . 5 (𝜑 → seq1( + , 𝐸) ⇝ -(log‘(1 − 𝑇)))
68 simpr 479 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
6968, 1syl6eleq 2849 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
703a1i 11 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))))
71 oveq1 6821 . . . . . . . . . . 11 (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1))
7271oveq2d 6830 . . . . . . . . . 10 (𝑗 = 𝑛 → (-1↑(𝑗 − 1)) = (-1↑(𝑛 − 1)))
73 oveq2 6822 . . . . . . . . . . 11 (𝑗 = 𝑛 → (𝑇𝑗) = (𝑇𝑛))
74 id 22 . . . . . . . . . . 11 (𝑗 = 𝑛𝑗 = 𝑛)
7573, 74oveq12d 6832 . . . . . . . . . 10 (𝑗 = 𝑛 → ((𝑇𝑗) / 𝑗) = ((𝑇𝑛) / 𝑛))
7672, 75oveq12d 6832 . . . . . . . . 9 (𝑗 = 𝑛 → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
7776adantl 473 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) ∧ 𝑗 = 𝑛) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
78 elfznn 12583 . . . . . . . . 9 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
7978adantl 473 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ)
80 1cnd 10268 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 1 ∈ ℂ)
8180negcld 10591 . . . . . . . . . . 11 (𝑛 ∈ ℕ → -1 ∈ ℂ)
82 nnm1nn0 11546 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
8381, 82expcld 13222 . . . . . . . . . 10 (𝑛 ∈ ℕ → (-1↑(𝑛 − 1)) ∈ ℂ)
8479, 83syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (-1↑(𝑛 − 1)) ∈ ℂ)
8514ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑇 ∈ ℂ)
8679nnnn0d 11563 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ0)
8785, 86expcld 13222 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑇𝑛) ∈ ℂ)
8879nncnd 11248 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℂ)
8979nnne0d 11277 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ≠ 0)
9087, 88, 89divcld 11013 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
9184, 90mulcld 10272 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
9270, 77, 79, 91fvmptd 6451 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
9392, 91eqeltrd 2839 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷𝑛) ∈ ℂ)
94 addcl 10230 . . . . . . 7 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
9594adantl 473 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
9669, 93, 95seqcl 13035 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐷)‘𝑘) ∈ ℂ)
9762a1i 11 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗)))
9875adantl 473 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) ∧ 𝑗 = 𝑛) → ((𝑇𝑗) / 𝑗) = ((𝑇𝑛) / 𝑛))
9997, 98, 79, 90fvmptd 6451 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸𝑛) = ((𝑇𝑛) / 𝑛))
10099, 90eqeltrd 2839 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸𝑛) ∈ ℂ)
10169, 100, 95seqcl 13035 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐸)‘𝑘) ∈ ℂ)
102 simpll 807 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑)
103 stirlinglem5.3 . . . . . . . . . 10 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)))
104103a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗))))
10576, 75oveq12d 6832 . . . . . . . . . 10 (𝑗 = 𝑛 → (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
106105adantl 473 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 = 𝑛) → (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
107 simpr 479 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
10883adantl 473 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈ ℂ)
10914adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑇 ∈ ℂ)
110107nnnn0d 11563 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
111109, 110expcld 13222 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑇𝑛) ∈ ℂ)
112107nncnd 11248 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
113107nnne0d 11277 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ≠ 0)
114111, 112, 113divcld 11013 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
115108, 114mulcld 10272 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
116115, 114addcld 10271 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ)
117104, 106, 107, 116fvmptd 6451 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
1183a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))))
11976adantl 473 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 = 𝑛) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
120118, 119, 107, 115fvmptd 6451 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐷𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
121120eqcomd 2766 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) = (𝐷𝑛))
12262a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗)))
12375adantl 473 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑗 = 𝑛) → ((𝑇𝑗) / 𝑗) = ((𝑇𝑛) / 𝑛))
124122, 123, 107, 114fvmptd 6451 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐸𝑛) = ((𝑇𝑛) / 𝑛))
125124eqcomd 2766 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑛) / 𝑛) = (𝐸𝑛))
126121, 125oveq12d 6832 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = ((𝐷𝑛) + (𝐸𝑛)))
127117, 126eqtrd 2794 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ((𝐷𝑛) + (𝐸𝑛)))
128102, 79, 127syl2anc 696 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐹𝑛) = ((𝐷𝑛) + (𝐸𝑛)))
12969, 93, 100, 128seradd 13057 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = ((seq1( + , 𝐷)‘𝑘) + (seq1( + , 𝐸)‘𝑘)))
1301, 2, 59, 61, 67, 96, 101, 129climadd 14581 . . . 4 (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) + -(log‘(1 − 𝑇))))
131 1rp 12049 . . . . . . . . 9 1 ∈ ℝ+
132131a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
133132, 12rpaddcld 12100 . . . . . . 7 (𝜑 → (1 + 𝑇) ∈ ℝ+)
134133rpne0d 12090 . . . . . 6 (𝜑 → (1 + 𝑇) ≠ 0)
13531, 134logcld 24537 . . . . 5 (𝜑 → (log‘(1 + 𝑇)) ∈ ℂ)
13630, 14subcld 10604 . . . . . 6 (𝜑 → (1 − 𝑇) ∈ ℂ)
13713, 51absltd 14387 . . . . . . . . . 10 (𝜑 → ((abs‘𝑇) < 1 ↔ (-1 < 𝑇𝑇 < 1)))
13845, 137mpbid 222 . . . . . . . . 9 (𝜑 → (-1 < 𝑇𝑇 < 1))
139138simprd 482 . . . . . . . 8 (𝜑𝑇 < 1)
14013, 139gtned 10384 . . . . . . 7 (𝜑 → 1 ≠ 𝑇)
14130, 14, 140subne0d 10613 . . . . . 6 (𝜑 → (1 − 𝑇) ≠ 0)
142136, 141logcld 24537 . . . . 5 (𝜑 → (log‘(1 − 𝑇)) ∈ ℂ)
143135, 142negsubd 10610 . . . 4 (𝜑 → ((log‘(1 + 𝑇)) + -(log‘(1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
144130, 143breqtrd 4830 . . 3 (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
145 nn0uz 11935 . . . 4 0 = (ℤ‘0)
146 0zd 11601 . . . 4 (𝜑 → 0 ∈ ℤ)
147 stirlinglem5.5 . . . . . 6 𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))
148 2nn0 11521 . . . . . . . . 9 2 ∈ ℕ0
149148a1i 11 . . . . . . . 8 (𝑗 ∈ ℕ0 → 2 ∈ ℕ0)
150 id 22 . . . . . . . 8 (𝑗 ∈ ℕ0𝑗 ∈ ℕ0)
151149, 150nn0mulcld 11568 . . . . . . 7 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℕ0)
152 nn0p1nn 11544 . . . . . . 7 ((2 · 𝑗) ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ)
153151, 152syl 17 . . . . . 6 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ)
154147, 153fmpti 6547 . . . . 5 𝐺:ℕ0⟶ℕ
155154a1i 11 . . . 4 (𝜑𝐺:ℕ0⟶ℕ)
156 2re 11302 . . . . . . . . 9 2 ∈ ℝ
157156a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℝ)
158 nn0re 11513 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
159157, 158remulcld 10282 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℝ)
160 1red 10267 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 1 ∈ ℝ)
161158, 160readdcld 10281 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℝ)
162157, 161remulcld 10282 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · (𝑘 + 1)) ∈ ℝ)
163 2rp 12050 . . . . . . . . 9 2 ∈ ℝ+
164163a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℝ+)
165158ltp1d 11166 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 < (𝑘 + 1))
166158, 161, 164, 165ltmul2dd 12141 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · 𝑘) < (2 · (𝑘 + 1)))
167159, 162, 160, 166ltadd1dd 10850 . . . . . 6 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) < ((2 · (𝑘 + 1)) + 1))
168147a1i 11 . . . . . . 7 (𝑘 ∈ ℕ0𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1)))
169 simpr 479 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → 𝑗 = 𝑘)
170169oveq2d 6830 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘))
171170oveq1d 6829 . . . . . . 7 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1))
172 id 22 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
173 2cnd 11305 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 2 ∈ ℂ)
174 nn0cn 11514 . . . . . . . . 9 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
175173, 174mulcld 10272 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℂ)
176 1cnd 10268 . . . . . . . 8 (𝑘 ∈ ℕ0 → 1 ∈ ℂ)
177175, 176addcld 10271 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℂ)
178168, 171, 172, 177fvmptd 6451 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐺𝑘) = ((2 · 𝑘) + 1))
179 simpr 479 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → 𝑗 = (𝑘 + 1))
180179oveq2d 6830 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → (2 · 𝑗) = (2 · (𝑘 + 1)))
181180oveq1d 6829 . . . . . . 7 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1))
182 peano2nn0 11545 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
183174, 176addcld 10271 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℂ)
184173, 183mulcld 10272 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2 · (𝑘 + 1)) ∈ ℂ)
185184, 176addcld 10271 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 · (𝑘 + 1)) + 1) ∈ ℂ)
186168, 181, 182, 185fvmptd 6451 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐺‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) + 1))
187167, 178, 1863brtr4d 4836 . . . . 5 (𝑘 ∈ ℕ0 → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
188187adantl 473 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
189 eldifi 3875 . . . . . . 7 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℕ)
190189adantl 473 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ)
191 1cnd 10268 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 1 ∈ ℂ)
192191negcld 10591 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → -1 ∈ ℂ)
193189, 82syl 17 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℕ0)
194192, 193expcld 13222 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) ∈ ℂ)
195194adantl 473 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) ∈ ℂ)
19614adantr 472 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑇 ∈ ℂ)
197190nnnn0d 11563 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ0)
198196, 197expcld 13222 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝑇𝑛) ∈ ℂ)
199190nncnd 11248 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℂ)
200190nnne0d 11277 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ≠ 0)
201198, 199, 200divcld 11013 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
202195, 201mulcld 10272 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
203202, 201addcld 10271 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ)
204105, 103fvmptg 6443 . . . . . 6 ((𝑛 ∈ ℕ ∧ (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
205190, 203, 204syl2anc 696 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
206 eldifn 3876 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 𝑛 ∈ ran 𝐺)
207 0nn0 11519 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
208 1nn0 11520 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
209148, 208num0h 11721 . . . . . . . . . . . . . . . 16 1 = ((2 · 0) + 1)
210 oveq2 6822 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 0 → (2 · 𝑗) = (2 · 0))
211210oveq1d 6829 . . . . . . . . . . . . . . . . . 18 (𝑗 = 0 → ((2 · 𝑗) + 1) = ((2 · 0) + 1))
212211eqeq2d 2770 . . . . . . . . . . . . . . . . 17 (𝑗 = 0 → (1 = ((2 · 𝑗) + 1) ↔ 1 = ((2 · 0) + 1)))
213212rspcev 3449 . . . . . . . . . . . . . . . 16 ((0 ∈ ℕ0 ∧ 1 = ((2 · 0) + 1)) → ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1))
214207, 209, 213mp2an 710 . . . . . . . . . . . . . . 15 𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1)
215 ax-1cn 10206 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
216147elrnmpt 5527 . . . . . . . . . . . . . . . 16 (1 ∈ ℂ → (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1)))
217215, 216ax-mp 5 . . . . . . . . . . . . . . 15 (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1))
218214, 217mpbir 221 . . . . . . . . . . . . . 14 1 ∈ ran 𝐺
219218a1i 11 . . . . . . . . . . . . 13 (𝑛 = 1 → 1 ∈ ran 𝐺)
220 eleq1 2827 . . . . . . . . . . . . 13 (𝑛 = 1 → (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺))
221219, 220mpbird 247 . . . . . . . . . . . 12 (𝑛 = 1 → 𝑛 ∈ ran 𝐺)
222206, 221nsyl 135 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 𝑛 = 1)
223 nn1m1nn 11252 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ))
224189, 223syl 17 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ))
225224ord 391 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 𝑛 = 1 → (𝑛 − 1) ∈ ℕ))
226222, 225mpd 15 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℕ)
227 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑗
228 nfmpt1 4899 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))
229147, 228nfcxfr 2900 . . . . . . . . . . . . . . . . . . 19 𝑗𝐺
230229nfrn 5523 . . . . . . . . . . . . . . . . . 18 𝑗ran 𝐺
231227, 230nfdif 3874 . . . . . . . . . . . . . . . . 17 𝑗(ℕ ∖ ran 𝐺)
232231nfcri 2896 . . . . . . . . . . . . . . . 16 𝑗 𝑛 ∈ (ℕ ∖ ran 𝐺)
233147elrnmpt 5527 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1)))
234206, 233mtbid 313 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))
235 ralnex 3130 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑗 ∈ ℕ0 ¬ 𝑛 = ((2 · 𝑗) + 1) ↔ ¬ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))
236234, 235sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ∀𝑗 ∈ ℕ0 ¬ 𝑛 = ((2 · 𝑗) + 1))
237236r19.21bi 3070 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → ¬ 𝑛 = ((2 · 𝑗) + 1))
238237neqned 2939 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → 𝑛 ≠ ((2 · 𝑗) + 1))
239238necomd 2987 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
240239adantlr 753 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
241 simplr 809 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
242 simpr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 𝑗 ∈ ℕ0)
243189ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → 𝑛 ∈ ℕ)
244156a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℝ)
245 simpl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
246245zred 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℝ)
247244, 246remulcld 10282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℝ)
248 0red 10253 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 0 ∈ ℝ)
249 1red 10267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 1 ∈ ℝ)
250 2cnd 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
251246recnd 10280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℂ)
252250, 251mulcomd 10273 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) = (𝑗 · 2))
253 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 𝑗 ∈ ℕ0)
254 elnn0z 11602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
255253, 254sylnib 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
256 nan 605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) ↔ (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗))
257255, 256mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗)
258257anabss1 890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 0 ≤ 𝑗)
259246, 248ltnled 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (𝑗 < 0 ↔ ¬ 0 ≤ 𝑗))
260258, 259mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 < 0)
261163a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℝ+)
262261rpregt0d 12091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 ∈ ℝ ∧ 0 < 2))
263 mulltgt0 39698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑗 · 2) < 0)
264246, 260, 262, 263syl21anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (𝑗 · 2) < 0)
265252, 264eqbrtrd 4826 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) < 0)
266247, 248, 249, 265ltadd1dd 10850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) < (0 + 1))
267 1cnd 10268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
268267addid2d 10449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (0 + 1) = 1)
269266, 268breqtrd 4830 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) < 1)
270247, 249readdcld 10281 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℝ)
271270, 249ltnled 10396 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (((2 · 𝑗) + 1) < 1 ↔ ¬ 1 ≤ ((2 · 𝑗) + 1)))
272269, 271mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 1 ≤ ((2 · 𝑗) + 1))
273 nnge1 11258 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑗) + 1) ∈ ℕ → 1 ≤ ((2 · 𝑗) + 1))
274272, 273nsyl 135 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ ((2 · 𝑗) + 1) ∈ ℕ)
275274adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 · 𝑗) + 1) ∈ ℕ)
276 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) = 𝑛)
277 simpl 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → 𝑛 ∈ ℕ)
278276, 277eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ)
279278adantll 752 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ)
280275, 279mtand 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 · 𝑗) + 1) = 𝑛)
281280neqned 2939 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ((2 · 𝑗) + 1) ≠ 𝑛)
282241, 242, 243, 281syl21anc 1476 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
283240, 282pm2.61dan 867 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) → ((2 · 𝑗) + 1) ≠ 𝑛)
284283neneqd 2937 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) → ¬ ((2 · 𝑗) + 1) = 𝑛)
285284ex 449 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑗 ∈ ℤ → ¬ ((2 · 𝑗) + 1) = 𝑛))
286232, 285ralrimi 3095 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ∀𝑗 ∈ ℤ ¬ ((2 · 𝑗) + 1) = 𝑛)
287 ralnex 3130 . . . . . . . . . . . . . . 15 (∀𝑗 ∈ ℤ ¬ ((2 · 𝑗) + 1) = 𝑛 ↔ ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛)
288286, 287sylib 208 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛)
289189nnzd 11693 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℤ)
290 odd2np1 15287 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℤ → (¬ 2 ∥ 𝑛 ↔ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛))
291289, 290syl 17 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 2 ∥ 𝑛 ↔ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛))
292288, 291mtbird 314 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ¬ 2 ∥ 𝑛)
293292notnotrd 128 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 2 ∥ 𝑛)
294189nncnd 11248 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℂ)
295294, 191npcand 10608 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ((𝑛 − 1) + 1) = 𝑛)
296293, 295breqtrrd 4832 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 2 ∥ ((𝑛 − 1) + 1))
297193nn0zd 11692 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℤ)
298 oddp1even 15290 . . . . . . . . . . . 12 ((𝑛 − 1) ∈ ℤ → (¬ 2 ∥ (𝑛 − 1) ↔ 2 ∥ ((𝑛 − 1) + 1)))
299297, 298syl 17 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 2 ∥ (𝑛 − 1) ↔ 2 ∥ ((𝑛 − 1) + 1)))
300296, 299mpbird 247 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 2 ∥ (𝑛 − 1))
301 oexpneg 15291 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ ∧ ¬ 2 ∥ (𝑛 − 1)) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1)))
302191, 226, 300, 301syl3anc 1477 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1)))
303 1exp 13103 . . . . . . . . . . 11 ((𝑛 − 1) ∈ ℤ → (1↑(𝑛 − 1)) = 1)
304297, 303syl 17 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (1↑(𝑛 − 1)) = 1)
305304negeqd 10487 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → -(1↑(𝑛 − 1)) = -1)
306302, 305eqtrd 2794 . . . . . . . 8 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) = -1)
307306adantl 473 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) = -1)
308307oveq1d 6829 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) = (-1 · ((𝑇𝑛) / 𝑛)))
309308oveq1d 6829 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
310201mulm1d 10694 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1 · ((𝑇𝑛) / 𝑛)) = -((𝑇𝑛) / 𝑛))
311310oveq1d 6829 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = (-((𝑇𝑛) / 𝑛) + ((𝑇𝑛) / 𝑛)))
312201negcld 10591 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → -((𝑇𝑛) / 𝑛) ∈ ℂ)
313312, 201addcomd 10450 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-((𝑇𝑛) / 𝑛) + ((𝑇𝑛) / 𝑛)) = (((𝑇𝑛) / 𝑛) + -((𝑇𝑛) / 𝑛)))
314201negidd 10594 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((𝑇𝑛) / 𝑛) + -((𝑇𝑛) / 𝑛)) = 0)
315311, 313, 3143eqtrd 2798 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = 0)
316205, 309, 3153eqtrd 2798 . . . 4 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹𝑛) = 0)
317117, 116eqeltrd 2839 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ℂ)
318103a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗))))
319 simpr 479 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → 𝑗 = ((2 · 𝑘) + 1))
320319oveq1d 6829 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑗 − 1) = (((2 · 𝑘) + 1) − 1))
321320oveq2d 6830 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (-1↑(𝑗 − 1)) = (-1↑(((2 · 𝑘) + 1) − 1)))
322319oveq2d 6830 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑇𝑗) = (𝑇↑((2 · 𝑘) + 1)))
323322, 319oveq12d 6832 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((𝑇𝑗) / 𝑗) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
324321, 323oveq12d 6832 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
325324, 323oveq12d 6832 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)) = (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
326148a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℕ0)
327 simpr 479 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
328326, 327nn0mulcld 11568 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
329 nn0p1nn 11544 . . . . . . . 8 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
330328, 329syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ)
331176negcld 10591 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → -1 ∈ ℂ)
332175, 176pncand 10605 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
333148a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → 2 ∈ ℕ0)
334333, 172nn0mulcld 11568 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℕ0)
335332, 334eqeltrd 2839 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) − 1) ∈ ℕ0)
336331, 335expcld 13222 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (-1↑(((2 · 𝑘) + 1) − 1)) ∈ ℂ)
337336adantl 473 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) ∈ ℂ)
33814adantr 472 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 𝑇 ∈ ℂ)
339208a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
340328, 339nn0addcld 11567 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ0)
341338, 340expcld 13222 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (𝑇↑((2 · 𝑘) + 1)) ∈ ℂ)
342 2cnd 11305 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℂ)
343174adantl 473 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
344342, 343mulcld 10272 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℂ)
345 1cnd 10268 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℂ)
346344, 345addcld 10271 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℂ)
347 0red 10253 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 0 ∈ ℝ)
348156a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℝ)
349158adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℝ)
350348, 349remulcld 10282 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℝ)
351 1red 10267 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℝ)
352 0le2 11323 . . . . . . . . . . . . . 14 0 ≤ 2
353352a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ 2)
354327nn0ge0d 11566 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ 𝑘)
355348, 349, 353, 354mulge0d 10816 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ (2 · 𝑘))
356 0lt1 10762 . . . . . . . . . . . . 13 0 < 1
357356a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 0 < 1)
358350, 351, 355, 357addgegt0d 10813 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 0 < ((2 · 𝑘) + 1))
359347, 358gtned 10384 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ≠ 0)
360341, 346, 359divcld 11013 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) ∈ ℂ)
361337, 360mulcld 10272 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ)
362361, 360addcld 10271 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ)
363318, 325, 330, 362fvmptd 6451 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘((2 · 𝑘) + 1)) = (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
364332adantl 473 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
365364oveq2d 6830 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) = (-1↑(2 · 𝑘)))
366 nn0z 11612 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
367 m1expeven 13121 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → (-1↑(2 · 𝑘)) = 1)
368366, 367syl 17 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (-1↑(2 · 𝑘)) = 1)
369368adantl 473 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (-1↑(2 · 𝑘)) = 1)
370365, 369eqtrd 2794 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) = 1)
371370oveq1d 6829 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
372360mulid2d 10270 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
373371, 372eqtrd 2794 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
374373oveq1d 6829 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
3753602timesd 11487 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (2 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
376341, 346, 359divrec2d 11017 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))
377376oveq2d 6830 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (2 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
378374, 375, 3773eqtr2d 2800 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
379363, 378eqtr2d 2795 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) = (𝐹‘((2 · 𝑘) + 1)))
380 stirlinglem5.4 . . . . . . 7 𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))))
381380a1i 11 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → 𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))))))
382 simpr 479 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
383382oveq2d 6830 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘))
384383oveq1d 6829 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1))
385384oveq2d 6830 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (1 / ((2 · 𝑗) + 1)) = (1 / ((2 · 𝑘) + 1)))
386384oveq2d 6830 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝑇↑((2 · 𝑗) + 1)) = (𝑇↑((2 · 𝑘) + 1)))
387385, 386oveq12d 6832 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))) = ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))
388387oveq2d 6830 . . . . . 6 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
389346, 359reccld 11006 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
390389, 341mulcld 10272 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))) ∈ ℂ)
391342, 390mulcld 10272 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) ∈ ℂ)
392381, 388, 327, 391fvmptd 6451 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
393208a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 1 ∈ ℕ0)
394334, 393nn0addcld 11567 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ0)
395168, 171, 172, 394fvmptd 6451 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝐺𝑘) = ((2 · 𝑘) + 1))
396395adantl 473 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = ((2 · 𝑘) + 1))
397396fveq2d 6357 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝐺𝑘)) = (𝐹‘((2 · 𝑘) + 1)))
398379, 392, 3973eqtr4d 2804 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
399145, 1, 146, 2, 155, 188, 316, 317, 398isercoll2 14618 . . 3 (𝜑 → (seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))) ↔ seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇)))))
400144, 399mpbird 247 . 2 (𝜑 → seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
40151, 13resubcld 10670 . . . 4 (𝜑 → (1 − 𝑇) ∈ ℝ)
40214subidd 10592 . . . . . 6 (𝜑 → (𝑇𝑇) = 0)
403402eqcomd 2766 . . . . 5 (𝜑 → 0 = (𝑇𝑇))
40413, 51, 13, 139ltsub1dd 10851 . . . . 5 (𝜑 → (𝑇𝑇) < (1 − 𝑇))
405403, 404eqbrtrd 4826 . . . 4 (𝜑 → 0 < (1 − 𝑇))
406401, 405elrpd 12082 . . 3 (𝜑 → (1 − 𝑇) ∈ ℝ+)
407133, 406relogdivd 24592 . 2 (𝜑 → (log‘((1 + 𝑇) / (1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
408400, 407breqtrrd 4832 1 (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  cdif 3712   class class class wbr 4804  cmpt 4881  ran crn 5267  ccom 5270  wf 6045  cfv 6049  (class class class)co 6814  cc 10146  cr 10147  0cc0 10148  1c1 10149   + caddc 10151   · cmul 10153  *cxr 10285   < clt 10286  cle 10287  cmin 10478  -cneg 10479   / cdiv 10896  cn 11232  2c2 11282  0cn0 11504  cz 11589  cuz 11899  +crp 12045  ...cfz 12539  seqcseq 13015  cexp 13074  abscabs 14193  cli 14434  cdvds 15202  ∞Metcxmt 19953  ballcbl 19955  logclog 24521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227  ax-mulf 10228
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-of 7063  df-om 7232  df-1st 7334  df-2nd 7335  df-supp 7465  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-ixp 8077  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fsupp 8443  df-fi 8484  df-sup 8515  df-inf 8516  df-oi 8582  df-card 8975  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-xnn0 11576  df-z 11590  df-dec 11706  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-ioo 12392  df-ioc 12393  df-ico 12394  df-icc 12395  df-fz 12540  df-fzo 12680  df-fl 12807  df-mod 12883  df-seq 13016  df-exp 13075  df-fac 13275  df-bc 13304  df-hash 13332  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-ef 15017  df-sin 15019  df-cos 15020  df-tan 15021  df-pi 15022  df-dvds 15203  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-ress 16087  df-plusg 16176  df-mulr 16177  df-starv 16178  df-sca 16179  df-vsca 16180  df-ip 16181  df-tset 16182  df-ple 16183  df-ds 16186  df-unif 16187  df-hom 16188  df-cco 16189  df-rest 16305  df-topn 16306  df-0g 16324  df-gsum 16325  df-topgen 16326  df-pt 16327  df-prds 16330  df-xrs 16384  df-qtop 16389  df-imas 16390  df-xps 16392  df-mre 16468  df-mrc 16469  df-acs 16471  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-submnd 17557  df-mulg 17762  df-cntz 17970  df-cmn 18415  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-fbas 19965  df-fg 19966  df-cnfld 19969  df-top 20921  df-topon 20938  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cn 21253  df-cnp 21254  df-haus 21341  df-cmp 21412  df-tx 21587  df-hmeo 21780  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-xms 22346  df-ms 22347  df-tms 22348  df-cncf 22902  df-limc 23849  df-dv 23850  df-ulm 24350  df-log 24523
This theorem is referenced by:  stirlinglem6  40817
  Copyright terms: Public domain W3C validator