| Step | Hyp | Ref
| Expression |
| 1 | | stirlinglem3.4 |
. 2
⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
((!‘𝑛)↑4)) /
((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) |
| 2 | | nnnn0 12533 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 3 | | faccl 14322 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (!‘𝑛) ∈
ℕ) |
| 4 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢
((!‘𝑛) ∈
ℕ → (!‘𝑛)
∈ ℂ) |
| 5 | 2, 3, 4 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(!‘𝑛) ∈
ℂ) |
| 6 | | 2cnd 12344 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) |
| 7 | | nncn 12274 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
| 8 | 6, 7 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) |
| 9 | 8 | sqrtcld 15476 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ∈ ℂ) |
| 10 | | ere 16125 |
. . . . . . . . . . . . . . . . 17
⊢ e ∈
ℝ |
| 11 | 10 | recni 11275 |
. . . . . . . . . . . . . . . 16
⊢ e ∈
ℂ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ∈
ℂ) |
| 13 | | epos 16243 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
e |
| 14 | 10, 13 | gt0ne0ii 11799 |
. . . . . . . . . . . . . . . 16
⊢ e ≠
0 |
| 15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → e ≠
0) |
| 16 | 7, 12, 15 | divcld 12043 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ∈
ℂ) |
| 17 | 16, 2 | expcld 14186 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ∈ ℂ) |
| 18 | 9, 17 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) |
| 19 | | 2rp 13039 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
| 20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ+) |
| 21 | | nnrp 13046 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
| 22 | 20, 21 | rpmulcld 13093 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ+) |
| 23 | 22 | sqrtgt0d 15451 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · 𝑛))) |
| 24 | 23 | gt0ne0d 11827 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(√‘(2 · 𝑛)) ≠ 0) |
| 25 | | nnne0 12300 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
| 26 | 7, 12, 25, 15 | divne0d 12059 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 / e) ≠ 0) |
| 27 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
| 28 | 16, 26, 27 | expne0d 14192 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑𝑛) ≠ 0) |
| 29 | 9, 17, 24, 28 | mulne0d 11915 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ≠ 0) |
| 30 | 5, 18, 29 | divcld 12043 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) |
| 31 | | stirlinglem3.1 |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛)))) |
| 32 | 31 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) ∈ ℂ) → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
| 33 | 30, 32 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) = ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐴‘𝑛)↑4) = (((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4)) |
| 35 | | stirlinglem3.3 |
. . . . . . . . . . . 12
⊢ 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))) |
| 36 | 35 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) ∈ ℂ) → (𝐸‘𝑛) = ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
| 37 | 18, 36 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐸‘𝑛) = ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) |
| 38 | 37 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝐸‘𝑛)↑4) = (((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4)) |
| 39 | 34, 38 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) = ((((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4))) |
| 40 | | 4nn0 12545 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
| 41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 4 ∈
ℕ0) |
| 42 | 5, 18, 29, 41 | expdivd 14200 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) = (((!‘𝑛)↑4) / (((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4))) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))↑4) · (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) = ((((!‘𝑛)↑4) / (((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛))↑4)) ·
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4))) |
| 44 | 5, 41 | expcld 14186 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
((!‘𝑛)↑4) ∈
ℂ) |
| 45 | 18, 41 | expcld 14186 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) ∈ ℂ) |
| 46 | 41 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 4 ∈
ℤ) |
| 47 | 18, 29, 46 | expne0d 14192 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) ≠ 0) |
| 48 | 44, 45, 47 | divcan1d 12044 |
. . . . . . . 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 7447 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) = ((2↑(4 · 𝑛)) · (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)))) |
| 52 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ0) |
| 54 | 53, 2 | nn0mulcld 12592 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ0) |
| 55 | | faccl 14322 |
. . . . . . . . . . 11
⊢ ((2
· 𝑛) ∈
ℕ0 → (!‘(2 · 𝑛)) ∈ ℕ) |
| 56 | | nncn 12274 |
. . . . . . . . . . 11
⊢
((!‘(2 · 𝑛)) ∈ ℕ → (!‘(2 ·
𝑛)) ∈
ℂ) |
| 57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(!‘(2 · 𝑛))
∈ ℂ) |
| 58 | 57 | sqcld 14184 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛))↑2) ∈ ℂ) |
| 59 | 6, 8 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛))
∈ ℂ) |
| 60 | 59 | sqrtcld 15476 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(√‘(2 · (2 · 𝑛))) ∈ ℂ) |
| 61 | 8, 12, 15 | divcld 12043 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) / e) ∈
ℂ) |
| 62 | 61, 54 | expcld 14186 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(2
· 𝑛)) ∈
ℂ) |
| 63 | 60, 62 | mulcld 11281 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))) ∈ ℂ) |
| 64 | 63 | sqcld 14184 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) ∈ ℂ) |
| 65 | 20, 22 | rpmulcld 13093 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛))
∈ ℝ+) |
| 66 | 65 | sqrtgt0d 15451 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 <
(√‘(2 · (2 · 𝑛)))) |
| 67 | 66 | gt0ne0d 11827 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(√‘(2 · (2 · 𝑛))) ≠ 0) |
| 68 | 20 | rpne0d 13082 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 2 ≠
0) |
| 69 | 6, 7, 68, 25 | mulne0d 11915 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ≠
0) |
| 70 | 8, 12, 69, 15 | divne0d 12059 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) / e) ≠
0) |
| 71 | | 2z 12649 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
| 72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 2 ∈
ℤ) |
| 73 | 72, 27 | zmulcld 12728 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℤ) |
| 74 | 61, 70, 73 | expne0d 14192 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑(2
· 𝑛)) ≠
0) |
| 75 | 60, 62, 67, 74 | mulne0d 11915 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛))) ≠ 0) |
| 76 | 63, 75, 72 | expne0d 14192 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) ≠ 0) |
| 77 | 58, 64, 76 | divcan1d 12044 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
((((!‘(2 · 𝑛))↑2) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))
· (((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2)) = ((!‘(2 · 𝑛))↑2)) |
| 78 | 57, 63, 75, 53 | expdivd 14200 |
. . . . . . . . . 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 7446 |
. . . . . . . 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 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (!‘𝑛) = (!‘𝑚)) |
| 83 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚)) |
| 84 | 83 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (√‘(2 · 𝑛)) = (√‘(2 ·
𝑚))) |
| 85 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑛 / e) = (𝑚 / e)) |
| 86 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → 𝑛 = 𝑚) |
| 87 | 85, 86 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑛 / e)↑𝑛) = ((𝑚 / e)↑𝑚)) |
| 88 | 84, 87 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)) = ((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚))) |
| 89 | 82, 88 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = ((!‘𝑚) / ((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))) |
| 90 | 89 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦
((!‘𝑛) /
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))) = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚)))) |
| 91 | 31, 90 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝐴 = (𝑚 ∈ ℕ ↦ ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚)))) |
| 92 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑚 = (2 · 𝑛) → (!‘𝑚) = (!‘(2 · 𝑛))) |
| 93 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → (2 · 𝑚) = (2 · (2 ·
𝑛))) |
| 94 | 93 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (2 · 𝑛) → (√‘(2
· 𝑚)) =
(√‘(2 · (2 · 𝑛)))) |
| 95 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → (𝑚 / e) = ((2 · 𝑛) / e)) |
| 96 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (2 · 𝑛) → 𝑚 = (2 · 𝑛)) |
| 97 | 95, 96 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (2 · 𝑛) → ((𝑚 / e)↑𝑚) = (((2 · 𝑛) / e)↑(2 · 𝑛))) |
| 98 | 94, 97 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑚 = (2 · 𝑛) → ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
| 99 | 92, 98 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑚 = (2 · 𝑛) → ((!‘𝑚) / ((√‘(2 ·
𝑚)) · ((𝑚 / e)↑𝑚))) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
| 100 | | 2nn 12339 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
| 101 | 100 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
| 102 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
| 103 | 101, 102 | nnmulcld 12319 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ) |
| 104 | 57, 63, 75 | divcld 12043 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((!‘(2 · 𝑛)) /
((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))) ∈ ℂ) |
| 105 | 91, 99, 103, 104 | fvmptd3 7039 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) = ((!‘(2 · 𝑛)) / ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛))))) |
| 106 | 105 | oveq1d 7446 |
. . . . . . . . 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 7446 |
. . . . . . 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 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 = (2 · 𝑛)) → ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
| 111 | 109, 110,
103, 63 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛)) = ((√‘(2 · (2 ·
𝑛))) · (((2 ·
𝑛) / e)↑(2 ·
𝑛)))) |
| 112 | 111 | oveq1d 7446 |
. . . . . . . . 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 7447 |
. . . . . . 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 5255 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚))) |
| 117 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))) = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
| 118 | 117 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛)) = ((𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))‘(2 · 𝑛))) |
| 119 | 118 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛)) = ((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))) |
| 120 | 119 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2) = (((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2)) |
| 121 | 120 | oveq2d 7447 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (((𝐴‘(2 · 𝑛))↑2) · (((𝑚 ∈ ℕ ↦
((√‘(2 · 𝑚)) · ((𝑚 / e)↑𝑚)))‘(2 · 𝑛))↑2)) = (((𝐴‘(2 · 𝑛))↑2) · (((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2))) |
| 122 | 105, 104 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) ∈
ℂ) |
| 123 | | stirlinglem3.2 |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛))) |
| 124 | 123 | fvmpt2 7027 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ (𝐴‘(2 · 𝑛)) ∈ ℂ) → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) |
| 125 | 122, 124 | mpdan 687 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) = (𝐴‘(2 · 𝑛))) |
| 126 | 125 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐴‘(2 · 𝑛)) = (𝐷‘𝑛)) |
| 127 | 126 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐴‘(2 · 𝑛))↑2) = ((𝐷‘𝑛)↑2)) |
| 128 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))) |
| 129 | 128 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) = ((𝑛 ∈ ℕ ↦ ((√‘(2
· 𝑛)) ·
((𝑛 / e)↑𝑛)))‘(2 · 𝑛))) |
| 130 | 129 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛)) = (𝐸‘(2 · 𝑛))) |
| 131 | 130 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝑛 ∈ ℕ ↦
((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))‘(2 · 𝑛))↑2) = ((𝐸‘(2 · 𝑛))↑2)) |
| 132 | 127, 131 | oveq12d 7449 |
. . . . . 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 7449 |
. . . 4
⊢ (𝑛 ∈ ℕ →
(((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) = (((2↑(4
· 𝑛)) ·
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
| 135 | 134 | oveq1d 7446 |
. . 3
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)) = ((((2↑(4 ·
𝑛)) · (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
| 136 | 135 | mpteq2ia 5245 |
. 2
⊢ (𝑛 ∈ ℕ ↦
((((2↑(4 · 𝑛))
· ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ ↦ ((((2↑(4
· 𝑛)) ·
(((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
| 137 | 41, 2 | nn0mulcld 12592 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (4
· 𝑛) ∈
ℕ0) |
| 138 | 6, 137 | expcld 14186 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑(4 · 𝑛))
∈ ℂ) |
| 139 | 49, 44 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) ∈ ℂ) |
| 140 | 138, 139 | mulcomd 11282 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) = ((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛)))) |
| 141 | 140 | oveq1d 7446 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2)))) |
| 142 | 141 | oveq1d 7446 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((2↑(4 · 𝑛))
· (((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
| 143 | 125, 122 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐷‘𝑛) ∈ ℂ) |
| 144 | 143 | sqcld 14184 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐷‘𝑛)↑2) ∈ ℂ) |
| 145 | 128, 117 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝐸 = (𝑚 ∈ ℕ ↦ ((√‘(2
· 𝑚)) ·
((𝑚 / e)↑𝑚)))) |
| 146 | 145, 110,
103, 63 | fvmptd 7023 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) = ((√‘(2 ·
(2 · 𝑛))) ·
(((2 · 𝑛) /
e)↑(2 · 𝑛)))) |
| 147 | 146, 63 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) ∈
ℂ) |
| 148 | 147 | sqcld 14184 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) ∈
ℂ) |
| 149 | | nnne0 12300 |
. . . . . . . . . . . 12
⊢
((!‘(2 · 𝑛)) ∈ ℕ → (!‘(2 ·
𝑛)) ≠
0) |
| 150 | 54, 55, 149 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(!‘(2 · 𝑛))
≠ 0) |
| 151 | 57, 63, 150, 75 | divne0d 12059 |
. . . . . . . . . 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 14192 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐷‘𝑛)↑2) ≠ 0) |
| 155 | 146, 75 | eqnetrd 3008 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝐸‘(2 · 𝑛)) ≠ 0) |
| 156 | 147, 155,
72 | expne0d 14192 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) ≠
0) |
| 157 | 139, 144,
138, 148, 154, 156 | divmuldivd 12084 |
. . . . . 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 7446 |
. . . 4
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) · (2↑(4 · 𝑛))) / (((𝐷‘𝑛)↑2) · ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
| 160 | 33, 30 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝐴‘𝑛) ∈ ℂ) |
| 161 | 160, 41 | expcld 14186 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝐴‘𝑛)↑4) ∈ ℂ) |
| 162 | 38, 45 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝐸‘𝑛)↑4) ∈ ℂ) |
| 163 | 161, 162,
144, 154 | div23d 12080 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4))) |
| 164 | 163 | oveq1d 7446 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = (((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) |
| 165 | 164 | oveq1d 7446 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) · ((𝐸‘𝑛)↑4)) / ((𝐷‘𝑛)↑2)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = ((((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1))) |
| 166 | 161, 144,
154 | divcld 12043 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) ∈ ℂ) |
| 167 | 138, 148,
156 | divcld 12043 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛)) /
((𝐸‘(2 · 𝑛))↑2)) ∈
ℂ) |
| 168 | 166, 162,
167 | mulassd 11284 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))))) |
| 169 | 168 | oveq1d 7446 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
((((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · ((𝐸‘𝑛)↑4)) · ((2↑(4 ·
𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = (((((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)) · (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2)))) / ((2 · 𝑛) + 1))) |
| 170 | 162, 167 | mulcld 11281 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) ∈ ℂ) |
| 171 | | 1cnd 11256 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
| 172 | 8, 171 | addcld 11280 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℂ) |
| 173 | | 0red 11264 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 0 ∈
ℝ) |
| 174 | 103 | nnred 12281 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
| 175 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 176 | 175 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ) |
| 177 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
| 178 | 176, 177 | remulcld 11291 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℝ) |
| 179 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
| 180 | 178, 179 | readdcld 11290 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ∈
ℝ) |
| 181 | 103 | nngt0d 12315 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 0 < (2
· 𝑛)) |
| 182 | 174 | ltp1d 12198 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) < ((2
· 𝑛) +
1)) |
| 183 | 173, 174,
180, 181, 182 | lttrd 11422 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 0 <
((2 · 𝑛) +
1)) |
| 184 | 183 | gt0ne0d 11827 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) + 1) ≠
0) |
| 185 | 166, 170,
172, 184 | divassd 12078 |
. . . . . 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 12079 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) = ((2↑(4 · 𝑛)) · (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)))) |
| 187 | 9, 17, 41 | mulexpd 14201 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) = (((√‘(2 ·
𝑛))↑4) ·
(((𝑛 / e)↑𝑛)↑4))) |
| 188 | 60, 62 | sqmuld 14198 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · (2 · 𝑛))) · (((2 · 𝑛) / e)↑(2 · 𝑛)))↑2) = (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2))) |
| 189 | 187, 188 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))↑4) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2)) =
((((√‘(2 · 𝑛))↑4) · (((𝑛 / e)↑𝑛)↑4)) / (((√‘(2 · (2
· 𝑛)))↑2)
· ((((2 · 𝑛)
/ e)↑(2 · 𝑛))↑2)))) |
| 190 | 146 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝐸‘(2 · 𝑛))↑2) = (((√‘(2
· (2 · 𝑛)))
· (((2 · 𝑛) /
e)↑(2 · 𝑛)))↑2)) |
| 191 | 38, 190 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2)) = ((((√‘(2 ·
𝑛)) · ((𝑛 / e)↑𝑛))↑4) / (((√‘(2 · (2
· 𝑛))) · (((2
· 𝑛) / e)↑(2
· 𝑛)))↑2))) |
| 192 | 9, 41 | expcld 14186 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) ∈ ℂ) |
| 193 | 60 | sqcld 14184 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) ∈ ℂ) |
| 194 | 17, 41 | expcld 14186 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (((𝑛 / e)↑𝑛)↑4) ∈ ℂ) |
| 195 | 62 | sqcld 14184 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) ∈
ℂ) |
| 196 | 60, 67, 72 | expne0d 14192 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((√‘(2 · (2 · 𝑛)))↑2) ≠ 0) |
| 197 | 62, 74, 72 | expne0d 14192 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2) ≠
0) |
| 198 | 192, 193,
194, 195, 196, 197 | divmuldivd 12084 |
. . . . . . . . . . . 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 7447 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (((𝐸‘𝑛)↑4) / ((𝐸‘(2 · 𝑛))↑2))) = ((2↑(4 · 𝑛)) · ((((√‘(2
· 𝑛))↑4) /
((√‘(2 · (2 · 𝑛)))↑2)) · ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2))))) |
| 201 | 65 | rprege0d 13084 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· (2 · 𝑛))
∈ ℝ ∧ 0 ≤ (2 · (2 · 𝑛)))) |
| 202 | | resqrtth 15294 |
. . . . . . . . . . . . . . . 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 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2)) =
(((√‘(2 · 𝑛))↑4) / (2 · (2 · 𝑛)))) |
| 205 | | 2t2e4 12430 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 2) = 4 |
| 206 | 205 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢ 4 = (2
· 2) |
| 207 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 = (2
· 2)) |
| 208 | 207 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) = ((√‘(2 ·
𝑛))↑(2 ·
2))) |
| 209 | 9, 53, 53 | expmuld 14189 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑(2 · 2)) = (((√‘(2
· 𝑛))↑2)↑2)) |
| 210 | 22 | rprege0d 13084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) ∈ ℝ
∧ 0 ≤ (2 · 𝑛))) |
| 211 | | resqrtth 15294 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· 𝑛) ∈ ℝ
∧ 0 ≤ (2 · 𝑛)) → ((√‘(2 · 𝑛))↑2) = (2 · 𝑛)) |
| 212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑2) = (2 · 𝑛)) |
| 213 | 212 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑2)↑2) = ((2 · 𝑛)↑2)) |
| 214 | 208, 209,
213 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
((√‘(2 · 𝑛))↑4) = ((2 · 𝑛)↑2)) |
| 215 | 6, 6, 7 | mulassd 11284 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 2) · 𝑛) =
(2 · (2 · 𝑛))) |
| 216 | 205 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (2
· 2) = 4) |
| 217 | 216 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 2) · 𝑛) =
(4 · 𝑛)) |
| 218 | 215, 217 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (2
· (2 · 𝑛)) =
(4 · 𝑛)) |
| 219 | 214, 218 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(((√‘(2 · 𝑛))↑4) / (2 · (2 · 𝑛))) = (((2 · 𝑛)↑2) / (4 · 𝑛))) |
| 220 | 6, 7 | sqmuld 14198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑2) =
((2↑2) · (𝑛↑2))) |
| 221 | | sq2 14236 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2↑2) = 4 |
| 222 | 221 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(2↑2) = 4) |
| 223 | 222 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((2↑2) · (𝑛↑2)) = (4 · (𝑛↑2))) |
| 224 | 220, 223 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑2) = (4
· (𝑛↑2))) |
| 225 | 224 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛)↑2) / (4
· 𝑛)) = ((4 ·
(𝑛↑2)) / (4 ·
𝑛))) |
| 226 | | 4cn 12351 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ∈
ℂ |
| 227 | | 4ne0 12374 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 ≠
0 |
| 228 | 226, 227 | dividi 12000 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 / 4) =
1 |
| 229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (4 / 4) =
1) |
| 230 | 7 | sqvald 14183 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛)) |
| 231 | 230 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = ((𝑛 · 𝑛) / 𝑛)) |
| 232 | 7, 7, 25 | divcan4d 12049 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑛 · 𝑛) / 𝑛) = 𝑛) |
| 233 | 231, 232 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛) |
| 234 | 229, 233 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((4 / 4)
· ((𝑛↑2) /
𝑛)) = (1 · 𝑛)) |
| 235 | 41 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 ∈
ℂ) |
| 236 | 7 | sqcld 14184 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈
ℂ) |
| 237 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 4 ≠
0) |
| 238 | 235, 235,
236, 7, 237, 25 | divmuldivd 12084 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((4 / 4)
· ((𝑛↑2) /
𝑛)) = ((4 · (𝑛↑2)) / (4 · 𝑛))) |
| 239 | 7 | mullidd 11279 |
. . . . . . . . . . . . . . . 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 11282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 · 4) = (4 · 𝑛)) |
| 244 | 243 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(𝑛 · 4)) = ((𝑛 / e)↑(4 · 𝑛))) |
| 245 | 16, 41, 2 | expmuld 14189 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(𝑛 · 4)) = (((𝑛 / e)↑𝑛)↑4)) |
| 246 | 7, 12, 15, 137 | expdivd 14200 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛 / e)↑(4 · 𝑛)) = ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) |
| 247 | 244, 245,
246 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (((𝑛 / e)↑𝑛)↑4) = ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) |
| 248 | 6, 7, 6 | mul32d 11471 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) · 2) =
((2 · 2) · 𝑛)) |
| 249 | 248, 217 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) · 2) =
(4 · 𝑛)) |
| 250 | 249 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑((2
· 𝑛) · 2)) =
(((2 · 𝑛) /
e)↑(4 · 𝑛))) |
| 251 | 61, 53, 54 | expmuld 14189 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) / e)↑((2
· 𝑛) · 2)) =
((((2 · 𝑛) /
e)↑(2 · 𝑛))↑2)) |
| 252 | 8, 12, 15, 137 | expdivd 14200 |
. . . . . . . . . . . . . . . 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 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → ((((𝑛 / e)↑𝑛)↑4) / ((((2 · 𝑛) / e)↑(2 · 𝑛))↑2)) = (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) / (((2 · 𝑛)↑(4 · 𝑛)) / (e↑(4 · 𝑛))))) |
| 255 | 247, 194 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) ∈
ℂ) |
| 256 | 8, 137 | expcld 14186 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) ∈
ℂ) |
| 257 | 12, 137 | expcld 14186 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(e↑(4 · 𝑛))
∈ ℂ) |
| 258 | 46, 27 | zmulcld 12728 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (4
· 𝑛) ∈
ℤ) |
| 259 | 8, 69, 258 | expne0d 14192 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) ≠
0) |
| 260 | 12, 15, 258 | expne0d 14192 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(e↑(4 · 𝑛))
≠ 0) |
| 261 | 255, 256,
257, 259, 260 | divdiv2d 12075 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) / (((2 · 𝑛)↑(4 · 𝑛)) / (e↑(4 · 𝑛)))) = ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 · 𝑛))) / ((2 · 𝑛)↑(4 · 𝑛)))) |
| 262 | 7, 137 | expcld 14186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑(4 · 𝑛)) ∈
ℂ) |
| 263 | 262, 257,
260 | divcan1d 12044 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) = (𝑛↑(4 · 𝑛))) |
| 264 | 263 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((((𝑛↑(4 · 𝑛)) / (e↑(4 · 𝑛))) · (e↑(4 ·
𝑛))) / ((2 · 𝑛)↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((2 · 𝑛)↑(4 · 𝑛)))) |
| 265 | 6, 7, 137 | mulexpd 14201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛)↑(4
· 𝑛)) = ((2↑(4
· 𝑛)) ·
(𝑛↑(4 · 𝑛)))) |
| 266 | 265 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2 · 𝑛)↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛))))) |
| 267 | 138, 262 | mulcomd 11282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (𝑛↑(4
· 𝑛))) = ((𝑛↑(4 · 𝑛)) · (2↑(4 ·
𝑛)))) |
| 268 | 267 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / ((2↑(4 · 𝑛)) · (𝑛↑(4 · 𝑛)))) = ((𝑛↑(4 · 𝑛)) / ((𝑛↑(4 · 𝑛)) · (2↑(4 · 𝑛))))) |
| 269 | 7, 25, 258 | expne0d 14192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛↑(4 · 𝑛)) ≠ 0) |
| 270 | 6, 68, 258 | expne0d 14192 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(2↑(4 · 𝑛))
≠ 0) |
| 271 | 262, 262,
138, 269, 270 | divdiv1d 12074 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) / (2↑(4 · 𝑛))) = ((𝑛↑(4 · 𝑛)) / ((𝑛↑(4 · 𝑛)) · (2↑(4 · 𝑛))))) |
| 272 | 262, 269 | dividd 12041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → ((𝑛↑(4 · 𝑛)) / (𝑛↑(4 · 𝑛))) = 1) |
| 273 | 272 | oveq1d 7446 |
. . . . . . . . . . . . . . . 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 7449 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2))) =
(𝑛 · (1 / (2↑(4
· 𝑛))))) |
| 278 | 277 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· ((((√‘(2 · 𝑛))↑4) / ((√‘(2 · (2
· 𝑛)))↑2))
· ((((𝑛 /
e)↑𝑛)↑4) / ((((2
· 𝑛) / e)↑(2
· 𝑛))↑2)))) =
((2↑(4 · 𝑛))
· (𝑛 · (1 /
(2↑(4 · 𝑛)))))) |
| 279 | 138, 270 | reccld 12036 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (1 /
(2↑(4 · 𝑛)))
∈ ℂ) |
| 280 | 138, 7, 279 | mul12d 11470 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (𝑛 · (1 /
(2↑(4 · 𝑛)))))
= (𝑛 · ((2↑(4
· 𝑛)) · (1 /
(2↑(4 · 𝑛)))))) |
| 281 | 7 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛) |
| 282 | 138, 270 | recidd 12038 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
((2↑(4 · 𝑛))
· (1 / (2↑(4 · 𝑛)))) = 1) |
| 283 | 282 | oveq2d 7447 |
. . . . . . . . . . . 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 7446 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((((𝐸‘𝑛)↑4) · ((2↑(4 · 𝑛)) / ((𝐸‘(2 · 𝑛))↑2))) / ((2 · 𝑛) + 1)) = (((𝑛↑2) / 𝑛) / ((2 · 𝑛) + 1))) |
| 288 | 236, 7, 172, 25, 184 | divdiv1d 12074 |
. . . . . . . 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 7447 |
. . . . . 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 5245 |
. 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))))) |