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 mulid2d 
 |-  ( 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 mulid1d 
 |-  ( 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 biimpi 
 |-  ( j e. NN -> j e. ( ZZ>= ` 1 ) )
132 131 adantl 
 |-  ( ( N e. NN /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
133 oveq2 
 |-  ( k = n -> ( 2 x. k ) = ( 2 x. n ) )
134 133 oveq1d 
 |-  ( k = n -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. n ) + 1 ) )
135 134 oveq2d 
 |-  ( k = n -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( 1 / ( ( 2 x. n ) + 1 ) ) )
136 134 oveq2d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) )
137 135 136 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 ) ) ) )
138 137 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 ) ) ) ) )
139 elfzuz 
 |-  ( n e. ( 1 ... j ) -> n e. ( ZZ>= ` 1 ) )
140 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
141 140 biimpri 
 |-  ( n e. ( ZZ>= ` 1 ) -> n e. NN )
142 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
143 139 141 142 3syl 
 |-  ( n e. ( 1 ... j ) -> n e. NN0 )
144 143 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. NN0 )
145 2cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 e. CC )
146 144 nn0cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. CC )
147 145 146 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. CC )
148 1cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 1 e. CC )
149 147 148 addcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. CC )
150 elfznn 
 |-  ( n e. ( 1 ... j ) -> n e. NN )
151 0red 
 |-  ( n e. NN -> 0 e. RR )
152 1red 
 |-  ( n e. NN -> 1 e. RR )
153 27 a1i 
 |-  ( n e. NN -> 2 e. RR )
154 nnre 
 |-  ( n e. NN -> n e. RR )
155 153 154 remulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR )
156 155 152 readdcld 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. RR )
157 36 a1i 
 |-  ( n e. NN -> 0 < 1 )
158 2rp 
 |-  2 e. RR+
159 158 a1i 
 |-  ( n e. NN -> 2 e. RR+ )
160 nnrp 
 |-  ( n e. NN -> n e. RR+ )
161 159 160 rpmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR+ )
162 152 161 ltaddrp2d 
 |-  ( n e. NN -> 1 < ( ( 2 x. n ) + 1 ) )
163 151 152 156 157 162 lttrd 
 |-  ( n e. NN -> 0 < ( ( 2 x. n ) + 1 ) )
164 163 gt0ne0d 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) =/= 0 )
165 150 164 syl 
 |-  ( n e. ( 1 ... j ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
166 165 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
167 149 166 reccld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) e. CC )
168 101 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 / ( ( 2 x. N ) + 1 ) ) e. CC )
169 62 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 e. NN0 )
170 169 144 nn0mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. NN0 )
171 65 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 1 e. NN0 )
172 170 171 nn0addcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. NN0 )
173 168 172 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. n ) + 1 ) ) e. CC )
174 167 173 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 )
175 145 174 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 )
176 3 138 144 175 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 ) ) ) ) )
177 176 175 eqeltrd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( H ` n ) e. CC )
178 addcl 
 |-  ( ( n e. CC /\ i e. CC ) -> ( n + i ) e. CC )
179 178 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( n + i ) e. CC )
180 132 177 179 seqcl 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , H ) ` j ) e. CC )
181 1cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> 1 e. CC )
182 2cnd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> 2 e. CC )
183 43 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> N e. CC )
184 182 183 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( 2 x. N ) e. CC )
185 181 184 addcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( 1 + ( 2 x. N ) ) e. CC )
186 185 halfcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> ( ( 1 + ( 2 x. N ) ) / 2 ) e. CC )
187 simprl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> n e. CC )
188 simprr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ ( n e. CC /\ i e. CC ) ) -> i e. CC )
189 186 187 188 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 ) ) )
190 133 oveq2d 
 |-  ( k = n -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) )
191 135 190 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 ) ) ) )
192 150 adantl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. NN )
193 168 170 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. n ) ) e. CC )
194 167 193 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 )
195 2 191 192 194 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 ) ) ) )
196 126 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 + ( 2 x. N ) ) e. CC )
197 2ne0 
 |-  2 =/= 0
198 197 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 =/= 0 )
199 196 145 175 198 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 ) ) )
200 174 145 198 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 ) ) ) )
201 200 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 ) ) ) ) )
202 196 167 173 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 ) ) ) ) )
203 100 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) e. CC )
204 59 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. N ) + 1 ) =/= 0 )
205 172 nn0zd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( 2 x. n ) + 1 ) e. ZZ )
206 203 204 205 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 ) ) ) )
207 206 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 ) ) ) ) )
208 203 172 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) e. CC )
209 203 204 205 expne0d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( ( 2 x. n ) + 1 ) ) =/= 0 )
210 196 208 209 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 ) ) ) ) )
211 43 ad2antrr 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> N e. CC )
212 145 211 mulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. N ) e. CC )
213 148 212 addcomd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 + ( 2 x. N ) ) = ( ( 2 x. N ) + 1 ) )
214 203 170 expcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) e. CC )
215 214 203 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 ) ) ) )
216 213 215 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 ) ) ) ) )
217 203 170 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 ) ) )
218 217 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 ) ) ) )
219 2z 
 |-  2 e. ZZ
220 219 a1i 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> 2 e. ZZ )
221 144 nn0zd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> n e. ZZ )
222 220 221 zmulcld 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 2 x. n ) e. ZZ )
223 203 204 222 expne0d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) ^ ( 2 x. n ) ) =/= 0 )
224 203 203 214 204 223 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 ) ) ) ) )
225 216 218 224 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 ) ) ) )
226 207 210 225 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 ) ) ) )
227 226 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 ) ) ) ) )
228 203 204 dividd 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = 1 )
229 1exp 
 |-  ( ( 2 x. n ) e. ZZ -> ( 1 ^ ( 2 x. n ) ) = 1 )
230 222 229 syl 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( 1 ^ ( 2 x. n ) ) = 1 )
231 228 230 eqtr4d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( ( ( 2 x. N ) + 1 ) / ( ( 2 x. N ) + 1 ) ) = ( 1 ^ ( 2 x. n ) ) )
232 231 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 ) ) ) )
233 148 203 204 170 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 ) ) ) )
234 232 233 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 ) ) )
235 234 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 ) ) ) )
236 202 227 235 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 ) ) ) )
237 199 201 236 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 ) ) ) )
238 176 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 ) )
239 238 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 ) ) )
240 195 237 239 3eqtr2d 
 |-  ( ( ( N e. NN /\ j e. NN ) /\ n e. ( 1 ... j ) ) -> ( K ` n ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( H ` n ) ) )
241 179 189 132 177 240 seqdistr 
 |-  ( ( N e. NN /\ j e. NN ) -> ( seq 1 ( + , K ) ` j ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( seq 1 ( + , H ) ` j ) ) )
242 4 5 125 127 129 180 241 climmulc2 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 2 / ( ( 2 x. N ) + 1 ) ) ) ) )
243 90 99 addcomd 
 |-  ( N e. NN -> ( 1 + ( 2 x. N ) ) = ( ( 2 x. N ) + 1 ) )
244 243 oveq1d 
 |-  ( N e. NN -> ( ( 1 + ( 2 x. N ) ) / 2 ) = ( ( ( 2 x. N ) + 1 ) / 2 ) )
245 244 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 ) ) ) ) )
246 244 127 eqeltrrd 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / 2 ) e. CC )
247 43 90 addcld 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
248 nnne0 
 |-  ( N e. NN -> N =/= 0 )
249 247 43 248 divcld 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) e. CC )
250 49 51 readdcld 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
251 49 ltp1d 
 |-  ( N e. NN -> N < ( N + 1 ) )
252 53 49 250 54 251 lttrd 
 |-  ( N e. NN -> 0 < ( N + 1 ) )
253 252 gt0ne0d 
 |-  ( N e. NN -> ( N + 1 ) =/= 0 )
254 247 43 253 248 divne0d 
 |-  ( N e. NN -> ( ( N + 1 ) / N ) =/= 0 )
255 249 254 logcld 
 |-  ( N e. NN -> ( log ` ( ( N + 1 ) / N ) ) e. CC )
256 87 100 59 divcld 
 |-  ( N e. NN -> ( 2 / ( ( 2 x. N ) + 1 ) ) e. CC )
257 246 255 256 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 ) ) ) ) )
258 99 90 addcomd 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) = ( 1 + ( 2 x. N ) ) )
259 258 oveq1d 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( ( 1 + ( 2 x. N ) ) / 2 ) )
260 259 oveq1d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
261 197 a1i 
 |-  ( N e. NN -> 2 =/= 0 )
262 100 87 59 261 divcan6d 
 |-  ( N e. NN -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) x. ( 2 / ( ( 2 x. N ) + 1 ) ) ) = 1 )
263 260 262 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 ) )
264 245 257 263 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 ) )
265 242 264 breqtrd 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
266 oveq2 
 |-  ( n = N -> ( 2 x. n ) = ( 2 x. N ) )
267 266 oveq2d 
 |-  ( n = N -> ( 1 + ( 2 x. n ) ) = ( 1 + ( 2 x. N ) ) )
268 267 oveq1d 
 |-  ( n = N -> ( ( 1 + ( 2 x. n ) ) / 2 ) = ( ( 1 + ( 2 x. N ) ) / 2 ) )
269 oveq1 
 |-  ( n = N -> ( n + 1 ) = ( N + 1 ) )
270 id 
 |-  ( n = N -> n = N )
271 269 270 oveq12d 
 |-  ( n = N -> ( ( n + 1 ) / n ) = ( ( N + 1 ) / N ) )
272 271 fveq2d 
 |-  ( n = N -> ( log ` ( ( n + 1 ) / n ) ) = ( log ` ( ( N + 1 ) / N ) ) )
273 268 272 oveq12d 
 |-  ( n = N -> ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) = ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) )
274 273 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 ) )
275 id 
 |-  ( N e. NN -> N e. NN )
276 127 255 mulcld 
 |-  ( N e. NN -> ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) e. CC )
277 276 90 subcld 
 |-  ( N e. NN -> ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) e. CC )
278 1 274 275 277 fvmptd3 
 |-  ( N e. NN -> ( J ` N ) = ( ( ( ( 1 + ( 2 x. N ) ) / 2 ) x. ( log ` ( ( N + 1 ) / N ) ) ) - 1 ) )
279 265 278 breqtrrd 
 |-  ( N e. NN -> seq 1 ( + , K ) ~~> ( J ` N ) )