Step | Hyp | Ref
| Expression |
1 | | nnre 10904 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
2 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
3 | 2 | nn0ge0d 11231 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
4 | 1, 3 | ge0p1rpd 11778 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ+) |
5 | | nnrp 11718 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
6 | 4, 5 | rpdivcld 11765 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈
ℝ+) |
7 | 6 | rpsqrtcld 13998 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(√‘((𝑁 + 1) /
𝑁)) ∈
ℝ+) |
8 | | nnz 11276 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
9 | 6, 8 | rpexpcld 12894 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 𝑁)↑𝑁) ∈
ℝ+) |
10 | 7, 9 | rpmulcld 11764 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((√‘((𝑁 + 1) /
𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) ∈
ℝ+) |
11 | | epr 14775 |
. . . . 5
⊢ e ∈
ℝ+ |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → e ∈
ℝ+) |
13 | 10, 12 | relogdivd 24176 |
. . 3
⊢ (𝑁 ∈ ℕ →
(log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) =
((log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) − (log‘e))) |
14 | 7, 9 | relogmuld 24175 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = ((log‘(√‘((𝑁 + 1) / 𝑁))) + (log‘(((𝑁 + 1) / 𝑁)↑𝑁)))) |
15 | | logsqrt 24250 |
. . . . . . . 8
⊢ (((𝑁 + 1) / 𝑁) ∈ ℝ+ →
(log‘(√‘((𝑁 + 1) / 𝑁))) = ((log‘((𝑁 + 1) / 𝑁)) / 2)) |
16 | 6, 15 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘(√‘((𝑁 + 1) / 𝑁))) = ((log‘((𝑁 + 1) / 𝑁)) / 2)) |
17 | | relogexp 24146 |
. . . . . . . 8
⊢ ((((𝑁 + 1) / 𝑁) ∈ ℝ+ ∧ 𝑁 ∈ ℤ) →
(log‘(((𝑁 + 1) /
𝑁)↑𝑁)) = (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) |
18 | 6, 8, 17 | syl2anc 691 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘(((𝑁 + 1) /
𝑁)↑𝑁)) = (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) |
19 | 16, 18 | oveq12d 6567 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((log‘(√‘((𝑁 + 1) / 𝑁))) + (log‘(((𝑁 + 1) / 𝑁)↑𝑁))) = (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁))))) |
20 | 14, 19 | eqtrd 2644 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = (((log‘((𝑁 + 1) / 𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁))))) |
21 | | peano2nn 10909 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
22 | 21 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
23 | | nncn 10905 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
24 | | nnne0 10930 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
25 | 22, 23, 24 | divcld 10680 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ) |
26 | 21 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≠ 0) |
27 | 22, 23, 26, 24 | divne0d 10696 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ≠ 0) |
28 | 25, 27 | logcld 24121 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(log‘((𝑁 + 1) / 𝑁)) ∈
ℂ) |
29 | | 2cnd 10970 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
30 | | 2rp 11713 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ+) |
32 | 31 | rpne0d 11753 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 2 ≠
0) |
33 | 28, 29, 32 | divrec2d 10684 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((log‘((𝑁 + 1) /
𝑁)) / 2) = ((1 / 2)
· (log‘((𝑁 +
1) / 𝑁)))) |
34 | 33 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(((log‘((𝑁 + 1) /
𝑁)) / 2) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) = (((1 / 2) · (log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁))))) |
35 | | 1cnd 9935 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
36 | 35 | halfcld 11154 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1 / 2)
∈ ℂ) |
37 | 36, 23, 28 | adddird 9944 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((1 / 2)
+ 𝑁) ·
(log‘((𝑁 + 1) / 𝑁))) = (((1 / 2) ·
(log‘((𝑁 + 1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁))))) |
38 | 23, 29, 32 | divcan4d 10686 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 · 2) / 2) = 𝑁) |
39 | 23, 29 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 · 2) = (2 · 𝑁)) |
40 | 39 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 · 2) / 2) = ((2 ·
𝑁) / 2)) |
41 | 38, 40 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 = ((2 · 𝑁) / 2)) |
42 | 41 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((1 / 2)
+ 𝑁) = ((1 / 2) + ((2
· 𝑁) /
2))) |
43 | 29, 23 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) |
44 | 35, 43, 29, 32 | divdird 10718 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((1 + (2
· 𝑁)) / 2) = ((1 /
2) + ((2 · 𝑁) /
2))) |
45 | 42, 44 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((1 / 2)
+ 𝑁) = ((1 + (2 ·
𝑁)) / 2)) |
46 | 45 | oveq1d 6564 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (((1 / 2)
+ 𝑁) ·
(log‘((𝑁 + 1) / 𝑁))) = (((1 + (2 · 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁)))) |
47 | 37, 46 | eqtr3d 2646 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((1 / 2)
· (log‘((𝑁 +
1) / 𝑁))) + (𝑁 · (log‘((𝑁 + 1) / 𝑁)))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁)))) |
48 | 20, 34, 47 | 3eqtrd 2648 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) = (((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁)))) |
49 | | loge 24137 |
. . . . 5
⊢
(log‘e) = 1 |
50 | 49 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(log‘e) = 1) |
51 | 48, 50 | oveq12d 6567 |
. . 3
⊢ (𝑁 ∈ ℕ →
((log‘((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) − (log‘e)) = ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
52 | 13, 51 | eqtrd 2644 |
. 2
⊢ (𝑁 ∈ ℕ →
(log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) = ((((1 + (2 · 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
53 | | stirlinglem4.1 |
. . . . . . 7
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
54 | 53 | stirlinglem2 38968 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) ∈
ℝ+) |
55 | 54 | relogcld 24173 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘𝑁)) ∈
ℝ) |
56 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑛𝑁 |
57 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑛log |
58 | | nfmpt1 4675 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
59 | 53, 58 | nfcxfr 2749 |
. . . . . . . 8
⊢
Ⅎ𝑛𝐴 |
60 | 59, 56 | nffv 6110 |
. . . . . . 7
⊢
Ⅎ𝑛(𝐴‘𝑁) |
61 | 57, 60 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑛(log‘(𝐴‘𝑁)) |
62 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝐴‘𝑛) = (𝐴‘𝑁)) |
63 | 62 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑁))) |
64 | | stirlinglem4.2 |
. . . . . 6
⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛))) |
65 | 56, 61, 63, 64 | fvmptf 6209 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧
(log‘(𝐴‘𝑁)) ∈ ℝ) → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
66 | 55, 65 | mpdan 699 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐵‘𝑁) = (log‘(𝐴‘𝑁))) |
67 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑘(log‘(𝐴‘𝑛)) |
68 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛𝑘 |
69 | 59, 68 | nffv 6110 |
. . . . . . . . 9
⊢
Ⅎ𝑛(𝐴‘𝑘) |
70 | 57, 69 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑛(log‘(𝐴‘𝑘)) |
71 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) |
72 | 71 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (log‘(𝐴‘𝑛)) = (log‘(𝐴‘𝑘))) |
73 | 67, 70, 72 | cbvmpt 4677 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦
(log‘(𝐴‘𝑛))) = (𝑘 ∈ ℕ ↦ (log‘(𝐴‘𝑘))) |
74 | 64, 73 | eqtri 2632 |
. . . . . 6
⊢ 𝐵 = (𝑘 ∈ ℕ ↦ (log‘(𝐴‘𝑘))) |
75 | 74 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝐵 = (𝑘 ∈ ℕ ↦ (log‘(𝐴‘𝑘)))) |
76 | | simpr 476 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → 𝑘 = (𝑁 + 1)) |
77 | 76 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (𝐴‘𝑘) = (𝐴‘(𝑁 + 1))) |
78 | 77 | fveq2d 6107 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (log‘(𝐴‘𝑘)) = (log‘(𝐴‘(𝑁 + 1)))) |
79 | 53 | stirlinglem2 38968 |
. . . . . . 7
⊢ ((𝑁 + 1) ∈ ℕ →
(𝐴‘(𝑁 + 1)) ∈
ℝ+) |
80 | 21, 79 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) ∈
ℝ+) |
81 | 80 | relogcld 24173 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(log‘(𝐴‘(𝑁 + 1))) ∈
ℝ) |
82 | 75, 78, 21, 81 | fvmptd 6197 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝐵‘(𝑁 + 1)) = (log‘(𝐴‘(𝑁 + 1)))) |
83 | 66, 82 | oveq12d 6567 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = ((log‘(𝐴‘𝑁)) − (log‘(𝐴‘(𝑁 + 1))))) |
84 | 54, 80 | relogdivd 24176 |
. . 3
⊢ (𝑁 ∈ ℕ →
(log‘((𝐴‘𝑁) / (𝐴‘(𝑁 + 1)))) = ((log‘(𝐴‘𝑁)) − (log‘(𝐴‘(𝑁 + 1))))) |
85 | | faccl 12932 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
86 | | nnrp 11718 |
. . . . . . . . 9
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℝ+) |
87 | 2, 85, 86 | 3syl 18 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℝ+) |
88 | 31, 5 | rpmulcld 11764 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ+) |
89 | 88 | rpsqrtcld 13998 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(√‘(2 · 𝑁)) ∈
ℝ+) |
90 | 5, 12 | rpdivcld 11765 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 / e) ∈
ℝ+) |
91 | 90, 8 | rpexpcld 12894 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ∈
ℝ+) |
92 | 89, 91 | rpmulcld 11764 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈
ℝ+) |
93 | 87, 92 | rpdivcld 11765 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈
ℝ+) |
94 | 53 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))))) |
95 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
96 | 95 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (!‘𝑛) = (!‘𝑁)) |
97 | 95 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (2 · 𝑛) = (2 · 𝑁)) |
98 | 97 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑁))) |
99 | 95 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → (𝑛 / e) = (𝑁 / e)) |
100 | 99, 95 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → ((𝑛 / e)↑𝑛) = ((𝑁 / e)↑𝑁)) |
101 | 98, 100 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) |
102 | 96, 101 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) ∧ 𝑛 = 𝑁) → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))) |
103 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈
ℕ) |
104 | 87 | rpcnd 11750 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℂ) |
105 | 104 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
(!‘𝑁) ∈
ℂ) |
106 | | 2cnd 10970 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 2
∈ ℂ) |
107 | 103 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈
ℂ) |
108 | 106, 107 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → (2
· 𝑁) ∈
ℂ) |
109 | 108 | sqrtcld 14024 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
(√‘(2 · 𝑁)) ∈ ℂ) |
110 | | ere 14658 |
. . . . . . . . . . . . . 14
⊢ e ∈
ℝ |
111 | 110 | recni 9931 |
. . . . . . . . . . . . 13
⊢ e ∈
ℂ |
112 | 111 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → e
∈ ℂ) |
113 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
114 | | epos 14774 |
. . . . . . . . . . . . . 14
⊢ 0 <
e |
115 | 113, 114 | gtneii 10028 |
. . . . . . . . . . . . 13
⊢ e ≠
0 |
116 | 115 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → e
≠ 0) |
117 | 107, 112,
116 | divcld 10680 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
(𝑁 / e) ∈
ℂ) |
118 | 103 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈
ℕ0) |
119 | 117, 118 | expcld 12870 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
((𝑁 / e)↑𝑁) ∈
ℂ) |
120 | 109, 119 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℂ) |
121 | 89 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(√‘(2 · 𝑁)) ≠ 0) |
122 | 121 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
(√‘(2 · 𝑁)) ≠ 0) |
123 | 103 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ≠ 0) |
124 | 107, 112,
123, 116 | divne0d 10696 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
(𝑁 / e) ≠
0) |
125 | 103 | nnzd 11357 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) → 𝑁 ∈
ℤ) |
126 | 117, 124,
125 | expne0d 12876 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
((𝑁 / e)↑𝑁) ≠ 0) |
127 | 109, 119,
122, 126 | mulne0d 10558 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ≠ 0) |
128 | 105, 120,
127 | divcld 10680 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℂ) |
129 | 94, 102, 103, 128 | fvmptd 6197 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧
((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) ∈ ℝ+) →
(𝐴‘𝑁) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))) |
130 | 93, 129 | mpdan 699 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐴‘𝑁) = ((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))) |
131 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑘((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
132 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑛((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) |
133 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘)) |
134 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘)) |
135 | 134 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑘))) |
136 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑛 / e) = (𝑘 / e)) |
137 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
138 | 136, 137 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → ((𝑛 / e)↑𝑛) = ((𝑘 / e)↑𝑘)) |
139 | 135, 138 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) |
140 | 133, 139 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘)))) |
141 | 131, 132,
140 | cbvmpt 4677 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 ·
𝑘)) · ((𝑘 / e)↑𝑘)))) |
142 | 53, 141 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐴 = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 ·
𝑘)) · ((𝑘 / e)↑𝑘)))) |
143 | 142 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝐴 = (𝑘 ∈ ℕ ↦ ((!‘𝑘) / ((√‘(2 ·
𝑘)) · ((𝑘 / e)↑𝑘))))) |
144 | 76 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (!‘𝑘) = (!‘(𝑁 + 1))) |
145 | 76 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (2 · 𝑘) = (2 · (𝑁 + 1))) |
146 | 145 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (√‘(2 ·
𝑘)) = (√‘(2
· (𝑁 +
1)))) |
147 | 76 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → (𝑘 / e) = ((𝑁 + 1) / e)) |
148 | 147, 76 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((𝑘 / e)↑𝑘) = (((𝑁 + 1) / e)↑(𝑁 + 1))) |
149 | 146, 148 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((√‘(2 ·
𝑘)) · ((𝑘 / e)↑𝑘)) = ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) |
150 | 144, 149 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 = (𝑁 + 1)) → ((!‘𝑘) / ((√‘(2 · 𝑘)) · ((𝑘 / e)↑𝑘))) = ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) |
151 | 21 | nnnn0d 11228 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
152 | | faccl 12932 |
. . . . . . . . 9
⊢ ((𝑁 + 1) ∈ ℕ0
→ (!‘(𝑁 + 1))
∈ ℕ) |
153 | | nnrp 11718 |
. . . . . . . . 9
⊢
((!‘(𝑁 + 1))
∈ ℕ → (!‘(𝑁 + 1)) ∈
ℝ+) |
154 | 151, 152,
153 | 3syl 18 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘(𝑁 + 1)) ∈
ℝ+) |
155 | 31, 4 | rpmulcld 11764 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 + 1)) ∈
ℝ+) |
156 | 155 | rpsqrtcld 13998 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(√‘(2 · (𝑁 + 1))) ∈
ℝ+) |
157 | 4, 12 | rpdivcld 11765 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / e) ∈
ℝ+) |
158 | 8 | peano2zd 11361 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℤ) |
159 | 157, 158 | rpexpcld 12894 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) ∈
ℝ+) |
160 | 156, 159 | rpmulcld 11764 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈
ℝ+) |
161 | 154, 160 | rpdivcld 11765 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) ∈
ℝ+) |
162 | 143, 150,
21, 161 | fvmptd 6197 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐴‘(𝑁 + 1)) = ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) |
163 | 130, 162 | oveq12d 6567 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((𝐴‘𝑁) / (𝐴‘(𝑁 + 1))) = (((!‘𝑁) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) |
164 | | facp1 12927 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 1)) =
((!‘𝑁) ·
(𝑁 + 1))) |
165 | 2, 164 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(!‘(𝑁 + 1)) =
((!‘𝑁) ·
(𝑁 + 1))) |
166 | 165 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = (((!‘𝑁) · (𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) |
167 | 160 | rpcnd 11750 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈ ℂ) |
168 | 160 | rpne0d 11753 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ≠ 0) |
169 | 104, 22, 167, 168 | divassd 10715 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) ·
(𝑁 + 1)) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) |
170 | 166, 169 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 + 1)) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) = ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) |
171 | 170 | oveq2d 6565 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (((!‘𝑁) / ((√‘(2 ·
𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))) |
172 | 92 | rpcnd 11750 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ∈ ℂ) |
173 | 22, 167, 168 | divcld 10680 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / ((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1)))) ∈
ℂ) |
174 | 104, 173 | mulcld 9939 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) ∈ ℂ) |
175 | 92 | rpne0d 11753 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)) ≠ 0) |
176 | 87 | rpne0d 11753 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ≠
0) |
177 | 22, 167, 26, 168 | divne0d 10696 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / ((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1)))) ≠
0) |
178 | 104, 173,
176, 177 | mulne0d 10558 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ·
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) ≠ 0) |
179 | 104, 172,
174, 175, 178 | divdiv32d 10705 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) = (((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2
· 𝑁)) ·
((𝑁 / e)↑𝑁)))) |
180 | 104, 104,
173, 176, 177 | divdiv1d 10711 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
(!‘𝑁)) / ((𝑁 + 1) / ((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1))))) = ((!‘𝑁) / ((!‘𝑁) · ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))))) |
181 | 180 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) /
((!‘𝑁) ·
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) = (((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) |
182 | 181 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
((!‘𝑁) ·
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 ·
𝑁)) · ((𝑁 / e)↑𝑁))) = ((((!‘𝑁) / (!‘𝑁)) / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2
· 𝑁)) ·
((𝑁 / e)↑𝑁)))) |
183 | 104, 176 | dividd 10678 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) /
(!‘𝑁)) =
1) |
184 | 183 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
(!‘𝑁)) / ((𝑁 + 1) / ((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1))))) = (1 / ((𝑁 + 1) / ((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1)))))) |
185 | 184 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((((!‘𝑁) /
(!‘𝑁)) / ((𝑁 + 1) / ((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2
· 𝑁)) ·
((𝑁 / e)↑𝑁))) = ((1 / ((𝑁 + 1) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2
· 𝑁)) ·
((𝑁 / e)↑𝑁)))) |
186 | 22, 167, 26, 168 | recdivd 10697 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (1 /
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) = (((√‘(2 ·
(𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1))) |
187 | 186 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((1 /
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 ·
𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))) |
188 | 167, 22, 26 | divcld 10680 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) ∈ ℂ) |
189 | 89 | rpcnd 11750 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(√‘(2 · 𝑁)) ∈ ℂ) |
190 | 91 | rpcnd 11750 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ∈ ℂ) |
191 | 91 | rpne0d 11753 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) ≠ 0) |
192 | 188, 189,
190, 121, 191 | divdiv1d 10711 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) / ((𝑁 / e)↑𝑁)) = ((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁)))) |
193 | 167, 22, 189, 26, 121 | divdiv32d 10705 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) = ((((√‘(2
· (𝑁 + 1))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2
· 𝑁))) / (𝑁 + 1))) |
194 | 156 | rpcnd 11750 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(√‘(2 · (𝑁 + 1))) ∈ ℂ) |
195 | 159 | rpcnd 11750 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) ∈
ℂ) |
196 | 194, 195,
189, 121 | div23d 10717 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) = (((√‘(2
· (𝑁 + 1))) /
(√‘(2 · 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) |
197 | 31 | rpred 11748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
198 | 31 | rpge0d 11752 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 0 ≤
2) |
199 | 21 | nnred 10912 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) |
200 | 151 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 0 ≤
(𝑁 + 1)) |
201 | 197, 198,
199, 200 | sqrtmuld 14011 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘(2 · (𝑁 + 1))) = ((√‘2) ·
(√‘(𝑁 +
1)))) |
202 | 197, 198,
1, 3 | sqrtmuld 14011 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘(2 · 𝑁)) = ((√‘2) ·
(√‘𝑁))) |
203 | 201, 202 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ →
((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) = (((√‘2)
· (√‘(𝑁
+ 1))) / ((√‘2) · (√‘𝑁)))) |
204 | 29 | sqrtcld 14024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘2) ∈ ℂ) |
205 | 22 | sqrtcld 14024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘(𝑁 + 1))
∈ ℂ) |
206 | 23 | sqrtcld 14024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘𝑁) ∈
ℂ) |
207 | 31 | rpsqrtcld 13998 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ →
(√‘2) ∈ ℝ+) |
208 | 207 | rpne0d 11753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘2) ≠ 0) |
209 | 5 | rpsqrtcld 13998 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ →
(√‘𝑁) ∈
ℝ+) |
210 | 209 | rpne0d 11753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(√‘𝑁) ≠
0) |
211 | 204, 204,
205, 206, 208, 210 | divmuldivd 10721 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ →
(((√‘2) / (√‘2)) · ((√‘(𝑁 + 1)) / (√‘𝑁))) = (((√‘2)
· (√‘(𝑁
+ 1))) / ((√‘2) · (√‘𝑁)))) |
212 | 204, 208 | dividd 10678 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
((√‘2) / (√‘2)) = 1) |
213 | 199, 200,
5 | sqrtdivd 14010 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ →
(√‘((𝑁 + 1) /
𝑁)) =
((√‘(𝑁 + 1)) /
(√‘𝑁))) |
214 | 213 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
((√‘(𝑁 + 1)) /
(√‘𝑁)) =
(√‘((𝑁 + 1) /
𝑁))) |
215 | 212, 214 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ →
(((√‘2) / (√‘2)) · ((√‘(𝑁 + 1)) / (√‘𝑁))) = (1 ·
(√‘((𝑁 + 1) /
𝑁)))) |
216 | 203, 211,
215 | 3eqtr2d 2650 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) = (1 ·
(√‘((𝑁 + 1) /
𝑁)))) |
217 | 216 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(((√‘(2 · (𝑁 + 1))) / (√‘(2 · 𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) = ((1 ·
(√‘((𝑁 + 1) /
𝑁))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) |
218 | 25 | sqrtcld 14024 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ →
(√‘((𝑁 + 1) /
𝑁)) ∈
ℂ) |
219 | 218 | mulid2d 9937 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (1
· (√‘((𝑁
+ 1) / 𝑁))) =
(√‘((𝑁 + 1) /
𝑁))) |
220 | 219 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((1
· (√‘((𝑁
+ 1) / 𝑁))) ·
(((𝑁 + 1) / e)↑(𝑁 + 1))) =
((√‘((𝑁 + 1) /
𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) |
221 | 196, 217,
220 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1)))) |
222 | 221 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (√‘(2 · 𝑁))) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1))) |
223 | 193, 222 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1))) |
224 | 223 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / (√‘(2 · 𝑁))) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁))) |
225 | 192, 224 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁))) |
226 | 218, 195 | mulcld 9939 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((√‘((𝑁 + 1) /
𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) ∈
ℂ) |
227 | 226, 22, 190, 26, 191 | divdiv32d 10705 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((((√‘((𝑁 + 1)
/ 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) / (𝑁 + 1))) |
228 | 218, 195,
190, 191 | divassd 10715 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁)))) |
229 | 12 | rpcnd 11750 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → e ∈
ℂ) |
230 | 12 | rpne0d 11753 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → e ≠
0) |
231 | 22, 229, 230, 151 | expdivd 12884 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / e)↑(𝑁 + 1)) = (((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1)))) |
232 | 23, 229, 230, 2 | expdivd 12884 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑁 / e)↑𝑁) = ((𝑁↑𝑁) / (e↑𝑁))) |
233 | 231, 232 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁)))) |
234 | 233 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((√‘((𝑁 + 1) /
𝑁)) · ((((𝑁 + 1) / e)↑(𝑁 + 1)) / ((𝑁 / e)↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁))))) |
235 | 22, 151 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)↑(𝑁 + 1)) ∈ ℂ) |
236 | 229, 151 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(e↑(𝑁 + 1)) ∈
ℂ) |
237 | 23, 2 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (𝑁↑𝑁) ∈ ℂ) |
238 | 229, 2 | expcld 12870 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(e↑𝑁) ∈
ℂ) |
239 | 229, 230,
158 | expne0d 12876 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(e↑(𝑁 + 1)) ≠
0) |
240 | 229, 230,
8 | expne0d 12876 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(e↑𝑁) ≠
0) |
241 | 23, 24, 8 | expne0d 12876 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (𝑁↑𝑁) ≠ 0) |
242 | 235, 236,
237, 238, 239, 240, 241 | divdivdivd 10727 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁))) = ((((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁)))) |
243 | 235, 238 | mulcomd 9940 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) = ((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1)))) |
244 | 243 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) · (e↑𝑁)) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))) = (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁)))) |
245 | 238, 236,
235, 237, 239, 241 | divmuldivd 10721 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(((e↑𝑁) /
(e↑(𝑁 + 1))) ·
(((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = (((e↑𝑁) · ((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁)))) |
246 | 229, 2 | expp1d 12871 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ →
(e↑(𝑁 + 1)) =
((e↑𝑁) ·
e)) |
247 | 246 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
((e↑𝑁) /
(e↑(𝑁 + 1))) =
((e↑𝑁) /
((e↑𝑁) ·
e))) |
248 | 238, 238,
229, 240, 230 | divdiv1d 10711 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(((e↑𝑁) /
(e↑𝑁)) / e) =
((e↑𝑁) /
((e↑𝑁) ·
e))) |
249 | 238, 240 | dividd 10678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ →
((e↑𝑁) / (e↑𝑁)) = 1) |
250 | 249 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ →
(((e↑𝑁) /
(e↑𝑁)) / e) = (1 /
e)) |
251 | 247, 248,
250 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ →
((e↑𝑁) /
(e↑(𝑁 + 1))) = (1 /
e)) |
252 | 251 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(((e↑𝑁) /
(e↑(𝑁 + 1))) ·
(((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) |
253 | 245, 252 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(((e↑𝑁) ·
((𝑁 + 1)↑(𝑁 + 1))) / ((e↑(𝑁 + 1)) · (𝑁↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) |
254 | 242, 244,
253 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁))) = ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) |
255 | 254 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((√‘((𝑁 + 1) /
𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (e↑(𝑁 + 1))) / ((𝑁↑𝑁) / (e↑𝑁)))) = ((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))))) |
256 | 228, 234,
255 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) = ((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))))) |
257 | 256 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((((√‘((𝑁 + 1)
/ 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / ((𝑁 / e)↑𝑁)) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) / (𝑁 + 1))) |
258 | 235, 237,
241 | divcld 10680 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) ∈ ℂ) |
259 | 35, 229, 258, 230 | div32d 10703 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((1 / e)
· (((𝑁 +
1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = (1 · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e))) |
260 | 258, 229,
230 | divcld 10680 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e) ∈ ℂ) |
261 | 260 | mulid2d 9937 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (1
· ((((𝑁 +
1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)) |
262 | 259, 261 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((1 / e)
· (((𝑁 +
1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e)) |
263 | 262 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) / (𝑁 + 1)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e))) |
264 | 229, 230 | reccld 10673 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (1 / e)
∈ ℂ) |
265 | 264, 258 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((1 / e)
· (((𝑁 +
1)↑(𝑁 + 1)) / (𝑁↑𝑁))) ∈ ℂ) |
266 | 218, 265,
22, 26 | div23d 10717 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) · ((1 / e)
· (((𝑁 +
1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) / (𝑁 + 1)) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((1 / e) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))))) |
267 | 218, 22, 26 | divcld 10680 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((√‘((𝑁 + 1) /
𝑁)) / (𝑁 + 1)) ∈ ℂ) |
268 | 267, 258,
229, 230 | divassd 10715 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((((√‘((𝑁 + 1)
/ 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e) = (((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / e))) |
269 | 263, 266,
268 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) · ((1 / e)
· (((𝑁 +
1)↑(𝑁 + 1)) / (𝑁↑𝑁)))) / (𝑁 + 1)) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e)) |
270 | 227, 257,
269 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((((√‘((𝑁 + 1)
/ 𝑁)) · (((𝑁 + 1) / e)↑(𝑁 + 1))) / (𝑁 + 1)) / ((𝑁 / e)↑𝑁)) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e)) |
271 | 187, 225,
270 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((1 /
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) / ((√‘(2 ·
𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e)) |
272 | 182, 185,
271 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
((!‘𝑁) ·
((𝑁 + 1) /
((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1)))))) / ((√‘(2 ·
𝑁)) · ((𝑁 / e)↑𝑁))) = ((((√‘((𝑁 + 1) / 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e)) |
273 | 171, 179,
272 | 3eqtrd 2648 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(((!‘𝑁) /
((√‘(2 · 𝑁)) · ((𝑁 / e)↑𝑁))) / ((!‘(𝑁 + 1)) / ((√‘(2 · (𝑁 + 1))) · (((𝑁 + 1) / e)↑(𝑁 + 1))))) =
((((√‘((𝑁 + 1)
/ 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e)) |
274 | 218, 22, 258, 26 | div32d 10703 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1)))) |
275 | 22, 2 | expp1d 12871 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)↑(𝑁 + 1)) = (((𝑁 + 1)↑𝑁) · (𝑁 + 1))) |
276 | 275 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) = ((((𝑁 + 1)↑𝑁) · (𝑁 + 1)) / (𝑁 + 1))) |
277 | 22, 2 | expcld 12870 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1)↑𝑁) ∈ ℂ) |
278 | 277, 22, 26 | divcan4d 10686 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑𝑁) · (𝑁 + 1)) / (𝑁 + 1)) = ((𝑁 + 1)↑𝑁)) |
279 | 276, 278 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) = ((𝑁 + 1)↑𝑁)) |
280 | 279 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) / (𝑁↑𝑁)) = (((𝑁 + 1)↑𝑁) / (𝑁↑𝑁))) |
281 | 235, 237,
22, 241, 26 | divdiv32d 10705 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1)) = ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁 + 1)) / (𝑁↑𝑁))) |
282 | 22, 23, 24, 2 | expdivd 12884 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) / 𝑁)↑𝑁) = (((𝑁 + 1)↑𝑁) / (𝑁↑𝑁))) |
283 | 280, 281,
282 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1)) = (((𝑁 + 1) / 𝑁)↑𝑁)) |
284 | 283 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((√‘((𝑁 + 1) /
𝑁)) · ((((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁)) / (𝑁 + 1))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) |
285 | 274, 284 | eqtrd 2644 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(((√‘((𝑁 + 1) /
𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) = ((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁))) |
286 | 285 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((((√‘((𝑁 + 1)
/ 𝑁)) / (𝑁 + 1)) · (((𝑁 + 1)↑(𝑁 + 1)) / (𝑁↑𝑁))) / e) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) |
287 | 163, 273,
286 | 3eqtrd 2648 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((𝐴‘𝑁) / (𝐴‘(𝑁 + 1))) = (((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e)) |
288 | 287 | fveq2d 6107 |
. . 3
⊢ (𝑁 ∈ ℕ →
(log‘((𝐴‘𝑁) / (𝐴‘(𝑁 + 1)))) =
(log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e))) |
289 | 83, 84, 288 | 3eqtr2d 2650 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) =
(log‘(((√‘((𝑁 + 1) / 𝑁)) · (((𝑁 + 1) / 𝑁)↑𝑁)) / e))) |
290 | 35, 43 | addcld 9938 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (1 + (2
· 𝑁)) ∈
ℂ) |
291 | 290 | halfcld 11154 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ((1 + (2
· 𝑁)) / 2) ∈
ℂ) |
292 | 291, 28 | mulcld 9939 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) ∈
ℂ) |
293 | 292, 35 | subcld 10271 |
. . 3
⊢ (𝑁 ∈ ℕ → ((((1 +
(2 · 𝑁)) / 2)
· (log‘((𝑁 +
1) / 𝑁))) − 1) ∈
ℂ) |
294 | | stirlinglem4.3 |
. . . . 5
⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 + (2 ·
𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) − 1)) |
295 | 294 | a1i 11 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
→ 𝐽 = (𝑛 ∈ ℕ ↦ ((((1 +
(2 · 𝑛)) / 2)
· (log‘((𝑛 +
1) / 𝑛))) −
1))) |
296 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
297 | 296 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → (2 · 𝑛) = (2 · 𝑁)) |
298 | 297 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → (1 + (2 · 𝑛)) = (1 + (2 · 𝑁))) |
299 | 298 | oveq1d 6564 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → ((1 + (2 · 𝑛)) / 2) = ((1 + (2 ·
𝑁)) / 2)) |
300 | 296 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → (𝑛 + 1) = (𝑁 + 1)) |
301 | 300, 296 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → ((𝑛 + 1) / 𝑛) = ((𝑁 + 1) / 𝑁)) |
302 | 301 | fveq2d 6107 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → (log‘((𝑛 + 1) / 𝑛)) = (log‘((𝑁 + 1) / 𝑁))) |
303 | 299, 302 | oveq12d 6567 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → (((1 + (2 · 𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) = (((1 + (2 · 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁)))) |
304 | 303 | oveq1d 6564 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
∧ 𝑛 = 𝑁) → ((((1 + (2 · 𝑛)) / 2) ·
(log‘((𝑛 + 1) / 𝑛))) − 1) = ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
305 | | simpl 472 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
→ 𝑁 ∈
ℕ) |
306 | | simpr 476 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
→ ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1) ∈
ℂ) |
307 | 295, 304,
305, 306 | fvmptd 6197 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ ((((1 + (2
· 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1) ∈ ℂ)
→ (𝐽‘𝑁) = ((((1 + (2 · 𝑁)) / 2) ·
(log‘((𝑁 + 1) / 𝑁))) − 1)) |
308 | 293, 307 | mpdan 699 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐽‘𝑁) = ((((1 + (2 · 𝑁)) / 2) · (log‘((𝑁 + 1) / 𝑁))) − 1)) |
309 | 52, 289, 308 | 3eqtr4d 2654 |
1
⊢ (𝑁 ∈ ℕ → ((𝐵‘𝑁) − (𝐵‘(𝑁 + 1))) = (𝐽‘𝑁)) |