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

Theorem stirlinglem5 42888
 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 12289 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 12021 . . . . 5 (𝜑 → 1 ∈ ℤ)
3 stirlinglem5.1 . . . . . . . . 9 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)))
43a1i 11 . . . . . . . 8 (𝜑𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))))
5 1cnd 10643 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℂ)
65negcld 10991 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → -1 ∈ ℂ)
7 nnm1nn0 11944 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ0)
87adantl 485 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝑗 − 1) ∈ ℕ0)
96, 8expcld 13526 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (-1↑(𝑗 − 1)) ∈ ℂ)
10 nncn 11651 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ∈ ℂ)
1110adantl 485 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℂ)
12 stirlinglem5.6 . . . . . . . . . . . . . . 15 (𝜑𝑇 ∈ ℝ+)
1312rpred 12439 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ ℝ)
1413recnd 10676 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℂ)
1514adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑇 ∈ ℂ)
16 nnnn0 11910 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
1716adantl 485 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
1815, 17expcld 13526 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) ∈ ℂ)
19 nnne0 11677 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → 𝑗 ≠ 0)
2019adantl 485 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → 𝑗 ≠ 0)
219, 11, 18, 20div32d 11446 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇𝑗)) = ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)))
225, 15pncan2d 11006 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ((1 + 𝑇) − 1) = 𝑇)
2322eqcomd 2804 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 𝑇 = ((1 + 𝑇) − 1))
2423oveq1d 7160 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (𝑇𝑗) = (((1 + 𝑇) − 1)↑𝑗))
2524oveq2d 7161 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))
2621, 25eqtr3d 2835 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))
2726mpteq2dva 5129 . . . . . . . 8 (𝜑 → (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))))
284, 27eqtrd 2833 . . . . . . 7 (𝜑𝐷 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))))
2928seqeq3d 13392 . . . . . 6 (𝜑 → seq1( + , 𝐷) = seq1( + , (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))))
30 1cnd 10643 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
3130, 14addcld 10667 . . . . . . . . . 10 (𝜑 → (1 + 𝑇) ∈ ℂ)
32 eqid 2798 . . . . . . . . . . 11 (abs ∘ − ) = (abs ∘ − )
3332cnmetdval 23417 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ) → (1(abs ∘ − )(1 + 𝑇)) = (abs‘(1 − (1 + 𝑇))))
3430, 31, 33syl2anc 587 . . . . . . . . 9 (𝜑 → (1(abs ∘ − )(1 + 𝑇)) = (abs‘(1 − (1 + 𝑇))))
35 1m1e0 11715 . . . . . . . . . . . . . 14 (1 − 1) = 0
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → (1 − 1) = 0)
3736oveq1d 7160 . . . . . . . . . . . 12 (𝜑 → ((1 − 1) − 𝑇) = (0 − 𝑇))
3830, 30, 14subsub4d 11035 . . . . . . . . . . . 12 (𝜑 → ((1 − 1) − 𝑇) = (1 − (1 + 𝑇)))
39 df-neg 10880 . . . . . . . . . . . . . 14 -𝑇 = (0 − 𝑇)
4039eqcomi 2807 . . . . . . . . . . . . 13 (0 − 𝑇) = -𝑇
4140a1i 11 . . . . . . . . . . . 12 (𝜑 → (0 − 𝑇) = -𝑇)
4237, 38, 413eqtr3d 2841 . . . . . . . . . . 11 (𝜑 → (1 − (1 + 𝑇)) = -𝑇)
4342fveq2d 6659 . . . . . . . . . 10 (𝜑 → (abs‘(1 − (1 + 𝑇))) = (abs‘-𝑇))
4414absnegd 14821 . . . . . . . . . . 11 (𝜑 → (abs‘-𝑇) = (abs‘𝑇))
45 stirlinglem5.7 . . . . . . . . . . 11 (𝜑 → (abs‘𝑇) < 1)
4644, 45eqbrtrd 5056 . . . . . . . . . 10 (𝜑 → (abs‘-𝑇) < 1)
4743, 46eqbrtrd 5056 . . . . . . . . 9 (𝜑 → (abs‘(1 − (1 + 𝑇))) < 1)
4834, 47eqbrtrd 5056 . . . . . . . 8 (𝜑 → (1(abs ∘ − )(1 + 𝑇)) < 1)
49 cnxmet 23419 . . . . . . . . . 10 (abs ∘ − ) ∈ (∞Met‘ℂ)
5049a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
51 1red 10649 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
5251rexrd 10698 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ*)
53 elbl2 23038 . . . . . . . . 9 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ)) → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1))
5450, 52, 30, 31, 53syl22anc 837 . . . . . . . 8 (𝜑 → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1))
5548, 54mpbird 260 . . . . . . 7 (𝜑 → (1 + 𝑇) ∈ (1(ball‘(abs ∘ − ))1))
56 eqid 2798 . . . . . . . 8 (1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘ − ))1)
5756logtayl2 25297 . . . . . . 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 5056 . . . . 5 (𝜑 → seq1( + , 𝐷) ⇝ (log‘(1 + 𝑇)))
60 seqex 13386 . . . . . 6 seq1( + , 𝐹) ∈ V
6160a1i 11 . . . . 5 (𝜑 → seq1( + , 𝐹) ∈ V)
62 stirlinglem5.2 . . . . . . . 8 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))
6362a1i 11 . . . . . . 7 (𝜑𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗)))
6463seqeq3d 13392 . . . . . 6 (𝜑 → seq1( + , 𝐸) = seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))))
65 logtayl 25295 . . . . . . 7 ((𝑇 ∈ ℂ ∧ (abs‘𝑇) < 1) → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇)))
6614, 45, 65syl2anc 587 . . . . . 6 (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇)))
6764, 66eqbrtrd 5056 . . . . 5 (𝜑 → seq1( + , 𝐸) ⇝ -(log‘(1 − 𝑇)))
68 simpr 488 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
6968, 1eleqtrdi 2900 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
70 oveq1 7152 . . . . . . . . . 10 (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1))
7170oveq2d 7161 . . . . . . . . 9 (𝑗 = 𝑛 → (-1↑(𝑗 − 1)) = (-1↑(𝑛 − 1)))
72 oveq2 7153 . . . . . . . . . 10 (𝑗 = 𝑛 → (𝑇𝑗) = (𝑇𝑛))
73 id 22 . . . . . . . . . 10 (𝑗 = 𝑛𝑗 = 𝑛)
7472, 73oveq12d 7163 . . . . . . . . 9 (𝑗 = 𝑛 → ((𝑇𝑗) / 𝑗) = ((𝑇𝑛) / 𝑛))
7571, 74oveq12d 7163 . . . . . . . 8 (𝑗 = 𝑛 → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
76 elfznn 12951 . . . . . . . . 9 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
7776adantl 485 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ)
78 1cnd 10643 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 1 ∈ ℂ)
7978negcld 10991 . . . . . . . . . . 11 (𝑛 ∈ ℕ → -1 ∈ ℂ)
80 nnm1nn0 11944 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
8179, 80expcld 13526 . . . . . . . . . 10 (𝑛 ∈ ℕ → (-1↑(𝑛 − 1)) ∈ ℂ)
8277, 81syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (-1↑(𝑛 − 1)) ∈ ℂ)
8314ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑇 ∈ ℂ)
8477nnnn0d 11963 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ0)
8583, 84expcld 13526 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑇𝑛) ∈ ℂ)
8677nncnd 11659 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℂ)
8777nnne0d 11693 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ≠ 0)
8885, 86, 87divcld 11423 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
8982, 88mulcld 10668 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
903, 75, 77, 89fvmptd3 6778 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
9190, 89eqeltrd 2890 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷𝑛) ∈ ℂ)
92 addcl 10626 . . . . . . 7 ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ)
9392adantl 485 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ)
9469, 91, 93seqcl 13406 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐷)‘𝑘) ∈ ℂ)
9562, 74, 77, 88fvmptd3 6778 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸𝑛) = ((𝑇𝑛) / 𝑛))
9695, 88eqeltrd 2890 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸𝑛) ∈ ℂ)
9769, 96, 93seqcl 13406 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐸)‘𝑘) ∈ ℂ)
98 simpll 766 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑)
99 stirlinglem5.3 . . . . . . . . 9 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)))
10075, 74oveq12d 7163 . . . . . . . . 9 (𝑗 = 𝑛 → (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
101 simpr 488 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
10281adantl 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈ ℂ)
10314adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑇 ∈ ℂ)
104101nnnn0d 11963 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
105103, 104expcld 13526 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑇𝑛) ∈ ℂ)
106101nncnd 11659 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
107101nnne0d 11693 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑛 ≠ 0)
108105, 106, 107divcld 11423 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
109102, 108mulcld 10668 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
110109, 108addcld 10667 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ)
11199, 100, 101, 110fvmptd3 6778 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
1123, 75, 101, 109fvmptd3 6778 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐷𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)))
113112eqcomd 2804 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) = (𝐷𝑛))
11462, 74, 101, 108fvmptd3 6778 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐸𝑛) = ((𝑇𝑛) / 𝑛))
115114eqcomd 2804 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑇𝑛) / 𝑛) = (𝐸𝑛))
116113, 115oveq12d 7163 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = ((𝐷𝑛) + (𝐸𝑛)))
117111, 116eqtrd 2833 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ((𝐷𝑛) + (𝐸𝑛)))
11898, 77, 117syl2anc 587 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐹𝑛) = ((𝐷𝑛) + (𝐸𝑛)))
11969, 91, 96, 118seradd 13428 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = ((seq1( + , 𝐷)‘𝑘) + (seq1( + , 𝐸)‘𝑘)))
1201, 2, 59, 61, 67, 94, 97, 119climadd 15000 . . . 4 (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) + -(log‘(1 − 𝑇))))
121 1rp 12401 . . . . . . . . 9 1 ∈ ℝ+
122121a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
123122, 12rpaddcld 12454 . . . . . . 7 (𝜑 → (1 + 𝑇) ∈ ℝ+)
124123rpne0d 12444 . . . . . 6 (𝜑 → (1 + 𝑇) ≠ 0)
12531, 124logcld 25206 . . . . 5 (𝜑 → (log‘(1 + 𝑇)) ∈ ℂ)
12630, 14subcld 11004 . . . . . 6 (𝜑 → (1 − 𝑇) ∈ ℂ)
12713, 51absltd 14801 . . . . . . . . . 10 (𝜑 → ((abs‘𝑇) < 1 ↔ (-1 < 𝑇𝑇 < 1)))
12845, 127mpbid 235 . . . . . . . . 9 (𝜑 → (-1 < 𝑇𝑇 < 1))
129128simprd 499 . . . . . . . 8 (𝜑𝑇 < 1)
13013, 129gtned 10782 . . . . . . 7 (𝜑 → 1 ≠ 𝑇)
13130, 14, 130subne0d 11013 . . . . . 6 (𝜑 → (1 − 𝑇) ≠ 0)
132126, 131logcld 25206 . . . . 5 (𝜑 → (log‘(1 − 𝑇)) ∈ ℂ)
133125, 132negsubd 11010 . . . 4 (𝜑 → ((log‘(1 + 𝑇)) + -(log‘(1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
134120, 133breqtrd 5060 . . 3 (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
135 nn0uz 12288 . . . 4 0 = (ℤ‘0)
136 0zd 12001 . . . 4 (𝜑 → 0 ∈ ℤ)
137 stirlinglem5.5 . . . . . 6 𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))
138 2nn0 11920 . . . . . . . . 9 2 ∈ ℕ0
139138a1i 11 . . . . . . . 8 (𝑗 ∈ ℕ0 → 2 ∈ ℕ0)
140 id 22 . . . . . . . 8 (𝑗 ∈ ℕ0𝑗 ∈ ℕ0)
141139, 140nn0mulcld 11968 . . . . . . 7 (𝑗 ∈ ℕ0 → (2 · 𝑗) ∈ ℕ0)
142 nn0p1nn 11942 . . . . . . 7 ((2 · 𝑗) ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ)
143141, 142syl 17 . . . . . 6 (𝑗 ∈ ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ)
144137, 143fmpti 6863 . . . . 5 𝐺:ℕ0⟶ℕ
145144a1i 11 . . . 4 (𝜑𝐺:ℕ0⟶ℕ)
146 2re 11717 . . . . . . . . 9 2 ∈ ℝ
147146a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℝ)
148 nn0re 11912 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
149147, 148remulcld 10678 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℝ)
150 1red 10649 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 1 ∈ ℝ)
151148, 150readdcld 10677 . . . . . . . 8 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℝ)
152147, 151remulcld 10678 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · (𝑘 + 1)) ∈ ℝ)
153 2rp 12402 . . . . . . . . 9 2 ∈ ℝ+
154153a1i 11 . . . . . . . 8 (𝑘 ∈ ℕ0 → 2 ∈ ℝ+)
155148ltp1d 11577 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 < (𝑘 + 1))
156148, 151, 154, 155ltmul2dd 12495 . . . . . . 7 (𝑘 ∈ ℕ0 → (2 · 𝑘) < (2 · (𝑘 + 1)))
157149, 152, 150, 156ltadd1dd 11258 . . . . . 6 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) < ((2 · (𝑘 + 1)) + 1))
158137a1i 11 . . . . . . 7 (𝑘 ∈ ℕ0𝐺 = (𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1)))
159 simpr 488 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → 𝑗 = 𝑘)
160159oveq2d 7161 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘))
161160oveq1d 7160 . . . . . . 7 ((𝑘 ∈ ℕ0𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1))
162 id 22 . . . . . . 7 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
163 2cnd 11721 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 2 ∈ ℂ)
164 nn0cn 11913 . . . . . . . . 9 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
165163, 164mulcld 10668 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℂ)
166 1cnd 10643 . . . . . . . 8 (𝑘 ∈ ℕ0 → 1 ∈ ℂ)
167165, 166addcld 10667 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℂ)
168158, 161, 162, 167fvmptd 6762 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐺𝑘) = ((2 · 𝑘) + 1))
169 simpr 488 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → 𝑗 = (𝑘 + 1))
170169oveq2d 7161 . . . . . . . 8 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → (2 · 𝑗) = (2 · (𝑘 + 1)))
171170oveq1d 7160 . . . . . . 7 ((𝑘 ∈ ℕ0𝑗 = (𝑘 + 1)) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1))
172 peano2nn0 11943 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
173164, 166addcld 10667 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℂ)
174163, 173mulcld 10668 . . . . . . . 8 (𝑘 ∈ ℕ0 → (2 · (𝑘 + 1)) ∈ ℂ)
175174, 166addcld 10667 . . . . . . 7 (𝑘 ∈ ℕ0 → ((2 · (𝑘 + 1)) + 1) ∈ ℂ)
176158, 171, 172, 175fvmptd 6762 . . . . . 6 (𝑘 ∈ ℕ0 → (𝐺‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) + 1))
177157, 168, 1763brtr4d 5066 . . . . 5 (𝑘 ∈ ℕ0 → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
178177adantl 485 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
179 eldifi 4057 . . . . . . 7 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℕ)
180179adantl 485 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ)
181 1cnd 10643 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 1 ∈ ℂ)
182181negcld 10991 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → -1 ∈ ℂ)
183179, 80syl 17 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℕ0)
184182, 183expcld 13526 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) ∈ ℂ)
185184adantl 485 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) ∈ ℂ)
18614adantr 484 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑇 ∈ ℂ)
187180nnnn0d 11963 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ0)
188186, 187expcld 13526 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝑇𝑛) ∈ ℂ)
189180nncnd 11659 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℂ)
190180nnne0d 11693 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ≠ 0)
191188, 189, 190divcld 11423 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((𝑇𝑛) / 𝑛) ∈ ℂ)
192185, 191mulcld 10668 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) ∈ ℂ)
193192, 191addcld 10667 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) ∈ ℂ)
19499, 100, 180, 193fvmptd3 6778 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
195 eldifn 4058 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 𝑛 ∈ ran 𝐺)
196 0nn0 11918 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
197 1nn0 11919 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
198138, 197num0h 12118 . . . . . . . . . . . . . . . 16 1 = ((2 · 0) + 1)
199 oveq2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 0 → (2 · 𝑗) = (2 · 0))
200199oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑗 = 0 → ((2 · 𝑗) + 1) = ((2 · 0) + 1))
201200eqeq2d 2809 . . . . . . . . . . . . . . . . 17 (𝑗 = 0 → (1 = ((2 · 𝑗) + 1) ↔ 1 = ((2 · 0) + 1)))
202201rspcev 3572 . . . . . . . . . . . . . . . 16 ((0 ∈ ℕ0 ∧ 1 = ((2 · 0) + 1)) → ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1))
203196, 198, 202mp2an 691 . . . . . . . . . . . . . . 15 𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1)
204 ax-1cn 10602 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
205137elrnmpt 5796 . . . . . . . . . . . . . . . 16 (1 ∈ ℂ → (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1)))
206204, 205ax-mp 5 . . . . . . . . . . . . . . 15 (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 · 𝑗) + 1))
207203, 206mpbir 234 . . . . . . . . . . . . . 14 1 ∈ ran 𝐺
208207a1i 11 . . . . . . . . . . . . 13 (𝑛 = 1 → 1 ∈ ran 𝐺)
209 eleq1 2877 . . . . . . . . . . . . 13 (𝑛 = 1 → (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺))
210208, 209mpbird 260 . . . . . . . . . . . 12 (𝑛 = 1 → 𝑛 ∈ ran 𝐺)
211195, 210nsyl 142 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 𝑛 = 1)
212 nn1m1nn 11664 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ))
213179, 212syl 17 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ))
214213ord 861 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 𝑛 = 1 → (𝑛 − 1) ∈ ℕ))
215211, 214mpd 15 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℕ)
216 nfcv 2955 . . . . . . . . . . . . . . . . . 18 𝑗
217 nfmpt1 5132 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ ℕ0 ↦ ((2 · 𝑗) + 1))
218137, 217nfcxfr 2953 . . . . . . . . . . . . . . . . . . 19 𝑗𝐺
219218nfrn 5792 . . . . . . . . . . . . . . . . . 18 𝑗ran 𝐺
220216, 219nfdif 4056 . . . . . . . . . . . . . . . . 17 𝑗(ℕ ∖ ran 𝐺)
221220nfcri 2943 . . . . . . . . . . . . . . . 16 𝑗 𝑛 ∈ (ℕ ∖ ran 𝐺)
222137elrnmpt 5796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1)))
223195, 222mtbid 327 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))
224 ralnex 3199 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑗 ∈ ℕ0 ¬ 𝑛 = ((2 · 𝑗) + 1) ↔ ¬ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))
225223, 224sylibr 237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ∀𝑗 ∈ ℕ0 ¬ 𝑛 = ((2 · 𝑗) + 1))
226225r19.21bi 3173 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → ¬ 𝑛 = ((2 · 𝑗) + 1))
227226neqned 2994 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → 𝑛 ≠ ((2 · 𝑗) + 1))
228227necomd 3042 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
229228adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
230 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
231 simpr 488 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 𝑗 ∈ ℕ0)
232179ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → 𝑛 ∈ ℕ)
233146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℝ)
234 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
235234zred 12095 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℝ)
236233, 235remulcld 10678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℝ)
237 0red 10651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 0 ∈ ℝ)
238 1red 10649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 1 ∈ ℝ)
239 2cnd 11721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℂ)
240235recnd 10676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 ∈ ℂ)
241239, 240mulcomd 10669 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) = (𝑗 · 2))
242 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 𝑗 ∈ ℕ0)
243 elnn0z 12002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ ℕ0 ↔ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
244242, 243sylnib 331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
245 nan 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) ↔ (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗))
246244, 245mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗)
247246anabss1 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 0 ≤ 𝑗)
248235, 237ltnled 10794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (𝑗 < 0 ↔ ¬ 0 ≤ 𝑗))
249247, 248mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 𝑗 < 0)
250153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 2 ∈ ℝ+)
251250rpregt0d 12445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 ∈ ℝ ∧ 0 < 2))
252 mulltgt0 41822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑗 · 2) < 0)
253235, 249, 251, 252syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (𝑗 · 2) < 0)
254241, 253eqbrtrd 5056 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (2 · 𝑗) < 0)
255236, 237, 238, 254ltadd1dd 11258 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) < (0 + 1))
256 1cnd 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → 1 ∈ ℂ)
257256addid2d 10848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (0 + 1) = 1)
258255, 257breqtrd 5060 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) < 1)
259236, 238readdcld 10677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ∈ ℝ)
260259, 238ltnled 10794 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → (((2 · 𝑗) + 1) < 1 ↔ ¬ 1 ≤ ((2 · 𝑗) + 1)))
261258, 260mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ 1 ≤ ((2 · 𝑗) + 1))
262 nnge1 11671 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · 𝑗) + 1) ∈ ℕ → 1 ≤ ((2 · 𝑗) + 1))
263261, 262nsyl 142 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) → ¬ ((2 · 𝑗) + 1) ∈ ℕ)
264263adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 · 𝑗) + 1) ∈ ℕ)
265 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) = 𝑛)
266 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → 𝑛 ∈ ℕ)
267265, 266eqeltrd 2890 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ ℕ ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ)
268267adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ)
269264, 268mtand 815 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 · 𝑗) + 1) = 𝑛)
270269neqned 2994 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0) ∧ 𝑛 ∈ ℕ) → ((2 · 𝑗) + 1) ≠ 𝑛)
271230, 231, 232, 270syl21anc 836 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0) → ((2 · 𝑗) + 1) ≠ 𝑛)
272229, 271pm2.61dan 812 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) → ((2 · 𝑗) + 1) ≠ 𝑛)
273272neneqd 2992 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℕ ∖ ran 𝐺) ∧ 𝑗 ∈ ℤ) → ¬ ((2 · 𝑗) + 1) = 𝑛)
274273ex 416 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑗 ∈ ℤ → ¬ ((2 · 𝑗) + 1) = 𝑛))
275221, 274ralrimi 3180 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ∀𝑗 ∈ ℤ ¬ ((2 · 𝑗) + 1) = 𝑛)
276 ralnex 3199 . . . . . . . . . . . . . . 15 (∀𝑗 ∈ ℤ ¬ ((2 · 𝑗) + 1) = 𝑛 ↔ ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛)
277275, 276sylib 221 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛)
278179nnzd 12094 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℤ)
279 odd2np1 15702 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℤ → (¬ 2 ∥ 𝑛 ↔ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛))
280278, 279syl 17 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 2 ∥ 𝑛 ↔ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛))
281277, 280mtbird 328 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ ¬ 2 ∥ 𝑛)
282281notnotrd 135 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 2 ∥ 𝑛)
283179nncnd 11659 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 𝑛 ∈ ℂ)
284283, 181npcand 11008 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ((𝑛 − 1) + 1) = 𝑛)
285282, 284breqtrrd 5062 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → 2 ∥ ((𝑛 − 1) + 1))
286183nn0zd 12093 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (𝑛 − 1) ∈ ℤ)
287 oddp1even 15705 . . . . . . . . . . . 12 ((𝑛 − 1) ∈ ℤ → (¬ 2 ∥ (𝑛 − 1) ↔ 2 ∥ ((𝑛 − 1) + 1)))
288286, 287syl 17 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (¬ 2 ∥ (𝑛 − 1) ↔ 2 ∥ ((𝑛 − 1) + 1)))
289285, 288mpbird 260 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → ¬ 2 ∥ (𝑛 − 1))
290 oexpneg 15706 . . . . . . . . . 10 ((1 ∈ ℂ ∧ (𝑛 − 1) ∈ ℕ ∧ ¬ 2 ∥ (𝑛 − 1)) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1)))
291181, 215, 289, 290syl3anc 1368 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1)))
292 1exp 13474 . . . . . . . . . . 11 ((𝑛 − 1) ∈ ℤ → (1↑(𝑛 − 1)) = 1)
293286, 292syl 17 . . . . . . . . . 10 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (1↑(𝑛 − 1)) = 1)
294293negeqd 10887 . . . . . . . . 9 (𝑛 ∈ (ℕ ∖ ran 𝐺) → -(1↑(𝑛 − 1)) = -1)
295291, 294eqtrd 2833 . . . . . . . 8 (𝑛 ∈ (ℕ ∖ ran 𝐺) → (-1↑(𝑛 − 1)) = -1)
296295adantl 485 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) = -1)
297296oveq1d 7160 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) = (-1 · ((𝑇𝑛) / 𝑛)))
298297oveq1d 7160 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)))
299191mulm1d 11099 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1 · ((𝑇𝑛) / 𝑛)) = -((𝑇𝑛) / 𝑛))
300299oveq1d 7160 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = (-((𝑇𝑛) / 𝑛) + ((𝑇𝑛) / 𝑛)))
301191negcld 10991 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → -((𝑇𝑛) / 𝑛) ∈ ℂ)
302301, 191addcomd 10849 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-((𝑇𝑛) / 𝑛) + ((𝑇𝑛) / 𝑛)) = (((𝑇𝑛) / 𝑛) + -((𝑇𝑛) / 𝑛)))
303191negidd 10994 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((𝑇𝑛) / 𝑛) + -((𝑇𝑛) / 𝑛)) = 0)
304300, 302, 3033eqtrd 2837 . . . . 5 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇𝑛) / 𝑛)) + ((𝑇𝑛) / 𝑛)) = 0)
305194, 298, 3043eqtrd 2837 . . . 4 ((𝜑𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹𝑛) = 0)
306111, 110eqeltrd 2890 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ ℂ)
30799a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) + ((𝑇𝑗) / 𝑗))))
308 simpr 488 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → 𝑗 = ((2 · 𝑘) + 1))
309308oveq1d 7160 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑗 − 1) = (((2 · 𝑘) + 1) − 1))
310309oveq2d 7161 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (-1↑(𝑗 − 1)) = (-1↑(((2 · 𝑘) + 1) − 1)))
311308oveq2d 7161 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑇𝑗) = (𝑇↑((2 · 𝑘) + 1)))
312311, 308oveq12d 7163 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((𝑇𝑗) / 𝑗) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
313310, 312oveq12d 7163 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((-1↑(𝑗 − 1)) · ((𝑇𝑗) / 𝑗)) = ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
314313, 312oveq12d 7163 . . . . . . 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 488 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
317315, 316nn0mulcld 11968 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
318 nn0p1nn 11942 . . . . . . . 8 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
319317, 318syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ)
320166negcld 10991 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → -1 ∈ ℂ)
321165, 166pncand 11005 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
322138a1i 11 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → 2 ∈ ℕ0)
323322, 162nn0mulcld 11968 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (2 · 𝑘) ∈ ℕ0)
324321, 323eqeltrd 2890 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (((2 · 𝑘) + 1) − 1) ∈ ℕ0)
325320, 324expcld 13526 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (-1↑(((2 · 𝑘) + 1) − 1)) ∈ ℂ)
326325adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) ∈ ℂ)
32714adantr 484 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 𝑇 ∈ ℂ)
328197a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
329317, 328nn0addcld 11967 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ0)
330327, 329expcld 13526 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (𝑇↑((2 · 𝑘) + 1)) ∈ ℂ)
331 2cnd 11721 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℂ)
332164adantl 485 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
333331, 332mulcld 10668 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℂ)
334 1cnd 10643 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℂ)
335333, 334addcld 10667 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℂ)
336 0red 10651 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 0 ∈ ℝ)
337146a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 2 ∈ ℝ)
338148adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℝ)
339337, 338remulcld 10678 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℝ)
340 1red 10649 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 1 ∈ ℝ)
341 0le2 11745 . . . . . . . . . . . . . 14 0 ≤ 2
342341a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ 2)
343316nn0ge0d 11966 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ 𝑘)
344337, 338, 342, 343mulge0d 11224 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 0 ≤ (2 · 𝑘))
345 0lt1 11169 . . . . . . . . . . . . 13 0 < 1
346345a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 0 < 1)
347339, 340, 344, 346addgegt0d 11220 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → 0 < ((2 · 𝑘) + 1))
348336, 347gtned 10782 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ≠ 0)
349330, 335, 348divcld 11423 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) ∈ ℂ)
350326, 349mulcld 10668 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ)
351350, 349addcld 10667 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ)
352307, 314, 319, 351fvmptd 6762 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘((2 · 𝑘) + 1)) = (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
353321adantl 485 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (((2 · 𝑘) + 1) − 1) = (2 · 𝑘))
354353oveq2d 7161 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) = (-1↑(2 · 𝑘)))
355 nn0z 12013 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
356 m1expeven 13492 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → (-1↑(2 · 𝑘)) = 1)
357355, 356syl 17 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (-1↑(2 · 𝑘)) = 1)
358357adantl 485 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (-1↑(2 · 𝑘)) = 1)
359354, 358eqtrd 2833 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ0) → (-1↑(((2 · 𝑘) + 1) − 1)) = 1)
360359oveq1d 7160 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
361349mulid2d 10666 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ0) → (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
362360, 361eqtrd 2833 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))
363362oveq1d 7160 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
3643492timesd 11886 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (2 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))))
365330, 335, 348divrec2d 11427 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))
366365oveq2d 7161 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (2 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
367363, 364, 3663eqtr2d 2839 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (((-1↑(((2 · 𝑘) + 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
368352, 367eqtr2d 2834 . . . . 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 488 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
372371oveq2d 7161 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘))
373372oveq1d 7160 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1))
374373oveq2d 7161 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (1 / ((2 · 𝑗) + 1)) = (1 / ((2 · 𝑘) + 1)))
375373oveq2d 7161 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝑇↑((2 · 𝑗) + 1)) = (𝑇↑((2 · 𝑘) + 1)))
376374, 375oveq12d 7163 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))) = ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))
377376oveq2d 7161 . . . . . 6 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
378335, 348reccld 11416 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
379378, 330mulcld 10668 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))) ∈ ℂ)
380331, 379mulcld 10668 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) ∈ ℂ)
381370, 377, 316, 380fvmptd 6762 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))))
382197a1i 11 . . . . . . . . 9 (𝑘 ∈ ℕ0 → 1 ∈ ℕ0)
383323, 382nn0addcld 11967 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ0)
384158, 161, 162, 383fvmptd 6762 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝐺𝑘) = ((2 · 𝑘) + 1))
385384adantl 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = ((2 · 𝑘) + 1))
386385fveq2d 6659 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹‘(𝐺𝑘)) = (𝐹‘((2 · 𝑘) + 1)))
387368, 381, 3863eqtr4d 2843 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
388135, 1, 136, 2, 145, 178, 305, 306, 387isercoll2 15037 . . 3 (𝜑 → (seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))) ↔ seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇)))))
389134, 388mpbird 260 . 2 (𝜑 → seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
39051, 13resubcld 11075 . . . 4 (𝜑 → (1 − 𝑇) ∈ ℝ)
39114subidd 10992 . . . . . 6 (𝜑 → (𝑇𝑇) = 0)
392391eqcomd 2804 . . . . 5 (𝜑 → 0 = (𝑇𝑇))
39313, 51, 13, 129ltsub1dd 11259 . . . . 5 (𝜑 → (𝑇𝑇) < (1 − 𝑇))
394392, 393eqbrtrd 5056 . . . 4 (𝜑 → 0 < (1 − 𝑇))
395390, 394elrpd 12436 . . 3 (𝜑 → (1 − 𝑇) ∈ ℝ+)
396123, 395relogdivd 25261 . 2 (𝜑 → (log‘((1 + 𝑇) / (1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇))))
397389, 396breqtrrd 5062 1 (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3442   ∖ cdif 3880   class class class wbr 5034   ↦ cmpt 5114  ran crn 5524   ∘ ccom 5527  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145  ℂcc 10542  ℝcr 10543  0cc0 10544  1c1 10545   + caddc 10547   · cmul 10549  ℝ*cxr 10681   < clt 10682   ≤ cle 10683   − cmin 10877  -cneg 10878   / cdiv 11304  ℕcn 11643  2c2 11698  ℕ0cn0 11903  ℤcz 11989  ℤ≥cuz 12251  ℝ+crp 12397  ...cfz 12905  seqcseq 13384  ↑cexp 13445  abscabs 14605   ⇝ cli 14853   ∥ cdvds 15619  ∞Metcxmet 20097  ballcbl 20099  logclog 25190 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-inf2 9106  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622  ax-addf 10623  ax-mulf 10624 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-iin 4888  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7400  df-om 7574  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-map 8409  df-pm 8410  df-ixp 8463  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-fsupp 8836  df-fi 8877  df-sup 8908  df-inf 8909  df-oi 8976  df-card 9370  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-xnn0 11976  df-z 11990  df-dec 12107  df-uz 12252  df-q 12357  df-rp 12398  df-xneg 12515  df-xadd 12516  df-xmul 12517  df-ioo 12750  df-ioc 12751  df-ico 12752  df-icc 12753  df-fz 12906  df-fzo 13049  df-fl 13177  df-mod 13253  df-seq 13385  df-exp 13446  df-fac 13650  df-bc 13679  df-hash 13707  df-shft 14438  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-limsup 14840  df-clim 14857  df-rlim 14858  df-sum 15055  df-ef 15433  df-sin 15435  df-cos 15436  df-tan 15437  df-pi 15438  df-dvds 15620  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-ress 16503  df-plusg 16590  df-mulr 16591  df-starv 16592  df-sca 16593  df-vsca 16594  df-ip 16595  df-tset 16596  df-ple 16597  df-ds 16599  df-unif 16600  df-hom 16601  df-cco 16602  df-rest 16708  df-topn 16709  df-0g 16727  df-gsum 16728  df-topgen 16729  df-pt 16730  df-prds 16733  df-xrs 16787  df-qtop 16792  df-imas 16793  df-xps 16795  df-mre 16869  df-mrc 16870  df-acs 16872  df-mgm 17864  df-sgrp 17913  df-mnd 17924  df-submnd 17969  df-mulg 18238  df-cntz 18460  df-cmn 18921  df-psmet 20104  df-xmet 20105  df-met 20106  df-bl 20107  df-mopn 20108  df-fbas 20109  df-fg 20110  df-cnfld 20113  df-top 21540  df-topon 21557  df-topsp 21579  df-bases 21592  df-cld 21665  df-ntr 21666  df-cls 21667  df-nei 21744  df-lp 21782  df-perf 21783  df-cn 21873  df-cnp 21874  df-haus 21961  df-cmp 22033  df-tx 22208  df-hmeo 22401  df-fil 22492  df-fm 22584  df-flim 22585  df-flf 22586  df-xms 22968  df-ms 22969  df-tms 22970  df-cncf 23524  df-limc 24510  df-dv 24511  df-ulm 25016  df-log 25192 This theorem is referenced by:  stirlinglem6  42889
 Copyright terms: Public domain W3C validator