This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stirlinglem7

Description: Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem7.1 
|- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
stirlinglem7.2 
|- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
stirlinglem7.3 
|- H = ( k e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) )
Assertion stirlinglem7 
|- ( N e. NN -> seq 1 ( + , K ) ~~> ( J ` N ) )

Proof

Step Hyp Ref Expression
1 stirlinglem7.1 
 |-  J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )
2 stirlinglem7.2 
 |-  K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )
3 stirlinglem7.3 
 |-  H = ( k e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( N e. NN -> 1 e. ZZ )
6 1e0p1 
 |-  1 = ( 0 + 1 )
7 6 a1i 
 |-  ( N e. NN -> 1 = ( 0 + 1 ) )
8 7 seqeq1d 
 |-  ( N e. NN -> seq 1 ( + , H ) = seq ( 0 + 1 ) ( + , H ) )
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 0nn0 
 |-  0 e. NN0
11 10 a1i 
 |-  ( N e. NN -> 0 e. NN0 )
12 oveq2 
 |-  ( k = j -> ( 2 x. k ) = ( 2 x. j ) )
13 12 oveq1d 
 |-  ( k = j -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. j ) + 1 ) )
14 13 oveq2d 
 |-  ( k = j -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. j ) + 1 ) ) )
15 13 oveq2d 
 |-  ( k = j -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) )
16 14 15 oveq12d 
 |-  ( k = j -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) = ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) )
17 16 oveq2d 
 |-  ( k = j -> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) = ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) ) )
18 simpr 
 |-  ( ( N e. NN /\ j e. NN0 ) -> j e. NN0 )
19 2cnd 
 |-  ( ( N e. NN /\ j e. NN0 ) -> 2 e. CC )
20 2cnd 
 |-  ( j e. NN0 -> 2 e. CC )
21 nn0cn 
 |-  ( j e. NN0 -> j e. CC )
22 20 21 mulcld 
 |-  ( j e. NN0 -> ( 2 x. j ) e. CC )
23 1cnd 
 |-  ( j e. NN0 -> 1 e. CC )
24 22 23 addcld 
 |-  ( j e. NN0 -> ( ( 2 x. j ) + 1 ) e. CC )
25 24 adantl 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 2 x. j ) + 1 ) e. CC )
26 0red 
 |-  ( j e. NN0 -> 0 e. RR )
27 2re 
 |-  2 e. RR
28 27 a1i 
 |-  ( j e. NN0 -> 2 e. RR )
29 nn0re 
 |-  ( j e. NN0 -> j e. RR )
30 28 29 remulcld 
 |-  ( j e. NN0 -> ( 2 x. j ) e. RR )
31 1red 
 |-  ( j e. NN0 -> 1 e. RR )
32 0le2 
 |-  0 <_ 2
33 32 a1i 
 |-  ( j e. NN0 -> 0 <_ 2 )
34 nn0ge0 
 |-  ( j e. NN0 -> 0 <_ j )
35 28 29 33 34 mulge0d 
 |-  ( j e. NN0 -> 0 <_ ( 2 x. j ) )
36 0lt1 
 |-  0 < 1
37 36 a1i 
 |-  ( j e. NN0 -> 0 < 1 )
38 30 31 35 37 addgegt0d 
 |-  ( j e. NN0 -> 0 < ( ( 2 x. j ) + 1 ) )
39 26 38 ltned 
 |-  ( j e. NN0 -> 0 =/= ( ( 2 x. j ) + 1 ) )
40 39 adantl 
 |-  ( ( N e. NN /\ j e. NN0 ) -> 0 =/= ( ( 2 x. j ) + 1 ) )
41 40 necomd 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 2 x. j ) + 1 ) =/= 0 )
42 25 41 reccld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( 1 / ( ( 2 x. j ) + 1 ) ) e. CC )
43 nncn 
 |-  ( N e. NN -> N e. CC )
44 43 adantr 
 |-  ( ( N e. NN /\ j e. NN0 ) -> N e. CC )
45 19 44 mulcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( 2 x. N ) e. CC )
46 1cnd 
 |-  ( ( N e. NN /\ j e. NN0 ) -> 1 e. CC )
47 45 46 addcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 2 x. N ) + 1 ) e. CC )
48 27 a1i 
 |-  ( N e. NN -> 2 e. RR )
49 nnre 
 |-  ( N e. NN -> N e. RR )
50 48 49 remulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
51 1red 
 |-  ( N e. NN -> 1 e. RR )
52 32 a1i 
 |-  ( N e. NN -> 0 <_ 2 )
53 0red 
 |-  ( N e. NN -> 0 e. RR )
54 nngt0 
 |-  ( N e. NN -> 0 < N )
55 53 49 54 ltled 
 |-  ( N e. NN -> 0 <_ N )
56 48 49 52 55 mulge0d 
 |-  ( N e. NN -> 0 <_ ( 2 x. N ) )
57 36 a1i 
 |-  ( N e. NN -> 0 < 1 )
58 50 51 56 57 addgegt0d 
 |-  ( N e. NN -> 0 < ( ( 2 x. N ) + 1 ) )
59 58 gt0ne0d 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) =/= 0 )
60 59 adantr 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 2 x. N ) + 1 ) =/= 0 )
61 47 60 reccld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
62 2nn0 
 |-  2 e. NN0
63 62 a1i 
 |-  ( ( N e. NN /\ j e. NN0 ) -> 2 e. NN0 )
64 63 18 nn0mulcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( 2 x. j ) e. NN0 )
65 1nn0 
 |-  1 e. NN0
66 65 a1i 
 |-  ( ( N e. NN /\ j e. NN0 ) -> 1 e. NN0 )
67 64 66 nn0addcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 2 x. j ) + 1 ) e. NN0 )
68 61 67 expcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) e. CC )
69 42 68 mulcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) e. CC )
70 19 69 mulcld 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) ) e. CC )
71 3 17 18 70 fvmptd3 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( H ` j ) = ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) ) )
72 71 70 eqeltrd 
 |-  ( ( N e. NN /\ j e. NN0 ) -> ( H ` j ) e. CC )
73 3 stirlinglem6 
 |-  ( N e. NN -> seq 0 ( + , H ) ~~> ( log ` ( ( N + 1 ) / N ) ) )
74 9 11 72 73 clim2ser 
 |-  ( N e. NN -> seq ( 0 + 1 ) ( + , H ) ~~> ( ( log ` ( ( N + 1 ) / N ) ) - ( seq 0 ( + , H ) ` 0 ) ) )
75 8 74 eqbrtrd 
 |-  ( N e. NN -> seq 1 ( + , H ) ~~> ( ( log ` ( ( N + 1 ) / N ) ) - ( seq 0 ( + , H ) ` 0 ) ) )
76 0z 
 |-  0 e. ZZ
77 seq1 
 |-  ( 0 e. ZZ -> ( seq 0 ( + , H ) ` 0 ) = ( H ` 0 ) )
78 76 77 mp1i 
 |-  ( N e. NN -> ( seq 0 ( + , H ) ` 0 ) = ( H ` 0 ) )
79 3 a1i 
 |-  ( N e. NN -> H = ( k e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) ) )
80 simpr 
 |-  ( ( N e. NN /\ k = 0 ) -> k = 0 )
81 80 oveq2d 
 |-  ( ( N e. NN /\ k = 0 ) -> ( 2 x. k ) = ( 2 x. 0 ) )
82 81 oveq1d 
 |-  ( ( N e. NN /\ k = 0 ) -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. 0 ) + 1 ) )
83 82 oveq2d 
 |-  ( ( N e. NN /\ k = 0 ) -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. 0 ) + 1 ) ) )
84 82 oveq2d 
 |-  ( ( N e. NN /\ k = 0 ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) )
85 83 84 oveq12d 
 |-  ( ( N e. NN /\ k = 0 ) -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) = ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) )
86 85 oveq2d 
 |-  ( ( N e. NN /\ k = 0 ) -> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) = ( 2 x. ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) ) )
87 2cnd 
 |-  ( N e. NN -> 2 e. CC )
88 0cnd 
 |-  ( N e. NN -> 0 e. CC )
89 87 88 mulcld 
 |-  ( N e. NN -> ( 2 x. 0 ) e. CC )
90 1cnd 
 |-  ( N e. NN -> 1 e. CC )
91 89 90 addcld 
 |-  ( N e. NN -> ( ( 2 x. 0 ) + 1 ) e. CC )
92 87 mul01d 
 |-  ( N e. NN -> ( 2 x. 0 ) = 0 )
93 92 eqcomd 
 |-  ( N e. NN -> 0 = ( 2 x. 0 ) )
94 93 oveq1d 
 |-  ( N e. NN -> ( 0 + 1 ) = ( ( 2 x. 0 ) + 1 ) )
95 7 94 eqtrd 
 |-  ( N e. NN -> 1 = ( ( 2 x. 0 ) + 1 ) )
96 57 95 breqtrd 
 |-  ( N e. NN -> 0 < ( ( 2 x. 0 ) + 1 ) )
97 96 gt0ne0d 
 |-  ( N e. NN -> ( ( 2 x. 0 ) + 1 ) =/= 0 )
98 91 97 reccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. 0 ) + 1 ) ) e. CC )
99 87 43 mulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. CC )
100 99 90 addcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. CC )
101 100 59 reccld 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
102 95 65 eqeltrrdi 
 |-  ( N e. NN -> ( ( 2 x. 0 ) + 1 ) e. NN0 )
103 101 102 expcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) e. CC )
104 98 103 mulcld 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) e. CC )
105 87 104 mulcld 
 |-  ( N e. NN -> ( 2 x. ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) ) e. CC )
106 79 86 11 105 fvmptd 
 |-  ( N e. NN -> ( H ` 0 ) = ( 2 x. ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) ) )
107 92 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. 0 ) + 1 ) = ( 0 + 1 ) )
108 107 6 eqtr4di 
 |-  ( N e. NN -> ( ( 2 x. 0 ) + 1 ) = 1 )
109 108 oveq2d 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. 0 ) + 1 ) ) = ( 1 / 1 ) )
110 90 div1d 
 |-  ( N e. NN -> ( 1 / 1 ) = 1 )
111 109 110 eqtrd 
 |-  ( N e. NN -> ( 1 / ( ( 2 x. 0 ) + 1 ) ) = 1 )
112 108 oveq2d 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ 1 ) )
113 101 exp1d 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ 1 ) = ( 1 / ( ( 2 x. N ) + 1 ) ) )
114 112 113 eqtrd 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) = ( 1 / ( ( 2 x. N ) + 1 ) ) )
115 111 114 oveq12d 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) = ( 1 x. ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
116 101 mullidd 
 |-  ( N e. NN -> ( 1 x. ( 1 / ( ( 2 x. N ) + 1 ) ) ) = ( 1 / ( ( 2 x. N ) + 1 ) ) )
117 115 116 eqtrd 
 |-  ( N e. NN -> ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) = ( 1 / ( ( 2 x. N ) + 1 ) ) )
118 117 oveq2d 
 |-  ( N e. NN -> ( 2 x. ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) ) = ( 2 x. ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
119 87 90 100 59 divassd 
 |-  ( N e. NN -> ( ( 2 x. 1 ) / ( ( 2 x. N ) + 1 ) ) = ( 2 x. ( 1 / ( ( 2 x. N ) + 1 ) ) ) )
120 87 mulridd 
 |-  ( N e. NN -> ( 2 x. 1 ) = 2 )
121 120 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. 1 ) / ( ( 2 x. N ) + 1 ) ) = ( 2 / ( ( 2 x. N ) + 1 ) ) )
122 118 119 121 3eqtr2d 
 |-  ( N e. NN -> ( 2 x. ( ( 1 / ( ( 2 x. 0 ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. 0 ) + 1 ) ) ) ) = ( 2 / ( ( 2 x. N ) + 1 ) ) )
123 78 106 122 3eqtrd 
 |-  ( N e. NN -> ( seq 0 ( + , H ) ` 0 ) = ( 2 / ( ( 2 x. N ) + 1 ) ) )
124 123 oveq2d 
 |-  ( N e. NN -> ( ( log ` ( ( N + 1 ) / N ) ) - ( seq 0 ( + , H ) ` 0 ) ) = ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) )
125 75 124 breqtrd 
 |-  ( N e. NN -> seq 1 ( + , H ) ~~> ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) )
126 90 99 addcld 
 |-  ( N e. NN -> ( 1 + ( 2 x. N ) ) e. CC )
127 126 halfcld 
 |-  ( N e. NN -> ( ( 1 + ( 2 x. N ) ) / 2 ) e. CC )
128 seqex 
 |-  seq 1 ( + , K ) e. _V
129 128 a1i 
 |-  ( N e. NN -> seq 1 ( + , K ) e. _V )
130 elnnuz 
 |-  ( j e. NN <-> j e. ( ZZ>= ` 1 ) )
131 130 bilani 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
132 oveq2 
 |-  ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
133 132 oveq1d 
 |-  ( k = n -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. n ) + 1 ) )
134 133 oveq2d 
 |-  ( k = n -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. n ) + 1 ) ) )
135 133 oveq2d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) )
136 134 135 oveq12d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) )
137 136 oveq2d 
 |-  ( k = n -> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) = ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) )
138 elfzuz 
 |-  ( n e. ( 1 ... j ) -> n e. ( ZZ>= ` 1 ) )
139 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
140 139 biimpri 
 |-  ( n e. ( ZZ>= ` 1 ) -> n e. NN )
141 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
142 138 140 141 3syl 
 |-  ( n e. ( 1 ... j ) -> n e. NN0 )
143 142 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. NN0 )
144 2cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 e. CC )
145 143 nn0cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. CC )
146 144 145 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. CC )
147 1cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 1 e. CC )
148 146 147 addcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. CC )
149 elfznn 
 |-  ( n e. ( 1 ... j ) -> n e. NN )
150 0red 
 |-  ( n e. NN -> 0 e. RR )
151 1red 
 |-  ( n e. NN -> 1 e. RR )
152 27 a1i 
 |-  ( n e. NN -> 2 e. RR )
153 nnre 
 |-  ( n e. NN -> n e. RR )
154 152 153 remulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR )
155 154 151 readdcld 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. RR )
156 36 a1i 
 |-  ( n e. NN -> 0 < 1 )
157 2rp 
 |-  2 e. RR+
158 157 a1i 
 |-  ( n e. NN -> 2 e. RR+ )
159 nnrp 
 |-  ( n e. NN -> n e. RR+ )
160 158 159 rpmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR+ )
161 151 160 ltaddrp2d 
 |-  ( n e. NN -> 1 < ( ( 2 x. n ) + 1 ) )
162 150 151 155 156 161 lttrd 
 |-  ( n e. NN -> 0 < ( ( 2 x. n ) + 1 ) )
163 162 gt0ne0d 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) =/= 0 )
164 149 163 syl 
 |-  ( n e. ( 1 ... j ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
165 164 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
166 148 165 reccld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. CC )
167 101 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
168 62 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 e. NN0 )
169 168 143 nn0mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. NN0 )
170 65 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 1 e. NN0 )
171 169 170 nn0addcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. NN0 )
172 167 171 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) e. CC )
173 166 172 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) e. CC )
174 144 173 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) e. CC )
175 3 137 143 174 fvmptd3 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( H ` n ) = ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) )
176 175 174 eqeltrd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( H ` n ) e. CC )
177 addcl 
 |-  ( ( n e. CC /\ i e. CC ) -> ( n + i ) e. CC )
178 177 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( n + i ) e. CC )
179 131 176 178 seqcl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , H ) ` j ) e. CC )
180 1cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> 1 e. CC )
181 2cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> 2 e. CC )
182 43 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> N e. CC )
183 181 182 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( 2 x. N ) e. CC )
184 180 183 addcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( 1 + ( 2 x. N ) ) e. CC )
185 184 halfcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( ( 1 + ( 2 x. N ) ) / 2 ) e. CC )
186 simprl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> n e. CC )
187 simprr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> i e. CC )
188 185 186 187 adddid 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( n + i ) ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. n ) + ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. i ) ) )
189 132 oveq2d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) )
190 134 189 oveq12d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
191 149 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. NN )
192 167 169 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) e. CC )
193 166 192 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) e. CC )
194 2 190 191 193 fvmptd3 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( K ` n ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
195 126 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 + ( 2 x. N ) ) e. CC )
196 2ne0 
 |-  2 =/= 0
197 196 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 =/= 0 )
198 195 144 174 197 div32d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) ) = ( ( 1 + ( 2 x. N ) ) x. ( ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) / 2 ) ) )
199 173 144 197 divcan3d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) / 2 ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) )
200 199 oveq2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) x. ( ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) / 2 ) ) = ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) )
201 195 166 172 mul12d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) )
202 100 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) e. CC )
203 59 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) =/= 0 )
204 171 nn0zd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. ZZ )
205 202 203 204 exprecd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) = ( 1 / ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) ) )
206 205 oveq2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) = ( ( 1 + ( 2 x. N ) ) x. ( 1 / ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) ) ) )
207 202 171 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) e. CC )
208 202 203 204 expne0d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) =/= 0 )
209 195 207 208 divrecd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) ) = ( ( 1 + ( 2 x. N ) ) x. ( 1 / ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) ) ) )
210 43 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> N e. CC )
211 144 210 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. N ) e. CC )
212 147 211 addcomd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 + ( 2 x. N ) ) = ( ( 2 x. N ) + 1 ) )
213 202 169 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) e. CC )
214 213 202 mulcomd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) x. ( ( 2 x. N ) + 1 ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) )
215 212 214 oveq12d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) / ( ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) x. ( ( 2 x. N ) + 1 ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( ( ( 2 x. N ) + 1 ) x. ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) ) )
216 202 169 expp1d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) = ( ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) x. ( ( 2 x. N ) + 1 ) ) )
217 216 oveq2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) ) = ( ( 1 + ( 2 x. N ) ) / ( ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) x. ( ( 2 x. N ) + 1 ) ) ) )
218 2z 
 |-  2 e. ZZ
219 218 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 e. ZZ )
220 143 nn0zd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. ZZ )
221 219 220 zmulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. ZZ )
222 202 203 221 expne0d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) =/= 0 )
223 202 202 213 203 222 divdiv1d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( ( ( 2 x. N ) + 1 ) x. ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) ) )
224 215 217 223 3eqtr4d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) )
225 206 209 224 3eqtr2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) )
226 225 oveq2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) ) )
227 202 203 dividd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = 1 )
228 1exp 
 |-  ( ( 2 x. n ) e. ZZ -> ( 1 ^ ( 2 x. n ) ) = 1 )
229 221 228 syl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 ^ ( 2 x. n ) ) = 1 )
230 227 229 eqtr4d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = ( 1 ^ ( 2 x. n ) ) )
231 230 oveq1d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) = ( ( 1 ^ ( 2 x. n ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) )
232 147 202 203 169 expdivd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) = ( ( 1 ^ ( 2 x. n ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) )
233 231 232 eqtr4d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) )
234 233 oveq2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) / ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
235 201 226 234 3eqtrd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 + ( 2 x. N ) ) x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
236 198 200 235 3eqtrd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) ) = ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) ) )
237 175 eqcomd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) = ( H ` n ) )
238 237 oveq2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( 2 x. ( ( 1 / ( ( 2 x. n ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( H ` n ) ) )
239 194 236 238 3eqtr2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( K ` n ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( H ` n ) ) )
240 178 188 131 176 239 seqdistr 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , K ) ` j ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( seq 1 ( + , H ) ` j ) ) )
241 4 5 125 127 129 179 240 climmulc2 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) )
242 90 99 addcomd 
 |-  ( N e. NN -> ( 1 + ( 2 x. N ) ) = ( ( 2 x. N ) + 1 ) )
243 242 oveq1d 
 |-  ( N e. NN -> ( ( 1 + ( 2 x. N ) ) / 2 ) = ( ( ( 2 x. N ) + 1 ) / 2 ) )
244 243 oveq1d 
 |-  ( N e. NN -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) )
245 243 127 eqeltrrd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / 2 ) e. CC )
246 43 90 addcld 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
247 nnne0 
 |-  ( N e. NN -> N =/= 0 )
248 246 43 247 divcld 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) e. CC )
249 49 51 readdcld 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
250 49 ltp1d 
 |-  ( N e. NN -> N < ( N + 1 ) )
251 53 49 249 54 250 lttrd 
 |-  ( N e. NN -> 0 < ( N + 1 ) )
252 251 gt0ne0d 
 |-  ( N e. NN -> ( N + 1 ) =/= 0 )
253 246 43 252 247 divne0d 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) =/= 0 )
254 248 253 logcld 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) / N ) ) e. CC )
255 87 100 59 divcld 
 |-  ( N e. NN -> ( 2 / ( ( 2 x. N ) + 1 ) ) e. CC )
256 245 254 255 subdid 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) )
257 99 90 addcomd 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) = ( 1 + ( 2 x. N ) ) )
258 257 oveq1d 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( ( 1 + ( 2 x. N ) ) / 2 ) )
259 258 oveq1d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
260 196 a1i 
 |-  ( N e. NN -> 2 =/= 0 )
261 100 87 59 260 divcan6d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( 2 / ( ( 2 x. N ) + 1 ) ) ) = 1 )
262 259 261 oveq12d 
 |-  ( N e. NN -> ( ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
263 244 256 262 3eqtrd 
 |-  ( N e. NN -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
264 241 263 breqtrd 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
265 oveq2 
 |-  ( n = N -> ( 2 x. n ) = ( 2 x. N ) )
266 265 oveq2d 
 |-  ( n = N -> ( 1 + ( 2 x. n ) ) = ( 1 + ( 2 x. N ) ) )
267 266 oveq1d 
 |-  ( n = N -> ( ( 1 + ( 2 x. n ) ) / 2 ) = ( ( 1 + ( 2 x. N ) ) / 2 ) )
268 oveq1 
 |-  ( n = N -> ( n + 1 ) = ( N + 1 ) )
269 id 
 |-  ( n = N -> n = N )
270 268 269 oveq12d 
 |-  ( n = N -> ( ( n + 1 ) / n ) = ( ( N + 1 ) / N ) )
271 270 fveq2d 
 |-  ( n = N -> ( log ` ( ( n + 1 ) / n ) ) = ( log ` ( ( N + 1 ) / N ) ) )
272 267 271 oveq12d 
 |-  ( n = N -> ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
273 272 oveq1d 
 |-  ( n = N -> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
274 id 
 |-  ( N e. NN -> N e. NN )
275 127 254 mulcld 
 |-  ( N e. NN -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) e. CC )
276 275 90 subcld 
 |-  ( N e. NN -> ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC )
277 1 273 274 276 fvmptd3 
 |-  ( N e. NN -> ( J ` N ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
278 264 277 breqtrrd 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( J ` N ) )