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 44405
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 12811 . . . . 5 β„• = (β„€β‰₯β€˜1)
2 1zzd 12539 . . . . 5 (πœ‘ β†’ 1 ∈ β„€)
3 stirlinglem5.1 . . . . . . . . 9 𝐷 = (𝑗 ∈ β„• ↦ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)))
43a1i 11 . . . . . . . 8 (πœ‘ β†’ 𝐷 = (𝑗 ∈ β„• ↦ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗))))
5 1cnd 11155 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 1 ∈ β„‚)
65negcld 11504 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ -1 ∈ β„‚)
7 nnm1nn0 12459 . . . . . . . . . . . . 13 (𝑗 ∈ β„• β†’ (𝑗 βˆ’ 1) ∈ β„•0)
87adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (𝑗 βˆ’ 1) ∈ β„•0)
96, 8expcld 14057 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (-1↑(𝑗 βˆ’ 1)) ∈ β„‚)
10 nncn 12166 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„‚)
1110adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„‚)
12 stirlinglem5.6 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑇 ∈ ℝ+)
1312rpred 12962 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑇 ∈ ℝ)
1413recnd 11188 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑇 ∈ β„‚)
1514adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑇 ∈ β„‚)
16 nnnn0 12425 . . . . . . . . . . . . 13 (𝑗 ∈ β„• β†’ 𝑗 ∈ β„•0)
1716adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•0)
1815, 17expcld 14057 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (𝑇↑𝑗) ∈ β„‚)
19 nnne0 12192 . . . . . . . . . . . 12 (𝑗 ∈ β„• β†’ 𝑗 β‰  0)
2019adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑗 β‰  0)
219, 11, 18, 20div32d 11959 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (𝑇↑𝑗)) = ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)))
225, 15pncan2d 11519 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((1 + 𝑇) βˆ’ 1) = 𝑇)
2322eqcomd 2739 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ 𝑇 = ((1 + 𝑇) βˆ’ 1))
2423oveq1d 7373 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (𝑇↑𝑗) = (((1 + 𝑇) βˆ’ 1)↑𝑗))
2524oveq2d 7374 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (𝑇↑𝑗)) = (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗)))
2621, 25eqtr3d 2775 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗)))
2726mpteq2dva 5206 . . . . . . . 8 (πœ‘ β†’ (𝑗 ∈ β„• ↦ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗))) = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗))))
284, 27eqtrd 2773 . . . . . . 7 (πœ‘ β†’ 𝐷 = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗))))
2928seqeq3d 13920 . . . . . 6 (πœ‘ β†’ seq1( + , 𝐷) = seq1( + , (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) / 𝑗) Β· (((1 + 𝑇) βˆ’ 1)↑𝑗)))))
30 1cnd 11155 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ β„‚)
3130, 14addcld 11179 . . . . . . . . . 10 (πœ‘ β†’ (1 + 𝑇) ∈ β„‚)
32 eqid 2733 . . . . . . . . . . 11 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
3332cnmetdval 24150 . . . . . . . . . 10 ((1 ∈ β„‚ ∧ (1 + 𝑇) ∈ β„‚) β†’ (1(abs ∘ βˆ’ )(1 + 𝑇)) = (absβ€˜(1 βˆ’ (1 + 𝑇))))
3430, 31, 33syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (1(abs ∘ βˆ’ )(1 + 𝑇)) = (absβ€˜(1 βˆ’ (1 + 𝑇))))
35 1m1e0 12230 . . . . . . . . . . . . . 14 (1 βˆ’ 1) = 0
3635a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 βˆ’ 1) = 0)
3736oveq1d 7373 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 βˆ’ 1) βˆ’ 𝑇) = (0 βˆ’ 𝑇))
3830, 30, 14subsub4d 11548 . . . . . . . . . . . 12 (πœ‘ β†’ ((1 βˆ’ 1) βˆ’ 𝑇) = (1 βˆ’ (1 + 𝑇)))
39 df-neg 11393 . . . . . . . . . . . . . 14 -𝑇 = (0 βˆ’ 𝑇)
4039eqcomi 2742 . . . . . . . . . . . . 13 (0 βˆ’ 𝑇) = -𝑇
4140a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (0 βˆ’ 𝑇) = -𝑇)
4237, 38, 413eqtr3d 2781 . . . . . . . . . . 11 (πœ‘ β†’ (1 βˆ’ (1 + 𝑇)) = -𝑇)
4342fveq2d 6847 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(1 βˆ’ (1 + 𝑇))) = (absβ€˜-𝑇))
4414absnegd 15340 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜-𝑇) = (absβ€˜π‘‡))
45 stirlinglem5.7 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜π‘‡) < 1)
4644, 45eqbrtrd 5128 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜-𝑇) < 1)
4743, 46eqbrtrd 5128 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(1 βˆ’ (1 + 𝑇))) < 1)
4834, 47eqbrtrd 5128 . . . . . . . 8 (πœ‘ β†’ (1(abs ∘ βˆ’ )(1 + 𝑇)) < 1)
49 cnxmet 24152 . . . . . . . . . 10 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
5049a1i 11 . . . . . . . . 9 (πœ‘ β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
51 1red 11161 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
5251rexrd 11210 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ ℝ*)
53 elbl2 23759 . . . . . . . . 9 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 1 ∈ ℝ*) ∧ (1 ∈ β„‚ ∧ (1 + 𝑇) ∈ β„‚)) β†’ ((1 + 𝑇) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1) ↔ (1(abs ∘ βˆ’ )(1 + 𝑇)) < 1))
5450, 52, 30, 31, 53syl22anc 838 . . . . . . . 8 (πœ‘ β†’ ((1 + 𝑇) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1) ↔ (1(abs ∘ βˆ’ )(1 + 𝑇)) < 1))
5548, 54mpbird 257 . . . . . . 7 (πœ‘ β†’ (1 + 𝑇) ∈ (1(ballβ€˜(abs ∘ βˆ’ ))1))
56 eqid 2733 . . . . . . . 8 (1(ballβ€˜(abs ∘ βˆ’ ))1) = (1(ballβ€˜(abs ∘ βˆ’ ))1)
5756logtayl2 26033 . . . . . . 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 5128 . . . . 5 (πœ‘ β†’ seq1( + , 𝐷) ⇝ (logβ€˜(1 + 𝑇)))
60 seqex 13914 . . . . . 6 seq1( + , 𝐹) ∈ V
6160a1i 11 . . . . 5 (πœ‘ β†’ seq1( + , 𝐹) ∈ V)
62 stirlinglem5.2 . . . . . . . 8 𝐸 = (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))
6362a1i 11 . . . . . . 7 (πœ‘ β†’ 𝐸 = (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗)))
6463seqeq3d 13920 . . . . . 6 (πœ‘ β†’ seq1( + , 𝐸) = seq1( + , (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))))
65 logtayl 26031 . . . . . . 7 ((𝑇 ∈ β„‚ ∧ (absβ€˜π‘‡) < 1) β†’ seq1( + , (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(logβ€˜(1 βˆ’ 𝑇)))
6614, 45, 65syl2anc 585 . . . . . 6 (πœ‘ β†’ seq1( + , (𝑗 ∈ β„• ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(logβ€˜(1 βˆ’ 𝑇)))
6764, 66eqbrtrd 5128 . . . . 5 (πœ‘ β†’ seq1( + , 𝐸) ⇝ -(logβ€˜(1 βˆ’ 𝑇)))
68 simpr 486 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
6968, 1eleqtrdi 2844 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
70 oveq1 7365 . . . . . . . . . 10 (𝑗 = 𝑛 β†’ (𝑗 βˆ’ 1) = (𝑛 βˆ’ 1))
7170oveq2d 7374 . . . . . . . . 9 (𝑗 = 𝑛 β†’ (-1↑(𝑗 βˆ’ 1)) = (-1↑(𝑛 βˆ’ 1)))
72 oveq2 7366 . . . . . . . . . 10 (𝑗 = 𝑛 β†’ (𝑇↑𝑗) = (𝑇↑𝑛))
73 id 22 . . . . . . . . . 10 (𝑗 = 𝑛 β†’ 𝑗 = 𝑛)
7472, 73oveq12d 7376 . . . . . . . . 9 (𝑗 = 𝑛 β†’ ((𝑇↑𝑗) / 𝑗) = ((𝑇↑𝑛) / 𝑛))
7571, 74oveq12d 7376 . . . . . . . 8 (𝑗 = 𝑛 β†’ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) = ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)))
76 elfznn 13476 . . . . . . . . 9 (𝑛 ∈ (1...π‘˜) β†’ 𝑛 ∈ β„•)
7776adantl 483 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 ∈ β„•)
78 1cnd 11155 . . . . . . . . . . . 12 (𝑛 ∈ β„• β†’ 1 ∈ β„‚)
7978negcld 11504 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ -1 ∈ β„‚)
80 nnm1nn0 12459 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ (𝑛 βˆ’ 1) ∈ β„•0)
8179, 80expcld 14057 . . . . . . . . . 10 (𝑛 ∈ β„• β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
8277, 81syl 17 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
8314ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑇 ∈ β„‚)
8477nnnn0d 12478 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 ∈ β„•0)
8583, 84expcld 14057 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (𝑇↑𝑛) ∈ β„‚)
8677nncnd 12174 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 ∈ β„‚)
8777nnne0d 12208 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ 𝑛 β‰  0)
8885, 86, 87divcld 11936 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ ((𝑇↑𝑛) / 𝑛) ∈ β„‚)
8982, 88mulcld 11180 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
903, 75, 77, 89fvmptd3 6972 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (π·β€˜π‘›) = ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)))
9190, 89eqeltrd 2834 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (π·β€˜π‘›) ∈ β„‚)
92 addcl 11138 . . . . . . 7 ((𝑛 ∈ β„‚ ∧ 𝑖 ∈ β„‚) β†’ (𝑛 + 𝑖) ∈ β„‚)
9392adantl 483 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (𝑛 ∈ β„‚ ∧ 𝑖 ∈ β„‚)) β†’ (𝑛 + 𝑖) ∈ β„‚)
9469, 91, 93seqcl 13934 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐷)β€˜π‘˜) ∈ β„‚)
9562, 74, 77, 88fvmptd3 6972 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (πΈβ€˜π‘›) = ((𝑇↑𝑛) / 𝑛))
9695, 88eqeltrd 2834 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (πΈβ€˜π‘›) ∈ β„‚)
9769, 96, 93seqcl 13934 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐸)β€˜π‘˜) ∈ β„‚)
98 simpll 766 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ πœ‘)
99 stirlinglem5.3 . . . . . . . . 9 𝐹 = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)))
10075, 74oveq12d 7376 . . . . . . . . 9 (𝑗 = 𝑛 β†’ (((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
101 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
10281adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
10314adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑇 ∈ β„‚)
104101nnnn0d 12478 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•0)
105103, 104expcld 14057 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑇↑𝑛) ∈ β„‚)
106101nncnd 12174 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„‚)
107101nnne0d 12208 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 β‰  0)
108105, 106, 107divcld 11936 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑇↑𝑛) / 𝑛) ∈ β„‚)
109102, 108mulcld 11180 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
110109, 108addcld 11179 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
11199, 100, 101, 110fvmptd3 6972 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
1123, 75, 101, 109fvmptd3 6972 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π·β€˜π‘›) = ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)))
113112eqcomd 2739 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) = (π·β€˜π‘›))
11462, 74, 101, 108fvmptd3 6972 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΈβ€˜π‘›) = ((𝑇↑𝑛) / 𝑛))
115114eqcomd 2739 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑇↑𝑛) / 𝑛) = (πΈβ€˜π‘›))
116113, 115oveq12d 7376 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((π·β€˜π‘›) + (πΈβ€˜π‘›)))
117111, 116eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = ((π·β€˜π‘›) + (πΈβ€˜π‘›)))
11898, 77, 117syl2anc 585 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...π‘˜)) β†’ (πΉβ€˜π‘›) = ((π·β€˜π‘›) + (πΈβ€˜π‘›)))
11969, 91, 96, 118seradd 13956 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) = ((seq1( + , 𝐷)β€˜π‘˜) + (seq1( + , 𝐸)β€˜π‘˜)))
1201, 2, 59, 61, 67, 94, 97, 119climadd 15520 . . . 4 (πœ‘ β†’ seq1( + , 𝐹) ⇝ ((logβ€˜(1 + 𝑇)) + -(logβ€˜(1 βˆ’ 𝑇))))
121 1rp 12924 . . . . . . . . 9 1 ∈ ℝ+
122121a1i 11 . . . . . . . 8 (πœ‘ β†’ 1 ∈ ℝ+)
123122, 12rpaddcld 12977 . . . . . . 7 (πœ‘ β†’ (1 + 𝑇) ∈ ℝ+)
124123rpne0d 12967 . . . . . 6 (πœ‘ β†’ (1 + 𝑇) β‰  0)
12531, 124logcld 25942 . . . . 5 (πœ‘ β†’ (logβ€˜(1 + 𝑇)) ∈ β„‚)
12630, 14subcld 11517 . . . . . 6 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ β„‚)
12713, 51absltd 15320 . . . . . . . . . 10 (πœ‘ β†’ ((absβ€˜π‘‡) < 1 ↔ (-1 < 𝑇 ∧ 𝑇 < 1)))
12845, 127mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (-1 < 𝑇 ∧ 𝑇 < 1))
129128simprd 497 . . . . . . . 8 (πœ‘ β†’ 𝑇 < 1)
13013, 129gtned 11295 . . . . . . 7 (πœ‘ β†’ 1 β‰  𝑇)
13130, 14, 130subne0d 11526 . . . . . 6 (πœ‘ β†’ (1 βˆ’ 𝑇) β‰  0)
132126, 131logcld 25942 . . . . 5 (πœ‘ β†’ (logβ€˜(1 βˆ’ 𝑇)) ∈ β„‚)
133125, 132negsubd 11523 . . . 4 (πœ‘ β†’ ((logβ€˜(1 + 𝑇)) + -(logβ€˜(1 βˆ’ 𝑇))) = ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
134120, 133breqtrd 5132 . . 3 (πœ‘ β†’ seq1( + , 𝐹) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
135 nn0uz 12810 . . . 4 β„•0 = (β„€β‰₯β€˜0)
136 0zd 12516 . . . 4 (πœ‘ β†’ 0 ∈ β„€)
137 stirlinglem5.5 . . . . . 6 𝐺 = (𝑗 ∈ β„•0 ↦ ((2 Β· 𝑗) + 1))
138 2nn0 12435 . . . . . . . . 9 2 ∈ β„•0
139138a1i 11 . . . . . . . 8 (𝑗 ∈ β„•0 β†’ 2 ∈ β„•0)
140 id 22 . . . . . . . 8 (𝑗 ∈ β„•0 β†’ 𝑗 ∈ β„•0)
141139, 140nn0mulcld 12483 . . . . . . 7 (𝑗 ∈ β„•0 β†’ (2 Β· 𝑗) ∈ β„•0)
142 nn0p1nn 12457 . . . . . . 7 ((2 Β· 𝑗) ∈ β„•0 β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
143141, 142syl 17 . . . . . 6 (𝑗 ∈ β„•0 β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
144137, 143fmpti 7061 . . . . 5 𝐺:β„•0βŸΆβ„•
145144a1i 11 . . . 4 (πœ‘ β†’ 𝐺:β„•0βŸΆβ„•)
146 2re 12232 . . . . . . . . 9 2 ∈ ℝ
147146a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 2 ∈ ℝ)
148 nn0re 12427 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ ℝ)
149147, 148remulcld 11190 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ ℝ)
150 1red 11161 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ 1 ∈ ℝ)
151148, 150readdcld 11189 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ ℝ)
152147, 151remulcld 11190 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2 Β· (π‘˜ + 1)) ∈ ℝ)
153 2rp 12925 . . . . . . . . 9 2 ∈ ℝ+
154153a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 2 ∈ ℝ+)
155148ltp1d 12090 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ π‘˜ < (π‘˜ + 1))
156148, 151, 154, 155ltmul2dd 13018 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) < (2 Β· (π‘˜ + 1)))
157149, 152, 150, 156ltadd1dd 11771 . . . . . 6 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) < ((2 Β· (π‘˜ + 1)) + 1))
158137a1i 11 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ 𝐺 = (𝑗 ∈ β„•0 ↦ ((2 Β· 𝑗) + 1)))
159 simpr 486 . . . . . . . . 9 ((π‘˜ ∈ β„•0 ∧ 𝑗 = π‘˜) β†’ 𝑗 = π‘˜)
160159oveq2d 7374 . . . . . . . 8 ((π‘˜ ∈ β„•0 ∧ 𝑗 = π‘˜) β†’ (2 Β· 𝑗) = (2 Β· π‘˜))
161160oveq1d 7373 . . . . . . 7 ((π‘˜ ∈ β„•0 ∧ 𝑗 = π‘˜) β†’ ((2 Β· 𝑗) + 1) = ((2 Β· π‘˜) + 1))
162 id 22 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„•0)
163 2cnd 12236 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ 2 ∈ β„‚)
164 nn0cn 12428 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
165163, 164mulcld 11180 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ β„‚)
166 1cnd 11155 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 1 ∈ β„‚)
167165, 166addcld 11179 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„‚)
168158, 161, 162, 167fvmptd 6956 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜π‘˜) = ((2 Β· π‘˜) + 1))
169 simpr 486 . . . . . . . . 9 ((π‘˜ ∈ β„•0 ∧ 𝑗 = (π‘˜ + 1)) β†’ 𝑗 = (π‘˜ + 1))
170169oveq2d 7374 . . . . . . . 8 ((π‘˜ ∈ β„•0 ∧ 𝑗 = (π‘˜ + 1)) β†’ (2 Β· 𝑗) = (2 Β· (π‘˜ + 1)))
171170oveq1d 7373 . . . . . . 7 ((π‘˜ ∈ β„•0 ∧ 𝑗 = (π‘˜ + 1)) β†’ ((2 Β· 𝑗) + 1) = ((2 Β· (π‘˜ + 1)) + 1))
172 peano2nn0 12458 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„•0)
173164, 166addcld 11179 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (π‘˜ + 1) ∈ β„‚)
174163, 173mulcld 11180 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (2 Β· (π‘˜ + 1)) ∈ β„‚)
175174, 166addcld 11179 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((2 Β· (π‘˜ + 1)) + 1) ∈ β„‚)
176158, 171, 172, 175fvmptd 6956 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜(π‘˜ + 1)) = ((2 Β· (π‘˜ + 1)) + 1))
177157, 168, 1763brtr4d 5138 . . . . 5 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜π‘˜) < (πΊβ€˜(π‘˜ + 1)))
178177adantl 483 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) < (πΊβ€˜(π‘˜ + 1)))
179 eldifi 4087 . . . . . . 7 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 𝑛 ∈ β„•)
180179adantl 483 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 ∈ β„•)
181 1cnd 11155 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 1 ∈ β„‚)
182181negcld 11504 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ -1 ∈ β„‚)
183179, 80syl 17 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 βˆ’ 1) ∈ β„•0)
184182, 183expcld 14057 . . . . . . . . 9 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
185184adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-1↑(𝑛 βˆ’ 1)) ∈ β„‚)
18614adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑇 ∈ β„‚)
187180nnnn0d 12478 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 ∈ β„•0)
188186, 187expcld 14057 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (𝑇↑𝑛) ∈ β„‚)
189180nncnd 12174 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 ∈ β„‚)
190180nnne0d 12208 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ 𝑛 β‰  0)
191188, 189, 190divcld 11936 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((𝑇↑𝑛) / 𝑛) ∈ β„‚)
192185, 191mulcld 11180 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
193192, 191addcld 11179 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ β„‚)
19499, 100, 180, 193fvmptd3 6972 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (πΉβ€˜π‘›) = (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
195 eldifn 4088 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ 𝑛 ∈ ran 𝐺)
196 0nn0 12433 . . . . . . . . . . . . . . . 16 0 ∈ β„•0
197 1nn0 12434 . . . . . . . . . . . . . . . . 17 1 ∈ β„•0
198138, 197num0h 12635 . . . . . . . . . . . . . . . 16 1 = ((2 Β· 0) + 1)
199 oveq2 7366 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 0 β†’ (2 Β· 𝑗) = (2 Β· 0))
200199oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (𝑗 = 0 β†’ ((2 Β· 𝑗) + 1) = ((2 Β· 0) + 1))
201200eqeq2d 2744 . . . . . . . . . . . . . . . . 17 (𝑗 = 0 β†’ (1 = ((2 Β· 𝑗) + 1) ↔ 1 = ((2 Β· 0) + 1)))
202201rspcev 3580 . . . . . . . . . . . . . . . 16 ((0 ∈ β„•0 ∧ 1 = ((2 Β· 0) + 1)) β†’ βˆƒπ‘— ∈ β„•0 1 = ((2 Β· 𝑗) + 1))
203196, 198, 202mp2an 691 . . . . . . . . . . . . . . 15 βˆƒπ‘— ∈ β„•0 1 = ((2 Β· 𝑗) + 1)
204 ax-1cn 11114 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
205137elrnmpt 5912 . . . . . . . . . . . . . . . 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 2822 . . . . . . . . . . . . 13 (𝑛 = 1 β†’ (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺))
210208, 209mpbird 257 . . . . . . . . . . . 12 (𝑛 = 1 β†’ 𝑛 ∈ ran 𝐺)
211195, 210nsyl 140 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ 𝑛 = 1)
212 nn1m1nn 12179 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (𝑛 = 1 ∨ (𝑛 βˆ’ 1) ∈ β„•))
213179, 212syl 17 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 = 1 ∨ (𝑛 βˆ’ 1) ∈ β„•))
214213ord 863 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (Β¬ 𝑛 = 1 β†’ (𝑛 βˆ’ 1) ∈ β„•))
215211, 214mpd 15 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 βˆ’ 1) ∈ β„•)
216 nfcv 2904 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗ℕ
217 nfmpt1 5214 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗(𝑗 ∈ β„•0 ↦ ((2 Β· 𝑗) + 1))
218137, 217nfcxfr 2902 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗𝐺
219218nfrn 5908 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗ran 𝐺
220216, 219nfdif 4086 . . . . . . . . . . . . . . . . 17 Ⅎ𝑗(β„• βˆ– ran 𝐺)
221220nfcri 2891 . . . . . . . . . . . . . . . 16 Ⅎ𝑗 𝑛 ∈ (β„• βˆ– ran 𝐺)
222137elrnmpt 5912 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 ∈ ran 𝐺 ↔ βˆƒπ‘— ∈ β„•0 𝑛 = ((2 Β· 𝑗) + 1)))
223195, 222mtbid 324 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ βˆƒπ‘— ∈ β„•0 𝑛 = ((2 Β· 𝑗) + 1))
224 ralnex 3072 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆ€π‘— ∈ β„•0 Β¬ 𝑛 = ((2 Β· 𝑗) + 1) ↔ Β¬ βˆƒπ‘— ∈ β„•0 𝑛 = ((2 Β· 𝑗) + 1))
225223, 224sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ βˆ€π‘— ∈ β„•0 Β¬ 𝑛 = ((2 Β· 𝑗) + 1))
226225r19.21bi 3233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„•0) β†’ Β¬ 𝑛 = ((2 Β· 𝑗) + 1))
227226neqned 2947 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„•0) β†’ 𝑛 β‰  ((2 Β· 𝑗) + 1))
228227necomd 2996 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
229228adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
230 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ β„€)
231 simpr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 𝑗 ∈ β„•0)
232179ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑛 ∈ β„•)
233146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 2 ∈ ℝ)
234 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ β„€)
235234zred 12612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ ℝ)
236233, 235remulcld 11190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 Β· 𝑗) ∈ ℝ)
237 0red 11163 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 0 ∈ ℝ)
238 1red 11161 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 1 ∈ ℝ)
239 2cnd 12236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 2 ∈ β„‚)
240235recnd 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 ∈ β„‚)
241239, 240mulcomd 11181 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 Β· 𝑗) = (𝑗 Β· 2))
242 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 𝑗 ∈ β„•0)
243 elnn0z 12517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ β„•0 ↔ (𝑗 ∈ β„€ ∧ 0 ≀ 𝑗))
244242, 243sylnib 328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ (𝑗 ∈ β„€ ∧ 0 ≀ 𝑗))
245 nan 829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ (𝑗 ∈ β„€ ∧ 0 ≀ 𝑗)) ↔ (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑗 ∈ β„€) β†’ Β¬ 0 ≀ 𝑗))
246244, 245mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑗 ∈ β„€) β†’ Β¬ 0 ≀ 𝑗)
247246anabss1 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 0 ≀ 𝑗)
248235, 237ltnled 11307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (𝑗 < 0 ↔ Β¬ 0 ≀ 𝑗))
249247, 248mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 𝑗 < 0)
250153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 2 ∈ ℝ+)
251250rpregt0d 12968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 ∈ ℝ ∧ 0 < 2))
252 mulltgt0 43315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ (𝑗 Β· 2) < 0)
253235, 249, 251, 252syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (𝑗 Β· 2) < 0)
254241, 253eqbrtrd 5128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (2 Β· 𝑗) < 0)
255236, 237, 238, 254ltadd1dd 11771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) < (0 + 1))
256 1cnd 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ 1 ∈ β„‚)
257256addid2d 11361 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (0 + 1) = 1)
258255, 257breqtrd 5132 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) < 1)
259236, 238readdcld 11189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) ∈ ℝ)
260259, 238ltnled 11307 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ (((2 Β· 𝑗) + 1) < 1 ↔ Β¬ 1 ≀ ((2 Β· 𝑗) + 1)))
261258, 260mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ 1 ≀ ((2 Β· 𝑗) + 1))
262 nnge1 12186 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 Β· 𝑗) + 1) ∈ β„• β†’ 1 ≀ ((2 Β· 𝑗) + 1))
263261, 262nsyl 140 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) β†’ Β¬ ((2 Β· 𝑗) + 1) ∈ β„•)
264263adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) β†’ Β¬ ((2 Β· 𝑗) + 1) ∈ β„•)
265 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ ((2 Β· 𝑗) + 1) = 𝑛)
266 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑛 ∈ β„• ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ 𝑛 ∈ β„•)
267265, 266eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ β„• ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
268267adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) ∧ ((2 Β· 𝑗) + 1) = 𝑛) β†’ ((2 Β· 𝑗) + 1) ∈ β„•)
269264, 268mtand 815 . . . . . . . . . . . . . . . . . . . . 21 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) β†’ Β¬ ((2 Β· 𝑗) + 1) = 𝑛)
270269neqned 2947 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 ∈ β„€ ∧ Β¬ 𝑗 ∈ β„•0) ∧ 𝑛 ∈ β„•) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
271230, 231, 232, 270syl21anc 837 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) ∧ Β¬ 𝑗 ∈ β„•0) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
272229, 271pm2.61dan 812 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) β†’ ((2 Β· 𝑗) + 1) β‰  𝑛)
273272neneqd 2945 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (β„• βˆ– ran 𝐺) ∧ 𝑗 ∈ β„€) β†’ Β¬ ((2 Β· 𝑗) + 1) = 𝑛)
274273ex 414 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑗 ∈ β„€ β†’ Β¬ ((2 Β· 𝑗) + 1) = 𝑛))
275221, 274ralrimi 3239 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ βˆ€π‘— ∈ β„€ Β¬ ((2 Β· 𝑗) + 1) = 𝑛)
276 ralnex 3072 . . . . . . . . . . . . . . 15 (βˆ€π‘— ∈ β„€ Β¬ ((2 Β· 𝑗) + 1) = 𝑛 ↔ Β¬ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛)
277275, 276sylib 217 . . . . . . . . . . . . . 14 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛)
278179nnzd 12531 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 𝑛 ∈ β„€)
279 odd2np1 16228 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„€ β†’ (Β¬ 2 βˆ₯ 𝑛 ↔ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛))
280278, 279syl 17 . . . . . . . . . . . . . 14 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (Β¬ 2 βˆ₯ 𝑛 ↔ βˆƒπ‘— ∈ β„€ ((2 Β· 𝑗) + 1) = 𝑛))
281277, 280mtbird 325 . . . . . . . . . . . . 13 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ Β¬ 2 βˆ₯ 𝑛)
282281notnotrd 133 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 2 βˆ₯ 𝑛)
283179nncnd 12174 . . . . . . . . . . . . 13 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 𝑛 ∈ β„‚)
284283, 181npcand 11521 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ ((𝑛 βˆ’ 1) + 1) = 𝑛)
285282, 284breqtrrd 5134 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ 2 βˆ₯ ((𝑛 βˆ’ 1) + 1))
286183nn0zd 12530 . . . . . . . . . . . 12 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (𝑛 βˆ’ 1) ∈ β„€)
287 oddp1even 16231 . . . . . . . . . . . 12 ((𝑛 βˆ’ 1) ∈ β„€ β†’ (Β¬ 2 βˆ₯ (𝑛 βˆ’ 1) ↔ 2 βˆ₯ ((𝑛 βˆ’ 1) + 1)))
288286, 287syl 17 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (Β¬ 2 βˆ₯ (𝑛 βˆ’ 1) ↔ 2 βˆ₯ ((𝑛 βˆ’ 1) + 1)))
289285, 288mpbird 257 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ Β¬ 2 βˆ₯ (𝑛 βˆ’ 1))
290 oexpneg 16232 . . . . . . . . . 10 ((1 ∈ β„‚ ∧ (𝑛 βˆ’ 1) ∈ β„• ∧ Β¬ 2 βˆ₯ (𝑛 βˆ’ 1)) β†’ (-1↑(𝑛 βˆ’ 1)) = -(1↑(𝑛 βˆ’ 1)))
291181, 215, 289, 290syl3anc 1372 . . . . . . . . 9 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (-1↑(𝑛 βˆ’ 1)) = -(1↑(𝑛 βˆ’ 1)))
292 1exp 14003 . . . . . . . . . . 11 ((𝑛 βˆ’ 1) ∈ β„€ β†’ (1↑(𝑛 βˆ’ 1)) = 1)
293286, 292syl 17 . . . . . . . . . 10 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (1↑(𝑛 βˆ’ 1)) = 1)
294293negeqd 11400 . . . . . . . . 9 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ -(1↑(𝑛 βˆ’ 1)) = -1)
295291, 294eqtrd 2773 . . . . . . . 8 (𝑛 ∈ (β„• βˆ– ran 𝐺) β†’ (-1↑(𝑛 βˆ’ 1)) = -1)
296295adantl 483 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-1↑(𝑛 βˆ’ 1)) = -1)
297296oveq1d 7373 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) = (-1 Β· ((𝑇↑𝑛) / 𝑛)))
298297oveq1d 7373 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (((-1↑(𝑛 βˆ’ 1)) Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((-1 Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)))
299191mulm1d 11612 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-1 Β· ((𝑇↑𝑛) / 𝑛)) = -((𝑇↑𝑛) / 𝑛))
300299oveq1d 7373 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1 Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛)))
301191negcld 11504 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ -((𝑇↑𝑛) / 𝑛) ∈ β„‚)
302301, 191addcomd 11362 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛)) = (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛)))
303191negidd 11507 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛)) = 0)
304300, 302, 3033eqtrd 2777 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ ((-1 Β· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = 0)
305194, 298, 3043eqtrd 2777 . . . 4 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– ran 𝐺)) β†’ (πΉβ€˜π‘›) = 0)
306111, 110eqeltrd 2834 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ β„‚)
30799a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐹 = (𝑗 ∈ β„• ↦ (((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗))))
308 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ 𝑗 = ((2 Β· π‘˜) + 1))
309308oveq1d 7373 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ (𝑗 βˆ’ 1) = (((2 Β· π‘˜) + 1) βˆ’ 1))
310309oveq2d 7374 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ (-1↑(𝑗 βˆ’ 1)) = (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)))
311308oveq2d 7374 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ (𝑇↑𝑗) = (𝑇↑((2 Β· π‘˜) + 1)))
312311, 308oveq12d 7376 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ ((𝑇↑𝑗) / 𝑗) = ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
313310, 312oveq12d 7376 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = ((2 Β· π‘˜) + 1)) β†’ ((-1↑(𝑗 βˆ’ 1)) Β· ((𝑇↑𝑗) / 𝑗)) = ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
314313, 312oveq12d 7376 . . . . . . 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 486 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„•0)
317315, 316nn0mulcld 12483 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ β„•0)
318 nn0p1nn 12457 . . . . . . . 8 ((2 Β· π‘˜) ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
319317, 318syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
320166negcld 11504 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ -1 ∈ β„‚)
321165, 166pncand 11518 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) βˆ’ 1) = (2 Β· π‘˜))
322138a1i 11 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ 2 ∈ β„•0)
323322, 162nn0mulcld 12483 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ β„•0)
324321, 323eqeltrd 2834 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) βˆ’ 1) ∈ β„•0)
325320, 324expcld 14057 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) ∈ β„‚)
326325adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) ∈ β„‚)
32714adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝑇 ∈ β„‚)
328197a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„•0)
329317, 328nn0addcld 12482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
330327, 329expcld 14057 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (𝑇↑((2 Β· π‘˜) + 1)) ∈ β„‚)
331 2cnd 12236 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 2 ∈ β„‚)
332164adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ β„‚)
333331, 332mulcld 11180 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ β„‚)
334 1cnd 11155 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ β„‚)
335333, 334addcld 11179 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) ∈ β„‚)
336 0red 11163 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ∈ ℝ)
337146a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 2 ∈ ℝ)
338148adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ π‘˜ ∈ ℝ)
339337, 338remulcld 11190 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ ℝ)
340 1red 11161 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 1 ∈ ℝ)
341 0le2 12260 . . . . . . . . . . . . . 14 0 ≀ 2
342341a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ 2)
343316nn0ge0d 12481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ π‘˜)
344337, 338, 342, 343mulge0d 11737 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 ≀ (2 Β· π‘˜))
345 0lt1 11682 . . . . . . . . . . . . 13 0 < 1
346345a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 < 1)
347339, 340, 344, 346addgegt0d 11733 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 0 < ((2 Β· π‘˜) + 1))
348336, 347gtned 11295 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((2 Β· π‘˜) + 1) β‰  0)
349330, 335, 348divcld 11936 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) ∈ β„‚)
350326, 349mulcld 11180 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) ∈ β„‚)
351350, 349addcld 11179 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) ∈ β„‚)
352307, 314, 319, 351fvmptd 6956 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜((2 Β· π‘˜) + 1)) = (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
353321adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((2 Β· π‘˜) + 1) βˆ’ 1) = (2 Β· π‘˜))
354353oveq2d 7374 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) = (-1↑(2 Β· π‘˜)))
355 nn0z 12529 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
356 m1expeven 14021 . . . . . . . . . . . . 13 (π‘˜ ∈ β„€ β†’ (-1↑(2 Β· π‘˜)) = 1)
357355, 356syl 17 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = 1)
358357adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(2 Β· π‘˜)) = 1)
359354, 358eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) = 1)
360359oveq1d 7373 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (1 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
361349mulid2d 11178 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
362360, 361eqtrd 2773 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
363362oveq1d 7373 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
3643492timesd 12401 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
365330, 335, 348divrec2d 11940 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)) = ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1))))
366365oveq2d 7374 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
367363, 364, 3663eqtr2d 2779 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (((-1↑(((2 Β· π‘˜) + 1) βˆ’ 1)) Β· ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) + ((𝑇↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
368352, 367eqtr2d 2774 . . . . 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 486 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ 𝑗 = π‘˜)
372371oveq2d 7374 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (2 Β· 𝑗) = (2 Β· π‘˜))
373372oveq1d 7373 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ ((2 Β· 𝑗) + 1) = ((2 Β· π‘˜) + 1))
374373oveq2d 7374 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (1 / ((2 Β· 𝑗) + 1)) = (1 / ((2 Β· π‘˜) + 1)))
375373oveq2d 7374 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (𝑇↑((2 Β· 𝑗) + 1)) = (𝑇↑((2 Β· π‘˜) + 1)))
376374, 375oveq12d 7376 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ ((1 / ((2 Β· 𝑗) + 1)) Β· (𝑇↑((2 Β· 𝑗) + 1))) = ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1))))
377376oveq2d 7374 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•0) ∧ 𝑗 = π‘˜) β†’ (2 Β· ((1 / ((2 Β· 𝑗) + 1)) Β· (𝑇↑((2 Β· 𝑗) + 1)))) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
378335, 348reccld 11929 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (1 / ((2 Β· π‘˜) + 1)) ∈ β„‚)
379378, 330mulcld 11180 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1))) ∈ β„‚)
380331, 379mulcld 11180 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))) ∈ β„‚)
381370, 377, 316, 380fvmptd 6956 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = (2 Β· ((1 / ((2 Β· π‘˜) + 1)) Β· (𝑇↑((2 Β· π‘˜) + 1)))))
382197a1i 11 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ 1 ∈ β„•0)
383323, 382nn0addcld 12482 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
384158, 161, 162, 383fvmptd 6956 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (πΊβ€˜π‘˜) = ((2 Β· π‘˜) + 1))
385384adantl 483 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) = ((2 Β· π‘˜) + 1))
386385fveq2d 6847 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜(πΊβ€˜π‘˜)) = (πΉβ€˜((2 Β· π‘˜) + 1)))
387368, 381, 3863eqtr4d 2783 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = (πΉβ€˜(πΊβ€˜π‘˜)))
388135, 1, 136, 2, 145, 178, 305, 306, 387isercoll2 15559 . . 3 (πœ‘ β†’ (seq0( + , 𝐻) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))) ↔ seq1( + , 𝐹) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇)))))
389134, 388mpbird 257 . 2 (πœ‘ β†’ seq0( + , 𝐻) ⇝ ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
39051, 13resubcld 11588 . . . 4 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ ℝ)
39114subidd 11505 . . . . . 6 (πœ‘ β†’ (𝑇 βˆ’ 𝑇) = 0)
392391eqcomd 2739 . . . . 5 (πœ‘ β†’ 0 = (𝑇 βˆ’ 𝑇))
39313, 51, 13, 129ltsub1dd 11772 . . . . 5 (πœ‘ β†’ (𝑇 βˆ’ 𝑇) < (1 βˆ’ 𝑇))
394392, 393eqbrtrd 5128 . . . 4 (πœ‘ β†’ 0 < (1 βˆ’ 𝑇))
395390, 394elrpd 12959 . . 3 (πœ‘ β†’ (1 βˆ’ 𝑇) ∈ ℝ+)
396123, 395relogdivd 25997 . 2 (πœ‘ β†’ (logβ€˜((1 + 𝑇) / (1 βˆ’ 𝑇))) = ((logβ€˜(1 + 𝑇)) βˆ’ (logβ€˜(1 βˆ’ 𝑇))))
397389, 396breqtrrd 5134 1 (πœ‘ β†’ seq0( + , 𝐻) ⇝ (logβ€˜((1 + 𝑇) / (1 βˆ’ 𝑇))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444   βˆ– cdif 3908   class class class wbr 5106   ↦ cmpt 5189  ran crn 5635   ∘ ccom 5638  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061  β„*cxr 11193   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390  -cneg 11391   / cdiv 11817  β„•cn 12158  2c2 12213  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„+crp 12920  ...cfz 13430  seqcseq 13912  β†‘cexp 13973  abscabs 15125   ⇝ cli 15372   βˆ₯ cdvds 16141  βˆžMetcxmet 20797  ballcbl 20799  logclog 25926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-xnn0 12491  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-sum 15577  df-ef 15955  df-sin 15957  df-cos 15958  df-tan 15959  df-pi 15960  df-dvds 16142  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-ulm 25752  df-log 25928
This theorem is referenced by:  stirlinglem6  44406
  Copyright terms: Public domain W3C validator