Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . 4
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
3 | | 1e0p1 11428 |
. . . . . . . 8
⊢ 1 = (0 +
1) |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 = (0 +
1)) |
5 | 4 | seqeq1d 12669 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐻) = seq(0 + 1)( + , 𝐻)) |
6 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
7 | | 0nn0 11184 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 0 ∈
ℕ0) |
9 | | stirlinglem7.3 |
. . . . . . . . . 10
⊢ 𝐻 = (𝑘 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))))) |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 𝐻 = (𝑘 ∈ ℕ0
↦ (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))) |
11 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
12 | 11 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → ((2 · 𝑘) + 1) = ((2 · 𝑗) + 1)) |
13 | 12 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑗) + 1))) |
14 | 12 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) |
15 | 13, 14 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 ·
𝑗) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑗) +
1)))) |
16 | 15 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑘) + 1)))) = (2
· ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))) |
17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
∧ 𝑘 = 𝑗) → (2 · ((1 / ((2
· 𝑘) + 1)) ·
((1 / ((2 · 𝑁) +
1))↑((2 · 𝑘) +
1)))) = (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))))) |
18 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 𝑗 ∈
ℕ0) |
19 | | 2cnd 10970 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 2 ∈ ℂ) |
20 | | 2cnd 10970 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ 2 ∈ ℂ) |
21 | | nn0cn 11179 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℂ) |
22 | 20, 21 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ (2 · 𝑗)
∈ ℂ) |
23 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ 1 ∈ ℂ) |
24 | 22, 23 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ ((2 · 𝑗) + 1)
∈ ℂ) |
25 | 24 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((2 · 𝑗) + 1)
∈ ℂ) |
26 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ 0 ∈ ℝ) |
27 | | 2re 10967 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ0
→ 2 ∈ ℝ) |
29 | | nn0re 11178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℝ) |
30 | 28, 29 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ (2 · 𝑗)
∈ ℝ) |
31 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ 1 ∈ ℝ) |
32 | | 0le2 10988 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
2 |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ0
→ 0 ≤ 2) |
34 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ0
→ 0 ≤ 𝑗) |
35 | 28, 29, 33, 34 | mulge0d 10483 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ 0 ≤ (2 · 𝑗)) |
36 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
1 |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ 0 < 1) |
38 | 30, 31, 35, 37 | addgegt0d 10480 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ 0 < ((2 · 𝑗) + 1)) |
39 | 26, 38 | ltned 10052 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ 0 ≠ ((2 · 𝑗) + 1)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 0 ≠ ((2 · 𝑗) + 1)) |
41 | 40 | necomd 2837 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((2 · 𝑗) + 1)
≠ 0) |
42 | 25, 41 | reccld 10673 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (1 / ((2 · 𝑗)
+ 1)) ∈ ℂ) |
43 | | nncn 10905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
45 | 19, 44 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (2 · 𝑁)
∈ ℂ) |
46 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 1 ∈ ℂ) |
47 | 45, 46 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((2 · 𝑁) + 1)
∈ ℂ) |
48 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
49 | | nnre 10904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
50 | 48, 49 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ) |
51 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
52 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 0 ≤
2) |
53 | | 0red 9920 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 0 ∈
ℝ) |
54 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
55 | 53, 49, 54 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
56 | 48, 49, 52, 55 | mulge0d 10483 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 0 ≤ (2
· 𝑁)) |
57 | 36 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 0 <
1) |
58 | 50, 51, 56, 57 | addgegt0d 10480 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 0 <
((2 · 𝑁) +
1)) |
59 | 58 | gt0ne0d 10471 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ≠
0) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((2 · 𝑁) + 1)
≠ 0) |
61 | 47, 60 | reccld 10673 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (1 / ((2 · 𝑁)
+ 1)) ∈ ℂ) |
62 | | 2nn0 11186 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 2 ∈ ℕ0) |
64 | 63, 18 | nn0mulcld 11233 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (2 · 𝑗)
∈ ℕ0) |
65 | | 1nn0 11185 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ 1 ∈ ℕ0) |
67 | 64, 66 | nn0addcld 11232 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((2 · 𝑗) + 1)
∈ ℕ0) |
68 | 61, 67 | expcld 12870 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)) ∈ ℂ) |
69 | 42, 68 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1))) ∈
ℂ) |
70 | 19, 69 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))) ∈
ℂ) |
71 | 10, 17, 18, 70 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (𝐻‘𝑗) = (2 · ((1 / ((2
· 𝑗) + 1)) ·
((1 / ((2 · 𝑁) +
1))↑((2 · 𝑗) +
1))))) |
72 | 71, 70 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ (𝐻‘𝑗) ∈
ℂ) |
73 | 9 | stirlinglem6 38972 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → seq0( + ,
𝐻) ⇝
(log‘((𝑁 + 1) / 𝑁))) |
74 | 6, 8, 72, 73 | clim2ser 14233 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → seq(0 +
1)( + , 𝐻) ⇝
((log‘((𝑁 + 1) /
𝑁)) − (seq0( + ,
𝐻)‘0))) |
75 | 5, 74 | eqbrtrd 4605 |
. . . . 5
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐻) ⇝
((log‘((𝑁 + 1) /
𝑁)) − (seq0( + ,
𝐻)‘0))) |
76 | | 0z 11265 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
77 | | seq1 12676 |
. . . . . . . 8
⊢ (0 ∈
ℤ → (seq0( + , 𝐻)‘0) = (𝐻‘0)) |
78 | 76, 77 | mp1i 13 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (seq0( +
, 𝐻)‘0) = (𝐻‘0)) |
79 | 9 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))) |
80 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → 𝑘 = 0) |
81 | 80 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · 𝑘) = (2 ·
0)) |
82 | 81 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((2 · 𝑘) + 1) = ((2 · 0) +
1)) |
83 | 82 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (1 / ((2 ·
𝑘) + 1)) = (1 / ((2
· 0) + 1))) |
84 | 82 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 ·
𝑁) + 1))↑((2 ·
𝑘) + 1)) = ((1 / ((2
· 𝑁) + 1))↑((2
· 0) + 1))) |
85 | 83, 84 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑘) + 1))) = ((1 /
((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) +
1)))) |
86 | 85 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = 0) → (2 · ((1 /
((2 · 𝑘) + 1))
· ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))) = (2 · ((1 / ((2 · 0)
+ 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) +
1))))) |
87 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
88 | | 0cnd 9912 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 0 ∈
ℂ) |
89 | 87, 88 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2
· 0) ∈ ℂ) |
90 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
91 | 89, 90 | addcld 9938 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 0) + 1) ∈ ℂ) |
92 | 87 | mul01d 10114 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (2
· 0) = 0) |
93 | 92 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 0 = (2
· 0)) |
94 | 93 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (0 + 1) =
((2 · 0) + 1)) |
95 | 4, 94 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 1 = ((2
· 0) + 1)) |
96 | 57, 95 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 0 <
((2 · 0) + 1)) |
97 | 96 | gt0ne0d 10471 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 0) + 1) ≠ 0) |
98 | 91, 97 | reccld 10673 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 0) + 1)) ∈ ℂ) |
99 | 87, 43 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) |
100 | 99, 90 | addcld 9938 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) ∈
ℂ) |
101 | 100, 59 | reccld 10673 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 𝑁) + 1)) ∈
ℂ) |
102 | 95, 65 | syl6eqelr 2697 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 0) + 1) ∈ ℕ0) |
103 | 101, 102 | expcld 12870 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑((2
· 0) + 1)) ∈ ℂ) |
104 | 98, 103 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) ∈
ℂ) |
105 | 87, 104 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) +
1)))) ∈ ℂ) |
106 | 79, 86, 8, 105 | fvmptd 6197 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝐻‘0) = (2 · ((1 /
((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) +
1))))) |
107 | 92 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((2
· 0) + 1) = (0 + 1)) |
108 | 107, 3 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((2
· 0) + 1) = 1) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 0) + 1)) = (1 / 1)) |
110 | 90 | div1d 10672 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (1 / 1) =
1) |
111 | 109, 110 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (1 / ((2
· 0) + 1)) = 1) |
112 | 108 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑((2
· 0) + 1)) = ((1 / ((2 · 𝑁) + 1))↑1)) |
113 | 101 | exp1d 12865 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑1) =
(1 / ((2 · 𝑁) +
1))) |
114 | 112, 113 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 𝑁) + 1))↑((2
· 0) + 1)) = (1 / ((2 · 𝑁) + 1))) |
115 | 111, 114 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1
· (1 / ((2 · 𝑁) + 1)))) |
116 | 101 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1
· (1 / ((2 · 𝑁) + 1))) = (1 / ((2 · 𝑁) + 1))) |
117 | 115, 116 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((1 / ((2
· 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) + 1))) = (1 /
((2 · 𝑁) +
1))) |
118 | 117 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) +
1)))) = (2 · (1 / ((2 · 𝑁) + 1)))) |
119 | 87, 90, 100, 59 | divassd 10715 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 1) / ((2 · 𝑁) + 1)) = (2 · (1 / ((2 ·
𝑁) + 1)))) |
120 | 87 | mulid1d 9936 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 1) = 2) |
121 | 120 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 1) / ((2 · 𝑁) + 1)) = (2 / ((2 · 𝑁) + 1))) |
122 | 118, 119,
121 | 3eqtr2d 2650 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· ((1 / ((2 · 0) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 0) +
1)))) = (2 / ((2 · 𝑁) + 1))) |
123 | 78, 106, 122 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (seq0( +
, 𝐻)‘0) = (2 / ((2
· 𝑁) +
1))) |
124 | 123 | oveq2d 6565 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((log‘((𝑁 + 1) /
𝑁)) − (seq0( + ,
𝐻)‘0)) =
((log‘((𝑁 + 1) /
𝑁)) − (2 / ((2
· 𝑁) +
1)))) |
125 | 75, 124 | breqtrd 4609 |
. . . 4
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐻) ⇝
((log‘((𝑁 + 1) /
𝑁)) − (2 / ((2
· 𝑁) +
1)))) |
126 | 90, 99 | addcld 9938 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (1 + (2
· 𝑁)) ∈
ℂ) |
127 | 126 | halfcld 11154 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((1 + (2
· 𝑁)) / 2) ∈
ℂ) |
128 | | seqex 12665 |
. . . . 5
⊢ seq1( + ,
𝐾) ∈
V |
129 | 128 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐾) ∈
V) |
130 | | elnnuz 11600 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↔ 𝑗 ∈
(ℤ≥‘1)) |
131 | 130 | biimpi 205 |
. . . . . 6
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
(ℤ≥‘1)) |
132 | 131 | adantl 481 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
133 | 9 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐻 = (𝑘 ∈ ℕ0 ↦ (2
· ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)))))) |
134 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛)) |
135 | 134 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1)) |
136 | 135 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (1 / ((2 · 𝑘) + 1)) = (1 / ((2 · 𝑛) + 1))) |
137 | 135 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1)) = ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) |
138 | 136, 137 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑘) + 1))) = ((1 / ((2 ·
𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) +
1)))) |
139 | 138 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑘) + 1)))) = (2
· ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) |
140 | 139 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) ∧ 𝑘 = 𝑛) → (2 · ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑘) + 1)))) = (2
· ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) |
141 | | elfzuz 12209 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈
(ℤ≥‘1)) |
142 | | elnnuz 11600 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
143 | 142 | biimpri 217 |
. . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ ℕ) |
144 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
145 | 141, 143,
144 | 3syl 18 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ0) |
146 | 145 | adantl 481 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ0) |
147 | | 2cnd 10970 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℂ) |
148 | 146 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℂ) |
149 | 147, 148 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℂ) |
150 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈ ℂ) |
151 | 149, 150 | addcld 9938 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℂ) |
152 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ) |
153 | | 0red 9920 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 ∈
ℝ) |
154 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
155 | 27 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ) |
156 | | nnre 10904 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
157 | 155, 156 | remulcld 9949 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
158 | 157, 154 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℝ) |
159 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 <
1) |
160 | | 2rp 11713 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ+) |
162 | | nnrp 11718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
163 | 161, 162 | rpmulcld 11764 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ+) |
164 | 154, 163 | ltaddrp2d 11782 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 1 <
((2 · 𝑛) +
1)) |
165 | 153, 154,
158, 159, 164 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 0 <
((2 · 𝑛) +
1)) |
166 | 165 | gt0ne0d 10471 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ≠
0) |
167 | 152, 166 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑗) → ((2 · 𝑛) + 1) ≠ 0) |
168 | 167 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ≠ 0) |
169 | 151, 168 | reccld 10673 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑛) + 1)) ∈
ℂ) |
170 | 101 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 / ((2 · 𝑁) + 1)) ∈ ℂ) |
171 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈
ℕ0) |
172 | 171, 146 | nn0mulcld 11233 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈
ℕ0) |
173 | 65 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 1 ∈
ℕ0) |
174 | 172, 173 | nn0addcld 11232 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈
ℕ0) |
175 | 170, 174 | expcld 12870 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) ∈
ℂ) |
176 | 169, 175 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1))) ∈
ℂ) |
177 | 147, 176 | mulcld 9939 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 ·
𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1)))) ∈
ℂ) |
178 | 133, 140,
146, 177 | fvmptd 6197 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻‘𝑛) = (2 · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) +
1))))) |
179 | 178, 177 | eqeltrd 2688 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐻‘𝑛) ∈ ℂ) |
180 | | addcl 9897 |
. . . . . 6
⊢ ((𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ) → (𝑛 + 𝑖) ∈ ℂ) |
181 | 180 | adantl 481 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (𝑛 + 𝑖) ∈ ℂ) |
182 | 132, 179,
181 | seqcl 12683 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐻)‘𝑗) ∈
ℂ) |
183 | | 1cnd 9935 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 1
∈ ℂ) |
184 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 2
∈ ℂ) |
185 | 43 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑁 ∈
ℂ) |
186 | 184, 185 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (2
· 𝑁) ∈
ℂ) |
187 | 183, 186 | addcld 9938 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (1 + (2
· 𝑁)) ∈
ℂ) |
188 | 187 | halfcld 11154 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → ((1 +
(2 · 𝑁)) / 2) ∈
ℂ) |
189 | | simprl 790 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑛 ∈
ℂ) |
190 | | simprr 792 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → 𝑖 ∈
ℂ) |
191 | 188, 189,
190 | adddid 9943 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑖 ∈ ℂ)) → (((1 +
(2 · 𝑁)) / 2)
· (𝑛 + 𝑖)) = ((((1 + (2 · 𝑁)) / 2) · 𝑛) + (((1 + (2 · 𝑁)) / 2) · 𝑖))) |
192 | | stirlinglem7.2 |
. . . . . . . 8
⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘)))) |
193 | 192 | a1i 11 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐾 = (𝑘 ∈ ℕ ↦ ((1 / ((2 ·
𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))))) |
194 | 134 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘)) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) |
195 | 136, 194 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑘))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑛)))) |
196 | 195 | adantl 481 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) ∧ 𝑘 = 𝑛) → ((1 / ((2 · 𝑘) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑘))) = ((1 / ((2
· 𝑛) + 1)) ·
((1 / ((2 · 𝑁) +
1))↑(2 · 𝑛)))) |
197 | 152 | adantl 481 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ) |
198 | 170, 172 | expcld 12870 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) ∈
ℂ) |
199 | 169, 198 | mulcld 9939 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑛))) ∈
ℂ) |
200 | 193, 196,
197, 199 | fvmptd 6197 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾‘𝑛) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))) |
201 | 126 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) ∈ ℂ) |
202 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
203 | 202 | a1i 11 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ≠ 0) |
204 | 201, 147,
177, 203 | div32d 10703 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1
/ ((2 · 𝑛) + 1))
· ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 + (2 · 𝑁)) · ((2 · ((1 /
((2 · 𝑛) + 1))
· ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) / 2))) |
205 | 176, 147,
203 | divcan3d 10685 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · ((1 / ((2 ·
𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1)))) / 2) =
((1 / ((2 · 𝑛) + 1))
· ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)))) |
206 | 205 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((2 · ((1 / ((2 ·
𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1)))) / 2)) =
((1 + (2 · 𝑁))
· ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) |
207 | 201, 169,
175 | mul12d 10124 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1)))) = ((1 /
((2 · 𝑛) + 1))
· ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) |
208 | 100 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ∈ ℂ) |
209 | 59 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑁) + 1) ≠ 0) |
210 | 174 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((2 · 𝑛) + 1) ∈ ℤ) |
211 | 208, 209,
210 | exprecd 12878 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1)) = (1 / (((2 ·
𝑁) + 1)↑((2 ·
𝑛) + 1)))) |
212 | 211 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((1 + (2 ·
𝑁)) · (1 / (((2
· 𝑁) + 1)↑((2
· 𝑛) +
1))))) |
213 | 208, 174 | expcld 12870 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ∈ ℂ) |
214 | 208, 209,
210 | expne0d 12876 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) ≠ 0) |
215 | 201, 213,
214 | divrecd 10683 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) · (1 / (((2 ·
𝑁) + 1)↑((2 ·
𝑛) +
1))))) |
216 | 43 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑁 ∈ ℂ) |
217 | 147, 216 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑁) ∈ ℂ) |
218 | 150, 217 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1 + (2 · 𝑁)) = ((2 · 𝑁) + 1)) |
219 | 208, 172 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ∈ ℂ) |
220 | 219, 208 | mulcomd 9940 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)) = (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛)))) |
221 | 218, 220 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))) |
222 | 208, 172 | expp1d 12871 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1)) = ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1))) |
223 | 222 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((1 + (2 · 𝑁)) / ((((2 · 𝑁) + 1)↑(2 · 𝑛)) · ((2 · 𝑁) + 1)))) |
224 | | 2z 11286 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
225 | 224 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 2 ∈ ℤ) |
226 | 146 | nn0zd 11356 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℤ) |
227 | 225, 226 | zmulcld 11364 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · 𝑛) ∈ ℤ) |
228 | 208, 209,
227 | expne0d 12876 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1)↑(2 · 𝑛)) ≠ 0) |
229 | 208, 208,
219, 209, 228 | divdiv1d 10711 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = (((2 · 𝑁) + 1) / (((2 · 𝑁) + 1) · (((2 · 𝑁) + 1)↑(2 · 𝑛))))) |
230 | 221, 223,
229 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) / (((2 · 𝑁) + 1)↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) |
231 | 212, 215,
230 | 3eqtr2d 2650 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) |
232 | 231 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((1 + (2
· 𝑁)) · ((1 /
((2 · 𝑁) +
1))↑((2 · 𝑛) +
1)))) = ((1 / ((2 · 𝑛) + 1)) · ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))))) |
233 | 208, 209 | dividd 10678 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1) |
234 | | 1exp 12751 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑛) ∈ ℤ
→ (1↑(2 · 𝑛)) = 1) |
235 | 227, 234 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (1↑(2 · 𝑛)) = 1) |
236 | 233, 235 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = (1↑(2 · 𝑛))) |
237 | 236 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) |
238 | 150, 208,
209, 172 | expdivd 12884 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)) = ((1↑(2 · 𝑛)) / (((2 · 𝑁) + 1)↑(2 · 𝑛)))) |
239 | 237, 238 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) / (((2 · 𝑁) + 1)↑(2 · 𝑛))) = ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛))) |
240 | 239 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 / ((2 · 𝑛) + 1)) · ((((2 ·
𝑁) + 1) / ((2 ·
𝑁) + 1)) / (((2 ·
𝑁) + 1)↑(2 ·
𝑛)))) = ((1 / ((2 ·
𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑛)))) |
241 | 207, 232,
240 | 3eqtrd 2648 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → ((1 + (2 · 𝑁)) · ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1)))) = ((1 /
((2 · 𝑛) + 1))
· ((1 / ((2 · 𝑁) + 1))↑(2 · 𝑛)))) |
242 | 204, 206,
241 | 3eqtrd 2648 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1
/ ((2 · 𝑛) + 1))
· ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = ((1 / ((2 · 𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑(2
· 𝑛)))) |
243 | 178 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2 · ((1 / ((2 ·
𝑛) + 1)) · ((1 / ((2
· 𝑁) + 1))↑((2
· 𝑛) + 1)))) =
(𝐻‘𝑛)) |
244 | 243 | oveq2d 6565 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((1 + (2 · 𝑁)) / 2) · (2 · ((1
/ ((2 · 𝑛) + 1))
· ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑛) + 1))))) = (((1 + (2 · 𝑁)) / 2) · (𝐻‘𝑛))) |
245 | 200, 242,
244 | 3eqtr2d 2650 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐾‘𝑛) = (((1 + (2 · 𝑁)) / 2) · (𝐻‘𝑛))) |
246 | 181, 191,
132, 179, 245 | seqdistr 12714 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐾)‘𝑗) = (((1 + (2 · 𝑁)) / 2) · (seq1( + ,
𝐻)‘𝑗))) |
247 | 1, 2, 125, 127, 129, 182, 246 | climmulc2 14215 |
. . 3
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐾) ⇝ (((1 + (2
· 𝑁)) / 2) ·
((log‘((𝑁 + 1) /
𝑁)) − (2 / ((2
· 𝑁) +
1))))) |
248 | 90, 99 | addcomd 10117 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 + (2
· 𝑁)) = ((2 ·
𝑁) + 1)) |
249 | 248 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 + (2
· 𝑁)) / 2) = (((2
· 𝑁) + 1) /
2)) |
250 | 249 | oveq1d 6564 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((1 + (2
· 𝑁)) / 2) ·
((log‘((𝑁 + 1) /
𝑁)) − (2 / ((2
· 𝑁) + 1)))) = ((((2
· 𝑁) + 1) / 2)
· ((log‘((𝑁 +
1) / 𝑁)) − (2 / ((2
· 𝑁) +
1))))) |
251 | 249, 127 | eqeltrrd 2689 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) + 1) / 2)
∈ ℂ) |
252 | 43, 90 | addcld 9938 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
253 | | nnne0 10930 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
254 | 252, 43, 253 | divcld 10680 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ) |
255 | 49, 51 | readdcld 9948 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
256 | 49 | ltp1d 10833 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1)) |
257 | 53, 49, 255, 54, 256 | lttrd 10077 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 <
(𝑁 + 1)) |
258 | 257 | gt0ne0d 10471 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0) |
259 | 252, 43, 258, 253 | divne0d 10696 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0) |
260 | 254, 259 | logcld 24121 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(log‘((𝑁 + 1) / 𝑁)) ∈
ℂ) |
261 | 87, 100, 59 | divcld 10680 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (2 / ((2
· 𝑁) + 1)) ∈
ℂ) |
262 | 251, 260,
261 | subdid 10365 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) / 2)
· ((log‘((𝑁 +
1) / 𝑁)) − (2 / ((2
· 𝑁) + 1)))) =
(((((2 · 𝑁) + 1) /
2) · (log‘((𝑁
+ 1) / 𝑁))) − ((((2
· 𝑁) + 1) / 2)
· (2 / ((2 · 𝑁) + 1))))) |
263 | 99, 90 | addcomd 10117 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) + 1) = (1 + (2
· 𝑁))) |
264 | 263 | oveq1d 6564 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) + 1) / 2) = ((1
+ (2 · 𝑁)) /
2)) |
265 | 264 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) / 2)
· (log‘((𝑁 +
1) / 𝑁))) = (((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁)))) |
266 | 202 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 2 ≠
0) |
267 | 100, 87, 59, 266 | divcan6d 10699 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) + 1) / 2)
· (2 / ((2 · 𝑁) + 1))) = 1) |
268 | 265, 267 | oveq12d 6567 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((((2
· 𝑁) + 1) / 2)
· (log‘((𝑁 +
1) / 𝑁))) − ((((2
· 𝑁) + 1) / 2)
· (2 / ((2 · 𝑁) + 1)))) = ((((1 + (2 · 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
269 | 250, 262,
268 | 3eqtrd 2648 |
. . 3
⊢ (𝑁 ∈ ℕ → (((1 + (2
· 𝑁)) / 2) ·
((log‘((𝑁 + 1) /
𝑁)) − (2 / ((2
· 𝑁) + 1)))) = ((((1
+ (2 · 𝑁)) / 2)
· (log‘((𝑁 +
1) / 𝑁))) −
1)) |
270 | 247, 269 | breqtrd 4609 |
. 2
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐾) ⇝ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
271 | | stirlinglem7.1 |
. . . 4
⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 ·
𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) − 1)) |
272 | 271 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 ·
𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) −
1))) |
273 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁)) |
274 | 273 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁))) |
275 | 274 | oveq1d 6564 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 · 𝑁)) / 2)) |
276 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑛 + 1) = (𝑁 + 1)) |
277 | | id 22 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) |
278 | 276, 277 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁)) |
279 | 278 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁))) |
280 | 275, 279 | oveq12d 6567 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((1 + (2 · 𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁)))) |
281 | 280 | oveq1d 6564 |
. . . 4
⊢ (𝑛 = 𝑁 → ((((1 + (2 · 𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
282 | 281 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 = 𝑁) → ((((1 + (2 · 𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
283 | | id 22 |
. . 3
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
284 | 127, 260 | mulcld 9939 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) ∈
ℂ) |
285 | 284, 90 | subcld 10271 |
. . 3
⊢ (𝑁 ∈ ℕ → ((((1 +
(2 · 𝑁)) / 2)
· (log‘((𝑁 +
1) / 𝑁))) − 1) ∈
ℂ) |
286 | 272, 282,
283, 285 | fvmptd 6197 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐽‘𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1)) |
287 | 270, 286 | breqtrrd 4611 |
1
⊢ (𝑁 ∈ ℕ → seq1( + ,
𝐾) ⇝ (𝐽‘𝑁)) |