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 43869
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 12701 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 12431 . . . . 5 (𝜑 → 1 ∈ ℤ)
3 stirlinglem5.1 . . . . . . . . 9 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)))
43a1i 11 . . . . . . . 8 (𝜑𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))))
5 1cnd 11050 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℂ)
65negcld 11399 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → -1 ∈ ℂ)
7 nnm1nn0 12354 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
87adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℕ0)
96, 8expcld 13944 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (-1↑(𝑗 − 1)) ∈ ℂ)
10 nncn 12061 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
1110adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℂ)
12 stirlinglem5.6 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℝ+)
1312rpred 12852 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ ℝ)
1413recnd 11083 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℂ)
1514adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
16 nnnn0 12320 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
1716adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
1815, 17expcld 13944 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℂ)
19 nnne0 12087 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ≠ 0)
2019adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ≠ 0)
219, 11, 18, 20div32d 11854 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇𝑗)) = ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)))
225, 15pncan2d 11414 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((1 + 𝑇) − 1) = 𝑇)
2322eqcomd 2743 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑇 = ((1 + 𝑇) − 1))
2423oveq1d 7332 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (((1 + 𝑇) − 1)↑𝑗))
2524oveq2d 7333 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))
2621, 25eqtr3d 2779 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))
2726mpteq2dva 5187 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))))
284, 27eqtrd 2777 . . . . . . 7 (𝜑𝐷 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))))
2928seqeq3d 13809 . . . . . 6 (𝜑 → seq1( + , 𝐷) = seq1( + , (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))))
30 1cnd 11050 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
3130, 14addcld 11074 . . . . . . . . . 10 (𝜑 → (1 + 𝑇) ∈ ℂ)
32 eqid 2737 . . . . . . . . . . 11 (abs ∘ − ) = (abs ∘ − )
3332cnmetdval 24017 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ) → (1(abs ∘ − )(1 + 𝑇)) = (abs‘(1 − (1 + 𝑇))))
3430, 31, 33syl2anc 584 . . . . . . . . 9 (𝜑 → (1(abs ∘ − )(1 + 𝑇)) = (abs‘(1 − (1 + 𝑇))))
35 1m1e0 12125 . . . . . . . . . . . . . 14 (1 − 1) = 0
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 − 1) = 0)
3736oveq1d 7332 . . . . . . . . . . . 12 (𝜑 → ((1 − 1) − 𝑇) = (0 − 𝑇))
3830, 30, 14subsub4d 11443 . . . . . . . . . . . 12 (𝜑 → ((1 − 1) − 𝑇) = (1 − (1 + 𝑇)))
39 df-neg 11288 . . . . . . . . . . . . . 14 -𝑇 = (0 − 𝑇)
4039eqcomi 2746 . . . . . . . . . . . . 13 (0 − 𝑇) = -𝑇
4140a1i 11 . . . . . . . . . . . 12 (𝜑 → (0 − 𝑇) = -𝑇)
4237, 38, 413eqtr3d 2785 . . . . . . . . . . 11 (𝜑 → (1 − (1 + 𝑇)) = -𝑇)
4342fveq2d 6816 . . . . . . . . . 10 (𝜑 → (abs‘(1 − (1 + 𝑇))) = (abs‘-𝑇))
4414absnegd 15240 . . . . . . . . . . 11 (𝜑 → (abs‘-𝑇) = (abs‘𝑇))
45 stirlinglem5.7 . . . . . . . . . . 11 (𝜑 → (abs‘𝑇) < 1)
4644, 45eqbrtrd 5109 . . . . . . . . . 10 (𝜑 → (abs‘-𝑇) < 1)
4743, 46eqbrtrd 5109 . . . . . . . . 9 (𝜑 → (abs‘(1 − (1 + 𝑇))) < 1)
4834, 47eqbrtrd 5109 . . . . . . . 8 (𝜑 → (1(abs ∘ − )(1 + 𝑇)) < 1)
49 cnxmet 24019 . . . . . . . . . 10 (abs ∘ − ) ∈ (∞Met‘ℂ)
5049a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51 1red 11056 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
5251rexrd 11105 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ*)
53 elbl2 23626 . . . . . . . . 9 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ)) → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1))
5450, 52, 30, 31, 53syl22anc 836 . . . . . . . 8 (𝜑 → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1))
5548, 54mpbird 256 . . . . . . 7 (𝜑 → (1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1))
56 eqid 2737 . . . . . . . 8 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
5756logtayl2 25900 . . . . . . 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 5109 . . . . 5 (𝜑 → seq1( + , 𝐷) ⇝ (log‘(1 + 𝑇)))
60 seqex 13803 . . . . . 6 seq1( + , 𝐹) ∈ V
6160a1i 11 . . . . 5 (𝜑 → seq1( + , 𝐹) ∈ V)
62 stirlinglem5.2 . . . . . . . 8 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))
6362a1i 11 . . . . . . 7 (𝜑𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗)))
6463seqeq3d 13809 . . . . . 6 (𝜑 → seq1( + , 𝐸) = seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))))
65 logtayl 25898 . . . . . . 7 ((𝑇 ∈ ℂ ∧ (abs‘𝑇) < 1) → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇)))
6614, 45, 65syl2anc 584 . . . . . 6 (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇)))
6764, 66eqbrtrd 5109 . . . . 5 (𝜑 → seq1( + , 𝐸) ⇝ -(log‘(1 − 𝑇)))
68 simpr 485 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
6968, 1eleqtrdi 2848 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
70 oveq1 7324 . . . . . . . . . 10 (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1))
7170oveq2d 7333 . . . . . . . . 9 (𝑗 = 𝑛 → (-1↑(𝑗 − 1)) = (-1↑(𝑛 − 1)))
72 oveq2 7325 . . . . . . . . . 10 (𝑗 = 𝑛 → (𝑇𝑗) = (𝑇𝑛))
73 id 22 . . . . . . . . . 10 (𝑗 = 𝑛𝑗 = 𝑛)
7472, 73oveq12d 7335 . . . . . . . . 9 (𝑗 = 𝑛 → ((𝑇𝑗) / 𝑗) = ((𝑇𝑛) / 𝑛))
7571, 74oveq12d 7335 . . . . . . . 8 (𝑗 = 𝑛 → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
76 elfznn 13365 . . . . . . . . 9 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
7776adantl 482 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ)
78 1cnd 11050 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 1 ∈ ℂ)
7978negcld 11399 . . . . . . . . . . 11 (𝑛 ∈ ℕ → -1 ∈ ℂ)
80 nnm1nn0 12354 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
8179, 80expcld 13944 . . . . . . . . . 10 (𝑛 ∈ ℕ → (-1↑(𝑛 − 1)) ∈ ℂ)
8277, 81syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (-1↑(𝑛 − 1)) ∈ ℂ)
8314ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑇 ∈ ℂ)
8477nnnn0d 12373 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ0)
8583, 84expcld 13944 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑇𝑛) ∈ ℂ)
8677nncnd 12069 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℂ)
8777nnne0d 12103 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ≠ 0)
8885, 86, 87divcld 11831 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
8982, 88mulcld 11075 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
903, 75, 77, 89fvmptd3 6938 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
9190, 89eqeltrd 2838 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷𝑛) ∈ ℂ)
92 addcl 11033 . . . . . . 7 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
9392adantl 482 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
9469, 91, 93seqcl 13823 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐷)‘𝑘) ∈ ℂ)
9562, 74, 77, 88fvmptd3 6938 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸𝑛) = ((𝑇𝑛) / 𝑛))
9695, 88eqeltrd 2838 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸𝑛) ∈ ℂ)
9769, 96, 93seqcl 13823 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐸)‘𝑘) ∈ ℂ)
98 simpll 764 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑)
99 stirlinglem5.3 . . . . . . . . 9 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)))
10075, 74oveq12d 7335 . . . . . . . . 9 (𝑗 = 𝑛 → (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
101 simpr 485 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
10281adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈ ℂ)
10314adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑇 ∈ ℂ)
104101nnnn0d 12373 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
105103, 104expcld 13944 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑇𝑛) ∈ ℂ)
106101nncnd 12069 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
107101nnne0d 12103 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ≠ 0)
108105, 106, 107divcld 11831 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
109102, 108mulcld 11075 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
110109, 108addcld 11074 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ)
11199, 100, 101, 110fvmptd3 6938 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
1123, 75, 101, 109fvmptd3 6938 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐷𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
113112eqcomd 2743 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) = (𝐷𝑛))
11462, 74, 101, 108fvmptd3 6938 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐸𝑛) = ((𝑇𝑛) / 𝑛))
115114eqcomd 2743 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑛) / 𝑛) = (𝐸𝑛))
116113, 115oveq12d 7335 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = ((𝐷𝑛) + (𝐸𝑛)))
117111, 116eqtrd 2777 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ((𝐷𝑛) + (𝐸𝑛)))
11898, 77, 117syl2anc 584 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐹𝑛) = ((𝐷𝑛) + (𝐸𝑛)))
11969, 91, 96, 118seradd 13845 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = ((seq1( + , 𝐷)‘𝑘) + (seq1( + , 𝐸)‘𝑘)))
1201, 2, 59, 61, 67, 94, 97, 119climadd 15420 . . . 4 (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) + -(log‘(1 − 𝑇))))
121 1rp 12814 . . . . . . . . 9 1 ∈ ℝ+
122121a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
123122, 12rpaddcld 12867 . . . . . . 7 (𝜑 → (1 + 𝑇) ∈ ℝ+)
124123rpne0d 12857 . . . . . 6 (𝜑 → (1 + 𝑇) ≠ 0)
12531, 124logcld 25809 . . . . 5 (𝜑 → (log‘(1 + 𝑇)) ∈ ℂ)
12630, 14subcld 11412 . . . . . 6 (𝜑 → (1 − 𝑇) ∈ ℂ)
12713, 51absltd 15220 . . . . . . . . . 10 (𝜑 → ((abs‘𝑇) < 1 ↔ (-1 < 𝑇𝑇 < 1)))
12845, 127mpbid 231 . . . . . . . . 9 (𝜑 → (-1 < 𝑇𝑇 < 1))
129128simprd 496 . . . . . . . 8 (𝜑𝑇 < 1)
13013, 129gtned 11190 . . . . . . 7 (𝜑 → 1 ≠ 𝑇)
13130, 14, 130subne0d 11421 . . . . . 6 (𝜑 → (1 − 𝑇) ≠ 0)
132126, 131logcld 25809 . . . . 5 (𝜑 → (log‘(1 − 𝑇)) ∈ ℂ)
133125, 132negsubd 11418 . . . 4 (𝜑 → ((log‘(1 + 𝑇)) + -(log‘(1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
134120, 133breqtrd 5113 . . 3 (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
135 nn0uz 12700 . . . 4 0 = (ℤ‘0)
136 0zd 12411 . . . 4 (𝜑 → 0 ∈ ℤ)
137 stirlinglem5.5 . . . . . 6 𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))
138 2nn0 12330 . . . . . . . . 9 2 ∈ ℕ0
139138a1i 11 . . . . . . . 8 (𝑗 ∈ ℕ0 → 2 ∈ ℕ0)
140 id 22 . . . . . . . 8 (𝑗 ∈ ℕ0𝑗 ∈ ℕ0)
141139, 140nn0mulcld 12378 . . . . . . 7 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℕ0)
142 nn0p1nn 12352 . . . . . . 7 ((2 · 𝑗) ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ)
143141, 142syl 17 . . . . . 6 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ)
144137, 143fmpti 7026 . . . . 5 𝐺:ℕ0⟶ℕ
145144a1i 11 . . . 4 (𝜑𝐺:ℕ0⟶ℕ)
146 2re 12127 . . . . . . . . 9 2 ∈ ℝ
147146a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℝ)
148 nn0re 12322 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
149147, 148remulcld 11085 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℝ)
150 1red 11056 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 1 ∈ ℝ)
151148, 150readdcld 11084 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℝ)
152147, 151remulcld 11085 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · (𝑘 + 1)) ∈ ℝ)
153 2rp 12815 . . . . . . . . 9 2 ∈ ℝ+
154153a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℝ+)
155148ltp1d 11985 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 < (𝑘 + 1))
156148, 151, 154, 155ltmul2dd 12908 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · 𝑘) < (2 · (𝑘 + 1)))
157149, 152, 150, 156ltadd1dd 11666 . . . . . 6 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) < ((2 · (𝑘 + 1)) + 1))
158137a1i 11 . . . . . . 7 (𝑘 ∈ ℕ0𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1)))
159 simpr 485 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → 𝑗 = 𝑘)
160159oveq2d 7333 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘))
161160oveq1d 7332 . . . . . . 7 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1))
162 id 22 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
163 2cnd 12131 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 2 ∈ ℂ)
164 nn0cn 12323 . . . . . . . . 9 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
165163, 164mulcld 11075 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℂ)
166 1cnd 11050 . . . . . . . 8 (𝑘 ∈ ℕ0 → 1 ∈ ℂ)
167165, 166addcld 11074 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℂ)
168158, 161, 162, 167fvmptd 6922 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐺𝑘) = ((2 · 𝑘) + 1))
169 simpr 485 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → 𝑗 = (𝑘 + 1))
170169oveq2d 7333 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → (2 · 𝑗) = (2 · (𝑘 + 1)))
171170oveq1d 7332 . . . . . . 7 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1))
172 peano2nn0 12353 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
173164, 166addcld 11074 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℂ)
174163, 173mulcld 11075 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2 · (𝑘 + 1)) ∈ ℂ)
175174, 166addcld 11074 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 · (𝑘 + 1)) + 1) ∈ ℂ)
176158, 171, 172, 175fvmptd 6922 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐺‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) + 1))
177157, 168, 1763brtr4d 5119 . . . . 5 (𝑘 ∈ ℕ0 → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
178177adantl 482 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
179 eldifi 4072 . . . . . . 7 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℕ)
180179adantl 482 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ)
181 1cnd 11050 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 1 ∈ ℂ)
182181negcld 11399 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → -1 ∈ ℂ)
183179, 80syl 17 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℕ0)
184182, 183expcld 13944 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) ∈ ℂ)
185184adantl 482 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) ∈ ℂ)
18614adantr 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑇 ∈ ℂ)
187180nnnn0d 12373 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ0)
188186, 187expcld 13944 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝑇𝑛) ∈ ℂ)
189180nncnd 12069 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℂ)
190180nnne0d 12103 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ≠ 0)
191188, 189, 190divcld 11831 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
192185, 191mulcld 11075 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
193192, 191addcld 11074 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ)
19499, 100, 180, 193fvmptd3 6938 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
195 eldifn 4073 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 𝑛 ∈ ran 𝐺)
196 0nn0 12328 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
197 1nn0 12329 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
198138, 197num0h 12529 . . . . . . . . . . . . . . . 16 1 = ((2 · 0) + 1)
199 oveq2 7325 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 0 → (2 · 𝑗) = (2 · 0))
200199oveq1d 7332 . . . . . . . . . . . . . . . . . 18 (𝑗 = 0 → ((2 · 𝑗) + 1) = ((2 · 0) + 1))
201200eqeq2d 2748 . . . . . . . . . . . . . . . . 17 (𝑗 = 0 → (1 = ((2 · 𝑗) + 1) ↔ 1 = ((2 · 0) + 1)))
202201rspcev 3570 . . . . . . . . . . . . . . . 16 ((0 ∈ ℕ0 ∧ 1 = ((2 · 0) + 1)) → ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1))
203196, 198, 202mp2an 689 . . . . . . . . . . . . . . 15 𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1)
204 ax-1cn 11009 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
205137elrnmpt 5885 . . . . . . . . . . . . . . . 16 (1 ∈ ℂ → (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1)))
206204, 205ax-mp 5 . . . . . . . . . . . . . . 15 (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1))
207203, 206mpbir 230 . . . . . . . . . . . . . 14 1 ∈ ran 𝐺
208207a1i 11 . . . . . . . . . . . . 13 (𝑛 = 1 → 1 ∈ ran 𝐺)
209 eleq1 2825 . . . . . . . . . . . . 13 (𝑛 = 1 → (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺))
210208, 209mpbird 256 . . . . . . . . . . . 12 (𝑛 = 1 → 𝑛 ∈ ran 𝐺)
211195, 210nsyl 140 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 𝑛 = 1)
212 nn1m1nn 12074 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ))
213179, 212syl 17 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ))
214213ord 861 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 𝑛 = 1 → (𝑛 − 1) ∈ ℕ))
215211, 214mpd 15 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℕ)
216 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑗
217 nfmpt1 5195 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))
218137, 217nfcxfr 2903 . . . . . . . . . . . . . . . . . . 19 𝑗𝐺
219218nfrn 5881 . . . . . . . . . . . . . . . . . 18 𝑗ran 𝐺
220216, 219nfdif 4071 . . . . . . . . . . . . . . . . 17 𝑗(ℕ ∖ ran 𝐺)
221220nfcri 2892 . . . . . . . . . . . . . . . 16 𝑗 𝑛 ∈ (ℕ ∖ ran 𝐺)
222137elrnmpt 5885 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1)))
223195, 222mtbid 323 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))
224 ralnex 3073 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑗 ∈ ℕ0 ¬ 𝑛 = ((2 · 𝑗) + 1) ↔ ¬ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))
225223, 224sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ∀𝑗 ∈ ℕ0 ¬ 𝑛 = ((2 · 𝑗) + 1))
226225r19.21bi 3231 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → ¬ 𝑛 = ((2 · 𝑗) + 1))
227226neqned 2948 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → 𝑛 ≠ ((2 · 𝑗) + 1))
228227necomd 2997 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
229228adantlr 712 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
230 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
231 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 𝑗 ∈ ℕ0)
232179ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → 𝑛 ∈ ℕ)
233146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℝ)
234 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
235234zred 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℝ)
236233, 235remulcld 11085 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℝ)
237 0red 11058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 0 ∈ ℝ)
238 1red 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 1 ∈ ℝ)
239 2cnd 12131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
240235recnd 11083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℂ)
241239, 240mulcomd 11076 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) = (𝑗 · 2))
242 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 𝑗 ∈ ℕ0)
243 elnn0z 12412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
244242, 243sylnib 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
245 nan 827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) ↔ (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗))
246244, 245mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗)
247246anabss1 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 0 ≤ 𝑗)
248235, 237ltnled 11202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (𝑗 < 0 ↔ ¬ 0 ≤ 𝑗))
249247, 248mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 < 0)
250153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℝ+)
251250rpregt0d 12858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 ∈ ℝ ∧ 0 < 2))
252 mulltgt0 42799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑗 · 2) < 0)
253235, 249, 251, 252syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (𝑗 · 2) < 0)
254241, 253eqbrtrd 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) < 0)
255236, 237, 238, 254ltadd1dd 11666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) < (0 + 1))
256 1cnd 11050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
257256addid2d 11256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (0 + 1) = 1)
258255, 257breqtrd 5113 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) < 1)
259236, 238readdcld 11084 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℝ)
260259, 238ltnled 11202 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (((2 · 𝑗) + 1) < 1 ↔ ¬ 1 ≤ ((2 · 𝑗) + 1)))
261258, 260mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 1 ≤ ((2 · 𝑗) + 1))
262 nnge1 12081 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑗) + 1) ∈ ℕ → 1 ≤ ((2 · 𝑗) + 1))
263261, 262nsyl 140 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ ((2 · 𝑗) + 1) ∈ ℕ)
264263adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 · 𝑗) + 1) ∈ ℕ)
265 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) = 𝑛)
266 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → 𝑛 ∈ ℕ)
267265, 266eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ)
268267adantll 711 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ)
269264, 268mtand 813 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 · 𝑗) + 1) = 𝑛)
270269neqned 2948 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ((2 · 𝑗) + 1) ≠ 𝑛)
271230, 231, 232, 270syl21anc 835 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
272229, 271pm2.61dan 810 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) → ((2 · 𝑗) + 1) ≠ 𝑛)
273272neneqd 2946 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) → ¬ ((2 · 𝑗) + 1) = 𝑛)
274273ex 413 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑗 ∈ ℤ → ¬ ((2 · 𝑗) + 1) = 𝑛))
275221, 274ralrimi 3237 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ∀𝑗 ∈ ℤ ¬ ((2 · 𝑗) + 1) = 𝑛)
276 ralnex 3073 . . . . . . . . . . . . . . 15 (∀𝑗 ∈ ℤ ¬ ((2 · 𝑗) + 1) = 𝑛 ↔ ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛)
277275, 276sylib 217 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛)
278179nnzd 12505 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℤ)
279 odd2np1 16129 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℤ → (¬ 2 ∥ 𝑛 ↔ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛))
280278, 279syl 17 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 2 ∥ 𝑛 ↔ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛))
281277, 280mtbird 324 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ¬ 2 ∥ 𝑛)
282281notnotrd 133 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 2 ∥ 𝑛)
283179nncnd 12069 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℂ)
284283, 181npcand 11416 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ((𝑛 − 1) + 1) = 𝑛)
285282, 284breqtrrd 5115 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 2 ∥ ((𝑛 − 1) + 1))
286183nn0zd 12504 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℤ)
287 oddp1even 16132 . . . . . . . . . . . 12 ((𝑛 − 1) ∈ ℤ → (¬ 2 ∥ (𝑛 − 1) ↔ 2 ∥ ((𝑛 − 1) + 1)))
288286, 287syl 17 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 2 ∥ (𝑛 − 1) ↔ 2 ∥ ((𝑛 − 1) + 1)))
289285, 288mpbird 256 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 2 ∥ (𝑛 − 1))
290 oexpneg 16133 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ ∧ ¬ 2 ∥ (𝑛 − 1)) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1)))
291181, 215, 289, 290syl3anc 1370 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1)))
292 1exp 13892 . . . . . . . . . . 11 ((𝑛 − 1) ∈ ℤ → (1↑(𝑛 − 1)) = 1)
293286, 292syl 17 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (1↑(𝑛 − 1)) = 1)
294293negeqd 11295 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → -(1↑(𝑛 − 1)) = -1)
295291, 294eqtrd 2777 . . . . . . . 8 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) = -1)
296295adantl 482 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) = -1)
297296oveq1d 7332 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) = (-1 · ((𝑇𝑛) / 𝑛)))
298297oveq1d 7332 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
299191mulm1d 11507 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1 · ((𝑇𝑛) / 𝑛)) = -((𝑇𝑛) / 𝑛))
300299oveq1d 7332 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = (-((𝑇𝑛) / 𝑛) + ((𝑇𝑛) / 𝑛)))
301191negcld 11399 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → -((𝑇𝑛) / 𝑛) ∈ ℂ)
302301, 191addcomd 11257 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-((𝑇𝑛) / 𝑛) + ((𝑇𝑛) / 𝑛)) = (((𝑇𝑛) / 𝑛) + -((𝑇𝑛) / 𝑛)))
303191negidd 11402 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((𝑇𝑛) / 𝑛) + -((𝑇𝑛) / 𝑛)) = 0)
304300, 302, 3033eqtrd 2781 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = 0)
305194, 298, 3043eqtrd 2781 . . . 4 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹𝑛) = 0)
306111, 110eqeltrd 2838 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ℂ)
30799a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗))))
308 simpr 485 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → 𝑗 = ((2 · 𝑘) + 1))
309308oveq1d 7332 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑗 − 1) = (((2 · 𝑘) + 1) − 1))
310309oveq2d 7333 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (-1↑(𝑗 − 1)) = (-1↑(((2 · 𝑘) + 1) − 1)))
311308oveq2d 7333 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑇𝑗) = (𝑇↑((2 · 𝑘) + 1)))
312311, 308oveq12d 7335 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((𝑇𝑗) / 𝑗) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
313310, 312oveq12d 7335 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
314313, 312oveq12d 7335 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)) = (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
315138a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℕ0)
316 simpr 485 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
317315, 316nn0mulcld 12378 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
318 nn0p1nn 12352 . . . . . . . 8 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
319317, 318syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ)
320166negcld 11399 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → -1 ∈ ℂ)
321165, 166pncand 11413 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
322138a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → 2 ∈ ℕ0)
323322, 162nn0mulcld 12378 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℕ0)
324321, 323eqeltrd 2838 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) − 1) ∈ ℕ0)
325320, 324expcld 13944 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (-1↑(((2 · 𝑘) + 1) − 1)) ∈ ℂ)
326325adantl 482 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) ∈ ℂ)
32714adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 𝑇 ∈ ℂ)
328197a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
329317, 328nn0addcld 12377 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ0)
330327, 329expcld 13944 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (𝑇↑((2 · 𝑘) + 1)) ∈ ℂ)
331 2cnd 12131 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℂ)
332164adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
333331, 332mulcld 11075 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℂ)
334 1cnd 11050 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℂ)
335333, 334addcld 11074 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℂ)
336 0red 11058 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 0 ∈ ℝ)
337146a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℝ)
338148adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℝ)
339337, 338remulcld 11085 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℝ)
340 1red 11056 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℝ)
341 0le2 12155 . . . . . . . . . . . . . 14 0 ≤ 2
342341a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ 2)
343316nn0ge0d 12376 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ 𝑘)
344337, 338, 342, 343mulge0d 11632 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ (2 · 𝑘))
345 0lt1 11577 . . . . . . . . . . . . 13 0 < 1
346345a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 0 < 1)
347339, 340, 344, 346addgegt0d 11628 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 0 < ((2 · 𝑘) + 1))
348336, 347gtned 11190 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ≠ 0)
349330, 335, 348divcld 11831 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) ∈ ℂ)
350326, 349mulcld 11075 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ)
351350, 349addcld 11074 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ)
352307, 314, 319, 351fvmptd 6922 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘((2 · 𝑘) + 1)) = (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
353321adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
354353oveq2d 7333 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) = (-1↑(2 · 𝑘)))
355 nn0z 12423 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
356 m1expeven 13910 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → (-1↑(2 · 𝑘)) = 1)
357355, 356syl 17 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (-1↑(2 · 𝑘)) = 1)
358357adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (-1↑(2 · 𝑘)) = 1)
359354, 358eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) = 1)
360359oveq1d 7332 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
361349mulid2d 11073 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
362360, 361eqtrd 2777 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
363362oveq1d 7332 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
3643492timesd 12296 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (2 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
365330, 335, 348divrec2d 11835 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))
366365oveq2d 7333 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (2 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
367363, 364, 3663eqtr2d 2783 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
368352, 367eqtr2d 2778 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) = (𝐹‘((2 · 𝑘) + 1)))
369 stirlinglem5.4 . . . . . . 7 𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))))
370369a1i 11 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → 𝐻 = (𝑗 ∈ ℕ0 ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))))))
371 simpr 485 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
372371oveq2d 7333 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘))
373372oveq1d 7332 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1))
374373oveq2d 7333 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (1 / ((2 · 𝑗) + 1)) = (1 / ((2 · 𝑘) + 1)))
375373oveq2d 7333 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝑇↑((2 · 𝑗) + 1)) = (𝑇↑((2 · 𝑘) + 1)))
376374, 375oveq12d 7335 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))) = ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))
377376oveq2d 7333 . . . . . 6 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
378335, 348reccld 11824 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
379378, 330mulcld 11075 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))) ∈ ℂ)
380331, 379mulcld 11075 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) ∈ ℂ)
381370, 377, 316, 380fvmptd 6922 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
382197a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 1 ∈ ℕ0)
383323, 382nn0addcld 12377 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ0)
384158, 161, 162, 383fvmptd 6922 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝐺𝑘) = ((2 · 𝑘) + 1))
385384adantl 482 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = ((2 · 𝑘) + 1))
386385fveq2d 6816 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝐺𝑘)) = (𝐹‘((2 · 𝑘) + 1)))
387368, 381, 3863eqtr4d 2787 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
388135, 1, 136, 2, 145, 178, 305, 306, 387isercoll2 15459 . . 3 (𝜑 → (seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))) ↔ seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇)))))
389134, 388mpbird 256 . 2 (𝜑 → seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
39051, 13resubcld 11483 . . . 4 (𝜑 → (1 − 𝑇) ∈ ℝ)
39114subidd 11400 . . . . . 6 (𝜑 → (𝑇𝑇) = 0)
392391eqcomd 2743 . . . . 5 (𝜑 → 0 = (𝑇𝑇))
39313, 51, 13, 129ltsub1dd 11667 . . . . 5 (𝜑 → (𝑇𝑇) < (1 − 𝑇))
394392, 393eqbrtrd 5109 . . . 4 (𝜑 → 0 < (1 − 𝑇))
395390, 394elrpd 12849 . . 3 (𝜑 → (1 − 𝑇) ∈ ℝ+)
396123, 395relogdivd 25864 . 2 (𝜑 → (log‘((1 + 𝑇) / (1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
397389, 396breqtrrd 5115 1 (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1540  wcel 2105  wne 2941  wral 3062  wrex 3071  Vcvv 3441  cdif 3894   class class class wbr 5087  cmpt 5170  ran crn 5609  ccom 5612  wf 6462  cfv 6466  (class class class)co 7317  cc 10949  cr 10950  0cc0 10951  1c1 10952   + caddc 10954   · cmul 10956  *cxr 11088   < clt 11089  cle 11090  cmin 11285  -cneg 11286   / cdiv 11712  cn 12053  2c2 12108  0cn0 12313  cz 12399  cuz 12662  +crp 12810  ...cfz 13319  seqcseq 13801  cexp 13862  abscabs 15024  cli 15272  cdvds 16042  ∞Metcxmet 20665  ballcbl 20667  logclog 25793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-inf2 9477  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-pre-sup 11029  ax-addf 11030  ax-mulf 11031
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-of 7575  df-om 7760  df-1st 7878  df-2nd 7879  df-supp 8027  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-2o 8347  df-oadd 8350  df-er 8548  df-map 8667  df-pm 8668  df-ixp 8736  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fsupp 9206  df-fi 9247  df-sup 9278  df-inf 9279  df-oi 9346  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122  df-9 12123  df-n0 12314  df-xnn0 12386  df-z 12400  df-dec 12518  df-uz 12663  df-q 12769  df-rp 12811  df-xneg 12928  df-xadd 12929  df-xmul 12930  df-ioo 13163  df-ioc 13164  df-ico 13165  df-icc 13166  df-fz 13320  df-fzo 13463  df-fl 13592  df-mod 13670  df-seq 13802  df-exp 13863  df-fac 14068  df-bc 14097  df-hash 14125  df-shft 14857  df-cj 14889  df-re 14890  df-im 14891  df-sqrt 15025  df-abs 15026  df-limsup 15259  df-clim 15276  df-rlim 15277  df-sum 15477  df-ef 15856  df-sin 15858  df-cos 15859  df-tan 15860  df-pi 15861  df-dvds 16043  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-starv 17054  df-sca 17055  df-vsca 17056  df-ip 17057  df-tset 17058  df-ple 17059  df-ds 17061  df-unif 17062  df-hom 17063  df-cco 17064  df-rest 17210  df-topn 17211  df-0g 17229  df-gsum 17230  df-topgen 17231  df-pt 17232  df-prds 17235  df-xrs 17290  df-qtop 17295  df-imas 17296  df-xps 17298  df-mre 17372  df-mrc 17373  df-acs 17375  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-submnd 18508  df-mulg 18777  df-cntz 18999  df-cmn 19463  df-psmet 20672  df-xmet 20673  df-met 20674  df-bl 20675  df-mopn 20676  df-fbas 20677  df-fg 20678  df-cnfld 20681  df-top 22126  df-topon 22143  df-topsp 22165  df-bases 22179  df-cld 22253  df-ntr 22254  df-cls 22255  df-nei 22332  df-lp 22370  df-perf 22371  df-cn 22461  df-cnp 22462  df-haus 22549  df-cmp 22621  df-tx 22796  df-hmeo 22989  df-fil 23080  df-fm 23172  df-flim 23173  df-flf 23174  df-xms 23556  df-ms 23557  df-tms 23558  df-cncf 24124  df-limc 25113  df-dv 25114  df-ulm 25619  df-log 25795
This theorem is referenced by:  stirlinglem6  43870
  Copyright terms: Public domain W3C validator