Metamath Proof Explorer

Theorem stirlinglem3

Description: Long but simple algebraic transformations are applied to show that V , the Wallis formula for π , can be expressed in terms of A , the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the A , in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem3.1 ⊢ 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
stirlinglem3.2 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝐴 ‘ ( 2 · 𝑛 ) ) )
stirlinglem3.3 ⊢ 𝐸 = ( 𝑛 ∈ ℕ ↦ ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
stirlinglem3.4 ⊢ 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 2 ↑ ( 4 · 𝑛 ) ) · ( ( ! ‘ 𝑛 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑛 ) ) ↑ 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
Assertion stirlinglem3 𝑉 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( 𝐴 ‘ 𝑛 ) ↑ 4 ) / ( ( 𝐷 ‘ 𝑛 ) ↑ 2 ) ) · ( ( 𝑛 ↑ 2 ) / ( 𝑛 · ( ( 2 · 𝑛 ) + 1 ) ) ) ) )

Proof

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