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 
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem3.2 
|- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
stirlinglem3.3 
|- E = ( n e. NN |-> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )
stirlinglem3.4 
|- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
Assertion stirlinglem3 
|- V = ( n e. NN |-> ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) )

Proof

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