Step | Hyp | Ref
| Expression |
1 | | nnuz 12477 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12208 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | stirlinglem5.1 |
. . . . . . . . 9
⊢ 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗))) |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)))) |
5 | | 1cnd 10828 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
6 | 5 | negcld 11176 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → -1 ∈
ℂ) |
7 | | nnm1nn0 12131 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
8 | 7 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 − 1) ∈
ℕ0) |
9 | 6, 8 | expcld 13716 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (-1↑(𝑗 − 1)) ∈
ℂ) |
10 | | nncn 11838 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
11 | 10 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℂ) |
12 | | stirlinglem5.6 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
13 | 12 | rpred 12628 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ ℝ) |
14 | 13 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ ℂ) |
15 | 14 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ) |
16 | | nnnn0 12097 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
17 | 16 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
18 | 15, 17 | expcld 13716 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇↑𝑗) ∈ ℂ) |
19 | | nnne0 11864 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ≠ 0) |
20 | 19 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ≠ 0) |
21 | 9, 11, 18, 20 | div32d 11631 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇↑𝑗)) = ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗))) |
22 | 5, 15 | pncan2d 11191 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((1 + 𝑇) − 1) = 𝑇) |
23 | 22 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 = ((1 + 𝑇) − 1)) |
24 | 23 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇↑𝑗) = (((1 + 𝑇) − 1)↑𝑗)) |
25 | 24 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇↑𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))) |
26 | 21, 25 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))) |
27 | 26 | mpteq2dva 5150 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) |
28 | 4, 27 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) |
29 | 28 | seqeq3d 13582 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐷) = seq1( + , (𝑗 ∈ ℕ ↦
(((-1↑(𝑗 − 1)) /
𝑗) · (((1 + 𝑇) − 1)↑𝑗))))) |
30 | | 1cnd 10828 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
31 | 30, 14 | addcld 10852 |
. . . . . . . . . 10
⊢ (𝜑 → (1 + 𝑇) ∈ ℂ) |
32 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
33 | 32 | cnmetdval 23668 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (1 + 𝑇) ∈ ℂ) → (1(abs ∘
− )(1 + 𝑇)) =
(abs‘(1 − (1 + 𝑇)))) |
34 | 30, 31, 33 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (1(abs ∘ − )(1
+ 𝑇)) = (abs‘(1
− (1 + 𝑇)))) |
35 | | 1m1e0 11902 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 − 1) =
0) |
37 | 36 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 − 1) −
𝑇) = (0 − 𝑇)) |
38 | 30, 30, 14 | subsub4d 11220 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 − 1) −
𝑇) = (1 − (1 + 𝑇))) |
39 | | df-neg 11065 |
. . . . . . . . . . . . . 14
⊢ -𝑇 = (0 − 𝑇) |
40 | 39 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ (0
− 𝑇) = -𝑇 |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 𝑇) = -𝑇) |
42 | 37, 38, 41 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 − (1 + 𝑇)) = -𝑇) |
43 | 42 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(1 − (1 +
𝑇))) = (abs‘-𝑇)) |
44 | 14 | absnegd 15013 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘-𝑇) = (abs‘𝑇)) |
45 | | stirlinglem5.7 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑇) < 1) |
46 | 44, 45 | eqbrtrd 5075 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘-𝑇) < 1) |
47 | 43, 46 | eqbrtrd 5075 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(1 − (1 +
𝑇))) <
1) |
48 | 34, 47 | eqbrtrd 5075 |
. . . . . . . 8
⊢ (𝜑 → (1(abs ∘ − )(1
+ 𝑇)) <
1) |
49 | | cnxmet 23670 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
51 | | 1red 10834 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
52 | 51 | rexrd 10883 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ*) |
53 | | elbl2 23288 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ)) → ((1 + 𝑇) ∈ (1(ball‘(abs
∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1)) |
54 | 50, 52, 30, 31, 53 | syl22anc 839 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ −
))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1)) |
55 | 48, 54 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑇) ∈ (1(ball‘(abs ∘ −
))1)) |
56 | | eqid 2737 |
. . . . . . . 8
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
57 | 56 | logtayl2 25550 |
. . . . . . 7
⊢ ((1 +
𝑇) ∈
(1(ball‘(abs ∘ − ))1) → seq1( + , (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) ⇝ (log‘(1 +
𝑇))) |
58 | 55, 57 | syl 17 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦
(((-1↑(𝑗 − 1)) /
𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) ⇝ (log‘(1 +
𝑇))) |
59 | 29, 58 | eqbrtrd 5075 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐷) ⇝ (log‘(1 + 𝑇))) |
60 | | seqex 13576 |
. . . . . 6
⊢ seq1( + ,
𝐹) ∈
V |
61 | 60 | a1i 11 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐹) ∈ V) |
62 | | stirlinglem5.2 |
. . . . . . . 8
⊢ 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗)) |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))) |
64 | 63 | seqeq3d 13582 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐸) = seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗)))) |
65 | | logtayl 25548 |
. . . . . . 7
⊢ ((𝑇 ∈ ℂ ∧
(abs‘𝑇) < 1)
→ seq1( + , (𝑗 ∈
ℕ ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇))) |
66 | 14, 45, 65 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇))) |
67 | 64, 66 | eqbrtrd 5075 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐸) ⇝ -(log‘(1 −
𝑇))) |
68 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
69 | 68, 1 | eleqtrdi 2848 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
70 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1)) |
71 | 70 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → (-1↑(𝑗 − 1)) = (-1↑(𝑛 − 1))) |
72 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → (𝑇↑𝑗) = (𝑇↑𝑛)) |
73 | | id 22 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → 𝑗 = 𝑛) |
74 | 72, 73 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → ((𝑇↑𝑗) / 𝑗) = ((𝑇↑𝑛) / 𝑛)) |
75 | 71, 74 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝑗 = 𝑛 → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
76 | | elfznn 13141 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
77 | 76 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ) |
78 | | 1cnd 10828 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
79 | 78 | negcld 11176 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → -1 ∈
ℂ) |
80 | | nnm1nn0 12131 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
81 | 79, 80 | expcld 13716 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(-1↑(𝑛 − 1))
∈ ℂ) |
82 | 77, 81 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (-1↑(𝑛 − 1)) ∈ ℂ) |
83 | 14 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑇 ∈ ℂ) |
84 | 77 | nnnn0d 12150 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ0) |
85 | 83, 84 | expcld 13716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑇↑𝑛) ∈ ℂ) |
86 | 77 | nncnd 11846 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℂ) |
87 | 77 | nnne0d 11880 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ≠ 0) |
88 | 85, 86, 87 | divcld 11608 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
89 | 82, 88 | mulcld 10853 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
90 | 3, 75, 77, 89 | fvmptd3 6841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷‘𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
91 | 90, 89 | eqeltrd 2838 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷‘𝑛) ∈ ℂ) |
92 | | addcl 10811 |
. . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ) |
93 | 92 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ) |
94 | 69, 91, 93 | seqcl 13596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐷)‘𝑘) ∈ ℂ) |
95 | 62, 74, 77, 88 | fvmptd3 6841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸‘𝑛) = ((𝑇↑𝑛) / 𝑛)) |
96 | 95, 88 | eqeltrd 2838 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸‘𝑛) ∈ ℂ) |
97 | 69, 96, 93 | seqcl 13596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐸)‘𝑘) ∈ ℂ) |
98 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑) |
99 | | stirlinglem5.3 |
. . . . . . . . 9
⊢ 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗))) |
100 | 75, 74 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
101 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
102 | 81 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈
ℂ) |
103 | 14 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 ∈ ℂ) |
104 | 101 | nnnn0d 12150 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
105 | 103, 104 | expcld 13716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇↑𝑛) ∈ ℂ) |
106 | 101 | nncnd 11846 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
107 | 101 | nnne0d 11880 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
108 | 105, 106,
107 | divcld 11608 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
109 | 102, 108 | mulcld 10853 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
110 | 109, 108 | addcld 10852 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
111 | 99, 100, 101, 110 | fvmptd3 6841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
112 | 3, 75, 101, 109 | fvmptd3 6841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
113 | 112 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) = (𝐷‘𝑛)) |
114 | 62, 74, 101, 108 | fvmptd3 6841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) = ((𝑇↑𝑛) / 𝑛)) |
115 | 114 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇↑𝑛) / 𝑛) = (𝐸‘𝑛)) |
116 | 113, 115 | oveq12d 7231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((𝐷‘𝑛) + (𝐸‘𝑛))) |
117 | 111, 116 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ((𝐷‘𝑛) + (𝐸‘𝑛))) |
118 | 98, 77, 117 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐹‘𝑛) = ((𝐷‘𝑛) + (𝐸‘𝑛))) |
119 | 69, 91, 96, 118 | seradd 13618 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = ((seq1( + , 𝐷)‘𝑘) + (seq1( + , 𝐸)‘𝑘))) |
120 | 1, 2, 59, 61, 67, 94, 97, 119 | climadd 15193 |
. . . 4
⊢ (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) + -(log‘(1 −
𝑇)))) |
121 | | 1rp 12590 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
122 | 121 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ+) |
123 | 122, 12 | rpaddcld 12643 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑇) ∈
ℝ+) |
124 | 123 | rpne0d 12633 |
. . . . . 6
⊢ (𝜑 → (1 + 𝑇) ≠ 0) |
125 | 31, 124 | logcld 25459 |
. . . . 5
⊢ (𝜑 → (log‘(1 + 𝑇)) ∈
ℂ) |
126 | 30, 14 | subcld 11189 |
. . . . . 6
⊢ (𝜑 → (1 − 𝑇) ∈
ℂ) |
127 | 13, 51 | absltd 14993 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝑇) < 1 ↔ (-1 < 𝑇 ∧ 𝑇 < 1))) |
128 | 45, 127 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (-1 < 𝑇 ∧ 𝑇 < 1)) |
129 | 128 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 < 1) |
130 | 13, 129 | gtned 10967 |
. . . . . . 7
⊢ (𝜑 → 1 ≠ 𝑇) |
131 | 30, 14, 130 | subne0d 11198 |
. . . . . 6
⊢ (𝜑 → (1 − 𝑇) ≠ 0) |
132 | 126, 131 | logcld 25459 |
. . . . 5
⊢ (𝜑 → (log‘(1 −
𝑇)) ∈
ℂ) |
133 | 125, 132 | negsubd 11195 |
. . . 4
⊢ (𝜑 → ((log‘(1 + 𝑇)) + -(log‘(1 −
𝑇))) = ((log‘(1 +
𝑇)) − (log‘(1
− 𝑇)))) |
134 | 120, 133 | breqtrd 5079 |
. . 3
⊢ (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇)))) |
135 | | nn0uz 12476 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
136 | | 0zd 12188 |
. . . 4
⊢ (𝜑 → 0 ∈
ℤ) |
137 | | stirlinglem5.5 |
. . . . . 6
⊢ 𝐺 = (𝑗 ∈ ℕ0 ↦ ((2
· 𝑗) +
1)) |
138 | | 2nn0 12107 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
139 | 138 | a1i 11 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ 2 ∈ ℕ0) |
140 | | id 22 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℕ0) |
141 | 139, 140 | nn0mulcld 12155 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ (2 · 𝑗)
∈ ℕ0) |
142 | | nn0p1nn 12129 |
. . . . . . 7
⊢ ((2
· 𝑗) ∈
ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ) |
143 | 141, 142 | syl 17 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0
→ ((2 · 𝑗) + 1)
∈ ℕ) |
144 | 137, 143 | fmpti 6929 |
. . . . 5
⊢ 𝐺:ℕ0⟶ℕ |
145 | 144 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺:ℕ0⟶ℕ) |
146 | | 2re 11904 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
147 | 146 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℝ) |
148 | | nn0re 12099 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
149 | 147, 148 | remulcld 10863 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℝ) |
150 | | 1red 10834 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℝ) |
151 | 148, 150 | readdcld 10862 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
152 | 147, 151 | remulcld 10863 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2 · (𝑘 + 1))
∈ ℝ) |
153 | | 2rp 12591 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
154 | 153 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℝ+) |
155 | 148 | ltp1d 11762 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 < (𝑘 + 1)) |
156 | 148, 151,
154, 155 | ltmul2dd 12684 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘) <
(2 · (𝑘 +
1))) |
157 | 149, 152,
150, 156 | ltadd1dd 11443 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
< ((2 · (𝑘 + 1))
+ 1)) |
158 | 137 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝐺 = (𝑗 ∈ ℕ0
↦ ((2 · 𝑗) +
1))) |
159 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) |
160 | 159 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘)) |
161 | 160 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1)) |
162 | | id 22 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) |
163 | | 2cnd 11908 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℂ) |
164 | | nn0cn 12100 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
165 | 163, 164 | mulcld 10853 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℂ) |
166 | | 1cnd 10828 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℂ) |
167 | 165, 166 | addcld 10852 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℂ) |
168 | 158, 161,
162, 167 | fvmptd 6825 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = ((2 · 𝑘) + 1)) |
169 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = (𝑘 + 1)) → 𝑗 = (𝑘 + 1)) |
170 | 169 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = (𝑘 + 1)) → (2 · 𝑗) = (2 · (𝑘 + 1))) |
171 | 170 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = (𝑘 + 1)) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1)) |
172 | | peano2nn0 12130 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
173 | 164, 166 | addcld 10852 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) |
174 | 163, 173 | mulcld 10853 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (2 · (𝑘 + 1))
∈ ℂ) |
175 | 174, 166 | addcld 10852 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((2 · (𝑘 +
1)) + 1) ∈ ℂ) |
176 | 158, 171,
172, 175 | fvmptd 6825 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) + 1)) |
177 | 157, 168,
176 | 3brtr4d 5085 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
178 | 177 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
179 | | eldifi 4041 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 𝑛 ∈
ℕ) |
180 | 179 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ) |
181 | | 1cnd 10828 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 1 ∈
ℂ) |
182 | 181 | negcld 11176 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → -1 ∈
ℂ) |
183 | 179, 80 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 − 1) ∈
ℕ0) |
184 | 182, 183 | expcld 13716 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (-1↑(𝑛 − 1)) ∈
ℂ) |
185 | 184 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) ∈
ℂ) |
186 | 14 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑇 ∈ ℂ) |
187 | 180 | nnnn0d 12150 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ0) |
188 | 186, 187 | expcld 13716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝑇↑𝑛) ∈ ℂ) |
189 | 180 | nncnd 11846 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℂ) |
190 | 180 | nnne0d 11880 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ≠ 0) |
191 | 188, 189,
190 | divcld 11608 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
192 | 185, 191 | mulcld 10853 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
193 | 192, 191 | addcld 10852 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
194 | 99, 100, 180, 193 | fvmptd3 6841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹‘𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
195 | | eldifn 4042 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ 𝑛 ∈ ran 𝐺) |
196 | | 0nn0 12105 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 |
197 | | 1nn0 12106 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ0 |
198 | 138, 197 | num0h 12305 |
. . . . . . . . . . . . . . . 16
⊢ 1 = ((2
· 0) + 1) |
199 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 0 → (2 · 𝑗) = (2 ·
0)) |
200 | 199 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 0 → ((2 · 𝑗) + 1) = ((2 · 0) +
1)) |
201 | 200 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 0 → (1 = ((2 ·
𝑗) + 1) ↔ 1 = ((2
· 0) + 1))) |
202 | 201 | rspcev 3537 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℕ0 ∧ 1 = ((2 · 0) + 1)) → ∃𝑗 ∈ ℕ0 1 =
((2 · 𝑗) +
1)) |
203 | 196, 198,
202 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢
∃𝑗 ∈
ℕ0 1 = ((2 · 𝑗) + 1) |
204 | | ax-1cn 10787 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
205 | 137 | elrnmpt 5825 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℂ → (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 ·
𝑗) + 1))) |
206 | 204, 205 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 =
((2 · 𝑗) +
1)) |
207 | 203, 206 | mpbir 234 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ran 𝐺 |
208 | 207 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → 1 ∈ ran 𝐺) |
209 | | eleq1 2825 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺)) |
210 | 208, 209 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → 𝑛 ∈ ran 𝐺) |
211 | 195, 210 | nsyl 142 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ 𝑛 = 1) |
212 | | nn1m1nn 11851 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ)) |
213 | 179, 212 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ)) |
214 | 213 | ord 864 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (¬ 𝑛 = 1 → (𝑛 − 1) ∈ ℕ)) |
215 | 211, 214 | mpd 15 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 − 1) ∈
ℕ) |
216 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗ℕ |
217 | | nfmpt1 5153 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗(𝑗 ∈ ℕ0 ↦ ((2
· 𝑗) +
1)) |
218 | 137, 217 | nfcxfr 2902 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝐺 |
219 | 218 | nfrn 5821 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗ran
𝐺 |
220 | 216, 219 | nfdif 4040 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(ℕ ∖ ran 𝐺) |
221 | 220 | nfcri 2891 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗 𝑛 ∈ (ℕ ∖ ran
𝐺) |
222 | 137 | elrnmpt 5825 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))) |
223 | 195, 222 | mtbid 327 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬
∃𝑗 ∈
ℕ0 𝑛 = ((2
· 𝑗) +
1)) |
224 | | ralnex 3158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑗 ∈
ℕ0 ¬ 𝑛
= ((2 · 𝑗) + 1)
↔ ¬ ∃𝑗
∈ ℕ0 𝑛 = ((2 · 𝑗) + 1)) |
225 | 223, 224 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ∀𝑗 ∈ ℕ0
¬ 𝑛 = ((2 ·
𝑗) + 1)) |
226 | 225 | r19.21bi 3130 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℕ0) → ¬
𝑛 = ((2 · 𝑗) + 1)) |
227 | 226 | neqned 2947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℕ0) → 𝑛 ≠ ((2 · 𝑗) + 1)) |
228 | 227 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℕ0) → ((2
· 𝑗) + 1) ≠ 𝑛) |
229 | 228 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ 𝑗 ∈ ℕ0) → ((2
· 𝑗) + 1) ≠ 𝑛) |
230 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ 𝑗 ∈
ℤ) |
231 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ ¬ 𝑗 ∈
ℕ0) |
232 | 179 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ 𝑛 ∈
ℕ) |
233 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 2 ∈ ℝ) |
234 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 ∈ ℤ) |
235 | 234 | zred 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 ∈ ℝ) |
236 | 233, 235 | remulcld 10863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 · 𝑗) ∈ ℝ) |
237 | | 0red 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 0 ∈ ℝ) |
238 | | 1red 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 1 ∈ ℝ) |
239 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 2 ∈ ℂ) |
240 | 235 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 ∈ ℂ) |
241 | 239, 240 | mulcomd 10854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 · 𝑗) = (𝑗 · 2)) |
242 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ 𝑗 ∈ ℕ0) |
243 | | elnn0z 12189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑗 ∈ ℕ0
↔ (𝑗 ∈ ℤ
∧ 0 ≤ 𝑗)) |
244 | 242, 243 | sylnib 331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) |
245 | | nan 830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) ↔ (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0)
∧ 𝑗 ∈ ℤ)
→ ¬ 0 ≤ 𝑗)) |
246 | 244, 245 | mpbi 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗) |
247 | 246 | anabss1 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ 0 ≤ 𝑗) |
248 | 235, 237 | ltnled 10979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (𝑗 < 0 ↔ ¬ 0 ≤ 𝑗)) |
249 | 247, 248 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 < 0) |
250 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 2 ∈ ℝ+) |
251 | 250 | rpregt0d 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 ∈ ℝ ∧ 0 < 2)) |
252 | | mulltgt0 42238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ
∧ 0 < 2)) → (𝑗
· 2) < 0) |
253 | 235, 249,
251, 252 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (𝑗 · 2) < 0) |
254 | 241, 253 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 · 𝑗) < 0) |
255 | 236, 237,
238, 254 | ltadd1dd 11443 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ((2 · 𝑗) + 1) < (0 + 1)) |
256 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 1 ∈ ℂ) |
257 | 256 | addid2d 11033 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (0 + 1) = 1) |
258 | 255, 257 | breqtrd 5079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ((2 · 𝑗) + 1) < 1) |
259 | 236, 238 | readdcld 10862 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ((2 · 𝑗) + 1) ∈ ℝ) |
260 | 259, 238 | ltnled 10979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (((2 · 𝑗) + 1) < 1 ↔ ¬ 1 ≤ ((2
· 𝑗) +
1))) |
261 | 258, 260 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ 1 ≤ ((2 · 𝑗) + 1)) |
262 | | nnge1 11858 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑗) + 1) ∈
ℕ → 1 ≤ ((2 · 𝑗) + 1)) |
263 | 261, 262 | nsyl 142 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ ((2 · 𝑗) + 1) ∈ ℕ) |
264 | 263 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 ·
𝑗) + 1) ∈
ℕ) |
265 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℕ ∧ ((2
· 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) = 𝑛) |
266 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℕ ∧ ((2
· 𝑗) + 1) = 𝑛) → 𝑛 ∈ ℕ) |
267 | 265, 266 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ ℕ ∧ ((2
· 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈
ℕ) |
268 | 267 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ) |
269 | 264, 268 | mtand 816 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 ·
𝑗) + 1) = 𝑛) |
270 | 269 | neqned 2947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ((2 · 𝑗) + 1) ≠ 𝑛) |
271 | 230, 231,
232, 270 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ ((2 · 𝑗) + 1)
≠ 𝑛) |
272 | 229, 271 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) → ((2 · 𝑗) + 1) ≠ 𝑛) |
273 | 272 | neneqd 2945 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) → ¬ ((2 ·
𝑗) + 1) = 𝑛) |
274 | 273 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑗 ∈ ℤ → ¬ ((2
· 𝑗) + 1) = 𝑛)) |
275 | 221, 274 | ralrimi 3137 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ∀𝑗 ∈ ℤ ¬ ((2
· 𝑗) + 1) = 𝑛) |
276 | | ralnex 3158 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑗 ∈
ℤ ¬ ((2 · 𝑗) + 1) = 𝑛 ↔ ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛) |
277 | 275, 276 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬
∃𝑗 ∈ ℤ ((2
· 𝑗) + 1) = 𝑛) |
278 | 179 | nnzd 12281 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 𝑛 ∈
ℤ) |
279 | | odd2np1 15902 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (¬ 2
∥ 𝑛 ↔
∃𝑗 ∈ ℤ ((2
· 𝑗) + 1) = 𝑛)) |
280 | 278, 279 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (¬ 2 ∥
𝑛 ↔ ∃𝑗 ∈ ℤ ((2 ·
𝑗) + 1) = 𝑛)) |
281 | 277, 280 | mtbird 328 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ ¬ 2
∥ 𝑛) |
282 | 281 | notnotrd 135 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 2 ∥ 𝑛) |
283 | 179 | nncnd 11846 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 𝑛 ∈
ℂ) |
284 | 283, 181 | npcand 11193 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ((𝑛 − 1) + 1) = 𝑛) |
285 | 282, 284 | breqtrrd 5081 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 2 ∥ ((𝑛 − 1) +
1)) |
286 | 183 | nn0zd 12280 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 − 1) ∈
ℤ) |
287 | | oddp1even 15905 |
. . . . . . . . . . . 12
⊢ ((𝑛 − 1) ∈ ℤ
→ (¬ 2 ∥ (𝑛
− 1) ↔ 2 ∥ ((𝑛 − 1) + 1))) |
288 | 286, 287 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (¬ 2 ∥
(𝑛 − 1) ↔ 2
∥ ((𝑛 − 1) +
1))) |
289 | 285, 288 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ 2 ∥
(𝑛 −
1)) |
290 | | oexpneg 15906 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝑛
− 1) ∈ ℕ ∧ ¬ 2 ∥ (𝑛 − 1)) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1))) |
291 | 181, 215,
289, 290 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1))) |
292 | | 1exp 13664 |
. . . . . . . . . . 11
⊢ ((𝑛 − 1) ∈ ℤ
→ (1↑(𝑛 −
1)) = 1) |
293 | 286, 292 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (1↑(𝑛 − 1)) =
1) |
294 | 293 | negeqd 11072 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → -(1↑(𝑛 − 1)) =
-1) |
295 | 291, 294 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (-1↑(𝑛 − 1)) =
-1) |
296 | 295 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) =
-1) |
297 | 296 | oveq1d 7228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) = (-1 · ((𝑇↑𝑛) / 𝑛))) |
298 | 297 | oveq1d 7228 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((-1 · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
299 | 191 | mulm1d 11284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1 · ((𝑇↑𝑛) / 𝑛)) = -((𝑇↑𝑛) / 𝑛)) |
300 | 299 | oveq1d 7228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛))) |
301 | 191 | negcld 11176 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → -((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
302 | 301, 191 | addcomd 11034 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛)) = (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛))) |
303 | 191 | negidd 11179 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛)) = 0) |
304 | 300, 302,
303 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = 0) |
305 | 194, 298,
304 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
306 | 111, 110 | eqeltrd 2838 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℂ) |
307 | 99 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)))) |
308 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → 𝑗 = ((2 · 𝑘) + 1)) |
309 | 308 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑗 − 1) = (((2 ·
𝑘) + 1) −
1)) |
310 | 309 | oveq2d 7229 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (-1↑(𝑗 − 1)) = (-1↑(((2
· 𝑘) + 1) −
1))) |
311 | 308 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑇↑𝑗) = (𝑇↑((2 · 𝑘) + 1))) |
312 | 311, 308 | oveq12d 7231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((𝑇↑𝑗) / 𝑗) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) |
313 | 310, 312 | oveq12d 7231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = ((-1↑(((2 · 𝑘) + 1) − 1)) ·
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
314 | 313, 312 | oveq12d 7231 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(((2 · 𝑘) + 1) − 1)) ·
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
315 | 138 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℕ0) |
316 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
317 | 315, 316 | nn0mulcld 12155 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℕ0) |
318 | | nn0p1nn 12129 |
. . . . . . . 8
⊢ ((2
· 𝑘) ∈
ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ) |
319 | 317, 318 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ∈
ℕ) |
320 | 166 | negcld 11176 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ -1 ∈ ℂ) |
321 | 165, 166 | pncand 11190 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) − 1) = (2 · 𝑘)) |
322 | 138 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℕ0) |
323 | 322, 162 | nn0mulcld 12155 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℕ0) |
324 | 321, 323 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) − 1) ∈ ℕ0) |
325 | 320, 324 | expcld 13716 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (-1↑(((2 · 𝑘) + 1) − 1)) ∈
ℂ) |
326 | 325 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(((2 · 𝑘) +
1) − 1)) ∈ ℂ) |
327 | 14 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑇 ∈
ℂ) |
328 | 197 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℕ0) |
329 | 317, 328 | nn0addcld 12154 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ∈
ℕ0) |
330 | 327, 329 | expcld 13716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑇↑((2 · 𝑘) + 1)) ∈
ℂ) |
331 | | 2cnd 11908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℂ) |
332 | 164 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
333 | 331, 332 | mulcld 10853 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℂ) |
334 | | 1cnd 10828 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℂ) |
335 | 333, 334 | addcld 10852 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ∈
ℂ) |
336 | | 0red 10836 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ∈
ℝ) |
337 | 146 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℝ) |
338 | 148 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
339 | 337, 338 | remulcld 10863 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℝ) |
340 | | 1red 10834 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℝ) |
341 | | 0le2 11932 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
2 |
342 | 341 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
2) |
343 | 316 | nn0ge0d 12153 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
𝑘) |
344 | 337, 338,
342, 343 | mulge0d 11409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ (2
· 𝑘)) |
345 | | 0lt1 11354 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
346 | 345 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 <
1) |
347 | 339, 340,
344, 346 | addgegt0d 11405 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 <
((2 · 𝑘) +
1)) |
348 | 336, 347 | gtned 10967 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ≠
0) |
349 | 330, 335,
348 | divcld 11608 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) ∈
ℂ) |
350 | 326, 349 | mulcld 10853 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ) |
351 | 350, 349 | addcld 10852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ) |
352 | 307, 314,
319, 351 | fvmptd 6825 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘((2 · 𝑘) + 1)) = (((-1↑(((2
· 𝑘) + 1) −
1)) · ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) +
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
353 | 321 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((2
· 𝑘) + 1) − 1)
= (2 · 𝑘)) |
354 | 353 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(((2 · 𝑘) +
1) − 1)) = (-1↑(2 · 𝑘))) |
355 | | nn0z 12200 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
356 | | m1expeven 13682 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ →
(-1↑(2 · 𝑘)) =
1) |
357 | 355, 356 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (-1↑(2 · 𝑘)) = 1) |
358 | 357 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(2 · 𝑘)) =
1) |
359 | 354, 358 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(((2 · 𝑘) +
1) − 1)) = 1) |
360 | 359 | oveq1d 7228 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
361 | 349 | mulid2d 10851 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) =
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) |
362 | 360, 361 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) |
363 | 362 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
364 | 349 | 2timesd 12073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) =
(((𝑇↑((2 ·
𝑘) + 1)) / ((2 ·
𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
365 | 330, 335,
348 | divrec2d 11612 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) = ((1 / ((2 ·
𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) |
366 | 365 | oveq2d 7229 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) = (2
· ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))) |
367 | 363, 364,
366 | 3eqtr2d 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 ·
𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))) |
368 | 352, 367 | eqtr2d 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) = (𝐹‘((2 · 𝑘) + 1))) |
369 | | stirlinglem5.4 |
. . . . . . 7
⊢ 𝐻 = (𝑗 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))))) |
370 | 369 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐻 = (𝑗 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))))) |
371 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) |
372 | 371 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘)) |
373 | 372 | oveq1d 7228 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1)) |
374 | 373 | oveq2d 7229 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (1 / ((2 · 𝑗) + 1)) = (1 / ((2 · 𝑘) + 1))) |
375 | 373 | oveq2d 7229 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝑇↑((2 · 𝑗) + 1)) = (𝑇↑((2 · 𝑘) + 1))) |
376 | 374, 375 | oveq12d 7231 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))) = ((1 / ((2 ·
𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) |
377 | 376 | oveq2d 7229 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))) = (2 · ((1 /
((2 · 𝑘) + 1))
· (𝑇↑((2
· 𝑘) +
1))))) |
378 | 335, 348 | reccld 11601 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / ((2
· 𝑘) + 1)) ∈
ℂ) |
379 | 378, 330 | mulcld 10853 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / ((2
· 𝑘) + 1)) ·
(𝑇↑((2 · 𝑘) + 1))) ∈
ℂ) |
380 | 331, 379 | mulcld 10853 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) ∈ ℂ) |
381 | 370, 377,
316, 380 | fvmptd 6825 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))) |
382 | 197 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℕ0) |
383 | 323, 382 | nn0addcld 12154 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℕ0) |
384 | 158, 161,
162, 383 | fvmptd 6825 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = ((2 · 𝑘) + 1)) |
385 | 384 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = ((2 · 𝑘) + 1)) |
386 | 385 | fveq2d 6721 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘((2 · 𝑘) + 1))) |
387 | 368, 381,
386 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
388 | 135, 1, 136, 2, 145, 178, 305, 306, 387 | isercoll2 15232 |
. . 3
⊢ (𝜑 → (seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇))) ↔ seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇))))) |
389 | 134, 388 | mpbird 260 |
. 2
⊢ (𝜑 → seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇)))) |
390 | 51, 13 | resubcld 11260 |
. . . 4
⊢ (𝜑 → (1 − 𝑇) ∈
ℝ) |
391 | 14 | subidd 11177 |
. . . . . 6
⊢ (𝜑 → (𝑇 − 𝑇) = 0) |
392 | 391 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → 0 = (𝑇 − 𝑇)) |
393 | 13, 51, 13, 129 | ltsub1dd 11444 |
. . . . 5
⊢ (𝜑 → (𝑇 − 𝑇) < (1 − 𝑇)) |
394 | 392, 393 | eqbrtrd 5075 |
. . . 4
⊢ (𝜑 → 0 < (1 − 𝑇)) |
395 | 390, 394 | elrpd 12625 |
. . 3
⊢ (𝜑 → (1 − 𝑇) ∈
ℝ+) |
396 | 123, 395 | relogdivd 25514 |
. 2
⊢ (𝜑 → (log‘((1 + 𝑇) / (1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇)))) |
397 | 389, 396 | breqtrrd 5081 |
1
⊢ (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇)))) |