Step | Hyp | Ref
| Expression |
1 | | stirlinglem3.4 |
. 2
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
((!‘𝑛)↑4)) /
((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
2 | | nnnn0 12097 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
3 | | faccl 13849 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
4 | | nncn 11838 |
. . . . . . . . . . . . 13
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℂ) |
5 | 2, 3, 4 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(!‘𝑛) ∈
ℂ) |
6 | | 2cnd 11908 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) |
7 | | nncn 11838 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
8 | 6, 7 | mulcld 10853 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) |
9 | 8 | sqrtcld 15001 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ∈ ℂ) |
10 | | ere 15650 |
. . . . . . . . . . . . . . . . 17
⊢ e ∈
ℝ |
11 | 10 | recni 10847 |
. . . . . . . . . . . . . . . 16
⊢ e ∈
ℂ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ∈
ℂ) |
13 | | epos 15768 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
e |
14 | 10, 13 | gt0ne0ii 11368 |
. . . . . . . . . . . . . . . 16
⊢ e ≠
0 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ≠
0) |
16 | 7, 12, 15 | divcld 11608 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ∈
ℂ) |
17 | 16, 2 | expcld 13716 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ∈ ℂ) |
18 | 9, 17 | mulcld 10853 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) |
19 | | 2rp 12591 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ+) |
21 | | nnrp 12597 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
22 | 20, 21 | rpmulcld 12644 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ+) |
23 | 22 | sqrtgt0d 14976 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · 𝑛))) |
24 | 23 | gt0ne0d 11396 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ≠ 0) |
25 | | nnne0 11864 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
26 | 7, 12, 25, 15 | divne0d 11624 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ≠ 0) |
27 | | nnz 12199 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
28 | 16, 26, 27 | expne0d 13722 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ≠ 0) |
29 | 9, 17, 24, 28 | mulne0d 11484 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ≠ 0) |
30 | 5, 18, 29 | divcld 11608 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) |
31 | | stirlinglem3.1 |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
32 | 31 | fvmpt2 6829 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
33 | 30, 32 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
34 | 33 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐴‘𝑛)↑4) = (((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4)) |
35 | | stirlinglem3.3 |
. . . . . . . . . . . 12
⊢ 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))) |
36 | 35 | fvmpt2 6829 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) → (𝐸‘𝑛) = ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
37 | 18, 36 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐸‘𝑛) = ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
38 | 37 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐸‘𝑛)↑4) = (((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4)) |
39 | 34, 38 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) = ((((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4))) |
40 | | 4nn0 12109 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 4 ∈
ℕ0) |
42 | 5, 18, 29, 41 | expdivd 13730 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) = (((!‘𝑛)↑4) / (((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4))) |
43 | 42 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) = ((((!‘𝑛)↑4) / (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) ·
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4))) |
44 | 5, 41 | expcld 13716 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
((!‘𝑛)↑4) ∈
ℂ) |
45 | 18, 41 | expcld 13716 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) ∈ ℂ) |
46 | 41 | nn0zd 12280 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 4 ∈
ℤ) |
47 | 18, 29, 46 | expne0d 13722 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) ≠ 0) |
48 | 44, 45, 47 | divcan1d 11609 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘𝑛)↑4) /
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4)) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) = ((!‘𝑛)↑4)) |
49 | 39, 43, 48 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) = ((!‘𝑛)↑4)) |
50 | 49 | eqcomd 2743 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((!‘𝑛)↑4) =
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) |
51 | 50 | oveq2d 7229 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) = ((2↑(4 · 𝑛)) · (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)))) |
52 | | 2nn0 12107 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ0) |
54 | 53, 2 | nn0mulcld 12155 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ0) |
55 | | faccl 13849 |
. . . . . . . . . . 11
⊢ ((2
· 𝑛) ∈
ℕ0 → (!‘(2 · 𝑛)) ∈ ℕ) |
56 | | nncn 11838 |
. . . . . . . . . . 11
⊢
((!‘(2 · 𝑛)) ∈ ℕ → (!‘(2 ·
𝑛)) ∈
ℂ) |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(!‘(2 · 𝑛))
∈ ℂ) |
58 | 57 | sqcld 13714 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) ∈ ℂ) |
59 | 6, 8 | mulcld 10853 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛))
∈ ℂ) |
60 | 59 | sqrtcld 15001 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(√‘(2 · (2 · 𝑛))) ∈ ℂ) |
61 | 8, 12, 15 | divcld 11608 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) / e) ∈
ℂ) |
62 | 61, 54 | expcld 13716 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(2
· 𝑛)) ∈
ℂ) |
63 | 60, 62 | mulcld 10853 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))) ∈ ℂ) |
64 | 63 | sqcld 13714 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) ∈ ℂ) |
65 | 20, 22 | rpmulcld 12644 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛))
∈ ℝ+) |
66 | 65 | sqrtgt0d 14976 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · (2 · 𝑛)))) |
67 | 66 | gt0ne0d 11396 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(√‘(2 · (2 · 𝑛))) ≠ 0) |
68 | 20 | rpne0d 12633 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 2 ≠
0) |
69 | 6, 7, 68, 25 | mulne0d 11484 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ≠
0) |
70 | 8, 12, 69, 15 | divne0d 11624 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) / e) ≠
0) |
71 | | 2z 12209 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 2 ∈
ℤ) |
73 | 72, 27 | zmulcld 12288 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℤ) |
74 | 61, 70, 73 | expne0d 13722 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(2
· 𝑛)) ≠
0) |
75 | 60, 62, 67, 74 | mulne0d 11484 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))) ≠ 0) |
76 | 63, 75, 72 | expne0d 13722 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) ≠ 0) |
77 | 58, 64, 76 | divcan1d 11609 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘(2 · 𝑛))↑2) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))
· (((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2)) = ((!‘(2 · 𝑛))↑2)) |
78 | 57, 63, 75, 53 | expdivd 13730 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2) = (((!‘(2 · 𝑛))↑2) / (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
79 | 78 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((!‘(2 · 𝑛))↑2) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) =
(((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2)) |
80 | 79 | oveq1d 7228 |
. . . . . . . 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 2779 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) = ((((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
82 | | fveq2 6717 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (!‘𝑛) = (!‘𝑚)) |
83 | | oveq2 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚)) |
84 | 83 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑚))) |
85 | | oveq1 7220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑛 / e) = (𝑚 / e)) |
86 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → 𝑛 = 𝑚) |
87 | 85, 86 | oveq12d 7231 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑛 / e)↑𝑛) = ((𝑚 / e)↑𝑚)) |
88 | 84, 87 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚))) |
89 | 82, 88 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑚) / ((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))) |
90 | 89 | cbvmptv 5158 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚)))) |
91 | 31, 90 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝐴 = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚)))) |
92 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑚 = (2 · 𝑛) → (!‘𝑚) = (!‘(2 · 𝑛))) |
93 | | oveq2 7221 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → (2 · 𝑚) = (2 · (2 ·
𝑛))) |
94 | 93 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (2 · 𝑛) → (√‘(2
· 𝑚)) =
(√‘(2 · (2 · 𝑛)))) |
95 | | oveq1 7220 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → (𝑚 / e) = ((2 · 𝑛) / e)) |
96 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → 𝑚 = (2 · 𝑛)) |
97 | 95, 96 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (2 · 𝑛) → ((𝑚 / e)↑𝑚) = (((2 · 𝑛) / e)↑(2 · 𝑛))) |
98 | 94, 97 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑚 = (2 · 𝑛) → ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
99 | 92, 98 | oveq12d 7231 |
. . . . . . . . . . 11
⊢ (𝑚 = (2 · 𝑛) → ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚))) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
100 | | 2nn 11903 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
102 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
103 | 101, 102 | nnmulcld 11883 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ) |
104 | 57, 63, 75 | divcld 11608 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))) ∈ ℂ) |
105 | 91, 99, 103, 104 | fvmptd3 6841 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
106 | 105 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐴‘(2 · 𝑛))↑2) = (((!‘(2
· 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2)) |
107 | 106 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2) = ((𝐴‘(2 · 𝑛))↑2)) |
108 | 107 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((((!‘(2 · 𝑛))
/ ((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2))) |
109 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
110 | 98 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 = (2 · 𝑛)) → ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
111 | 109, 110,
103, 63 | fvmptd 6825 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛)) = ((√‘(2 · (2 ·
𝑛))) · (((2 ·
𝑛) / e)↑(2 ·
𝑛)))) |
112 | 111 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2) = (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) |
113 | 112 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) = (((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2)) |
114 | 113 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) ·
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2))) |
115 | 81, 108, 114 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2))) |
116 | 88 | cbvmptv 5158 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚))) |
117 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
118 | 117 | fveq1d 6719 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛)) = ((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))) |
119 | 118 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛)) = ((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))) |
120 | 119 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2) = (((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2)) |
121 | 120 | oveq2d 7229 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2))) |
122 | 105, 104 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) ∈
ℂ) |
123 | | stirlinglem3.2 |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛))) |
124 | 123 | fvmpt2 6829 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝐴‘(2 · 𝑛)) ∈ ℂ) → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) |
125 | 122, 124 | mpdan 687 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) |
126 | 125 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) = (𝐷‘𝑛)) |
127 | 126 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐴‘(2 · 𝑛))↑2) = ((𝐷‘𝑛)↑2)) |
128 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))) |
129 | 128 | fveq1d 6719 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) = ((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))) |
130 | 129 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛)) = (𝐸‘(2 · 𝑛))) |
131 | 130 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2) = ((𝐸‘(2 · 𝑛))↑2)) |
132 | 127, 131 | oveq12d 7231 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) · (((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2)) = (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) |
133 | 115, 121,
132 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) = (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) |
134 | 51, 133 | oveq12d 7231 |
. . . 4
⊢ (𝑛 ∈ ℕ →
(((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) = (((2↑(4
· 𝑛)) ·
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
135 | 134 | oveq1d 7228 |
. . 3
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)) = ((((2↑(4 ·
𝑛)) · (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
136 | 135 | mpteq2ia 5146 |
. 2
⊢ (𝑛 ∈ ℕ ↦
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
137 | 41, 2 | nn0mulcld 12155 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (4
· 𝑛) ∈
ℕ0) |
138 | 6, 137 | expcld 13716 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑(4 · 𝑛))
∈ ℂ) |
139 | 49, 44 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) ∈ ℂ) |
140 | 138, 139 | mulcomd 10854 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) = ((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛)))) |
141 | 140 | oveq1d 7228 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
142 | 141 | oveq1d 7228 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
143 | 125, 122 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) ∈ ℂ) |
144 | 143 | sqcld 13714 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐷‘𝑛)↑2) ∈ ℂ) |
145 | 128, 117 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝐸 = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
146 | 145, 110,
103, 63 | fvmptd 6825 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
147 | 146, 63 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) ∈
ℂ) |
148 | 147 | sqcld 13714 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) ∈
ℂ) |
149 | | nnne0 11864 |
. . . . . . . . . . . 12
⊢
((!‘(2 · 𝑛)) ∈ ℕ → (!‘(2 ·
𝑛)) ≠
0) |
150 | 54, 55, 149 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(!‘(2 · 𝑛))
≠ 0) |
151 | 57, 63, 150, 75 | divne0d 11624 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))) ≠ 0) |
152 | 105, 151 | eqnetrd 3008 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) ≠ 0) |
153 | 125, 152 | eqnetrd 3008 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) ≠ 0) |
154 | 143, 153,
72 | expne0d 13722 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐷‘𝑛)↑2) ≠ 0) |
155 | 146, 75 | eqnetrd 3008 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) ≠ 0) |
156 | 147, 155,
72 | expne0d 13722 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) ≠
0) |
157 | 139, 144,
138, 148, 154, 156 | divmuldivd 11649 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
158 | 157 | eqcomd 2743 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) |
159 | 158 | oveq1d 7228 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
160 | 33, 30 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ∈ ℂ) |
161 | 160, 41 | expcld 13716 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝐴‘𝑛)↑4) ∈ ℂ) |
162 | 38, 45 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝐸‘𝑛)↑4) ∈ ℂ) |
163 | 161, 162,
144, 154 | div23d 11645 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4))) |
164 | 163 | oveq1d 7228 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) |
165 | 164 | oveq1d 7228 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
166 | 161, 144,
154 | divcld 11608 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) ∈ ℂ) |
167 | 138, 148,
156 | divcld 11608 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛)) /
((𝐸‘(2 · 𝑛))↑2)) ∈
ℂ) |
168 | 166, 162,
167 | mulassd 10856 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))))) |
169 | 168 | oveq1d 7228 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = (((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1))) |
170 | 162, 167 | mulcld 10853 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) ∈ ℂ) |
171 | | 1cnd 10828 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
172 | 8, 171 | addcld 10852 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℂ) |
173 | | 0red 10836 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 0 ∈
ℝ) |
174 | 103 | nnred 11845 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
175 | | 2re 11904 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
176 | 175 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ) |
177 | | nnre 11837 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
178 | 176, 177 | remulcld 10863 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
179 | | 1red 10834 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
180 | 178, 179 | readdcld 10862 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℝ) |
181 | 103 | nngt0d 11879 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 0 < (2
· 𝑛)) |
182 | 174 | ltp1d 11762 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) < ((2
· 𝑛) +
1)) |
183 | 173, 174,
180, 181, 182 | lttrd 10993 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 0 <
((2 · 𝑛) +
1)) |
184 | 183 | gt0ne0d 11396 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ≠
0) |
185 | 166, 170,
172, 184 | divassd 11643 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)))) |
186 | 162, 138,
148, 156 | div12d 11644 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((2↑(4 · 𝑛)) · (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)))) |
187 | 9, 17, 41 | mulexpd 13731 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) = (((√‘(2 ·
𝑛))↑4) ·
(((𝑛 / e)↑𝑛)↑4))) |
188 | 60, 62 | sqmuld 13728 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) = (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2))) |
189 | 187, 188 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) =
((((√‘(2 · 𝑛))↑4) · (((𝑛 / e)↑𝑛)↑4)) / (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2)))) |
190 | 146 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) = (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2)) |
191 | 38, 190 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)) = ((((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))) |
192 | 9, 41 | expcld 13716 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) ∈ ℂ) |
193 | 60 | sqcld 13714 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) ∈ ℂ) |
194 | 17, 41 | expcld 13716 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (((𝑛 / e)↑𝑛)↑4) ∈ ℂ) |
195 | 62 | sqcld 13714 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) ∈
ℂ) |
196 | 60, 67, 72 | expne0d 13722 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) ≠ 0) |
197 | 62, 74, 72 | expne0d 13722 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) ≠
0) |
198 | 192, 193,
194, 195, 196, 197 | divmuldivd 11649 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2))) =
((((√‘(2 · 𝑛))↑4) · (((𝑛 / e)↑𝑛)↑4)) / (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2)))) |
199 | 189, 191,
198 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)) = ((((√‘(2 ·
𝑛))↑4) /
((√‘(2 · (2 · 𝑛)))↑2)) · ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)))) |
200 | 199 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2))) = ((2↑(4 · 𝑛)) · ((((√‘(2
· 𝑛))↑4) /
((√‘(2 · (2 · 𝑛)))↑2)) · ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2))))) |
201 | 65 | rprege0d 12635 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· (2 · 𝑛))
∈ ℝ ∧ 0 ≤ (2 · (2 · 𝑛)))) |
202 | | resqrtth 14819 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· (2 · 𝑛))
∈ ℝ ∧ 0 ≤ (2 · (2 · 𝑛))) → ((√‘(2 · (2
· 𝑛)))↑2) = (2
· (2 · 𝑛))) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) = (2 · (2 · 𝑛))) |
204 | 203 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2)) =
(((√‘(2 · 𝑛))↑4) / (2 · (2 · 𝑛)))) |
205 | | 2t2e4 11994 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 2) = 4 |
206 | 205 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 = (2
· 2) |
207 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 = (2
· 2)) |
208 | 207 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) = ((√‘(2 ·
𝑛))↑(2 ·
2))) |
209 | 9, 53, 53 | expmuld 13719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑(2 · 2)) = (((√‘(2
· 𝑛))↑2)↑2)) |
210 | 22 | rprege0d 12635 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) ∈ ℝ
∧ 0 ≤ (2 · 𝑛))) |
211 | | resqrtth 14819 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑛) ∈ ℝ
∧ 0 ≤ (2 · 𝑛)) → ((√‘(2 · 𝑛))↑2) = (2 · 𝑛)) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑2) = (2 · 𝑛)) |
213 | 212 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑2)↑2) = ((2 · 𝑛)↑2)) |
214 | 208, 209,
213 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) = ((2 · 𝑛)↑2)) |
215 | 6, 6, 7 | mulassd 10856 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 2) · 𝑛) =
(2 · (2 · 𝑛))) |
216 | 205 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (2
· 2) = 4) |
217 | 216 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 2) · 𝑛) =
(4 · 𝑛)) |
218 | 215, 217 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛)) =
(4 · 𝑛)) |
219 | 214, 218 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / (2 · (2 · 𝑛))) = (((2 · 𝑛)↑2) / (4 · 𝑛))) |
220 | 6, 7 | sqmuld 13728 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑2) =
((2↑2) · (𝑛↑2))) |
221 | | sq2 13766 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2↑2) = 4 |
222 | 221 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(2↑2) = 4) |
223 | 222 | oveq1d 7228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((2↑2) · (𝑛↑2)) = (4 · (𝑛↑2))) |
224 | 220, 223 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑2) = (4
· (𝑛↑2))) |
225 | 224 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛)↑2) / (4
· 𝑛)) = ((4 ·
(𝑛↑2)) / (4 ·
𝑛))) |
226 | | 4cn 11915 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℂ |
227 | | 4ne0 11938 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ≠
0 |
228 | 226, 227 | dividi 11565 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 / 4) =
1 |
229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (4 / 4) =
1) |
230 | 7 | sqvald 13713 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛)) |
231 | 230 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = ((𝑛 · 𝑛) / 𝑛)) |
232 | 7, 7, 25 | divcan4d 11614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛 · 𝑛) / 𝑛) = 𝑛) |
233 | 231, 232 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛) |
234 | 229, 233 | oveq12d 7231 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((4 / 4)
· ((𝑛↑2) /
𝑛)) = (1 · 𝑛)) |
235 | 41 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 ∈
ℂ) |
236 | 7 | sqcld 13714 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈
ℂ) |
237 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 ≠
0) |
238 | 235, 235,
236, 7, 237, 25 | divmuldivd 11649 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((4 / 4)
· ((𝑛↑2) /
𝑛)) = ((4 · (𝑛↑2)) / (4 · 𝑛))) |
239 | 7 | mulid2d 10851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (1
· 𝑛) = 𝑛) |
240 | 234, 238,
239 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((4
· (𝑛↑2)) / (4
· 𝑛)) = 𝑛) |
241 | 225, 240 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛)↑2) / (4
· 𝑛)) = 𝑛) |
242 | 204, 219,
241 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2)) =
𝑛) |
243 | 7, 235 | mulcomd 10854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 · 4) = (4 · 𝑛)) |
244 | 243 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(𝑛 · 4)) = ((𝑛 / e)↑(4 · 𝑛))) |
245 | 16, 41, 2 | expmuld 13719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(𝑛 · 4)) = (((𝑛 / e)↑𝑛)↑4)) |
246 | 7, 12, 15, 137 | expdivd 13730 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(4 · 𝑛)) = ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) |
247 | 244, 245,
246 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((𝑛 / e)↑𝑛)↑4) = ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) |
248 | 6, 7, 6 | mul32d 11042 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) · 2) =
((2 · 2) · 𝑛)) |
249 | 248, 217 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) · 2) =
(4 · 𝑛)) |
250 | 249 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑((2
· 𝑛) · 2)) =
(((2 · 𝑛) /
e)↑(4 · 𝑛))) |
251 | 61, 53, 54 | expmuld 13719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑((2
· 𝑛) · 2)) =
((((2 · 𝑛) /
e)↑(2 · 𝑛))↑2)) |
252 | 8, 12, 15, 137 | expdivd 13730 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(4
· 𝑛)) = (((2
· 𝑛)↑(4
· 𝑛)) / (e↑(4
· 𝑛)))) |
253 | 250, 251,
252 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) = (((2
· 𝑛)↑(4
· 𝑛)) / (e↑(4
· 𝑛)))) |
254 | 247, 253 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)) = (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) / (((2 · 𝑛)↑(4 · 𝑛)) / (e↑(4 · 𝑛))))) |
255 | 247, 194 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) ∈
ℂ) |
256 | 8, 137 | expcld 13716 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) ∈
ℂ) |
257 | 12, 137 | expcld 13716 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(e↑(4 · 𝑛))
∈ ℂ) |
258 | 46, 27 | zmulcld 12288 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (4
· 𝑛) ∈
ℤ) |
259 | 8, 69, 258 | expne0d 13722 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) ≠
0) |
260 | 12, 15, 258 | expne0d 13722 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(e↑(4 · 𝑛))
≠ 0) |
261 | 255, 256,
257, 259, 260 | divdiv2d 11640 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) / (((2 · 𝑛)↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) = ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 · 𝑛))) / ((2 · 𝑛)↑(4 · 𝑛)))) |
262 | 7, 137 | expcld 13716 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑(4 · 𝑛)) ∈
ℂ) |
263 | 262, 257,
260 | divcan1d 11609 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) = (𝑛↑(4 · 𝑛))) |
264 | 263 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) / ((2 · 𝑛)↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((2 · 𝑛)↑(4 · 𝑛)))) |
265 | 6, 7, 137 | mulexpd 13731 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) = ((2↑(4
· 𝑛)) ·
(𝑛↑(4 · 𝑛)))) |
266 | 265 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2 · 𝑛)↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛))))) |
267 | 138, 262 | mulcomd 10854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (𝑛↑(4
· 𝑛))) = ((𝑛↑(4 · 𝑛)) · (2↑(4 ·
𝑛)))) |
268 | 267 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛)))) = ((𝑛↑(4 · 𝑛)) / ((𝑛↑(4 · 𝑛)) · (2↑(4 · 𝑛))))) |
269 | 7, 25, 258 | expne0d 13722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑(4 · 𝑛)) ≠ 0) |
270 | 6, 68, 258 | expne0d 13722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(2↑(4 · 𝑛))
≠ 0) |
271 | 262, 262,
138, 269, 270 | divdiv1d 11639 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) / (2↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((𝑛↑(4 · 𝑛)) · (2↑(4 · 𝑛))))) |
272 | 262, 269 | dividd 11606 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) = 1) |
273 | 272 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) / (2↑(4 · 𝑛))) = (1 / (2↑(4 · 𝑛)))) |
274 | 268, 271,
273 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛)))) = (1 / (2↑(4 · 𝑛)))) |
275 | 264, 266,
274 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) / ((2 · 𝑛)↑(4 · 𝑛))) = (1 / (2↑(4 ·
𝑛)))) |
276 | 254, 261,
275 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)) = (1 / (2↑(4 · 𝑛)))) |
277 | 242, 276 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2))) =
(𝑛 · (1 / (2↑(4
· 𝑛))))) |
278 | 277 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2)))) =
((2↑(4 · 𝑛))
· (𝑛 · (1 /
(2↑(4 · 𝑛)))))) |
279 | 138, 270 | reccld 11601 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (1 /
(2↑(4 · 𝑛)))
∈ ℂ) |
280 | 138, 7, 279 | mul12d 11041 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (𝑛 · (1 /
(2↑(4 · 𝑛)))))
= (𝑛 · ((2↑(4
· 𝑛)) · (1 /
(2↑(4 · 𝑛)))))) |
281 | 7 | mulid1d 10850 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛) |
282 | 138, 270 | recidd 11603 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (1 / (2↑(4 · 𝑛)))) = 1) |
283 | 282 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · ((2↑(4 ·
𝑛)) · (1 /
(2↑(4 · 𝑛)))))
= (𝑛 ·
1)) |
284 | 281, 283,
233 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 · ((2↑(4 ·
𝑛)) · (1 /
(2↑(4 · 𝑛)))))
= ((𝑛↑2) / 𝑛)) |
285 | 278, 280,
284 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2)))) =
((𝑛↑2) / 𝑛)) |
286 | 186, 200,
285 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((𝑛↑2) / 𝑛)) |
287 | 286 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = (((𝑛↑2) / 𝑛) / ((2 · 𝑛) + 1))) |
288 | 236, 7, 172, 25, 184 | divdiv1d 11639 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝑛↑2) / 𝑛) / ((2 · 𝑛) + 1)) = ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) |
289 | 287, 288 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) |
290 | 289 | oveq2d 7229 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
291 | 185, 290 | eqtrd 2777 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
292 | 165, 169,
291 | 3eqtrd 2781 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
293 | 142, 159,
292 | 3eqtrd 2781 |
. . 3
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
294 | 293 | mpteq2ia 5146 |
. 2
⊢ (𝑛 ∈ ℕ ↦
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ ↦ ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |
295 | 1, 136, 294 | 3eqtri 2769 |
1
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))) |