Metamath Proof Explorer

Theorem stirlinglem4

Description: Algebraic manipulation of ( ( B n ) - ( B ( n + 1 ) ) ) . It will be used in other theorems to show that B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem4.1 
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem4.2 
|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
stirlinglem4.3 
|- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
Assertion stirlinglem4 
|- ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( J ` N ) )

Proof

Step Hyp Ref Expression
1 stirlinglem4.1 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2 stirlinglem4.2 
 |-  B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3 stirlinglem4.3 
 |-  J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
4 nnre 
 |-  ( N e. NN -> N e. RR )
5 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 5 nn0ge0d 
 |-  ( N e. NN -> 0 <_ N )
7 4 6 ge0p1rpd 
 |-  ( N e. NN -> ( N + 1 ) e. RR+ )
8 nnrp 
 |-  ( N e. NN -> N e. RR+ )
9 7 8 rpdivcld 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) e. RR+ )
10 9 rpsqrtcld 
 |-  ( N e. NN -> ( sqrt ` ( ( N + 1 ) / N ) ) e. RR+ )
11 nnz 
 |-  ( N e. NN -> N e. ZZ )
12 9 11 rpexpcld 
 |-  ( N e. NN -> ( ( ( N + 1 ) / N ) ^ N ) e. RR+ )
13 10 12 rpmulcld 
 |-  ( N e. NN -> ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) e. RR+ )
14 epr 
 |-  _e e. RR+
15 14 a1i 
 |-  ( N e. NN -> _e e. RR+ )
16 13 15 relogdivd 
 |-  ( N e. NN -> ( log ` ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) / _e ) ) = ( ( log ` ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) ) - ( log ` _e ) ) )
17 10 12 relogmuld 
 |-  ( N e. NN -> ( log ` ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) ) = ( ( log ` ( sqrt ` ( ( N + 1 ) / N ) ) ) + ( log ` ( ( ( N + 1 ) / N ) ^ N ) ) ) )
18 logsqrt 
 |-  ( ( ( N + 1 ) / N ) e. RR+ -> ( log ` ( sqrt ` ( ( N + 1 ) / N ) ) ) = ( ( log ` ( ( N + 1 ) / N ) ) / 2 ) )
19 9 18 syl 
 |-  ( N e. NN -> ( log ` ( sqrt ` ( ( N + 1 ) / N ) ) ) = ( ( log ` ( ( N + 1 ) / N ) ) / 2 ) )
20 relogexp 
 |-  ( ( ( ( N + 1 ) / N ) e. RR+ /\ N e. ZZ ) -> ( log ` ( ( ( N + 1 ) / N ) ^ N ) ) = ( N x. ( log ` ( ( N + 1 ) / N ) ) ) )
21 9 11 20 syl2anc 
 |-  ( N e. NN -> ( log ` ( ( ( N + 1 ) / N ) ^ N ) ) = ( N x. ( log ` ( ( N + 1 ) / N ) ) ) )
22 19 21 oveq12d 
 |-  ( N e. NN -> ( ( log ` ( sqrt ` ( ( N + 1 ) / N ) ) ) + ( log ` ( ( ( N + 1 ) / N ) ^ N ) ) ) = ( ( ( log ` ( ( N + 1 ) / N ) ) / 2 ) + ( N x. ( log ` ( ( N + 1 ) / N ) ) ) ) )
23 17 22 eqtrd 
 |-  ( N e. NN -> ( log ` ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) ) = ( ( ( log ` ( ( N + 1 ) / N ) ) / 2 ) + ( N x. ( log ` ( ( N + 1 ) / N ) ) ) ) )
24 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
25 24 nncnd 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
26 nncn 
 |-  ( N e. NN -> N e. CC )
27 nnne0 
 |-  ( N e. NN -> N =/= 0 )
28 25 26 27 divcld 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) e. CC )
29 24 nnne0d 
 |-  ( N e. NN -> ( N + 1 ) =/= 0 )
30 25 26 29 27 divne0d 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) =/= 0 )
31 28 30 logcld 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) / N ) ) e. CC )
32 2cnd 
 |-  ( N e. NN -> 2 e. CC )
33 2rp 
 |-  2 e. RR+
34 33 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
35 34 rpne0d 
 |-  ( N e. NN -> 2 =/= 0 )
36 31 32 35 divrec2d 
 |-  ( N e. NN -> ( ( log ` ( ( N + 1 ) / N ) ) / 2 ) = ( ( 1 / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
37 36 oveq1d 
 |-  ( N e. NN -> ( ( ( log ` ( ( N + 1 ) / N ) ) / 2 ) + ( N x. ( log ` ( ( N + 1 ) / N ) ) ) ) = ( ( ( 1 / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) + ( N x. ( log ` ( ( N + 1 ) / N ) ) ) ) )
38 1cnd 
 |-  ( N e. NN -> 1 e. CC )
39 38 halfcld 
 |-  ( N e. NN -> ( 1 / 2 ) e. CC )
40 39 26 31 adddird 
 |-  ( N e. NN -> ( ( ( 1 / 2 ) + N ) x. ( log ` ( ( N + 1 ) / N ) ) ) = ( ( ( 1 / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) + ( N x. ( log ` ( ( N + 1 ) / N ) ) ) ) )
41 26 32 35 divcan4d 
 |-  ( N e. NN -> ( ( N x. 2 ) / 2 ) = N )
42 26 32 mulcomd 
 |-  ( N e. NN -> ( N x. 2 ) = ( 2 x. N ) )
43 42 oveq1d 
 |-  ( N e. NN -> ( ( N x. 2 ) / 2 ) = ( ( 2 x. N ) / 2 ) )
44 41 43 eqtr3d 
 |-  ( N e. NN -> N = ( ( 2 x. N ) / 2 ) )
45 44 oveq2d 
 |-  ( N e. NN -> ( ( 1 / 2 ) + N ) = ( ( 1 / 2 ) + ( ( 2 x. N ) / 2 ) ) )
46 32 26 mulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. CC )
47 38 46 32 35 divdird 
 |-  ( N e. NN -> ( ( 1 + ( 2 x. N ) ) / 2 ) = ( ( 1 / 2 ) + ( ( 2 x. N ) / 2 ) ) )
48 45 47 eqtr4d 
 |-  ( N e. NN -> ( ( 1 / 2 ) + N ) = ( ( 1 + ( 2 x. N ) ) / 2 ) )
49 48 oveq1d 
 |-  ( N e. NN -> ( ( ( 1 / 2 ) + N ) x. ( log ` ( ( N + 1 ) / N ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
50 40 49 eqtr3d 
 |-  ( N e. NN -> ( ( ( 1 / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) + ( N x. ( log ` ( ( N + 1 ) / N ) ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
51 23 37 50 3eqtrd 
 |-  ( N e. NN -> ( log ` ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
52 loge 
 |-  ( log ` _e ) = 1
53 52 a1i 
 |-  ( N e. NN -> ( log ` _e ) = 1 )
54 51 53 oveq12d 
 |-  ( N e. NN -> ( ( log ` ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) ) - ( log ` _e ) ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
55 16 54 eqtrd 
 |-  ( N e. NN -> ( log ` ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) / _e ) ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
56 1 stirlinglem2 
 |-  ( N e. NN -> ( A ` N ) e. RR+ )
57 56 relogcld 
 |-  ( N e. NN -> ( log ` ( A ` N ) ) e. RR )
58 nfcv 
 |-  F/_ n N
59 nfcv 
 |-  F/_ n log
60 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
61 1 60 nfcxfr 
 |-  F/_ n A
62 61 58 nffv 
 |-  F/_ n ( A ` N )
63 59 62 nffv 
 |-  F/_ n ( log ` ( A ` N ) )
64 2fveq3 
 |-  ( n = N -> ( log ` ( A ` n ) ) = ( log ` ( A ` N ) ) )
65 58 63 64 2 fvmptf 
 |-  ( ( N e. NN /\ ( log ` ( A ` N ) ) e. RR ) -> ( B ` N ) = ( log ` ( A ` N ) ) )
66 57 65 mpdan 
 |-  ( N e. NN -> ( B ` N ) = ( log ` ( A ` N ) ) )
67 nfcv 
 |-  F/_ k ( log ` ( A ` n ) )
68 nfcv 
 |-  F/_ n k
69 61 68 nffv 
 |-  F/_ n ( A ` k )
70 59 69 nffv 
 |-  F/_ n ( log ` ( A ` k ) )
71 2fveq3 
 |-  ( n = k -> ( log ` ( A ` n ) ) = ( log ` ( A ` k ) ) )
72 67 70 71 cbvmpt 
 |-  ( n e. NN |-> ( log ` ( A ` n ) ) ) = ( k e. NN |-> ( log ` ( A ` k ) ) )
73 2 72 eqtri 
 |-  B = ( k e. NN |-> ( log ` ( A ` k ) ) )
74 73 a1i 
 |-  ( N e. NN -> B = ( k e. NN |-> ( log ` ( A ` k ) ) ) )
75 simpr 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> k = ( N + 1 ) )
76 75 fveq2d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( A ` k ) = ( A ` ( N + 1 ) ) )
77 76 fveq2d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( log ` ( A ` k ) ) = ( log ` ( A ` ( N + 1 ) ) ) )
78 1 stirlinglem2 
 |-  ( ( N + 1 ) e. NN -> ( A ` ( N + 1 ) ) e. RR+ )
79 24 78 syl 
 |-  ( N e. NN -> ( A ` ( N + 1 ) ) e. RR+ )
80 79 relogcld 
 |-  ( N e. NN -> ( log ` ( A ` ( N + 1 ) ) ) e. RR )
81 74 77 24 80 fvmptd 
 |-  ( N e. NN -> ( B ` ( N + 1 ) ) = ( log ` ( A ` ( N + 1 ) ) ) )
82 66 81 oveq12d 
 |-  ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( ( log ` ( A ` N ) ) - ( log ` ( A ` ( N + 1 ) ) ) ) )
83 56 79 relogdivd 
 |-  ( N e. NN -> ( log ` ( ( A ` N ) / ( A ` ( N + 1 ) ) ) ) = ( ( log ` ( A ` N ) ) - ( log ` ( A ` ( N + 1 ) ) ) ) )
84 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
85 nnrp 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. RR+ )
86 5 84 85 3syl 
 |-  ( N e. NN -> ( ! ` N ) e. RR+ )
87 34 8 rpmulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR+ )
88 87 rpsqrtcld 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. N ) ) e. RR+ )
89 8 15 rpdivcld 
 |-  ( N e. NN -> ( N / _e ) e. RR+ )
90 89 11 rpexpcld 
 |-  ( N e. NN -> ( ( N / _e ) ^ N ) e. RR+ )
91 88 90 rpmulcld 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) e. RR+ )
92 86 91 rpdivcld 
 |-  ( N e. NN -> ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ )
93 1 a1i 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
94 simpr 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> n = N )
95 94 fveq2d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( ! ` n ) = ( ! ` N ) )
96 94 oveq2d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( 2 x. n ) = ( 2 x. N ) )
97 96 fveq2d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. N ) ) )
98 94 oveq1d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( n / _e ) = ( N / _e ) )
99 98 94 oveq12d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( ( n / _e ) ^ n ) = ( ( N / _e ) ^ N ) )
100 97 99 oveq12d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) )
101 95 100 oveq12d 
 |-  ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ n = N ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
102 simpl 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> N e. NN )
103 86 rpcnd 
 |-  ( N e. NN -> ( ! ` N ) e. CC )
104 103 adantr 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ! ` N ) e. CC )
105 2cnd 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> 2 e. CC )
106 102 nncnd 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> N e. CC )
107 105 106 mulcld 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( 2 x. N ) e. CC )
108 107 sqrtcld 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( sqrt ` ( 2 x. N ) ) e. CC )
109 ere 
 |-  _e e. RR
110 109 recni 
 |-  _e e. CC
111 110 a1i 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> _e e. CC )
112 0re 
 |-  0 e. RR
113 epos 
 |-  0 < _e
114 112 113 gtneii 
 |-  _e =/= 0
115 114 a1i 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> _e =/= 0 )
116 106 111 115 divcld 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( N / _e ) e. CC )
117 102 nnnn0d 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> N e. NN0 )
118 116 117 expcld 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ( N / _e ) ^ N ) e. CC )
119 108 118 mulcld 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) e. CC )
120 88 rpne0d 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. N ) ) =/= 0 )
121 120 adantr 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( sqrt ` ( 2 x. N ) ) =/= 0 )
122 102 nnne0d 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> N =/= 0 )
123 106 111 122 115 divne0d 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( N / _e ) =/= 0 )
124 102 nnzd 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> N e. ZZ )
125 116 123 124 expne0d 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ( N / _e ) ^ N ) =/= 0 )
126 108 118 121 125 mulne0d 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) =/= 0 )
127 104 119 126 divcld 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. CC )
128 93 101 102 127 fvmptd 
 |-  ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( A ` N ) = ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
129 92 128 mpdan 
 |-  ( N e. NN -> ( A ` N ) = ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
130 nfcv 
 |-  F/_ k ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )
131 nfcv 
 |-  F/_ n ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) )
132 fveq2 
 |-  ( n = k -> ( ! ` n ) = ( ! ` k ) )
133 oveq2 
 |-  ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
134 133 fveq2d 
 |-  ( n = k -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. k ) ) )
135 oveq1 
 |-  ( n = k -> ( n / _e ) = ( k / _e ) )
136 id 
 |-  ( n = k -> n = k )
137 135 136 oveq12d 
 |-  ( n = k -> ( ( n / _e ) ^ n ) = ( ( k / _e ) ^ k ) )
138 134 137 oveq12d 
 |-  ( n = k -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) )
139 132 138 oveq12d 
 |-  ( n = k -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
140 130 131 139 cbvmpt 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) = ( k e. NN |-> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
141 1 140 eqtri 
 |-  A = ( k e. NN |-> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
142 141 a1i 
 |-  ( N e. NN -> A = ( k e. NN |-> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) )
143 75 fveq2d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( ! ` k ) = ( ! ` ( N + 1 ) ) )
144 75 oveq2d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( 2 x. k ) = ( 2 x. ( N + 1 ) ) )
145 144 fveq2d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( sqrt ` ( 2 x. k ) ) = ( sqrt ` ( 2 x. ( N + 1 ) ) ) )
146 75 oveq1d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( k / _e ) = ( ( N + 1 ) / _e ) )
147 146 75 oveq12d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( ( k / _e ) ^ k ) = ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) )
148 145 147 oveq12d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) = ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) )
149 143 148 oveq12d 
 |-  ( ( N e. NN /\ k = ( N + 1 ) ) -> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) = ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) )
150 24 nnnn0d 
 |-  ( N e. NN -> ( N + 1 ) e. NN0 )
151 faccl 
 |-  ( ( N + 1 ) e. NN0 -> ( ! ` ( N + 1 ) ) e. NN )
152 nnrp 
 |-  ( ( ! ` ( N + 1 ) ) e. NN -> ( ! ` ( N + 1 ) ) e. RR+ )
153 150 151 152 3syl 
 |-  ( N e. NN -> ( ! ` ( N + 1 ) ) e. RR+ )
154 34 7 rpmulcld 
 |-  ( N e. NN -> ( 2 x. ( N + 1 ) ) e. RR+ )
155 154 rpsqrtcld 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. ( N + 1 ) ) ) e. RR+ )
156 7 15 rpdivcld 
 |-  ( N e. NN -> ( ( N + 1 ) / _e ) e. RR+ )
157 11 peano2zd 
 |-  ( N e. NN -> ( N + 1 ) e. ZZ )
158 156 157 rpexpcld 
 |-  ( N e. NN -> ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) e. RR+ )
159 155 158 rpmulcld 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) e. RR+ )
160 153 159 rpdivcld 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) e. RR+ )
161 142 149 24 160 fvmptd 
 |-  ( N e. NN -> ( A ` ( N + 1 ) ) = ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) )
162 129 161 oveq12d 
 |-  ( N e. NN -> ( ( A ` N ) / ( A ` ( N + 1 ) ) ) = ( ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) / ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) )
163 facp1 
 |-  ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
164 5 163 syl 
 |-  ( N e. NN -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
165 164 oveq1d 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) )
166 159 rpcnd 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) e. CC )
167 159 rpne0d 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) =/= 0 )
168 103 25 166 167 divassd 
 |-  ( N e. NN -> ( ( ( ! ` N ) x. ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) = ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) )
169 165 168 eqtrd 
 |-  ( N e. NN -> ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) = ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) )
170 169 oveq2d 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) / ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) = ( ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) )
171 91 rpcnd 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) e. CC )
172 25 166 167 divcld 
 |-  ( N e. NN -> ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) e. CC )
173 103 172 mulcld 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) e. CC )
174 91 rpne0d 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) =/= 0 )
175 86 rpne0d 
 |-  ( N e. NN -> ( ! ` N ) =/= 0 )
176 25 166 29 167 divne0d 
 |-  ( N e. NN -> ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) =/= 0 )
177 103 172 175 176 mulne0d 
 |-  ( N e. NN -> ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) =/= 0 )
178 103 171 173 174 177 divdiv32d 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) = ( ( ( ! ` N ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
179 103 103 172 175 176 divdiv1d 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ! ` N ) ) / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) = ( ( ! ` N ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) )
180 179 eqcomd 
 |-  ( N e. NN -> ( ( ! ` N ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) = ( ( ( ! ` N ) / ( ! ` N ) ) / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) )
181 180 oveq1d 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) = ( ( ( ( ! ` N ) / ( ! ` N ) ) / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
182 103 175 dividd 
 |-  ( N e. NN -> ( ( ! ` N ) / ( ! ` N ) ) = 1 )
183 182 oveq1d 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ! ` N ) ) / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) = ( 1 / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) )
184 183 oveq1d 
 |-  ( N e. NN -> ( ( ( ( ! ` N ) / ( ! ` N ) ) / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) = ( ( 1 / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
185 25 166 29 167 recdivd 
 |-  ( N e. NN -> ( 1 / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) = ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
186 185 oveq1d 
 |-  ( N e. NN -> ( ( 1 / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) = ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
187 166 25 29 divcld 
 |-  ( N e. NN -> ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) e. CC )
188 88 rpcnd 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. N ) ) e. CC )
189 90 rpcnd 
 |-  ( N e. NN -> ( ( N / _e ) ^ N ) e. CC )
190 90 rpne0d 
 |-  ( N e. NN -> ( ( N / _e ) ^ N ) =/= 0 )
191 187 188 189 120 190 divdiv1d 
 |-  ( N e. NN -> ( ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( sqrt ` ( 2 x. N ) ) ) / ( ( N / _e ) ^ N ) ) = ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) )
192 166 25 188 29 120 divdiv32d 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( sqrt ` ( 2 x. N ) ) ) = ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) / ( N + 1 ) ) )
193 155 rpcnd 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. ( N + 1 ) ) ) e. CC )
194 158 rpcnd 
 |-  ( N e. NN -> ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) e. CC )
195 193 194 188 120 div23d 
 |-  ( N e. NN -> ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) = ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) )
196 34 rpred 
 |-  ( N e. NN -> 2 e. RR )
197 34 rpge0d 
 |-  ( N e. NN -> 0 <_ 2 )
198 24 nnred 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
199 150 nn0ge0d 
 |-  ( N e. NN -> 0 <_ ( N + 1 ) )
200 196 197 198 199 sqrtmuld 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. ( N + 1 ) ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` ( N + 1 ) ) ) )
201 196 197 4 6 sqrtmuld 
 |-  ( N e. NN -> ( sqrt ` ( 2 x. N ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) )
202 200 201 oveq12d 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) = ( ( ( sqrt ` 2 ) x. ( sqrt ` ( N + 1 ) ) ) / ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) ) )
203 32 sqrtcld 
 |-  ( N e. NN -> ( sqrt ` 2 ) e. CC )
204 25 sqrtcld 
 |-  ( N e. NN -> ( sqrt ` ( N + 1 ) ) e. CC )
205 26 sqrtcld 
 |-  ( N e. NN -> ( sqrt ` N ) e. CC )
206 34 rpsqrtcld 
 |-  ( N e. NN -> ( sqrt ` 2 ) e. RR+ )
207 206 rpne0d 
 |-  ( N e. NN -> ( sqrt ` 2 ) =/= 0 )
208 8 rpsqrtcld 
 |-  ( N e. NN -> ( sqrt ` N ) e. RR+ )
209 208 rpne0d 
 |-  ( N e. NN -> ( sqrt ` N ) =/= 0 )
210 203 203 204 205 207 209 divmuldivd 
 |-  ( N e. NN -> ( ( ( sqrt ` 2 ) / ( sqrt ` 2 ) ) x. ( ( sqrt ` ( N + 1 ) ) / ( sqrt ` N ) ) ) = ( ( ( sqrt ` 2 ) x. ( sqrt ` ( N + 1 ) ) ) / ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) ) )
211 203 207 dividd 
 |-  ( N e. NN -> ( ( sqrt ` 2 ) / ( sqrt ` 2 ) ) = 1 )
212 198 199 8 sqrtdivd 
 |-  ( N e. NN -> ( sqrt ` ( ( N + 1 ) / N ) ) = ( ( sqrt ` ( N + 1 ) ) / ( sqrt ` N ) ) )
213 212 eqcomd 
 |-  ( N e. NN -> ( ( sqrt ` ( N + 1 ) ) / ( sqrt ` N ) ) = ( sqrt ` ( ( N + 1 ) / N ) ) )
214 211 213 oveq12d 
 |-  ( N e. NN -> ( ( ( sqrt ` 2 ) / ( sqrt ` 2 ) ) x. ( ( sqrt ` ( N + 1 ) ) / ( sqrt ` N ) ) ) = ( 1 x. ( sqrt ` ( ( N + 1 ) / N ) ) ) )
215 202 210 214 3eqtr2d 
 |-  ( N e. NN -> ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) = ( 1 x. ( sqrt ` ( ( N + 1 ) / N ) ) ) )
216 215 oveq1d 
 |-  ( N e. NN -> ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) = ( ( 1 x. ( sqrt ` ( ( N + 1 ) / N ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) )
217 28 sqrtcld 
 |-  ( N e. NN -> ( sqrt ` ( ( N + 1 ) / N ) ) e. CC )
218 217 mulid2d 
 |-  ( N e. NN -> ( 1 x. ( sqrt ` ( ( N + 1 ) / N ) ) ) = ( sqrt ` ( ( N + 1 ) / N ) ) )
219 218 oveq1d 
 |-  ( N e. NN -> ( ( 1 x. ( sqrt ` ( ( N + 1 ) / N ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) )
220 195 216 219 3eqtrd 
 |-  ( N e. NN -> ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) )
221 220 oveq1d 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( sqrt ` ( 2 x. N ) ) ) / ( N + 1 ) ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
222 192 221 eqtrd 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( sqrt ` ( 2 x. N ) ) ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
223 222 oveq1d 
 |-  ( N e. NN -> ( ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( sqrt ` ( 2 x. N ) ) ) / ( ( N / _e ) ^ N ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) )
224 191 223 eqtr3d 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) )
225 217 194 mulcld 
 |-  ( N e. NN -> ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) e. CC )
226 225 25 189 29 190 divdiv32d 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( ( N / _e ) ^ N ) ) / ( N + 1 ) ) )
227 217 194 189 190 divassd 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( ( N / _e ) ^ N ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) ) )
228 15 rpcnd 
 |-  ( N e. NN -> _e e. CC )
229 15 rpne0d 
 |-  ( N e. NN -> _e =/= 0 )
230 25 228 229 150 expdivd 
 |-  ( N e. NN -> ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) = ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( _e ^ ( N + 1 ) ) ) )
231 26 228 229 5 expdivd 
 |-  ( N e. NN -> ( ( N / _e ) ^ N ) = ( ( N ^ N ) / ( _e ^ N ) ) )
232 230 231 oveq12d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) = ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( _e ^ ( N + 1 ) ) ) / ( ( N ^ N ) / ( _e ^ N ) ) ) )
233 232 oveq2d 
 |-  ( N e. NN -> ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( _e ^ ( N + 1 ) ) ) / ( ( N ^ N ) / ( _e ^ N ) ) ) ) )
234 25 150 expcld 
 |-  ( N e. NN -> ( ( N + 1 ) ^ ( N + 1 ) ) e. CC )
235 228 150 expcld 
 |-  ( N e. NN -> ( _e ^ ( N + 1 ) ) e. CC )
236 26 5 expcld 
 |-  ( N e. NN -> ( N ^ N ) e. CC )
237 228 5 expcld 
 |-  ( N e. NN -> ( _e ^ N ) e. CC )
238 228 229 157 expne0d 
 |-  ( N e. NN -> ( _e ^ ( N + 1 ) ) =/= 0 )
239 228 229 11 expne0d 
 |-  ( N e. NN -> ( _e ^ N ) =/= 0 )
240 26 27 11 expne0d 
 |-  ( N e. NN -> ( N ^ N ) =/= 0 )
241 234 235 236 237 238 239 240 divdivdivd 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( _e ^ ( N + 1 ) ) ) / ( ( N ^ N ) / ( _e ^ N ) ) ) = ( ( ( ( N + 1 ) ^ ( N + 1 ) ) x. ( _e ^ N ) ) / ( ( _e ^ ( N + 1 ) ) x. ( N ^ N ) ) ) )
242 234 237 mulcomd 
 |-  ( N e. NN -> ( ( ( N + 1 ) ^ ( N + 1 ) ) x. ( _e ^ N ) ) = ( ( _e ^ N ) x. ( ( N + 1 ) ^ ( N + 1 ) ) ) )
243 242 oveq1d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) x. ( _e ^ N ) ) / ( ( _e ^ ( N + 1 ) ) x. ( N ^ N ) ) ) = ( ( ( _e ^ N ) x. ( ( N + 1 ) ^ ( N + 1 ) ) ) / ( ( _e ^ ( N + 1 ) ) x. ( N ^ N ) ) ) )
244 237 235 234 236 238 240 divmuldivd 
 |-  ( N e. NN -> ( ( ( _e ^ N ) / ( _e ^ ( N + 1 ) ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) = ( ( ( _e ^ N ) x. ( ( N + 1 ) ^ ( N + 1 ) ) ) / ( ( _e ^ ( N + 1 ) ) x. ( N ^ N ) ) ) )
245 228 5 expp1d 
 |-  ( N e. NN -> ( _e ^ ( N + 1 ) ) = ( ( _e ^ N ) x. _e ) )
246 245 oveq2d 
 |-  ( N e. NN -> ( ( _e ^ N ) / ( _e ^ ( N + 1 ) ) ) = ( ( _e ^ N ) / ( ( _e ^ N ) x. _e ) ) )
247 237 237 228 239 229 divdiv1d 
 |-  ( N e. NN -> ( ( ( _e ^ N ) / ( _e ^ N ) ) / _e ) = ( ( _e ^ N ) / ( ( _e ^ N ) x. _e ) ) )
248 237 239 dividd 
 |-  ( N e. NN -> ( ( _e ^ N ) / ( _e ^ N ) ) = 1 )
249 248 oveq1d 
 |-  ( N e. NN -> ( ( ( _e ^ N ) / ( _e ^ N ) ) / _e ) = ( 1 / _e ) )
250 246 247 249 3eqtr2d 
 |-  ( N e. NN -> ( ( _e ^ N ) / ( _e ^ ( N + 1 ) ) ) = ( 1 / _e ) )
251 250 oveq1d 
 |-  ( N e. NN -> ( ( ( _e ^ N ) / ( _e ^ ( N + 1 ) ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) = ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) )
252 244 251 eqtr3d 
 |-  ( N e. NN -> ( ( ( _e ^ N ) x. ( ( N + 1 ) ^ ( N + 1 ) ) ) / ( ( _e ^ ( N + 1 ) ) x. ( N ^ N ) ) ) = ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) )
253 241 243 252 3eqtrd 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( _e ^ ( N + 1 ) ) ) / ( ( N ^ N ) / ( _e ^ N ) ) ) = ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) )
254 253 oveq2d 
 |-  ( N e. NN -> ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( _e ^ ( N + 1 ) ) ) / ( ( N ^ N ) / ( _e ^ N ) ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) )
255 227 233 254 3eqtrd 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( ( N / _e ) ^ N ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) )
256 255 oveq1d 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( ( N / _e ) ^ N ) ) / ( N + 1 ) ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) / ( N + 1 ) ) )
257 234 236 240 divcld 
 |-  ( N e. NN -> ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) e. CC )
258 38 228 257 229 div32d 
 |-  ( N e. NN -> ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) = ( 1 x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) ) )
259 257 228 229 divcld 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) e. CC )
260 259 mulid2d 
 |-  ( N e. NN -> ( 1 x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) ) = ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) )
261 258 260 eqtrd 
 |-  ( N e. NN -> ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) = ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) )
262 261 oveq2d 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) ) )
263 228 229 reccld 
 |-  ( N e. NN -> ( 1 / _e ) e. CC )
264 263 257 mulcld 
 |-  ( N e. NN -> ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) e. CC )
265 217 264 25 29 div23d 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) / ( N + 1 ) ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) )
266 217 25 29 divcld 
 |-  ( N e. NN -> ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) e. CC )
267 266 257 228 229 divassd 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / _e ) ) )
268 262 265 267 3eqtr4d 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( 1 / _e ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) ) / ( N + 1 ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) )
269 226 256 268 3eqtrd 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) / ( N + 1 ) ) / ( ( N / _e ) ^ N ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) )
270 186 224 269 3eqtrd 
 |-  ( N e. NN -> ( ( 1 / ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) )
271 181 184 270 3eqtrd 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ( ! ` N ) x. ( ( N + 1 ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) )
272 170 178 271 3eqtrd 
 |-  ( N e. NN -> ( ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) / ( ( ! ` ( N + 1 ) ) / ( ( sqrt ` ( 2 x. ( N + 1 ) ) ) x. ( ( ( N + 1 ) / _e ) ^ ( N + 1 ) ) ) ) ) = ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) )
273 217 25 257 29 div32d 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / ( N + 1 ) ) ) )
274 25 5 expp1d 
 |-  ( N e. NN -> ( ( N + 1 ) ^ ( N + 1 ) ) = ( ( ( N + 1 ) ^ N ) x. ( N + 1 ) ) )
275 274 oveq1d 
 |-  ( N e. NN -> ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N + 1 ) ) = ( ( ( ( N + 1 ) ^ N ) x. ( N + 1 ) ) / ( N + 1 ) ) )
276 25 5 expcld 
 |-  ( N e. NN -> ( ( N + 1 ) ^ N ) e. CC )
277 276 25 29 divcan4d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ N ) x. ( N + 1 ) ) / ( N + 1 ) ) = ( ( N + 1 ) ^ N ) )
278 275 277 eqtrd 
 |-  ( N e. NN -> ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N + 1 ) ) = ( ( N + 1 ) ^ N ) )
279 278 oveq1d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N + 1 ) ) / ( N ^ N ) ) = ( ( ( N + 1 ) ^ N ) / ( N ^ N ) ) )
280 234 236 25 240 29 divdiv32d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / ( N + 1 ) ) = ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N + 1 ) ) / ( N ^ N ) ) )
281 25 26 27 5 expdivd 
 |-  ( N e. NN -> ( ( ( N + 1 ) / N ) ^ N ) = ( ( ( N + 1 ) ^ N ) / ( N ^ N ) ) )
282 279 280 281 3eqtr4d 
 |-  ( N e. NN -> ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / ( N + 1 ) ) = ( ( ( N + 1 ) / N ) ^ N ) )
283 282 oveq2d 
 |-  ( N e. NN -> ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) / ( N + 1 ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) )
284 273 283 eqtrd 
 |-  ( N e. NN -> ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) = ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) )
285 284 oveq1d 
 |-  ( N e. NN -> ( ( ( ( sqrt ` ( ( N + 1 ) / N ) ) / ( N + 1 ) ) x. ( ( ( N + 1 ) ^ ( N + 1 ) ) / ( N ^ N ) ) ) / _e ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) / _e ) )
286 162 272 285 3eqtrd 
 |-  ( N e. NN -> ( ( A ` N ) / ( A ` ( N + 1 ) ) ) = ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) / _e ) )
287 286 fveq2d 
 |-  ( N e. NN -> ( log ` ( ( A ` N ) / ( A ` ( N + 1 ) ) ) ) = ( log ` ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) / _e ) ) )
288 82 83 287 3eqtr2d 
 |-  ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( log ` ( ( ( sqrt ` ( ( N + 1 ) / N ) ) x. ( ( ( N + 1 ) / N ) ^ N ) ) / _e ) ) )
289 38 46 addcld 
 |-  ( N e. NN -> ( 1 + ( 2 x. N ) ) e. CC )
290 289 halfcld 
 |-  ( N e. NN -> ( ( 1 + ( 2 x. N ) ) / 2 ) e. CC )
291 290 31 mulcld 
 |-  ( N e. NN -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) e. CC )
292 291 38 subcld 
 |-  ( N e. NN -> ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC )
293 3 a1i 
 |-  ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) -> J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) ) )
294 simpr 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> n = N )
295 294 oveq2d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( 2 x. n ) = ( 2 x. N ) )
296 295 oveq2d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( 1 + ( 2 x. n ) ) = ( 1 + ( 2 x. N ) ) )
297 296 oveq1d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( ( 1 + ( 2 x. n ) ) / 2 ) = ( ( 1 + ( 2 x. N ) ) / 2 ) )
298 294 oveq1d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( n + 1 ) = ( N + 1 ) )
299 298 294 oveq12d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( ( n + 1 ) / n ) = ( ( N + 1 ) / N ) )
300 299 fveq2d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( log ` ( ( n + 1 ) / n ) ) = ( log ` ( ( N + 1 ) / N ) ) )
301 297 300 oveq12d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
302 301 oveq1d 
 |-  ( ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) /\ n = N ) -> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
303 simpl 
 |-  ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) -> N e. NN )
304 simpr 
 |-  ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) -> ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC )
305 293 302 303 304 fvmptd 
 |-  ( ( N e. NN /\ ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC ) -> ( J ` N ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
306 292 305 mpdan 
 |-  ( N e. NN -> ( J ` N ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
307 55 288 306 3eqtr4d 
 |-  ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( J ` N ) )