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 45525
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 12890 . . . . 5 β„• = (β„€β‰₯β€˜1)
2 1zzd 12618 . . . . 5 (πœ‘ β†’ 1 ∈ β„€)
3 stirlinglem5.1 . . . . . . . . 9 𝐷 = (𝑗 ∈ β„• ↦ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)))
43a1i 11 . . . . . . . 8 (πœ‘ β†’ 𝐷 = (𝑗 ∈ β„• ↦ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗))))
5 1cnd 11234 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 1 ∈ β„‚)
65negcld 11583 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ -1 ∈ β„‚)
7 nnm1nn0 12538 . . . . . . . . . . . . 13 (𝑗 ∈ β„• β†’ (𝑗 βˆ’ 1) ∈ β„•0)
87adantl 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (𝑗 βˆ’ 1) ∈ β„•0)
96, 8expcld 14137 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (-1↑(𝑗 βˆ’ 1)) ∈ β„‚)
10 nncn 12245 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„‚)
1110adantl 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„‚)
12 stirlinglem5.6 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑇 ∈ ℝ+)
1312rpred 13043 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑇 ∈ ℝ)
1413recnd 11267 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑇 ∈ β„‚)
1514adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑇 ∈ β„‚)
16 nnnn0 12504 . . . . . . . . . . . . 13 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„•0)
1716adantl 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•0)
1815, 17expcld 14137 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (𝑇↑𝑗) ∈ β„‚)
19 nnne0 12271 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ 𝑗 β‰  0)
2019adantl 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 β‰  0)
219, 11, 18, 20div32d 12038 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (𝑇↑𝑗)) = ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)))
225, 15pncan2d 11598 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((1 + 𝑇) βˆ’ 1) = 𝑇)
2322eqcomd 2731 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑇 = ((1 + 𝑇) βˆ’ 1))
2423oveq1d 7428 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (𝑇↑𝑗) = (((1 + 𝑇) βˆ’ 1)↑𝑗))
2524oveq2d 7429 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (𝑇↑𝑗)) = (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗)))
2621, 25eqtr3d 2767 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗)))
2726mpteq2dva 5244 . . . . . . . 8 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗))) = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗))))
284, 27eqtrd 2765 . . . . . . 7 (πœ‘ β†’ 𝐷 = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗))))
2928seqeq3d 14001 . . . . . 6 (πœ‘ β†’ seq1( + , 𝐷) = seq1( + , (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗)))))
30 1cnd 11234 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ β„‚)
3130, 14addcld 11258 . . . . . . . . . 10 (πœ‘ β†’ (1 + 𝑇) ∈ β„‚)
32 eqid 2725 . . . . . . . . . . 11 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
3332cnmetdval 24700 . . . . . . . . . 10 ((1 ∈ β„‚ ∧ (1 + 𝑇) ∈ β„‚) β†’ (1(abs ∘ βˆ’ )(1 + 𝑇)) = (absβ€˜(1 βˆ’ (1 + 𝑇))))
3430, 31, 33syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ (1(abs ∘ βˆ’ )(1 + 𝑇)) = (absβ€˜(1 βˆ’ (1 + 𝑇))))
35 1m1e0 12309 . . . . . . . . . . . . . 14 (1 βˆ’ 1) = 0
3635a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 βˆ’ 1) = 0)
3736oveq1d 7428 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 βˆ’ 1) βˆ’ 𝑇) = (0 βˆ’ 𝑇))
3830, 30, 14subsub4d 11627 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 βˆ’ 1) βˆ’ 𝑇) = (1 βˆ’ (1 + 𝑇)))
39 df-neg 11472 . . . . . . . . . . . . . 14 -𝑇 = (0 βˆ’ 𝑇)
4039eqcomi 2734 . . . . . . . . . . . . 13 (0 βˆ’ 𝑇) = -𝑇
4140a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (0 βˆ’ 𝑇) = -𝑇)
4237, 38, 413eqtr3d 2773 . . . . . . . . . . 11 (πœ‘ β†’ (1 βˆ’ (1 + 𝑇)) = -𝑇)
4342fveq2d 6894 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(1 βˆ’ (1 + 𝑇))) = (absβ€˜-𝑇))
4414absnegd 15423 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜-𝑇) = (absβ€˜π‘‡))
45 stirlinglem5.7 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜π‘‡) < 1)
4644, 45eqbrtrd 5166 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜-𝑇) < 1)
4743, 46eqbrtrd 5166 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(1 βˆ’ (1 + 𝑇))) < 1)
4834, 47eqbrtrd 5166 . . . . . . . 8 (πœ‘ β†’ (1(abs ∘ βˆ’ )(1 + 𝑇)) < 1)
49 cnxmet 24702 . . . . . . . . . 10 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
5049a1i 11 . . . . . . . . 9 (πœ‘ β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
51 1red 11240 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
5251rexrd 11289 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ ℝ*)
53 elbl2 24309 . . . . . . . . 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 256 . . . . . . 7 (πœ‘ β†’ (1 + 𝑇) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1))
56 eqid 2725 . . . . . . . 8 (1(ballβ€˜(abs ∘ βˆ’ ))1) = (1(ballβ€˜(abs ∘ βˆ’ ))1)
5756logtayl2 26609 . . . . . . 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 5166 . . . . 5 (πœ‘ β†’ seq1( + , 𝐷) ⇝ (logβ€˜(1 + 𝑇)))
60 seqex 13995 . . . . . 6 seq1( + , 𝐹) ∈ V
6160a1i 11 . . . . 5 (πœ‘ β†’ seq1( + , 𝐹) ∈ V)
62 stirlinglem5.2 . . . . . . . 8 𝐸 = (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))
6362a1i 11 . . . . . . 7 (πœ‘ β†’ 𝐸 = (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗)))
6463seqeq3d 14001 . . . . . 6 (πœ‘ β†’ seq1( + , 𝐸) = seq1( + , (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))))
65 logtayl 26607 . . . . . . 7 ((𝑇 ∈ β„‚ ∧ (absβ€˜π‘‡) < 1) β†’ seq1( + , (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(logβ€˜(1 βˆ’ 𝑇)))
6614, 45, 65syl2anc 582 . . . . . 6 (πœ‘ β†’ seq1( + , (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(logβ€˜(1 βˆ’ 𝑇)))
6764, 66eqbrtrd 5166 . . . . 5 (πœ‘ β†’ seq1( + , 𝐸) ⇝ -(logβ€˜(1 βˆ’ 𝑇)))
68 simpr 483 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
6968, 1eleqtrdi 2835 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
70 oveq1 7420 . . . . . . . . . 10 (𝑗 = 𝑛 β†’ (𝑗 βˆ’ 1) = (𝑛 βˆ’ 1))
7170oveq2d 7429 . . . . . . . . 9 (𝑗 = 𝑛 β†’ (-1↑(𝑗 βˆ’ 1)) = (-1↑(𝑛 βˆ’ 1)))
72 oveq2 7421 . . . . . . . . . 10 (𝑗 = 𝑛 β†’ (𝑇↑𝑗) = (𝑇↑𝑛))
73 id 22 . . . . . . . . . 10 (𝑗 = 𝑛 β†’ 𝑗 = 𝑛)
7472, 73oveq12d 7431 . . . . . . . . 9 (𝑗 = 𝑛 β†’ ((𝑇↑𝑗) / 𝑗) = ((𝑇↑𝑛) / 𝑛))
7571, 74oveq12d 7431 . . . . . . . 8 (𝑗 = 𝑛 β†’ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) = ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)))
76 elfznn 13557 . . . . . . . . 9 (𝑛 ∈ (1...π‘˜) β†’ 𝑛 ∈ β„•)
7776adantl 480 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 ∈ β„•)
78 1cnd 11234 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ 1 ∈ β„‚)
7978negcld 11583 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ -1 ∈ β„‚)
80 nnm1nn0 12538 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ (𝑛 βˆ’ 1) ∈ β„•0)
8179, 80expcld 14137 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
8277, 81syl 17 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
8314ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑇 ∈ β„‚)
8477nnnn0d 12557 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 ∈ β„•0)
8583, 84expcld 14137 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (𝑇↑𝑛) ∈ β„‚)
8677nncnd 12253 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 ∈ β„‚)
8777nnne0d 12287 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 β‰  0)
8885, 86, 87divcld 12015 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ ((𝑇↑𝑛) / 𝑛) ∈ β„‚)
8982, 88mulcld 11259 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
903, 75, 77, 89fvmptd3 7021 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (π·β€˜π‘›) = ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)))
9190, 89eqeltrd 2825 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (π·β€˜π‘›) ∈ β„‚)
92 addcl 11215 . . . . . . 7 ((𝑛 ∈ β„‚ ∧ 𝑖 ∈ β„‚) β†’ (𝑛 + 𝑖) ∈ β„‚)
9392adantl 480 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (𝑛 ∈ β„‚ ∧ 𝑖 ∈ β„‚)) β†’ (𝑛 + 𝑖) ∈ β„‚)
9469, 91, 93seqcl 14014 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐷)β€˜π‘˜) ∈ β„‚)
9562, 74, 77, 88fvmptd3 7021 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (πΈβ€˜π‘›) = ((𝑇↑𝑛) / 𝑛))
9695, 88eqeltrd 2825 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (πΈβ€˜π‘›) ∈ β„‚)
9769, 96, 93seqcl 14014 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐸)β€˜π‘˜) ∈ β„‚)
98 simpll 765 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ πœ‘)
99 stirlinglem5.3 . . . . . . . . 9 𝐹 = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)))
10075, 74oveq12d 7431 . . . . . . . . 9 (𝑗 = 𝑛 β†’ (((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
101 simpr 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
10281adantl 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
10314adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑇 ∈ β„‚)
104101nnnn0d 12557 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•0)
105103, 104expcld 14137 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑇↑𝑛) ∈ β„‚)
106101nncnd 12253 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„‚)
107101nnne0d 12287 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 β‰  0)
108105, 106, 107divcld 12015 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑇↑𝑛) / 𝑛) ∈ β„‚)
109102, 108mulcld 11259 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
110109, 108addcld 11258 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
11199, 100, 101, 110fvmptd3 7021 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
1123, 75, 101, 109fvmptd3 7021 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π·β€˜π‘›) = ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)))
113112eqcomd 2731 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) = (π·β€˜π‘›))
11462, 74, 101, 108fvmptd3 7021 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΈβ€˜π‘›) = ((𝑇↑𝑛) / 𝑛))
115114eqcomd 2731 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑇↑𝑛) / 𝑛) = (πΈβ€˜π‘›))
116113, 115oveq12d 7431 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((π·β€˜π‘›) + (πΈβ€˜π‘›)))
117111, 116eqtrd 2765 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = ((π·β€˜π‘›) + (πΈβ€˜π‘›)))
11898, 77, 117syl2anc 582 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (πΉβ€˜π‘›) = ((π·β€˜π‘›) + (πΈβ€˜π‘›)))
11969, 91, 96, 118seradd 14036 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) = ((seq1( + , 𝐷)β€˜π‘˜) + (seq1( + , 𝐸)β€˜π‘˜)))
1201, 2, 59, 61, 67, 94, 97, 119climadd 15603 . . . 4 (πœ‘ β†’ seq1( + , 𝐹) ⇝ ((logβ€˜(1 + 𝑇)) + -(logβ€˜(1 βˆ’ 𝑇))))
121 1rp 13005 . . . . . . . . 9 1 ∈ ℝ+
122121a1i 11 . . . . . . . 8 (πœ‘ β†’ 1 ∈ ℝ+)
123122, 12rpaddcld 13058 . . . . . . 7 (πœ‘ β†’ (1 + 𝑇) ∈ ℝ+)
124123rpne0d 13048 . . . . . 6 (πœ‘ β†’ (1 + 𝑇) β‰  0)
12531, 124logcld 26517 . . . . 5 (πœ‘ β†’ (logβ€˜(1 + 𝑇)) ∈ β„‚)
12630, 14subcld 11596 . . . . . 6 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ β„‚)
12713, 51absltd 15403 . . . . . . . . . 10 (πœ‘ β†’ ((absβ€˜π‘‡) < 1 ↔ (-1 < 𝑇 ∧ 𝑇 < 1)))
12845, 127mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (-1 < 𝑇 ∧ 𝑇 < 1))
129128simprd 494 . . . . . . . 8 (πœ‘ β†’ 𝑇 < 1)
13013, 129gtned 11374 . . . . . . 7 (πœ‘ β†’ 1 β‰  𝑇)
13130, 14, 130subne0d 11605 . . . . . 6 (πœ‘ β†’ (1 βˆ’ 𝑇) β‰  0)
132126, 131logcld 26517 . . . . 5 (πœ‘ β†’ (logβ€˜(1 βˆ’ 𝑇)) ∈ β„‚)
133125, 132negsubd 11602 . . . 4 (πœ‘ β†’ ((logβ€˜(1 + 𝑇)) + -(logβ€˜(1 βˆ’ 𝑇))) = ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
134120, 133breqtrd 5170 . . 3 (πœ‘ β†’ seq1( + , 𝐹) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
135 nn0uz 12889 . . . 4 β„•0 = (β„€β‰₯β€˜0)
136 0zd 12595 . . . 4 (πœ‘ β†’ 0 ∈ β„€)
137 stirlinglem5.5 . . . . . 6 𝐺 = (𝑗 ∈ β„•0 ↦ ((2 Β· 𝑗) + 1))
138 2nn0 12514 . . . . . . . . 9 2 ∈ β„•0
139138a1i 11 . . . . . . . 8 (𝑗 ∈ β„•0 β†’ 2 ∈ β„•0)
140 id 22 . . . . . . . 8 (𝑗 ∈ β„•0 β†’ 𝑗 ∈ β„•0)
141139, 140nn0mulcld 12562 . . . . . . 7 (𝑗 ∈ β„•0 β†’ (2 Β· 𝑗) ∈ β„•0)
142 nn0p1nn 12536 . . . . . . 7 ((2 Β· 𝑗) ∈ β„•0 β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
143141, 142syl 17 . . . . . 6 (𝑗 ∈ β„•0 β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
144137, 143fmpti 7115 . . . . 5 𝐺:β„•0βŸΆβ„•
145144a1i 11 . . . 4 (πœ‘ β†’ 𝐺:β„•0βŸΆβ„•)
146 2re 12311 . . . . . . . . 9 2 ∈ ℝ
147146a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 2 ∈ ℝ)
148 nn0re 12506 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ ℝ)
149147, 148remulcld 11269 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ ℝ)
150 1red 11240 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ 1 ∈ ℝ)
151148, 150readdcld 11268 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ ℝ)
152147, 151remulcld 11269 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2 Β· (π‘˜ + 1)) ∈ ℝ)
153 2rp 13006 . . . . . . . . 9 2 ∈ ℝ+
154153a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 2 ∈ ℝ+)
155148ltp1d 12169 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ π‘˜ < (π‘˜ + 1))
156148, 151, 154, 155ltmul2dd 13099 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) < (2 Β· (π‘˜ + 1)))
157149, 152, 150, 156ltadd1dd 11850 . . . . . 6 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) < ((2 Β· (π‘˜ + 1)) + 1))
158137a1i 11 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ 𝐺 = (𝑗 ∈ β„•0 ↦ ((2 Β· 𝑗) + 1)))
159 simpr 483 . . . . . . . . 9 ((π‘˜ ∈ β„•0 ∧ 𝑗 = π‘˜) β†’ 𝑗 = π‘˜)
160159oveq2d 7429 . . . . . . . 8 ((π‘˜ ∈ β„•0 ∧ 𝑗 = π‘˜) β†’ (2 Β· 𝑗) = (2 Β· π‘˜))
161160oveq1d 7428 . . . . . . 7 ((π‘˜ ∈ β„•0 ∧ 𝑗 = π‘˜) β†’ ((2 Β· 𝑗) + 1) = ((2 Β· π‘˜) + 1))
162 id 22 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„•0)
163 2cnd 12315 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ 2 ∈ β„‚)
164 nn0cn 12507 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
165163, 164mulcld 11259 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ β„‚)
166 1cnd 11234 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 1 ∈ β„‚)
167165, 166addcld 11258 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„‚)
168158, 161, 162, 167fvmptd 7005 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜π‘˜) = ((2 Β· π‘˜) + 1))
169 simpr 483 . . . . . . . . 9 ((π‘˜ ∈ β„•0 ∧ 𝑗 = (π‘˜ + 1)) β†’ 𝑗 = (π‘˜ + 1))
170169oveq2d 7429 . . . . . . . 8 ((π‘˜ ∈ β„•0 ∧ 𝑗 = (π‘˜ + 1)) β†’ (2 Β· 𝑗) = (2 Β· (π‘˜ + 1)))
171170oveq1d 7428 . . . . . . 7 ((π‘˜ ∈ β„•0 ∧ 𝑗 = (π‘˜ + 1)) β†’ ((2 Β· 𝑗) + 1) = ((2 Β· (π‘˜ + 1)) + 1))
172 peano2nn0 12537 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•0)
173164, 166addcld 11258 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„‚)
174163, 173mulcld 11259 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2 Β· (π‘˜ + 1)) ∈ β„‚)
175174, 166addcld 11258 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((2 Β· (π‘˜ + 1)) + 1) ∈ β„‚)
176158, 171, 172, 175fvmptd 7005 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜(π‘˜ + 1)) = ((2 Β· (π‘˜ + 1)) + 1))
177157, 168, 1763brtr4d 5176 . . . . 5 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜π‘˜) < (πΊβ€˜(π‘˜ + 1)))
178177adantl 480 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) < (πΊβ€˜(π‘˜ + 1)))
179 eldifi 4120 . . . . . . 7 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 𝑛 ∈ β„•)
180179adantl 480 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 ∈ β„•)
181 1cnd 11234 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 1 ∈ β„‚)
182181negcld 11583 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ -1 ∈ β„‚)
183179, 80syl 17 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 βˆ’ 1) ∈ β„•0)
184182, 183expcld 14137 . . . . . . . . 9 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
185184adantl 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
18614adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑇 ∈ β„‚)
187180nnnn0d 12557 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 ∈ β„•0)
188186, 187expcld 14137 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (𝑇↑𝑛) ∈ β„‚)
189180nncnd 12253 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 ∈ β„‚)
190180nnne0d 12287 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 β‰  0)
191188, 189, 190divcld 12015 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((𝑇↑𝑛) / 𝑛) ∈ β„‚)
192185, 191mulcld 11259 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
193192, 191addcld 11258 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
19499, 100, 180, 193fvmptd3 7021 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (πΉβ€˜π‘›) = (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
195 eldifn 4121 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ 𝑛 ∈ ran 𝐺)
196 0nn0 12512 . . . . . . . . . . . . . . . 16 0 ∈ β„•0
197 1nn0 12513 . . . . . . . . . . . . . . . . 17 1 ∈ β„•0
198138, 197num0h 12714 . . . . . . . . . . . . . . . 16 1 = ((2 Β· 0) + 1)
199 oveq2 7421 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 0 β†’ (2 Β· 𝑗) = (2 Β· 0))
200199oveq1d 7428 . . . . . . . . . . . . . . . . . 18 (𝑗 = 0 β†’ ((2 Β· 𝑗) + 1) = ((2 Β· 0) + 1))
201200eqeq2d 2736 . . . . . . . . . . . . . . . . 17 (𝑗 = 0 β†’ (1 = ((2 Β· 𝑗) + 1) ↔ 1 = ((2 Β· 0) + 1)))
202201rspcev 3603 . . . . . . . . . . . . . . . 16 ((0 ∈ β„•0 ∧ 1 = ((2 Β· 0) + 1)) β†’ βˆƒπ‘— ∈ β„•0 1 = ((2 Β· 𝑗) + 1))
203196, 198, 202mp2an 690 . . . . . . . . . . . . . . 15 βˆƒπ‘— ∈ β„•0 1 = ((2 Β· 𝑗) + 1)
204 ax-1cn 11191 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
205137elrnmpt 5953 . . . . . . . . . . . . . . . 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 2813 . . . . . . . . . . . . 13 (𝑛 = 1 β†’ (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺))
210208, 209mpbird 256 . . . . . . . . . . . 12 (𝑛 = 1 β†’ 𝑛 ∈ ran 𝐺)
211195, 210nsyl 140 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ 𝑛 = 1)
212 nn1m1nn 12258 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (𝑛 = 1 ∨ (𝑛 βˆ’ 1) ∈ β„•))
213179, 212syl 17 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 = 1 ∨ (𝑛 βˆ’ 1) ∈ β„•))
214213ord 862 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (Β¬ 𝑛 = 1 β†’ (𝑛 βˆ’ 1) ∈ β„•))
215211, 214mpd 15 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 βˆ’ 1) ∈ β„•)
216 nfcv 2892 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗ℕ
217 nfmpt1 5252 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗(𝑗 ∈ β„•0 ↦ ((2 Β· 𝑗) + 1))
218137, 217nfcxfr 2890 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗𝐺
219218nfrn 5949 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗ran 𝐺
220216, 219nfdif 4118 . . . . . . . . . . . . . . . . 17 Ⅎ𝑗(β„• βˆ– ran 𝐺)
221220nfcri 2882 . . . . . . . . . . . . . . . 16 Ⅎ𝑗 𝑛 ∈ (β„• βˆ– ran 𝐺)
222137elrnmpt 5953 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 ∈ ran 𝐺 ↔ βˆƒπ‘— ∈ β„•0 𝑛 = ((2 Β· 𝑗) + 1)))
223195, 222mtbid 323 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ βˆƒπ‘— ∈ β„•0 𝑛 = ((2 Β· 𝑗) + 1))
224 ralnex 3062 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆ€π‘— ∈ β„•0 Β¬ 𝑛 = ((2 Β· 𝑗) + 1) ↔ Β¬ βˆƒπ‘— ∈ β„•0 𝑛 = ((2 Β· 𝑗) + 1))
225223, 224sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ βˆ€π‘— ∈ β„•0 Β¬ 𝑛 = ((2 Β· 𝑗) + 1))
226225r19.21bi 3239 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„•0) β†’ Β¬ 𝑛 = ((2 Β· 𝑗) + 1))
227226neqned 2937 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„•0) β†’ 𝑛 β‰  ((2 Β· 𝑗) + 1))
228227necomd 2986 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
229228adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
230 simplr 767 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ β„€)
231 simpr 483 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 𝑗 ∈ β„•0)
232179ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑛 ∈ β„•)
233146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 2 ∈ ℝ)
234 simpl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ β„€)
235234zred 12691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ ℝ)
236233, 235remulcld 11269 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 Β· 𝑗) ∈ ℝ)
237 0red 11242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 0 ∈ ℝ)
238 1red 11240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 1 ∈ ℝ)
239 2cnd 12315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 2 ∈ β„‚)
240235recnd 11267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ β„‚)
241239, 240mulcomd 11260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 Β· 𝑗) = (𝑗 Β· 2))
242 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 𝑗 ∈ β„•0)
243 elnn0z 12596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ β„•0 ↔ (𝑗 ∈ β„€ ∧ 0 ≀ 𝑗))
244242, 243sylnib 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ (𝑗 ∈ β„€ ∧ 0 ≀ 𝑗))
245 nan 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ (𝑗 ∈ β„€ ∧ 0 ≀ 𝑗)) ↔ (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑗 ∈ β„€) β†’ Β¬ 0 ≀ 𝑗))
246244, 245mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑗 ∈ β„€) β†’ Β¬ 0 ≀ 𝑗)
247246anabss1 664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 0 ≀ 𝑗)
248235, 237ltnled 11386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (𝑗 < 0 ↔ Β¬ 0 ≀ 𝑗))
249247, 248mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 < 0)
250153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 2 ∈ ℝ+)
251250rpregt0d 13049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 ∈ ℝ ∧ 0 < 2))
252 mulltgt0 44445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ (𝑗 Β· 2) < 0)
253235, 249, 251, 252syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (𝑗 Β· 2) < 0)
254241, 253eqbrtrd 5166 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 Β· 𝑗) < 0)
255236, 237, 238, 254ltadd1dd 11850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) < (0 + 1))
256 1cnd 11234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 1 ∈ β„‚)
257256addlidd 11440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (0 + 1) = 1)
258255, 257breqtrd 5170 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) < 1)
259236, 238readdcld 11268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) ∈ ℝ)
260259, 238ltnled 11386 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (((2 Β· 𝑗) + 1) < 1 ↔ Β¬ 1 ≀ ((2 Β· 𝑗) + 1)))
261258, 260mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 1 ≀ ((2 Β· 𝑗) + 1))
262 nnge1 12265 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 Β· 𝑗) + 1) ∈ β„• β†’ 1 ≀ ((2 Β· 𝑗) + 1))
263261, 262nsyl 140 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ ((2 Β· 𝑗) + 1) ∈ β„•)
264263adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) β†’ Β¬ ((2 Β· 𝑗) + 1) ∈ β„•)
265 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ ((2 Β· 𝑗) + 1) = 𝑛)
266 simpl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ 𝑛 ∈ β„•)
267265, 266eqeltrd 2825 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„• ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
268267adantll 712 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
269264, 268mtand 814 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) β†’ Β¬ ((2 Β· 𝑗) + 1) = 𝑛)
270269neqned 2937 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
271230, 231, 232, 270syl21anc 836 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
272229, 271pm2.61dan 811 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
273272neneqd 2935 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) β†’ Β¬ ((2 Β· 𝑗) + 1) = 𝑛)
274273ex 411 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑗 ∈ β„€ β†’ Β¬ ((2 Β· 𝑗) + 1) = 𝑛))
275221, 274ralrimi 3245 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ βˆ€π‘— ∈ β„€ Β¬ ((2 Β· 𝑗) + 1) = 𝑛)
276 ralnex 3062 . . . . . . . . . . . . . . 15 (βˆ€π‘— ∈ β„€ Β¬ ((2 Β· 𝑗) + 1) = 𝑛 ↔ Β¬ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛)
277275, 276sylib 217 . . . . . . . . . . . . . 14 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛)
278179nnzd 12610 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 𝑛 ∈ β„€)
279 odd2np1 16312 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„€ β†’ (Β¬ 2 βˆ₯ 𝑛 ↔ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛))
280278, 279syl 17 . . . . . . . . . . . . . 14 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (Β¬ 2 βˆ₯ 𝑛 ↔ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛))
281277, 280mtbird 324 . . . . . . . . . . . . 13 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ Β¬ 2 βˆ₯ 𝑛)
282281notnotrd 133 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 2 βˆ₯ 𝑛)
283179nncnd 12253 . . . . . . . . . . . . 13 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 𝑛 ∈ β„‚)
284283, 181npcand 11600 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ ((𝑛 βˆ’ 1) + 1) = 𝑛)
285282, 284breqtrrd 5172 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 2 βˆ₯ ((𝑛 βˆ’ 1) + 1))
286183nn0zd 12609 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 βˆ’ 1) ∈ β„€)
287 oddp1even 16315 . . . . . . . . . . . 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 16316 . . . . . . . . . 10 ((1 ∈ β„‚ ∧ (𝑛 βˆ’ 1) ∈ β„• ∧ Β¬ 2 βˆ₯ (𝑛 βˆ’ 1)) β†’ (-1↑(𝑛 βˆ’ 1)) = -(1↑(𝑛 βˆ’ 1)))
291181, 215, 289, 290syl3anc 1368 . . . . . . . . 9 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (-1↑(𝑛 βˆ’ 1)) = -(1↑(𝑛 βˆ’ 1)))
292 1exp 14083 . . . . . . . . . . 11 ((𝑛 βˆ’ 1) ∈ β„€ β†’ (1↑(𝑛 βˆ’ 1)) = 1)
293286, 292syl 17 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (1↑(𝑛 βˆ’ 1)) = 1)
294293negeqd 11479 . . . . . . . . 9 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ -(1↑(𝑛 βˆ’ 1)) = -1)
295291, 294eqtrd 2765 . . . . . . . 8 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (-1↑(𝑛 βˆ’ 1)) = -1)
296295adantl 480 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-1↑(𝑛 βˆ’ 1)) = -1)
297296oveq1d 7428 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) = (-1 Β· ((𝑇↑𝑛) / 𝑛)))
298297oveq1d 7428 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((-1 Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
299191mulm1d 11691 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-1 Β· ((𝑇↑𝑛) / 𝑛)) = -((𝑇↑𝑛) / 𝑛))
300299oveq1d 7428 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1 Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛)))
301191negcld 11583 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ -((𝑇↑𝑛) / 𝑛) ∈ β„‚)
302301, 191addcomd 11441 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛)) = (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛)))
303191negidd 11586 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛)) = 0)
304300, 302, 3033eqtrd 2769 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1 Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = 0)
305194, 298, 3043eqtrd 2769 . . . 4 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (πΉβ€˜π‘›) = 0)
306111, 110eqeltrd 2825 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ β„‚)
30799a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐹 = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗))))
308 simpr 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ 𝑗 = ((2 Β· π‘˜) + 1))
309308oveq1d 7428 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ (𝑗 βˆ’ 1) = (((2 Β· π‘˜) + 1) βˆ’ 1))
310309oveq2d 7429 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ (-1↑(𝑗 βˆ’ 1)) = (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)))
311308oveq2d 7429 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ (𝑇↑𝑗) = (𝑇↑((2 Β· π‘˜) + 1)))
312311, 308oveq12d 7431 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ ((𝑇↑𝑗) / 𝑗) = ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
313310, 312oveq12d 7431 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) = ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
314313, 312oveq12d 7431 . . . . . . 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 483 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
317315, 316nn0mulcld 12562 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ β„•0)
318 nn0p1nn 12536 . . . . . . . 8 ((2 Β· π‘˜) ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
319317, 318syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
320166negcld 11583 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ -1 ∈ β„‚)
321165, 166pncand 11597 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) βˆ’ 1) = (2 Β· π‘˜))
322138a1i 11 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ 2 ∈ β„•0)
323322, 162nn0mulcld 12562 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ β„•0)
324321, 323eqeltrd 2825 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) βˆ’ 1) ∈ β„•0)
325320, 324expcld 14137 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) ∈ β„‚)
326325adantl 480 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) ∈ β„‚)
32714adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝑇 ∈ β„‚)
328197a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„•0)
329317, 328nn0addcld 12561 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
330327, 329expcld 14137 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝑇↑((2 Β· π‘˜) + 1)) ∈ β„‚)
331 2cnd 12315 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 2 ∈ β„‚)
332164adantl 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
333331, 332mulcld 11259 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ β„‚)
334 1cnd 11234 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„‚)
335333, 334addcld 11258 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) ∈ β„‚)
336 0red 11242 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ∈ ℝ)
337146a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 2 ∈ ℝ)
338148adantl 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ ℝ)
339337, 338remulcld 11269 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ ℝ)
340 1red 11240 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ ℝ)
341 0le2 12339 . . . . . . . . . . . . . 14 0 ≀ 2
342341a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ 2)
343316nn0ge0d 12560 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ π‘˜)
344337, 338, 342, 343mulge0d 11816 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (2 Β· π‘˜))
345 0lt1 11761 . . . . . . . . . . . . 13 0 < 1
346345a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 < 1)
347339, 340, 344, 346addgegt0d 11812 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 < ((2 Β· π‘˜) + 1))
348336, 347gtned 11374 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) β‰  0)
349330, 335, 348divcld 12015 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) ∈ β„‚)
350326, 349mulcld 11259 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) ∈ β„‚)
351350, 349addcld 11258 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) ∈ β„‚)
352307, 314, 319, 351fvmptd 7005 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜((2 Β· π‘˜) + 1)) = (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
353321adantl 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((2 Β· π‘˜) + 1) βˆ’ 1) = (2 Β· π‘˜))
354353oveq2d 7429 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) = (-1↑(2 Β· π‘˜)))
355 nn0z 12608 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
356 m1expeven 14101 . . . . . . . . . . . . 13 (π‘˜ ∈ β„€ β†’ (-1↑(2 Β· π‘˜)) = 1)
357355, 356syl 17 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = 1)
358357adantl 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(2 Β· π‘˜)) = 1)
359354, 358eqtrd 2765 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) = 1)
360359oveq1d 7428 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (1 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
361349mullidd 11257 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
362360, 361eqtrd 2765 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
363362oveq1d 7428 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
3643492timesd 12480 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
365330, 335, 348divrec2d 12019 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) = ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1))))
366365oveq2d 7429 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
367363, 364, 3663eqtr2d 2771 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
368352, 367eqtr2d 2766 . . . . 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 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ 𝑗 = π‘˜)
372371oveq2d 7429 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (2 Β· 𝑗) = (2 Β· π‘˜))
373372oveq1d 7428 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ ((2 Β· 𝑗) + 1) = ((2 Β· π‘˜) + 1))
374373oveq2d 7429 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (1 / ((2 Β· 𝑗) + 1)) = (1 / ((2 Β· π‘˜) + 1)))
375373oveq2d 7429 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (𝑇↑((2 Β· 𝑗) + 1)) = (𝑇↑((2 Β· π‘˜) + 1)))
376374, 375oveq12d 7431 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ ((1 / ((2 Β· 𝑗) + 1)) Β· (𝑇↑((2 Β· 𝑗) + 1))) = ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1))))
377376oveq2d 7429 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (2 Β· ((1 / ((2 Β· 𝑗) + 1)) Β· (𝑇↑((2 Β· 𝑗) + 1)))) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
378335, 348reccld 12008 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / ((2 Β· π‘˜) + 1)) ∈ β„‚)
379378, 330mulcld 11259 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1))) ∈ β„‚)
380331, 379mulcld 11259 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))) ∈ β„‚)
381370, 377, 316, 380fvmptd 7005 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
382197a1i 11 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ 1 ∈ β„•0)
383323, 382nn0addcld 12561 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
384158, 161, 162, 383fvmptd 7005 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜π‘˜) = ((2 Β· π‘˜) + 1))
385384adantl 480 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) = ((2 Β· π‘˜) + 1))
386385fveq2d 6894 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜(πΊβ€˜π‘˜)) = (πΉβ€˜((2 Β· π‘˜) + 1)))
387368, 381, 3863eqtr4d 2775 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = (πΉβ€˜(πΊβ€˜π‘˜)))
388135, 1, 136, 2, 145, 178, 305, 306, 387isercoll2 15642 . . 3 (πœ‘ β†’ (seq0( + , 𝐻) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))) ↔ seq1( + , 𝐹) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇)))))
389134, 388mpbird 256 . 2 (πœ‘ β†’ seq0( + , 𝐻) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
39051, 13resubcld 11667 . . . 4 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ ℝ)
39114subidd 11584 . . . . . 6 (πœ‘ β†’ (𝑇 βˆ’ 𝑇) = 0)
392391eqcomd 2731 . . . . 5 (πœ‘ β†’ 0 = (𝑇 βˆ’ 𝑇))
39313, 51, 13, 129ltsub1dd 11851 . . . . 5 (πœ‘ β†’ (𝑇 βˆ’ 𝑇) < (1 βˆ’ 𝑇))
394392, 393eqbrtrd 5166 . . . 4 (πœ‘ β†’ 0 < (1 βˆ’ 𝑇))
395390, 394elrpd 13040 . . 3 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ ℝ+)
396123, 395relogdivd 26573 . 2 (πœ‘ β†’ (logβ€˜((1 + 𝑇) / (1 βˆ’ 𝑇))) = ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
397389, 396breqtrrd 5172 1 (πœ‘ β†’ seq0( + , 𝐻) ⇝ (logβ€˜((1 + 𝑇) / (1 βˆ’ 𝑇))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  βˆƒwrex 3060  Vcvv 3463   βˆ– cdif 3938   class class class wbr 5144   ↦ cmpt 5227  ran crn 5674   ∘ ccom 5677  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7413  β„‚cc 11131  β„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   Β· cmul 11138  β„*cxr 11272   < clt 11273   ≀ cle 11274   βˆ’ cmin 11469  -cneg 11470   / cdiv 11896  β„•cn 12237  2c2 12292  β„•0cn0 12497  β„€cz 12583  β„€β‰₯cuz 12847  β„+crp 13001  ...cfz 13511  seqcseq 13993  β†‘cexp 14053  abscabs 15208   ⇝ cli 15455   βˆ₯ cdvds 16225  βˆžMetcxmet 21263  ballcbl 21265  logclog 26501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211  ax-addf 11212
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7866  df-1st 7987  df-2nd 7988  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8718  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9381  df-fi 9429  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-xnn0 12570  df-z 12584  df-dec 12703  df-uz 12848  df-q 12958  df-rp 13002  df-xneg 13119  df-xadd 13120  df-xmul 13121  df-ioo 13355  df-ioc 13356  df-ico 13357  df-icc 13358  df-fz 13512  df-fzo 13655  df-fl 13784  df-mod 13862  df-seq 13994  df-exp 14054  df-fac 14260  df-bc 14289  df-hash 14317  df-shft 15041  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-limsup 15442  df-clim 15459  df-rlim 15460  df-sum 15660  df-ef 16038  df-sin 16040  df-cos 16041  df-tan 16042  df-pi 16043  df-dvds 16226  df-struct 17110  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-rest 17398  df-topn 17399  df-0g 17417  df-gsum 17418  df-topgen 17419  df-pt 17420  df-prds 17423  df-xrs 17478  df-qtop 17483  df-imas 17484  df-xps 17486  df-mre 17560  df-mrc 17561  df-acs 17563  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-submnd 18735  df-mulg 19023  df-cntz 19267  df-cmn 19736  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-fbas 21275  df-fg 21276  df-cnfld 21279  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-perf 23054  df-cn 23144  df-cnp 23145  df-haus 23232  df-cmp 23304  df-tx 23479  df-hmeo 23672  df-fil 23763  df-fm 23855  df-flim 23856  df-flf 23857  df-xms 24239  df-ms 24240  df-tms 24241  df-cncf 24811  df-limc 25808  df-dv 25809  df-ulm 26326  df-log 26503
This theorem is referenced by:  stirlinglem6  45526
  Copyright terms: Public domain W3C validator