Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | stirlinglem5.1 |
. . . . . . . . 9
⊢ 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗))) |
4 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)))) |
5 | | 1cnd 9935 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
ℂ) |
6 | 5 | negcld 10258 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → -1 ∈
ℂ) |
7 | | nnm1nn0 11211 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
8 | 7 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 − 1) ∈
ℕ0) |
9 | 6, 8 | expcld 12870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (-1↑(𝑗 − 1)) ∈
ℂ) |
10 | | nncn 10905 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
11 | 10 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℂ) |
12 | | stirlinglem5.6 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
13 | 12 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ ℝ) |
14 | 13 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ ℂ) |
15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 ∈ ℂ) |
16 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
17 | 16 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
18 | 15, 17 | expcld 12870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇↑𝑗) ∈ ℂ) |
19 | | nnne0 10930 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → 𝑗 ≠ 0) |
20 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ≠ 0) |
21 | 9, 11, 18, 20 | div32d 10703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇↑𝑗)) = ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗))) |
22 | 5, 15 | pncan2d 10273 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((1 + 𝑇) − 1) = 𝑇) |
23 | 22 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑇 = ((1 + 𝑇) − 1)) |
24 | 23 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇↑𝑗) = (((1 + 𝑇) − 1)↑𝑗)) |
25 | 24 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((-1↑(𝑗 − 1)) / 𝑗) · (𝑇↑𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))) |
26 | 21, 25 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗))) |
27 | 26 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) |
28 | 4, 27 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) / 𝑗) · (((1 + 𝑇) − 1)↑𝑗)))) |
29 | 28 | seqeq3d 12671 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐷) = seq1( + , (𝑗 ∈ ℕ ↦
(((-1↑(𝑗 − 1)) /
𝑗) · (((1 + 𝑇) − 1)↑𝑗))))) |
30 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
31 | 30, 14 | addcld 9938 |
. . . . . . . . . 10
⊢ (𝜑 → (1 + 𝑇) ∈ ℂ) |
32 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
33 | 32 | cnmetdval 22384 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (1 + 𝑇) ∈ ℂ) → (1(abs ∘
− )(1 + 𝑇)) =
(abs‘(1 − (1 + 𝑇)))) |
34 | 30, 31, 33 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (1(abs ∘ − )(1
+ 𝑇)) = (abs‘(1
− (1 + 𝑇)))) |
35 | | 1m1e0 10966 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 − 1) =
0) |
37 | 36 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 − 1) −
𝑇) = (0 − 𝑇)) |
38 | 30, 30, 14 | subsub4d 10302 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 − 1) −
𝑇) = (1 − (1 + 𝑇))) |
39 | | df-neg 10148 |
. . . . . . . . . . . . . 14
⊢ -𝑇 = (0 − 𝑇) |
40 | 39 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ (0
− 𝑇) = -𝑇 |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 − 𝑇) = -𝑇) |
42 | 37, 38, 41 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 − (1 + 𝑇)) = -𝑇) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(1 − (1 +
𝑇))) = (abs‘-𝑇)) |
44 | 14 | absnegd 14036 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘-𝑇) = (abs‘𝑇)) |
45 | | stirlinglem5.7 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑇) < 1) |
46 | 44, 45 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘-𝑇) < 1) |
47 | 43, 46 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(1 − (1 +
𝑇))) <
1) |
48 | 34, 47 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (𝜑 → (1(abs ∘ − )(1
+ 𝑇)) <
1) |
49 | | cnxmet 22386 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
51 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
52 | 51 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ*) |
53 | | elbl2 22005 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ (1 + 𝑇) ∈ ℂ)) → ((1 + 𝑇) ∈ (1(ball‘(abs
∘ − ))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1)) |
54 | 50, 52, 30, 31, 53 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝑇) ∈ (1(ball‘(abs ∘ −
))1) ↔ (1(abs ∘ − )(1 + 𝑇)) < 1)) |
55 | 48, 54 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑇) ∈ (1(ball‘(abs ∘ −
))1)) |
56 | | eqid 2610 |
. . . . . . . 8
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
57 | 56 | logtayl2 24208 |
. . . . . . 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 4605 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐷) ⇝ (log‘(1 + 𝑇))) |
60 | | seqex 12665 |
. . . . . 6
⊢ seq1( + ,
𝐹) ∈
V |
61 | 60 | a1i 11 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐹) ∈ V) |
62 | | stirlinglem5.2 |
. . . . . . . 8
⊢ 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗)) |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))) |
64 | 63 | seqeq3d 12671 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐸) = seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗)))) |
65 | | logtayl 24206 |
. . . . . . 7
⊢ ((𝑇 ∈ ℂ ∧
(abs‘𝑇) < 1)
→ seq1( + , (𝑗 ∈
ℕ ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇))) |
66 | 14, 45, 65 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))) ⇝ -(log‘(1 − 𝑇))) |
67 | 64, 66 | eqbrtrd 4605 |
. . . . 5
⊢ (𝜑 → seq1( + , 𝐸) ⇝ -(log‘(1 −
𝑇))) |
68 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
69 | 68, 1 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
70 | 3 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)))) |
71 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1)) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → (-1↑(𝑗 − 1)) = (-1↑(𝑛 − 1))) |
73 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (𝑇↑𝑗) = (𝑇↑𝑛)) |
74 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → 𝑗 = 𝑛) |
75 | 73, 74 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → ((𝑇↑𝑗) / 𝑗) = ((𝑇↑𝑛) / 𝑛)) |
76 | 72, 75 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
77 | 76 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) ∧ 𝑗 = 𝑛) → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
78 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) |
79 | 78 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ) |
80 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
81 | 80 | negcld 10258 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → -1 ∈
ℂ) |
82 | | nnm1nn0 11211 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
83 | 81, 82 | expcld 12870 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(-1↑(𝑛 − 1))
∈ ℂ) |
84 | 79, 83 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (-1↑(𝑛 − 1)) ∈ ℂ) |
85 | 14 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑇 ∈ ℂ) |
86 | 79 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ0) |
87 | 85, 86 | expcld 12870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝑇↑𝑛) ∈ ℂ) |
88 | 79 | nncnd 10913 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℂ) |
89 | 79 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ≠ 0) |
90 | 87, 88, 89 | divcld 10680 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
91 | 84, 90 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
92 | 70, 77, 79, 91 | fvmptd 6197 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷‘𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
93 | 92, 91 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐷‘𝑛) ∈ ℂ) |
94 | | addcl 9897 |
. . . . . . 7
⊢ ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ) |
95 | 94 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ) |
96 | 69, 93, 95 | seqcl 12683 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐷)‘𝑘) ∈ ℂ) |
97 | 62 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))) |
98 | 75 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) ∧ 𝑗 = 𝑛) → ((𝑇↑𝑗) / 𝑗) = ((𝑇↑𝑛) / 𝑛)) |
99 | 97, 98, 79, 90 | fvmptd 6197 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸‘𝑛) = ((𝑇↑𝑛) / 𝑛)) |
100 | 99, 90 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐸‘𝑛) ∈ ℂ) |
101 | 69, 100, 95 | seqcl 12683 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐸)‘𝑘) ∈ ℂ) |
102 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑) |
103 | | stirlinglem5.3 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗))) |
104 | 103 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)))) |
105 | 76, 75 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
106 | 105 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 = 𝑛) → (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
107 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
108 | 83 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (-1↑(𝑛 − 1)) ∈
ℂ) |
109 | 14 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 ∈ ℂ) |
110 | 107 | nnnn0d 11228 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
111 | 109, 110 | expcld 12870 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇↑𝑛) ∈ ℂ) |
112 | 107 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
113 | 107 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
114 | 111, 112,
113 | divcld 10680 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
115 | 108, 114 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
116 | 115, 114 | addcld 9938 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
117 | 104, 106,
107, 116 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
118 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)))) |
119 | 76 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 = 𝑛) → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
120 | 118, 119,
107, 115 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛))) |
121 | 120 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) = (𝐷‘𝑛)) |
122 | 62 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐸 = (𝑗 ∈ ℕ ↦ ((𝑇↑𝑗) / 𝑗))) |
123 | 75 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 = 𝑛) → ((𝑇↑𝑗) / 𝑗) = ((𝑇↑𝑛) / 𝑛)) |
124 | 122, 123,
107, 114 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸‘𝑛) = ((𝑇↑𝑛) / 𝑛)) |
125 | 124 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇↑𝑛) / 𝑛) = (𝐸‘𝑛)) |
126 | 121, 125 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((𝐷‘𝑛) + (𝐸‘𝑛))) |
127 | 117, 126 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ((𝐷‘𝑛) + (𝐸‘𝑛))) |
128 | 102, 79, 127 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐹‘𝑛) = ((𝐷‘𝑛) + (𝐸‘𝑛))) |
129 | 69, 93, 100, 128 | seradd 12705 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) = ((seq1( + , 𝐷)‘𝑘) + (seq1( + , 𝐸)‘𝑘))) |
130 | 1, 2, 59, 61, 67, 96, 101, 129 | climadd 14210 |
. . . 4
⊢ (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) + -(log‘(1 −
𝑇)))) |
131 | | 1rp 11712 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
132 | 131 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ+) |
133 | 132, 12 | rpaddcld 11763 |
. . . . . . 7
⊢ (𝜑 → (1 + 𝑇) ∈
ℝ+) |
134 | 133 | rpne0d 11753 |
. . . . . 6
⊢ (𝜑 → (1 + 𝑇) ≠ 0) |
135 | 31, 134 | logcld 24121 |
. . . . 5
⊢ (𝜑 → (log‘(1 + 𝑇)) ∈
ℂ) |
136 | 30, 14 | subcld 10271 |
. . . . . 6
⊢ (𝜑 → (1 − 𝑇) ∈
ℂ) |
137 | 13, 51 | absltd 14016 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝑇) < 1 ↔ (-1 < 𝑇 ∧ 𝑇 < 1))) |
138 | 45, 137 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → (-1 < 𝑇 ∧ 𝑇 < 1)) |
139 | 138 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 < 1) |
140 | 13, 139 | gtned 10051 |
. . . . . . 7
⊢ (𝜑 → 1 ≠ 𝑇) |
141 | 30, 14, 140 | subne0d 10280 |
. . . . . 6
⊢ (𝜑 → (1 − 𝑇) ≠ 0) |
142 | 136, 141 | logcld 24121 |
. . . . 5
⊢ (𝜑 → (log‘(1 −
𝑇)) ∈
ℂ) |
143 | 135, 142 | negsubd 10277 |
. . . 4
⊢ (𝜑 → ((log‘(1 + 𝑇)) + -(log‘(1 −
𝑇))) = ((log‘(1 +
𝑇)) − (log‘(1
− 𝑇)))) |
144 | 130, 143 | breqtrd 4609 |
. . 3
⊢ (𝜑 → seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇)))) |
145 | | nn0uz 11598 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
146 | | 0zd 11266 |
. . . 4
⊢ (𝜑 → 0 ∈
ℤ) |
147 | | stirlinglem5.5 |
. . . . . 6
⊢ 𝐺 = (𝑗 ∈ ℕ0 ↦ ((2
· 𝑗) +
1)) |
148 | | 2nn0 11186 |
. . . . . . . . 9
⊢ 2 ∈
ℕ0 |
149 | 148 | a1i 11 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ 2 ∈ ℕ0) |
150 | | id 22 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℕ0) |
151 | 149, 150 | nn0mulcld 11233 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ (2 · 𝑗)
∈ ℕ0) |
152 | | nn0p1nn 11209 |
. . . . . . 7
⊢ ((2
· 𝑗) ∈
ℕ0 → ((2 · 𝑗) + 1) ∈ ℕ) |
153 | 151, 152 | syl 17 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0
→ ((2 · 𝑗) + 1)
∈ ℕ) |
154 | 147, 153 | fmpti 6291 |
. . . . 5
⊢ 𝐺:ℕ0⟶ℕ |
155 | 154 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺:ℕ0⟶ℕ) |
156 | | 2re 10967 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
157 | 156 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℝ) |
158 | | nn0re 11178 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
159 | 157, 158 | remulcld 9949 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℝ) |
160 | | 1red 9934 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℝ) |
161 | 158, 160 | readdcld 9948 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
162 | 157, 161 | remulcld 9949 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2 · (𝑘 + 1))
∈ ℝ) |
163 | | 2rp 11713 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
164 | 163 | a1i 11 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℝ+) |
165 | 158 | ltp1d 10833 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 < (𝑘 + 1)) |
166 | 158, 161,
164, 165 | ltmul2dd 11804 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘) <
(2 · (𝑘 +
1))) |
167 | 159, 162,
160, 166 | ltadd1dd 10517 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
< ((2 · (𝑘 + 1))
+ 1)) |
168 | 147 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝐺 = (𝑗 ∈ ℕ0
↦ ((2 · 𝑗) +
1))) |
169 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) |
170 | 169 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘)) |
171 | 170 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1)) |
172 | | id 22 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) |
173 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℂ) |
174 | | nn0cn 11179 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
175 | 173, 174 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℂ) |
176 | | 1cnd 9935 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℂ) |
177 | 175, 176 | addcld 9938 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℂ) |
178 | 168, 171,
172, 177 | fvmptd 6197 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = ((2 · 𝑘) + 1)) |
179 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = (𝑘 + 1)) → 𝑗 = (𝑘 + 1)) |
180 | 179 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = (𝑘 + 1)) → (2 · 𝑗) = (2 · (𝑘 + 1))) |
181 | 180 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 = (𝑘 + 1)) → ((2 · 𝑗) + 1) = ((2 · (𝑘 + 1)) + 1)) |
182 | | peano2nn0 11210 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
183 | 174, 176 | addcld 9938 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) |
184 | 173, 183 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (2 · (𝑘 + 1))
∈ ℂ) |
185 | 184, 176 | addcld 9938 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((2 · (𝑘 +
1)) + 1) ∈ ℂ) |
186 | 168, 181,
182, 185 | fvmptd 6197 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘(𝑘 + 1)) = ((2 · (𝑘 + 1)) + 1)) |
187 | 167, 178,
186 | 3brtr4d 4615 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
188 | 187 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1))) |
189 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 𝑛 ∈
ℕ) |
190 | 189 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ) |
191 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 1 ∈
ℂ) |
192 | 191 | negcld 10258 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → -1 ∈
ℂ) |
193 | 189, 82 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 − 1) ∈
ℕ0) |
194 | 192, 193 | expcld 12870 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (-1↑(𝑛 − 1)) ∈
ℂ) |
195 | 194 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) ∈
ℂ) |
196 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑇 ∈ ℂ) |
197 | 190 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℕ0) |
198 | 196, 197 | expcld 12870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝑇↑𝑛) ∈ ℂ) |
199 | 190 | nncnd 10913 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ∈ ℂ) |
200 | 190 | nnne0d 10942 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → 𝑛 ≠ 0) |
201 | 198, 199,
200 | divcld 10680 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
202 | 195, 201 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
203 | 202, 201 | addcld 9938 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) |
204 | 105, 103 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧
(((-1↑(𝑛 − 1))
· ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) ∈ ℂ) → (𝐹‘𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
205 | 190, 203,
204 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹‘𝑛) = (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
206 | | eldifn 3695 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ 𝑛 ∈ ran 𝐺) |
207 | | 0nn0 11184 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 |
208 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ0 |
209 | 148, 208 | num0h 11385 |
. . . . . . . . . . . . . . . 16
⊢ 1 = ((2
· 0) + 1) |
210 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 0 → (2 · 𝑗) = (2 ·
0)) |
211 | 210 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 0 → ((2 · 𝑗) + 1) = ((2 · 0) +
1)) |
212 | 211 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 0 → (1 = ((2 ·
𝑗) + 1) ↔ 1 = ((2
· 0) + 1))) |
213 | 212 | rspcev 3282 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℕ0 ∧ 1 = ((2 · 0) + 1)) → ∃𝑗 ∈ ℕ0 1 =
((2 · 𝑗) +
1)) |
214 | 207, 209,
213 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢
∃𝑗 ∈
ℕ0 1 = ((2 · 𝑗) + 1) |
215 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
216 | 147 | elrnmpt 5293 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℂ → (1 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 = ((2 ·
𝑗) + 1))) |
217 | 215, 216 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 1 =
((2 · 𝑗) +
1)) |
218 | 214, 217 | mpbir 220 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ran 𝐺 |
219 | 218 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → 1 ∈ ran 𝐺) |
220 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (𝑛 ∈ ran 𝐺 ↔ 1 ∈ ran 𝐺)) |
221 | 219, 220 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝑛 = 1 → 𝑛 ∈ ran 𝐺) |
222 | 206, 221 | nsyl 134 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ 𝑛 = 1) |
223 | | nn1m1nn 10917 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ)) |
224 | 189, 223 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 = 1 ∨ (𝑛 − 1) ∈ ℕ)) |
225 | 224 | ord 391 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (¬ 𝑛 = 1 → (𝑛 − 1) ∈ ℕ)) |
226 | 222, 225 | mpd 15 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 − 1) ∈
ℕ) |
227 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗ℕ |
228 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗(𝑗 ∈ ℕ0 ↦ ((2
· 𝑗) +
1)) |
229 | 147, 228 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝐺 |
230 | 229 | nfrn 5289 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗ran
𝐺 |
231 | 227, 230 | nfdif 3693 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(ℕ ∖ ran 𝐺) |
232 | 231 | nfcri 2745 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗 𝑛 ∈ (ℕ ∖ ran
𝐺) |
233 | 147 | elrnmpt 5293 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 ∈ ran 𝐺 ↔ ∃𝑗 ∈ ℕ0 𝑛 = ((2 · 𝑗) + 1))) |
234 | 206, 233 | mtbid 313 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬
∃𝑗 ∈
ℕ0 𝑛 = ((2
· 𝑗) +
1)) |
235 | | ralnex 2975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑗 ∈
ℕ0 ¬ 𝑛
= ((2 · 𝑗) + 1)
↔ ¬ ∃𝑗
∈ ℕ0 𝑛 = ((2 · 𝑗) + 1)) |
236 | 234, 235 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ∀𝑗 ∈ ℕ0
¬ 𝑛 = ((2 ·
𝑗) + 1)) |
237 | 236 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℕ0) → ¬
𝑛 = ((2 · 𝑗) + 1)) |
238 | 237 | neqned 2789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℕ0) → 𝑛 ≠ ((2 · 𝑗) + 1)) |
239 | 238 | necomd 2837 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℕ0) → ((2
· 𝑗) + 1) ≠ 𝑛) |
240 | 239 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ 𝑗 ∈ ℕ0) → ((2
· 𝑗) + 1) ≠ 𝑛) |
241 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ 𝑗 ∈
ℤ) |
242 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ ¬ 𝑗 ∈
ℕ0) |
243 | 189 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ 𝑛 ∈
ℕ) |
244 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 2 ∈ ℝ) |
245 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 ∈ ℤ) |
246 | 245 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 ∈ ℝ) |
247 | 244, 246 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 · 𝑗) ∈ ℝ) |
248 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 0 ∈ ℝ) |
249 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 1 ∈ ℝ) |
250 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 2 ∈ ℂ) |
251 | 246 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 ∈ ℂ) |
252 | 250, 251 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 · 𝑗) = (𝑗 · 2)) |
253 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ 𝑗 ∈ ℕ0) |
254 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑗 ∈ ℕ0
↔ (𝑗 ∈ ℤ
∧ 0 ≤ 𝑗)) |
255 | 253, 254 | sylnib 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) |
256 | | nan 602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ (𝑗 ∈ ℤ ∧ 0 ≤ 𝑗)) ↔ (((𝑗 ∈ ℤ ∧ ¬ 𝑗 ∈ ℕ0)
∧ 𝑗 ∈ ℤ)
→ ¬ 0 ≤ 𝑗)) |
257 | 255, 256 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑗 ∈ ℤ) → ¬ 0 ≤ 𝑗) |
258 | 257 | anabss1 851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ 0 ≤ 𝑗) |
259 | 246, 248 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (𝑗 < 0 ↔ ¬ 0 ≤ 𝑗)) |
260 | 258, 259 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 𝑗 < 0) |
261 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 2 ∈ ℝ+) |
262 | 261 | rpregt0d 11754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 ∈ ℝ ∧ 0 < 2)) |
263 | | mulltgt0 38204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑗 ∈ ℝ ∧ 𝑗 < 0) ∧ (2 ∈ ℝ
∧ 0 < 2)) → (𝑗
· 2) < 0) |
264 | 246, 260,
262, 263 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (𝑗 · 2) < 0) |
265 | 252, 264 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (2 · 𝑗) < 0) |
266 | 247, 248,
249, 265 | ltadd1dd 10517 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ((2 · 𝑗) + 1) < (0 + 1)) |
267 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → 1 ∈ ℂ) |
268 | 267 | addid2d 10116 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (0 + 1) = 1) |
269 | 266, 268 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ((2 · 𝑗) + 1) < 1) |
270 | 247, 249 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ((2 · 𝑗) + 1) ∈ ℝ) |
271 | 270, 249 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → (((2 · 𝑗) + 1) < 1 ↔ ¬ 1 ≤ ((2
· 𝑗) +
1))) |
272 | 269, 271 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ 1 ≤ ((2 · 𝑗) + 1)) |
273 | | nnge1 10923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· 𝑗) + 1) ∈
ℕ → 1 ≤ ((2 · 𝑗) + 1)) |
274 | 272, 273 | nsyl 134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) → ¬ ((2 · 𝑗) + 1) ∈ ℕ) |
275 | 274 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 ·
𝑗) + 1) ∈
ℕ) |
276 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℕ ∧ ((2
· 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) = 𝑛) |
277 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℕ ∧ ((2
· 𝑗) + 1) = 𝑛) → 𝑛 ∈ ℕ) |
278 | 276, 277 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 ∈ ℕ ∧ ((2
· 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈
ℕ) |
279 | 278 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) ∧ ((2 · 𝑗) + 1) = 𝑛) → ((2 · 𝑗) + 1) ∈ ℕ) |
280 | 275, 279 | mtand 689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ¬ ((2 ·
𝑗) + 1) = 𝑛) |
281 | 280 | neqned 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑗 ∈ ℤ ∧ ¬
𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ((2 · 𝑗) + 1) ≠ 𝑛) |
282 | 241, 242,
243, 281 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) ∧ ¬ 𝑗 ∈ ℕ0)
→ ((2 · 𝑗) + 1)
≠ 𝑛) |
283 | 240, 282 | pm2.61dan 828 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) → ((2 · 𝑗) + 1) ≠ 𝑛) |
284 | 283 | neneqd 2787 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (ℕ ∖ ran
𝐺) ∧ 𝑗 ∈ ℤ) → ¬ ((2 ·
𝑗) + 1) = 𝑛) |
285 | 284 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑗 ∈ ℤ → ¬ ((2
· 𝑗) + 1) = 𝑛)) |
286 | 232, 285 | ralrimi 2940 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ∀𝑗 ∈ ℤ ¬ ((2
· 𝑗) + 1) = 𝑛) |
287 | | ralnex 2975 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑗 ∈
ℤ ¬ ((2 · 𝑗) + 1) = 𝑛 ↔ ¬ ∃𝑗 ∈ ℤ ((2 · 𝑗) + 1) = 𝑛) |
288 | 286, 287 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬
∃𝑗 ∈ ℤ ((2
· 𝑗) + 1) = 𝑛) |
289 | 189 | nnzd 11357 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 𝑛 ∈
ℤ) |
290 | | odd2np1 14903 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (¬ 2
∥ 𝑛 ↔
∃𝑗 ∈ ℤ ((2
· 𝑗) + 1) = 𝑛)) |
291 | 289, 290 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (¬ 2 ∥
𝑛 ↔ ∃𝑗 ∈ ℤ ((2 ·
𝑗) + 1) = 𝑛)) |
292 | 288, 291 | mtbird 314 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ ¬ 2
∥ 𝑛) |
293 | 292 | notnotrd 127 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 2 ∥ 𝑛) |
294 | 189 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 𝑛 ∈
ℂ) |
295 | 294, 191 | npcand 10275 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ((𝑛 − 1) + 1) = 𝑛) |
296 | 293, 295 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → 2 ∥ ((𝑛 − 1) +
1)) |
297 | 193 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (𝑛 − 1) ∈
ℤ) |
298 | | oddp1even 14906 |
. . . . . . . . . . . 12
⊢ ((𝑛 − 1) ∈ ℤ
→ (¬ 2 ∥ (𝑛
− 1) ↔ 2 ∥ ((𝑛 − 1) + 1))) |
299 | 297, 298 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (¬ 2 ∥
(𝑛 − 1) ↔ 2
∥ ((𝑛 − 1) +
1))) |
300 | 296, 299 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → ¬ 2 ∥
(𝑛 −
1)) |
301 | | oexpneg 14907 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝑛
− 1) ∈ ℕ ∧ ¬ 2 ∥ (𝑛 − 1)) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1))) |
302 | 191, 226,
300, 301 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (-1↑(𝑛 − 1)) = -(1↑(𝑛 − 1))) |
303 | | 1exp 12751 |
. . . . . . . . . . 11
⊢ ((𝑛 − 1) ∈ ℤ
→ (1↑(𝑛 −
1)) = 1) |
304 | 297, 303 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (1↑(𝑛 − 1)) =
1) |
305 | 304 | negeqd 10154 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → -(1↑(𝑛 − 1)) =
-1) |
306 | 302, 305 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℕ ∖ ran
𝐺) → (-1↑(𝑛 − 1)) =
-1) |
307 | 306 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1↑(𝑛 − 1)) =
-1) |
308 | 307 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) = (-1 · ((𝑇↑𝑛) / 𝑛))) |
309 | 308 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((-1↑(𝑛 − 1)) · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = ((-1 · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛))) |
310 | 201 | mulm1d 10361 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-1 · ((𝑇↑𝑛) / 𝑛)) = -((𝑇↑𝑛) / 𝑛)) |
311 | 310 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛))) |
312 | 201 | negcld 10258 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → -((𝑇↑𝑛) / 𝑛) ∈ ℂ) |
313 | 312, 201 | addcomd 10117 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (-((𝑇↑𝑛) / 𝑛) + ((𝑇↑𝑛) / 𝑛)) = (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛))) |
314 | 201 | negidd 10261 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (((𝑇↑𝑛) / 𝑛) + -((𝑇↑𝑛) / 𝑛)) = 0) |
315 | 311, 313,
314 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → ((-1 · ((𝑇↑𝑛) / 𝑛)) + ((𝑇↑𝑛) / 𝑛)) = 0) |
316 | 205, 309,
315 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ ran 𝐺)) → (𝐹‘𝑛) = 0) |
317 | 117, 116 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℂ) |
318 | 103 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)))) |
319 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → 𝑗 = ((2 · 𝑘) + 1)) |
320 | 319 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑗 − 1) = (((2 ·
𝑘) + 1) −
1)) |
321 | 320 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (-1↑(𝑗 − 1)) = (-1↑(((2
· 𝑘) + 1) −
1))) |
322 | 319 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (𝑇↑𝑗) = (𝑇↑((2 · 𝑘) + 1))) |
323 | 322, 319 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((𝑇↑𝑗) / 𝑗) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) |
324 | 321, 323 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → ((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) = ((-1↑(((2 · 𝑘) + 1) − 1)) ·
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
325 | 324, 323 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = ((2 · 𝑘) + 1)) → (((-1↑(𝑗 − 1)) · ((𝑇↑𝑗) / 𝑗)) + ((𝑇↑𝑗) / 𝑗)) = (((-1↑(((2 · 𝑘) + 1) − 1)) ·
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
326 | 148 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℕ0) |
327 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
328 | 326, 327 | nn0mulcld 11233 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℕ0) |
329 | | nn0p1nn 11209 |
. . . . . . . 8
⊢ ((2
· 𝑘) ∈
ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ) |
330 | 328, 329 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ∈
ℕ) |
331 | 176 | negcld 10258 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ -1 ∈ ℂ) |
332 | 175, 176 | pncand 10272 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) − 1) = (2 · 𝑘)) |
333 | 148 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℕ0) |
334 | 333, 172 | nn0mulcld 11233 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (2 · 𝑘)
∈ ℕ0) |
335 | 332, 334 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (((2 · 𝑘) +
1) − 1) ∈ ℕ0) |
336 | 331, 335 | expcld 12870 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (-1↑(((2 · 𝑘) + 1) − 1)) ∈
ℂ) |
337 | 336 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(((2 · 𝑘) +
1) − 1)) ∈ ℂ) |
338 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑇 ∈
ℂ) |
339 | 208 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℕ0) |
340 | 328, 339 | nn0addcld 11232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ∈
ℕ0) |
341 | 338, 340 | expcld 12870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑇↑((2 · 𝑘) + 1)) ∈
ℂ) |
342 | | 2cnd 10970 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℂ) |
343 | 174 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
344 | 342, 343 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℂ) |
345 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℂ) |
346 | 344, 345 | addcld 9938 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ∈
ℂ) |
347 | | 0red 9920 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ∈
ℝ) |
348 | 156 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 2 ∈
ℝ) |
349 | 158 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
350 | 348, 349 | remulcld 9949 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℝ) |
351 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℝ) |
352 | | 0le2 10988 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
2 |
353 | 352 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
2) |
354 | 327 | nn0ge0d 11231 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
𝑘) |
355 | 348, 349,
353, 354 | mulge0d 10483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤ (2
· 𝑘)) |
356 | | 0lt1 10429 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
357 | 356 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 <
1) |
358 | 350, 351,
355, 357 | addgegt0d 10480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 <
((2 · 𝑘) +
1)) |
359 | 347, 358 | gtned 10051 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((2
· 𝑘) + 1) ≠
0) |
360 | 341, 346,
359 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) ∈
ℂ) |
361 | 337, 360 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ) |
362 | 361, 360 | addcld 9938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) ∈ ℂ) |
363 | 318, 325,
330, 362 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘((2 · 𝑘) + 1)) = (((-1↑(((2
· 𝑘) + 1) −
1)) · ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) +
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
364 | 332 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((2
· 𝑘) + 1) − 1)
= (2 · 𝑘)) |
365 | 364 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(((2 · 𝑘) +
1) − 1)) = (-1↑(2 · 𝑘))) |
366 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
367 | | m1expeven 12769 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ →
(-1↑(2 · 𝑘)) =
1) |
368 | 366, 367 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (-1↑(2 · 𝑘)) = 1) |
369 | 368 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(2 · 𝑘)) =
1) |
370 | 365, 369 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(-1↑(((2 · 𝑘) +
1) − 1)) = 1) |
371 | 370 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (1 · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
372 | 360 | mulid2d 9937 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) =
((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) |
373 | 371, 372 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) |
374 | 373 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
375 | 360 | 2timesd 11152 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) =
(((𝑇↑((2 ·
𝑘) + 1)) / ((2 ·
𝑘) + 1)) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)))) |
376 | 341, 346,
359 | divrec2d 10684 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1)) = ((1 / ((2 ·
𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) |
377 | 376 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((𝑇↑((2
· 𝑘) + 1)) / ((2
· 𝑘) + 1))) = (2
· ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))) |
378 | 374, 375,
377 | 3eqtr2d 2650 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((-1↑(((2 · 𝑘)
+ 1) − 1)) · ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) + ((𝑇↑((2 · 𝑘) + 1)) / ((2 · 𝑘) + 1))) = (2 · ((1 / ((2 ·
𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))) |
379 | 363, 378 | eqtr2d 2645 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) = (𝐹‘((2 · 𝑘) + 1))) |
380 | | stirlinglem5.4 |
. . . . . . 7
⊢ 𝐻 = (𝑗 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))))) |
381 | 380 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐻 = (𝑗 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))))) |
382 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) |
383 | 382 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · 𝑗) = (2 · 𝑘)) |
384 | 383 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((2 · 𝑗) + 1) = ((2 · 𝑘) + 1)) |
385 | 384 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (1 / ((2 · 𝑗) + 1)) = (1 / ((2 · 𝑘) + 1))) |
386 | 384 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝑇↑((2 · 𝑗) + 1)) = (𝑇↑((2 · 𝑘) + 1))) |
387 | 385, 386 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1))) = ((1 / ((2 ·
𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) |
388 | 387 | oveq2d 6565 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (2 · ((1 / ((2 · 𝑗) + 1)) · (𝑇↑((2 · 𝑗) + 1)))) = (2 · ((1 /
((2 · 𝑘) + 1))
· (𝑇↑((2
· 𝑘) +
1))))) |
389 | 346, 359 | reccld 10673 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 / ((2
· 𝑘) + 1)) ∈
ℂ) |
390 | 389, 341 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((1 / ((2
· 𝑘) + 1)) ·
(𝑇↑((2 · 𝑘) + 1))) ∈
ℂ) |
391 | 342, 390 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (2
· ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1)))) ∈ ℂ) |
392 | 381, 388,
327, 391 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (2 · ((1 / ((2 · 𝑘) + 1)) · (𝑇↑((2 · 𝑘) + 1))))) |
393 | 208 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℕ0) |
394 | 334, 393 | nn0addcld 11232 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((2 · 𝑘) + 1)
∈ ℕ0) |
395 | 168, 171,
172, 394 | fvmptd 6197 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = ((2 · 𝑘) + 1)) |
396 | 395 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = ((2 · 𝑘) + 1)) |
397 | 396 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘((2 · 𝑘) + 1))) |
398 | 379, 392,
397 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘))) |
399 | 145, 1, 146, 2, 155, 188, 316, 317, 398 | isercoll2 14247 |
. . 3
⊢ (𝜑 → (seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇))) ↔ seq1( + , 𝐹) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇))))) |
400 | 144, 399 | mpbird 246 |
. 2
⊢ (𝜑 → seq0( + , 𝐻) ⇝ ((log‘(1 + 𝑇)) − (log‘(1 −
𝑇)))) |
401 | 51, 13 | resubcld 10337 |
. . . 4
⊢ (𝜑 → (1 − 𝑇) ∈
ℝ) |
402 | 14 | subidd 10259 |
. . . . . 6
⊢ (𝜑 → (𝑇 − 𝑇) = 0) |
403 | 402 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → 0 = (𝑇 − 𝑇)) |
404 | 13, 51, 13, 139 | ltsub1dd 10518 |
. . . . 5
⊢ (𝜑 → (𝑇 − 𝑇) < (1 − 𝑇)) |
405 | 403, 404 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → 0 < (1 − 𝑇)) |
406 | 401, 405 | elrpd 11745 |
. . 3
⊢ (𝜑 → (1 − 𝑇) ∈
ℝ+) |
407 | 133, 406 | relogdivd 24176 |
. 2
⊢ (𝜑 → (log‘((1 + 𝑇) / (1 − 𝑇))) = ((log‘(1 + 𝑇)) − (log‘(1 − 𝑇)))) |
408 | 400, 407 | breqtrrd 4611 |
1
⊢ (𝜑 → seq0( + , 𝐻) ⇝ (log‘((1 + 𝑇) / (1 − 𝑇)))) |