Step | Hyp | Ref
| Expression |
1 | | stirlinglem3.4 |
. 2
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
((!‘𝑛)↑4)) /
((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
2 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
3 | | faccl 12932 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
4 | | nncn 10905 |
. . . . . . . . . . . . 13
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℂ) |
5 | 2, 3, 4 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(!‘𝑛) ∈
ℂ) |
6 | | 2cnd 10970 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) |
7 | | nncn 10905 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
8 | 6, 7 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) |
9 | 8 | sqrtcld 14024 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ∈ ℂ) |
10 | | ere 14658 |
. . . . . . . . . . . . . . . . 17
⊢ e ∈
ℝ |
11 | 10 | recni 9931 |
. . . . . . . . . . . . . . . 16
⊢ e ∈
ℂ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ∈
ℂ) |
13 | | epos 14774 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
e |
14 | 10, 13 | gt0ne0ii 10443 |
. . . . . . . . . . . . . . . 16
⊢ e ≠
0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ≠
0) |
16 | 7, 12, 15 | divcld 10680 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ∈
ℂ) |
17 | 16, 2 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ∈ ℂ) |
18 | 9, 17 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) |
19 | | 2rp 11713 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ+) |
21 | | nnrp 11718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
22 | 20, 21 | rpmulcld 11764 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ+) |
23 | 22 | sqrtgt0d 13999 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · 𝑛))) |
24 | 23 | gt0ne0d 10471 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ≠ 0) |
25 | | nnne0 10930 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
26 | 7, 12, 25, 15 | divne0d 10696 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ≠ 0) |
27 | | nnz 11276 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
28 | 16, 26, 27 | expne0d 12876 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ≠ 0) |
29 | 9, 17, 24, 28 | mulne0d 10558 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ≠ 0) |
30 | 5, 18, 29 | divcld 10680 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) |
31 | | stirlinglem3.1 |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
32 | 31 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
33 | 30, 32 | mpdan 699 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
34 | 33 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐴‘𝑛)↑4) = (((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4)) |
35 | | stirlinglem3.3 |
. . . . . . . . . . . 12
⊢ 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))) |
36 | 35 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) → (𝐸‘𝑛) = ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
37 | 18, 36 | mpdan 699 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐸‘𝑛) = ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
38 | 37 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐸‘𝑛)↑4) = (((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4)) |
39 | 34, 38 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) = ((((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4))) |
40 | | 4nn0 11188 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 4 ∈
ℕ0) |
42 | 5, 18, 29, 41 | expdivd 12884 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) = (((!‘𝑛)↑4) / (((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4))) |
43 | 42 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) = ((((!‘𝑛)↑4) / (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) ·
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4))) |
44 | 5, 41 | expcld 12870 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
((!‘𝑛)↑4) ∈
ℂ) |
45 | 18, 41 | expcld 12870 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) ∈ ℂ) |
46 | 41 | nn0zd 11356 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 4 ∈
ℤ) |
47 | 18, 29, 46 | expne0d 12876 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) ≠ 0) |
48 | 44, 45, 47 | divcan1d 10681 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘𝑛)↑4) /
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4)) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) = ((!‘𝑛)↑4)) |
49 | 39, 43, 48 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) = ((!‘𝑛)↑4)) |
50 | 49 | eqcomd 2616 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((!‘𝑛)↑4) =
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) |
51 | 50 | oveq2d 6565 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) = ((2↑(4 · 𝑛)) · (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)))) |
52 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ0) |
54 | 53, 2 | nn0mulcld 11233 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ0) |
55 | | faccl 12932 |
. . . . . . . . . . 11
⊢ ((2
· 𝑛) ∈
ℕ0 → (!‘(2 · 𝑛)) ∈ ℕ) |
56 | | nncn 10905 |
. . . . . . . . . . 11
⊢
((!‘(2 · 𝑛)) ∈ ℕ → (!‘(2 ·
𝑛)) ∈
ℂ) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(!‘(2 · 𝑛))
∈ ℂ) |
58 | 57 | sqcld 12868 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) ∈ ℂ) |
59 | 6, 8 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛))
∈ ℂ) |
60 | 59 | sqrtcld 14024 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(√‘(2 · (2 · 𝑛))) ∈ ℂ) |
61 | 8, 12, 15 | divcld 10680 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) / e) ∈
ℂ) |
62 | 61, 54 | expcld 12870 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(2
· 𝑛)) ∈
ℂ) |
63 | 60, 62 | mulcld 9939 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))) ∈ ℂ) |
64 | 63 | sqcld 12868 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) ∈ ℂ) |
65 | 20, 22 | rpmulcld 11764 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛))
∈ ℝ+) |
66 | 65 | sqrtgt0d 13999 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · (2 · 𝑛)))) |
67 | 66 | gt0ne0d 10471 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(√‘(2 · (2 · 𝑛))) ≠ 0) |
68 | 20 | rpne0d 11753 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 2 ≠
0) |
69 | 6, 7, 68, 25 | mulne0d 10558 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ≠
0) |
70 | 8, 12, 69, 15 | divne0d 10696 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) / e) ≠
0) |
71 | | 2z 11286 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 2 ∈
ℤ) |
73 | 72, 27 | zmulcld 11364 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℤ) |
74 | 61, 70, 73 | expne0d 12876 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(2
· 𝑛)) ≠
0) |
75 | 60, 62, 67, 74 | mulne0d 10558 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))) ≠ 0) |
76 | 63, 75, 72 | expne0d 12876 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) ≠ 0) |
77 | 58, 64, 76 | divcan1d 10681 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘(2 · 𝑛))↑2) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))
· (((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2)) = ((!‘(2 · 𝑛))↑2)) |
78 | 57, 63, 75, 53 | expdivd 12884 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2) = (((!‘(2 · 𝑛))↑2) / (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
79 | 78 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((!‘(2 · 𝑛))↑2) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) =
(((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2)) |
80 | 79 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘(2 · 𝑛))↑2) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))
· (((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2)) = ((((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
81 | 77, 80 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) = ((((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
82 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (!‘𝑛) = (!‘𝑚)) |
83 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑚))) |
85 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝑛 / e) = (𝑚 / e)) |
86 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → 𝑛 = 𝑚) |
87 | 85, 86 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((𝑛 / e)↑𝑛) = ((𝑚 / e)↑𝑚)) |
88 | 84, 87 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚))) |
89 | 82, 88 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑚) / ((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))) |
90 | 89 | cbvmptv 4678 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚)))) |
91 | 31, 90 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚)))) |
92 | 91 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝐴 = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚))))) |
93 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (2 · 𝑛) → (!‘𝑚) = (!‘(2 · 𝑛))) |
94 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (2 · 𝑛) → (2 · 𝑚) = (2 · (2 ·
𝑛))) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → (√‘(2
· 𝑚)) =
(√‘(2 · (2 · 𝑛)))) |
96 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (2 · 𝑛) → (𝑚 / e) = ((2 · 𝑛) / e)) |
97 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (2 · 𝑛) → 𝑚 = (2 · 𝑛)) |
98 | 96, 97 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → ((𝑚 / e)↑𝑚) = (((2 · 𝑛) / e)↑(2 · 𝑛))) |
99 | 95, 98 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (2 · 𝑛) → ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
100 | 93, 99 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑚 = (2 · 𝑛) → ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚))) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
101 | 100 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 = (2 · 𝑛)) → ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚))) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
102 | | 2nn 11062 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
104 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
105 | 103, 104 | nnmulcld 10945 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ) |
106 | 57, 63, 75 | divcld 10680 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))) ∈ ℂ) |
107 | 92, 101, 105, 106 | fvmptd 6197 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
108 | 107 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐴‘(2 · 𝑛))↑2) = (((!‘(2
· 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2)) |
109 | 108 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2) = ((𝐴‘(2 · 𝑛))↑2)) |
110 | 109 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
111 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
112 | 99 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 = (2 · 𝑛)) → ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
113 | 111, 112,
105, 63 | fvmptd 6197 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛)) = ((√‘(2 · (2 ·
𝑛))) · (((2 ·
𝑛) / e)↑(2 ·
𝑛)))) |
114 | 113 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2) = (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) |
115 | 114 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) = (((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2)) |
116 | 115 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) ·
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2))) |
117 | 81, 110, 116 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2))) |
118 | 88 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚))) |
119 | 118 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
120 | 119 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛)) = ((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))) |
121 | 120 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛)) = ((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))) |
122 | 121 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2) = (((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2)) |
123 | 122 | oveq2d 6565 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2))) |
124 | 107, 106 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) ∈
ℂ) |
125 | | stirlinglem3.2 |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛))) |
126 | 125 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝐴‘(2 · 𝑛)) ∈ ℂ) → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) |
127 | 124, 126 | mpdan 699 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) |
128 | 127 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) = (𝐷‘𝑛)) |
129 | 128 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐴‘(2 · 𝑛))↑2) = ((𝐷‘𝑛)↑2)) |
130 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))) |
131 | 130 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) = ((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))) |
132 | 131 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛)) = (𝐸‘(2 · 𝑛))) |
133 | 132 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2) = ((𝐸‘(2 · 𝑛))↑2)) |
134 | 129, 133 | oveq12d 6567 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) · (((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2)) = (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) |
135 | 117, 123,
134 | 3eqtrd 2648 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) = (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) |
136 | 51, 135 | oveq12d 6567 |
. . . 4
⊢ (𝑛 ∈ ℕ →
(((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) = (((2↑(4
· 𝑛)) ·
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
137 | 136 | oveq1d 6564 |
. . 3
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)) = ((((2↑(4 ·
𝑛)) · (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
138 | 137 | mpteq2ia 4668 |
. 2
⊢ (𝑛 ∈ ℕ ↦
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
139 | 41, 2 | nn0mulcld 11233 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (4
· 𝑛) ∈
ℕ0) |
140 | 6, 139 | expcld 12870 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑(4 · 𝑛))
∈ ℂ) |
141 | 49, 44 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) ∈ ℂ) |
142 | 140, 141 | mulcomd 9940 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) = ((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛)))) |
143 | 142 | oveq1d 6564 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
144 | 143 | oveq1d 6564 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
145 | 127, 124 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) ∈ ℂ) |
146 | 145 | sqcld 12868 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐷‘𝑛)↑2) ∈ ℂ) |
147 | 130, 119 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝐸 = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
148 | 147, 112,
105, 63 | fvmptd 6197 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
149 | 148, 63 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) ∈
ℂ) |
150 | 149 | sqcld 12868 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) ∈
ℂ) |
151 | | nnne0 10930 |
. . . . . . . . . . . 12
⊢
((!‘(2 · 𝑛)) ∈ ℕ → (!‘(2 ·
𝑛)) ≠
0) |
152 | 54, 55, 151 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(!‘(2 · 𝑛))
≠ 0) |
153 | 57, 63, 152, 75 | divne0d 10696 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))) ≠ 0) |
154 | 107, 153 | eqnetrd 2849 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) ≠ 0) |
155 | 127, 154 | eqnetrd 2849 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) ≠ 0) |
156 | 145, 155,
72 | expne0d 12876 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐷‘𝑛)↑2) ≠ 0) |
157 | 148, 75 | eqnetrd 2849 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) ≠ 0) |
158 | 149, 157,
72 | expne0d 12876 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) ≠
0) |
159 | 141, 146,
140, 150, 156, 158 | divmuldivd 10721 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
160 | 159 | eqcomd 2616 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) |
161 | 160 | oveq1d 6564 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
162 | 33, 30 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ∈ ℂ) |
163 | 162, 41 | expcld 12870 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝐴‘𝑛)↑4) ∈ ℂ) |
164 | 38, 45 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝐸‘𝑛)↑4) ∈ ℂ) |
165 | 163, 164,
146, 156 | div23d 10717 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4))) |
166 | 165 | oveq1d 6564 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) |
167 | 166 | oveq1d 6564 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
168 | 163, 146,
156 | divcld 10680 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) ∈ ℂ) |
169 | 140, 150,
158 | divcld 10680 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛)) /
((𝐸‘(2 · 𝑛))↑2)) ∈
ℂ) |
170 | 168, 164,
169 | mulassd 9942 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))))) |
171 | 170 | oveq1d 6564 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = (((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1))) |
172 | 164, 169 | mulcld 9939 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) ∈ ℂ) |
173 | | 1cnd 9935 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
174 | 8, 173 | addcld 9938 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℂ) |
175 | | 0red 9920 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 0 ∈
ℝ) |
176 | 105 | nnred 10912 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
177 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
178 | 177 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ) |
179 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
180 | 178, 179 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
181 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
182 | 180, 181 | readdcld 9948 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℝ) |
183 | 105 | nngt0d 10941 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 0 < (2
· 𝑛)) |
184 | 176 | ltp1d 10833 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) < ((2
· 𝑛) +
1)) |
185 | 175, 176,
182, 183, 184 | lttrd 10077 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 0 <
((2 · 𝑛) +
1)) |
186 | 185 | gt0ne0d 10471 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ≠
0) |
187 | 168, 172,
174, 186 | divassd 10715 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)))) |
188 | 164, 140,
150, 158 | div12d 10716 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((2↑(4 · 𝑛)) · (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)))) |
189 | 9, 17, 41 | mulexpd 12885 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) = (((√‘(2 ·
𝑛))↑4) ·
(((𝑛 / e)↑𝑛)↑4))) |
190 | 60, 62 | sqmuld 12882 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) = (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2))) |
191 | 189, 190 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) =
((((√‘(2 · 𝑛))↑4) · (((𝑛 / e)↑𝑛)↑4)) / (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2)))) |
192 | 148 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) = (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2)) |
193 | 38, 192 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)) = ((((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))) |
194 | 9, 41 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) ∈ ℂ) |
195 | 60 | sqcld 12868 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) ∈ ℂ) |
196 | 17, 41 | expcld 12870 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (((𝑛 / e)↑𝑛)↑4) ∈ ℂ) |
197 | 62 | sqcld 12868 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) ∈
ℂ) |
198 | 60, 67, 72 | expne0d 12876 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) ≠ 0) |
199 | 62, 74, 72 | expne0d 12876 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) ≠
0) |
200 | 194, 195,
196, 197, 198, 199 | divmuldivd 10721 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2))) =
((((√‘(2 · 𝑛))↑4) · (((𝑛 / e)↑𝑛)↑4)) / (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2)))) |
201 | 191, 193,
200 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)) = ((((√‘(2 ·
𝑛))↑4) /
((√‘(2 · (2 · 𝑛)))↑2)) · ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)))) |
202 | 201 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2))) = ((2↑(4 · 𝑛)) · ((((√‘(2
· 𝑛))↑4) /
((√‘(2 · (2 · 𝑛)))↑2)) · ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2))))) |
203 | 65 | rprege0d 11755 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· (2 · 𝑛))
∈ ℝ ∧ 0 ≤ (2 · (2 · 𝑛)))) |
204 | | resqrtth 13844 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· (2 · 𝑛))
∈ ℝ ∧ 0 ≤ (2 · (2 · 𝑛))) → ((√‘(2 · (2
· 𝑛)))↑2) = (2
· (2 · 𝑛))) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) = (2 · (2 · 𝑛))) |
206 | 205 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2)) =
(((√‘(2 · 𝑛))↑4) / (2 · (2 · 𝑛)))) |
207 | | 2t2e4 11054 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 2) = 4 |
208 | 207 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 = (2
· 2) |
209 | 208 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 = (2
· 2)) |
210 | 209 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) = ((√‘(2 ·
𝑛))↑(2 ·
2))) |
211 | 9, 53, 53 | expmuld 12873 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑(2 · 2)) = (((√‘(2
· 𝑛))↑2)↑2)) |
212 | 22 | rprege0d 11755 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) ∈ ℝ
∧ 0 ≤ (2 · 𝑛))) |
213 | | resqrtth 13844 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑛) ∈ ℝ
∧ 0 ≤ (2 · 𝑛)) → ((√‘(2 · 𝑛))↑2) = (2 · 𝑛)) |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑2) = (2 · 𝑛)) |
215 | 214 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑2)↑2) = ((2 · 𝑛)↑2)) |
216 | 210, 211,
215 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) = ((2 · 𝑛)↑2)) |
217 | 6, 6, 7 | mulassd 9942 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 2) · 𝑛) =
(2 · (2 · 𝑛))) |
218 | 207 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (2
· 2) = 4) |
219 | 218 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 2) · 𝑛) =
(4 · 𝑛)) |
220 | 217, 219 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛)) =
(4 · 𝑛)) |
221 | 216, 220 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / (2 · (2 · 𝑛))) = (((2 · 𝑛)↑2) / (4 · 𝑛))) |
222 | 6, 7 | sqmuld 12882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑2) =
((2↑2) · (𝑛↑2))) |
223 | | sq2 12822 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2↑2) = 4 |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(2↑2) = 4) |
225 | 224 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((2↑2) · (𝑛↑2)) = (4 · (𝑛↑2))) |
226 | 222, 225 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑2) = (4
· (𝑛↑2))) |
227 | 226 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛)↑2) / (4
· 𝑛)) = ((4 ·
(𝑛↑2)) / (4 ·
𝑛))) |
228 | | 4cn 10975 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℂ |
229 | | 4ne0 10994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ≠
0 |
230 | 228, 229 | dividi 10637 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 / 4) =
1 |
231 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (4 / 4) =
1) |
232 | 7 | sqvald 12867 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛)) |
233 | 232 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = ((𝑛 · 𝑛) / 𝑛)) |
234 | 7, 7, 25 | divcan4d 10686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛 · 𝑛) / 𝑛) = 𝑛) |
235 | 233, 234 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛) |
236 | 231, 235 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((4 / 4)
· ((𝑛↑2) /
𝑛)) = (1 · 𝑛)) |
237 | 41 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 ∈
ℂ) |
238 | 7 | sqcld 12868 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈
ℂ) |
239 | 229 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 ≠
0) |
240 | 237, 237,
238, 7, 239, 25 | divmuldivd 10721 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((4 / 4)
· ((𝑛↑2) /
𝑛)) = ((4 · (𝑛↑2)) / (4 · 𝑛))) |
241 | 7 | mulid2d 9937 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (1
· 𝑛) = 𝑛) |
242 | 236, 240,
241 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((4
· (𝑛↑2)) / (4
· 𝑛)) = 𝑛) |
243 | 227, 242 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛)↑2) / (4
· 𝑛)) = 𝑛) |
244 | 206, 221,
243 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2)) =
𝑛) |
245 | 7, 237 | mulcomd 9940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 · 4) = (4 · 𝑛)) |
246 | 245 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(𝑛 · 4)) = ((𝑛 / e)↑(4 · 𝑛))) |
247 | 16, 41, 2 | expmuld 12873 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(𝑛 · 4)) = (((𝑛 / e)↑𝑛)↑4)) |
248 | 7, 12, 15, 139 | expdivd 12884 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(4 · 𝑛)) = ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) |
249 | 246, 247,
248 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((𝑛 / e)↑𝑛)↑4) = ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) |
250 | 6, 7, 6 | mul32d 10125 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) · 2) =
((2 · 2) · 𝑛)) |
251 | 250, 219 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) · 2) =
(4 · 𝑛)) |
252 | 251 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑((2
· 𝑛) · 2)) =
(((2 · 𝑛) /
e)↑(4 · 𝑛))) |
253 | 61, 53, 54 | expmuld 12873 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑((2
· 𝑛) · 2)) =
((((2 · 𝑛) /
e)↑(2 · 𝑛))↑2)) |
254 | 8, 12, 15, 139 | expdivd 12884 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(4
· 𝑛)) = (((2
· 𝑛)↑(4
· 𝑛)) / (e↑(4
· 𝑛)))) |
255 | 252, 253,
254 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) = (((2
· 𝑛)↑(4
· 𝑛)) / (e↑(4
· 𝑛)))) |
256 | 249, 255 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)) = (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) / (((2 · 𝑛)↑(4 · 𝑛)) / (e↑(4 · 𝑛))))) |
257 | 249, 196 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) ∈
ℂ) |
258 | 8, 139 | expcld 12870 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) ∈
ℂ) |
259 | 12, 139 | expcld 12870 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(e↑(4 · 𝑛))
∈ ℂ) |
260 | 46, 27 | zmulcld 11364 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (4
· 𝑛) ∈
ℤ) |
261 | 8, 69, 260 | expne0d 12876 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) ≠
0) |
262 | 12, 15, 260 | expne0d 12876 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(e↑(4 · 𝑛))
≠ 0) |
263 | 257, 258,
259, 261, 262 | divdiv2d 10712 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) / (((2 · 𝑛)↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) = ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 · 𝑛))) / ((2 · 𝑛)↑(4 · 𝑛)))) |
264 | 7, 139 | expcld 12870 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑(4 · 𝑛)) ∈
ℂ) |
265 | 264, 259,
262 | divcan1d 10681 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) = (𝑛↑(4 · 𝑛))) |
266 | 265 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) / ((2 · 𝑛)↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((2 · 𝑛)↑(4 · 𝑛)))) |
267 | 6, 7, 139 | mulexpd 12885 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) = ((2↑(4
· 𝑛)) ·
(𝑛↑(4 · 𝑛)))) |
268 | 267 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2 · 𝑛)↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛))))) |
269 | 140, 264 | mulcomd 9940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (𝑛↑(4
· 𝑛))) = ((𝑛↑(4 · 𝑛)) · (2↑(4 ·
𝑛)))) |
270 | 269 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛)))) = ((𝑛↑(4 · 𝑛)) / ((𝑛↑(4 · 𝑛)) · (2↑(4 · 𝑛))))) |
271 | 7, 25, 260 | expne0d 12876 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑(4 · 𝑛)) ≠ 0) |
272 | 6, 68, 260 | expne0d 12876 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(2↑(4 · 𝑛))
≠ 0) |
273 | 264, 264,
140, 271, 272 | divdiv1d 10711 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) / (2↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((𝑛↑(4 · 𝑛)) · (2↑(4 · 𝑛))))) |
274 | 264, 271 | dividd 10678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) = 1) |
275 | 274 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) / (2↑(4 · 𝑛))) = (1 / (2↑(4 · 𝑛)))) |
276 | 270, 273,
275 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛)))) = (1 / (2↑(4 · 𝑛)))) |
277 | 266, 268,
276 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) / ((2 · 𝑛)↑(4 · 𝑛))) = (1 / (2↑(4 ·
𝑛)))) |
278 | 256, 263,
277 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)) = (1 / (2↑(4 · 𝑛)))) |
279 | 244, 278 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2))) =
(𝑛 · (1 / (2↑(4
· 𝑛))))) |
280 | 279 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2)))) =
((2↑(4 · 𝑛))
· (𝑛 · (1 /
(2↑(4 · 𝑛)))))) |
281 | 140, 272 | reccld 10673 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (1 /
(2↑(4 · 𝑛)))
∈ ℂ) |
282 | 140, 7, 281 | mul12d 10124 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (𝑛 · (1 /
(2↑(4 · 𝑛)))))
= (𝑛 · ((2↑(4
· 𝑛)) · (1 /
(2↑(4 · 𝑛)))))) |
283 | 7 | mulid1d 9936 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛) |
284 | 140, 272 | recidd 10675 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (1 / (2↑(4 · 𝑛)))) = 1) |
285 | 284 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · ((2↑(4 ·
𝑛)) · (1 /
(2↑(4 · 𝑛)))))
= (𝑛 ·
1)) |
286 | 283, 285,
235 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 · ((2↑(4 ·
𝑛)) · (1 /
(2↑(4 · 𝑛)))))
= ((𝑛↑2) / 𝑛)) |
287 | 280, 282,
286 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2)))) =
((𝑛↑2) / 𝑛)) |
288 | 188, 202,
287 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((𝑛↑2) / 𝑛)) |
289 | 288 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = (((𝑛↑2) / 𝑛) / ((2 · 𝑛) + 1))) |
290 | 238, 7, 174, 25, 186 | divdiv1d 10711 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) / 𝑛) / ((2 · 𝑛) + 1)) = ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) |
291 | 289, 290 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) |
292 | 291 | oveq2d 6565 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
293 | 187, 292 | eqtrd 2644 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
294 | 167, 171,
293 | 3eqtrd 2648 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
295 | 144, 161,
294 | 3eqtrd 2648 |
. . 3
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
296 | 295 | mpteq2ia 4668 |
. 2
⊢ (𝑛 ∈ ℕ ↦
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ ↦ ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
297 | 1, 138, 296 | 3eqtri 2636 |
1
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |