Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wallispi2lem1 Structured version   Unicode version

Theorem wallispi2lem1 29837
Description: An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
Assertion
Ref Expression
wallispi2lem1  |-  ( N  e.  NN  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  N )  =  ( ( 1  /  (
( 2  x.  N
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  N ) ) )

Proof of Theorem wallispi2lem1
Dummy variables  w  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5686 . . 3  |-  ( x  =  1  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 1 ) )
2 oveq2 6094 . . . . . 6  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
32oveq1d 6101 . . . . 5  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43oveq2d 6102 . . . 4  |-  ( x  =  1  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  1 )  +  1 ) ) )
5 fveq2 5686 . . . 4  |-  ( x  =  1  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 1 ) )
64, 5oveq12d 6104 . . 3  |-  ( x  =  1  ->  (
( 1  /  (
( 2  x.  x
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  =  ( ( 1  / 
( ( 2  x.  1 )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 ) ) )
71, 6eqeq12d 2452 . 2  |-  ( x  =  1  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 x )  =  ( ( 1  / 
( ( 2  x.  x )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  <->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) ` 
1 )  =  ( ( 1  /  (
( 2  x.  1 )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 ) ) ) )
8 fveq2 5686 . . 3  |-  ( x  =  y  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 y ) )
9 oveq2 6094 . . . . . 6  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
109oveq1d 6101 . . . . 5  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1110oveq2d 6102 . . . 4  |-  ( x  =  y  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  y )  +  1 ) ) )
12 fveq2 5686 . . . 4  |-  ( x  =  y  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y ) )
1311, 12oveq12d 6104 . . 3  |-  ( x  =  y  ->  (
( 1  /  (
( 2  x.  x
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  =  ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) ) )
148, 13eqeq12d 2452 . 2  |-  ( x  =  y  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 x )  =  ( ( 1  / 
( ( 2  x.  x )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  <->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  y )  =  ( ( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) ) ) )
15 fveq2 5686 . . 3  |-  ( x  =  ( y  +  1 )  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 ( y  +  1 ) ) )
16 oveq2 6094 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
1716oveq1d 6101 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
1817oveq2d 6102 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
19 fveq2 5686 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 ( y  +  1 ) ) )
2018, 19oveq12d 6104 . . 3  |-  ( x  =  ( y  +  1 )  ->  (
( 1  /  (
( 2  x.  x
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  =  ( ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  ( y  +  1 ) ) ) )
2115, 20eqeq12d 2452 . 2  |-  ( x  =  ( y  +  1 )  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 x )  =  ( ( 1  / 
( ( 2  x.  x )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  <->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  ( y  +  1 ) )  =  ( ( 1  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  ( y  +  1 ) ) ) ) )
22 fveq2 5686 . . 3  |-  ( x  =  N  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 N ) )
23 oveq2 6094 . . . . . 6  |-  ( x  =  N  ->  (
2  x.  x )  =  ( 2  x.  N ) )
2423oveq1d 6101 . . . . 5  |-  ( x  =  N  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  N )  +  1 ) )
2524oveq2d 6102 . . . 4  |-  ( x  =  N  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  N )  +  1 ) ) )
26 fveq2 5686 . . . 4  |-  ( x  =  N  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 N ) )
2725, 26oveq12d 6104 . . 3  |-  ( x  =  N  ->  (
( 1  /  (
( 2  x.  x
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  =  ( ( 1  / 
( ( 2  x.  N )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  N ) ) )
2822, 27eqeq12d 2452 . 2  |-  ( x  =  N  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 x )  =  ( ( 1  / 
( ( 2  x.  x )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  x ) )  <->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  N )  =  ( ( 1  /  (
( 2  x.  N
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  N ) ) ) )
29 1z 10668 . . . 4  |-  1  e.  ZZ
30 seq1 11811 . . . 4  |-  ( 1  e.  ZZ  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) ` 
1 )  =  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) `  1
) )
3129, 30ax-mp 5 . . 3  |-  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) ` 
1 )  =  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) `  1
)
32 1nn 10325 . . . 4  |-  1  e.  NN
33 oveq2 6094 . . . . . . 7  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
3433oveq1d 6101 . . . . . . 7  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
3533, 34oveq12d 6104 . . . . . 6  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  -  1 ) ) )
3633oveq1d 6101 . . . . . . 7  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
3733, 36oveq12d 6104 . . . . . 6  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )
3835, 37oveq12d 6104 . . . . 5  |-  ( k  =  1  ->  (
( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  - 
1 ) )  x.  ( ( 2  x.  1 )  /  (
( 2  x.  1 )  +  1 ) ) ) )
39 eqid 2438 . . . . 5  |-  ( k  e.  NN  |->  ( ( ( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  x.  ( ( 2  x.  k )  / 
( ( 2  x.  k )  +  1 ) ) ) )  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) )
40 ovex 6111 . . . . 5  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  e. 
_V
4138, 39, 40fvmpt 5769 . . . 4  |-  ( 1  e.  NN  ->  (
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) `  1
)  =  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) ) )
4232, 41ax-mp 5 . . 3  |-  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) ) ) `  1 )  =  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  - 
1 ) )  x.  ( ( 2  x.  1 )  /  (
( 2  x.  1 )  +  1 ) ) )
43 2cn 10384 . . . . . . . 8  |-  2  e.  CC
4443mulid1i 9380 . . . . . . 7  |-  ( 2  x.  1 )  =  2
4544oveq1i 6096 . . . . . . . 8  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
46 2m1e1 10428 . . . . . . . 8  |-  ( 2  -  1 )  =  1
4745, 46eqtri 2458 . . . . . . 7  |-  ( ( 2  x.  1 )  -  1 )  =  1
4844, 47oveq12i 6098 . . . . . 6  |-  ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  - 
1 ) )  =  ( 2  /  1
)
4944oveq1i 6096 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
50 2p1e3 10437 . . . . . . . 8  |-  ( 2  +  1 )  =  3
5149, 50eqtri 2458 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
5244, 51oveq12i 6098 . . . . . 6  |-  ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  +  1 ) )  =  ( 2  /  3
)
5348, 52oveq12i 6098 . . . . 5  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( ( 2  / 
1 )  x.  (
2  /  3 ) )
54 ax-1cn 9332 . . . . . 6  |-  1  e.  CC
55 3cn 10388 . . . . . 6  |-  3  e.  CC
56 ax-1ne0 9343 . . . . . 6  |-  1  =/=  0
57 3ne0 10408 . . . . . 6  |-  3  =/=  0
5843, 54, 43, 55, 56, 57divmuldivi 10083 . . . . 5  |-  ( ( 2  /  1 )  x.  ( 2  / 
3 ) )  =  ( ( 2  x.  2 )  /  (
1  x.  3 ) )
59 2t2e4 10463 . . . . . 6  |-  ( 2  x.  2 )  =  4
6055mulid2i 9381 . . . . . 6  |-  ( 1  x.  3 )  =  3
6159, 60oveq12i 6098 . . . . 5  |-  ( ( 2  x.  2 )  /  ( 1  x.  3 ) )  =  ( 4  /  3
)
6253, 58, 613eqtri 2462 . . . 4  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( 4  /  3
)
63 4cn 10391 . . . . 5  |-  4  e.  CC
64 divrec2 10003 . . . . 5  |-  ( ( 4  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )  ->  (
4  /  3 )  =  ( ( 1  /  3 )  x.  4 ) )
6563, 55, 57, 64mp3an 1314 . . . 4  |-  ( 4  /  3 )  =  ( ( 1  / 
3 )  x.  4 )
6651eqcomi 2442 . . . . . 6  |-  3  =  ( ( 2  x.  1 )  +  1 )
6766oveq2i 6097 . . . . 5  |-  ( 1  /  3 )  =  ( 1  /  (
( 2  x.  1 )  +  1 ) )
68 seq1 11811 . . . . . . . 8  |-  ( 1  e.  ZZ  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 )  =  ( ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) `  1
) )
6929, 68ax-mp 5 . . . . . . 7  |-  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 )  =  ( ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) `  1
)
7033oveq1d 6101 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( 2  x.  k
) ^ 4 )  =  ( ( 2  x.  1 ) ^
4 ) )
7133, 34oveq12d 6104 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) )
7271oveq1d 6101 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )
7370, 72oveq12d 6104 . . . . . . . . 9  |-  ( k  =  1  ->  (
( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) )  =  ( ( ( 2  x.  1 ) ^ 4 )  / 
( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) ^ 2 ) ) )
74 eqid 2438 . . . . . . . . 9  |-  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) )  =  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) )
75 ovex 6111 . . . . . . . . 9  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  e. 
_V
7673, 74, 75fvmpt 5769 . . . . . . . 8  |-  ( 1  e.  NN  ->  (
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) `  1
)  =  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) ) )
7732, 76ax-mp 5 . . . . . . 7  |-  ( ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) `  1 )  =  ( ( ( 2  x.  1 ) ^ 4 )  / 
( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) ^ 2 ) )
7844oveq1i 6096 . . . . . . . . 9  |-  ( ( 2  x.  1 ) ^ 4 )  =  ( 2 ^ 4 )
7944, 47oveq12i 6098 . . . . . . . . . . 11  |-  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) )  =  ( 2  x.  1 )
8079, 44eqtri 2458 . . . . . . . . . 10  |-  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) )  =  2
8180oveq1i 6096 . . . . . . . . 9  |-  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) ^ 2 )  =  ( 2 ^ 2 )
8278, 81oveq12i 6098 . . . . . . . 8  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  =  ( ( 2 ^ 4 )  /  (
2 ^ 2 ) )
83 2exp4 14106 . . . . . . . . . 10  |-  ( 2 ^ 4 )  = ; 1
6
84 sq2 11954 . . . . . . . . . 10  |-  ( 2 ^ 2 )  =  4
8583, 84oveq12i 6098 . . . . . . . . 9  |-  ( ( 2 ^ 4 )  /  ( 2 ^ 2 ) )  =  (; 1 6  /  4
)
86 4t4e16 10820 . . . . . . . . . . 11  |-  ( 4  x.  4 )  = ; 1
6
8786eqcomi 2442 . . . . . . . . . 10  |- ; 1 6  =  ( 4  x.  4 )
8887oveq1i 6096 . . . . . . . . 9  |-  (; 1 6  /  4
)  =  ( ( 4  x.  4 )  /  4 )
89 4ne0 10410 . . . . . . . . . 10  |-  4  =/=  0
9063, 63, 89divcan3i 10069 . . . . . . . . 9  |-  ( ( 4  x.  4 )  /  4 )  =  4
9185, 88, 903eqtri 2462 . . . . . . . 8  |-  ( ( 2 ^ 4 )  /  ( 2 ^ 2 ) )  =  4
9282, 91eqtri 2458 . . . . . . 7  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  =  4
9369, 77, 923eqtri 2462 . . . . . 6  |-  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 )  =  4
9493eqcomi 2442 . . . . 5  |-  4  =  (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  1
)
9567, 94oveq12i 6098 . . . 4  |-  ( ( 1  /  3 )  x.  4 )  =  ( ( 1  / 
( ( 2  x.  1 )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 ) )
9662, 65, 953eqtri 2462 . . 3  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( ( 1  / 
( ( 2  x.  1 )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 ) )
9731, 42, 963eqtri 2462 . 2  |-  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) ` 
1 )  =  ( ( 1  /  (
( 2  x.  1 )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 ) )
98 elnnuz 10889 . . . . . . 7  |-  ( y  e.  NN  <->  y  e.  ( ZZ>= `  1 )
)
9998biimpi 194 . . . . . 6  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
10099adantr 465 . . . . 5  |-  ( ( y  e.  NN  /\  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 y )  =  ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) ) )  ->  y  e.  (
ZZ>= `  1 ) )
101 seqp1 11813 . . . . 5  |-  ( y  e.  ( ZZ>= `  1
)  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  ( y  +  1 ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  x.  ( ( 2  x.  k )  / 
( ( 2  x.  k )  +  1 ) ) ) ) ) `  y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  x.  ( ( 2  x.  k )  / 
( ( 2  x.  k )  +  1 ) ) ) ) `
 ( y  +  1 ) ) ) )
102100, 101syl 16 . . . 4  |-  ( ( y  e.  NN  /\  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 y )  =  ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) ) )  ->  (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  (
y  +  1 ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) `  ( y  +  1 ) ) ) )
103 simpr 461 . . . . 5  |-  ( ( y  e.  NN  /\  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 y )  =  ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) ) )  ->  (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  y
)  =  ( ( 1  /  ( ( 2  x.  y )  +  1 ) )  x.  (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  y
) ) )
104103oveq1d 6101 . . . 4  |-  ( ( y  e.  NN  /\  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) ) `
 y )  =  ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) ) )  ->  ( (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) ) `  y )  x.  (
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) `  (
y  +  1 ) ) )  =  ( ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) `  ( y  +  1 ) ) ) )
105 eqidd 2439 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
k  e.  NN  |->  ( ( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) ) )  =  ( k  e.  NN  |->  ( ( ( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  x.  ( ( 2  x.  k )  / 
( ( 2  x.  k )  +  1 ) ) ) ) )
106 oveq2 6094 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
107106oveq1d 6101 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
108106, 107oveq12d 6104 . . . . . . . . . . 11  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
109106oveq1d 6101 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
110106, 109oveq12d 6104 . . . . . . . . . . 11  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
111108, 110oveq12d 6104 . . . . . . . . . 10  |-  ( k  =  ( y  +  1 )  ->  (
( ( 2  x.  k )  /  (
( 2  x.  k
)  -  1 ) )  x.  ( ( 2  x.  k )  /  ( ( 2  x.  k )  +  1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
112111adantl 466 . . . . . . . . 9  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) )
113 peano2nn 10326 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
114 2rp 10988 . . . . . . . . . . . . 13  |-  2  e.  RR+
115114a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  e.  RR+ )
116 nnre 10321 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  RR )
117 nnnn0 10578 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  NN0 )
118117nn0ge0d 10631 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  y )
119116, 118ge0p1rpd 11045 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
120115, 119rpmulcld 11035 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
121 2re 10383 . . . . . . . . . . . . . . 15  |-  2  e.  RR
122121a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  RR )
123 1re 9377 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
124123a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  e.  RR )
125116, 124readdcld 9405 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
126122, 125remulcld 9406 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
127126, 124resubcld 9768 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
128 1lt2 10480 . . . . . . . . . . . . . . 15  |-  1  <  2
129128a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <  2 )
130 nnrp 10992 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  RR+ )
131124, 130ltaddrp2d 11049 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
132122, 125, 129, 131mulgt1d 10261 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  1  <  ( 2  x.  (
y  +  1 ) ) )
133124, 126posdifd 9918 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  <  ( 2  x.  ( y  +  1 ) )  <->  0  <  ( ( 2  x.  (
y  +  1 ) )  -  1 ) ) )
134132, 133mpbid 210 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  0  <  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )
135127, 134elrpd 11017 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR+ )
136120, 135rpdivcld 11036 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR+ )
137115rpge0d 11023 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  2 )
138 0le1 9855 . . . . . . . . . . . . . . 15  |-  0  <_  1
139138a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  1 )
140116, 124, 118, 139addge0d 9907 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  ( y  +  1 ) )
141122, 125, 137, 140mulge0d 9908 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  (
y  +  1 ) ) )
142126, 141ge0p1rpd 11045 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR+ )
143120, 142rpdivcld 11036 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR+ )
144136, 143rpmulcld 11035 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  e.  RR+ )
145105, 112, 113, 144fvmptd 5774 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( k  e.  NN  |->  ( ( ( 2  x.  k )  / 
( ( 2  x.  k )  -  1 ) )  x.  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) ) ) ) `  (
y  +  1 ) )  =  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) )
146145oveq2d 6102 . . . . . . 7  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) `  ( y  +  1 ) ) )  =  ( ( ( 1  /  ( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  y ) )  x.  ( ( ( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) ) )
147126recnd 9404 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
148127recnd 9404 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  CC )
149142rpcnd 11021 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  CC )
150134gt0ne0d 9896 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
151142rpne0d 11024 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
152147, 148, 147, 149, 150, 151divmuldivd 10140 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  - 
1 )  x.  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
153147, 147mulcld 9398 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
154153, 148, 149, 150, 151divdiv1d 10130 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  - 
1 )  x.  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
155147sqvald 11997 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  (
y  +  1 ) ) ) )
156155eqcomd 2443 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  =  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )
157156oveq1d 6101 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
2  x.  ( y  +  1 ) ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
158157oveq1d 6101 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  (
y  +  1 ) ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( ( ( 2  x.  (
y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
159152, 154, 1583eqtr2d 2476 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )  =  ( ( ( ( 2  x.  (
y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
160159oveq2d 6102 . . . . . . 7  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) ) ) )  =  ( ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) ) )
161147sqcld 11998 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  e.  CC )
162161, 148, 150divcld 10099 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  CC )
163162, 149, 151divrec2d 10103 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  =  ( ( 1  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ) )
164163oveq2d 6102 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) )  =  ( ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ) ) )
165 2cnd 10386 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  e.  CC )
166 nncn 10322 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  CC )
167165, 166mulcld 9398 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
16854a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  1  e.  CC )
169167, 168addcld 9397 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
170 2nn 10471 . . . . . . . . . . . . . . 15  |-  2  e.  NN
171170a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  NN )
172 id 22 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  NN )
173171, 172nnmulcld 10361 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN )
174173peano2nnd 10331 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  NN )
175174nnne0d 10358 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
176169, 175reccld 10092 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
1  /  ( ( 2  x.  y )  +  1 ) )  e.  CC )
177 eqidd 2439 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) )  =  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) )
178 oveq2 6094 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  (
2  x.  k )  =  ( 2  x.  x ) )
179178oveq1d 6101 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( 2  x.  k
) ^ 4 )  =  ( ( 2  x.  x ) ^
4 ) )
180178oveq1d 6101 . . . . . . . . . . . . . . . . 17  |-  ( k  =  x  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  x )  - 
1 ) )
181178, 180oveq12d 6104 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  (
( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) )
182181oveq1d 6101 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  - 
1 ) ) ^
2 ) )
183179, 182oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) )  =  ( ( ( 2  x.  x ) ^ 4 )  / 
( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) ) )
184183adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  /\  k  =  x )  ->  ( (
( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) )  =  ( ( ( 2  x.  x ) ^
4 )  /  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 ) ) )
185 elfznn 11470 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... y )  ->  x  e.  NN )
186185adantl 466 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  x  e.  NN )
187170a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  e.  NN )
188 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  e.  NN )
189187, 188nnmulcld 10361 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  NN )
190 4nn0 10590 . . . . . . . . . . . . . . . . . . 19  |-  4  e.  NN0
191190a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  4  e.  NN0 )
192189, 191nnexpcld 12021 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
) ^ 4 )  e.  NN )
193192nncnd 10330 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( 2  x.  x
) ^ 4 )  e.  CC )
194 2cnd 10386 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  e.  CC )
195 nncn 10322 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  e.  CC )
196194, 195mulcld 9398 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  CC )
19754a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  1  e.  CC )
198196, 197subcld 9711 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  -  1 )  e.  CC )
199196, 198mulcld 9398 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) )  e.  CC )
200199sqcld 11998 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 )  e.  CC )
201187nnne0d 10358 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  =/=  0 )
202 nnne0 10346 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  =/=  0 )
203194, 195, 201, 202mulne0d 9980 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  =/=  0 )
204123a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  NN  ->  1  e.  RR )
205121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  2  e.  RR )
206205, 204remulcld 9406 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  1 )  e.  RR )
207 nnre 10321 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  x  e.  RR )
208205, 207remulcld 9406 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  RR )
20944a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  (
2  x.  1 )  =  2 )
210128, 209syl5breqr 4323 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  1  <  ( 2  x.  1 ) )
211 0le2 10404 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <_  2
212211a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  0  <_  2 )
213 nnge1 10340 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  1  <_  x )
214204, 207, 205, 212, 213lemul2ad 10265 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  1 )  <_  ( 2  x.  x ) )
215204, 206, 208, 210, 214ltletrd 9523 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  NN  ->  1  <  ( 2  x.  x
) )
216204, 215gtned 9501 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  (
2  x.  x )  =/=  1 )
217196, 197, 216subne0d 9720 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  -  1 )  =/=  0 )
218196, 198, 203, 217mulne0d 9980 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) )  =/=  0 )
219 2z 10670 . . . . . . . . . . . . . . . . . 18  |-  2  e.  ZZ
220219a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  2  e.  ZZ )
221199, 218, 220expne0d 12006 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 )  =/=  0 )
222193, 200, 221divcld 10099 . . . . . . . . . . . . . . 15  |-  ( x  e.  NN  ->  (
( ( 2  x.  x ) ^ 4 )  /  ( ( ( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
223185, 222syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... y )  ->  (
( ( 2  x.  x ) ^ 4 )  /  ( ( ( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
224223adantl 466 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  ( ( ( 2  x.  x ) ^ 4 )  / 
( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
225177, 184, 186, 224fvmptd 5774 . . . . . . . . . . . 12  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) `
 x )  =  ( ( ( 2  x.  x ) ^
4 )  /  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 ) ) )
226225, 224eqeltrd 2512 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) `
 x )  e.  CC )
227 mulcl 9358 . . . . . . . . . . . 12  |-  ( ( x  e.  CC  /\  w  e.  CC )  ->  ( x  x.  w
)  e.  CC )
228227adantl 466 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  ( x  e.  CC  /\  w  e.  CC ) )  ->  ( x  x.  w )  e.  CC )
22999, 226, 228seqcl 11818 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y )  e.  CC )
230176, 229mulcld 9398 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  e.  CC )
231149, 151reccld 10092 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
1  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  CC )
232230, 231, 162mul12d 9570 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ) )  =  ( ( 1  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) )  x.  ( ( ( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ) ) )
233176, 229mulcomd 9399 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  =  ( (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  y
)  x.  ( 1  /  ( ( 2  x.  y )  +  1 ) ) ) )
234233oveq1d 6101 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) )  =  ( ( (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  y
)  x.  ( 1  /  ( ( 2  x.  y )  +  1 ) ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ) )
235229, 176, 162mulassd 9401 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  y
)  x.  ( 1  /  ( ( 2  x.  y )  +  1 ) ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )  =  ( (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  y
)  x.  ( ( 1  /  ( ( 2  x.  y )  +  1 ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ) ) )
236168, 169, 161, 148, 175, 150divmuldivd 10140 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( ( 2  x.  (
y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ) )  =  ( ( 1  x.  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )  / 
( ( ( 2  x.  y )  +  1 )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ) )
237161mulid2d 9396 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  x.  ( ( 2  x.  ( y  +  1 ) ) ^ 2 ) )  =  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )
238165, 166, 168adddid 9402 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
23944a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
240239oveq2d 6102 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
241238, 240eqtrd 2470 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
242241oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
243167, 165, 168addsubassd 9731 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
24446a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  -  1 )  =  1 )
245244oveq2d 6102 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
246242, 243, 2453eqtrd 2474 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
247246oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  1 ) ) )
248169sqvald 11997 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 ) ^ 2 )  =  ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  1 ) ) )
249247, 248eqtr4d 2473 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  y )  +  1 ) ^
2 ) )
250237, 249oveq12d 6104 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 1  x.  (
( 2  x.  (
y  +  1 ) ) ^ 2 ) )  /  ( ( ( 2  x.  y
)  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( ( 2  x.  y )  +  1 ) ^ 2 ) ) )
251 2p2e4 10431 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  +  2 )  =  4
25263, 43, 43, 251subaddrii 9689 . . . . . . . . . . . . . . . . . 18  |-  ( 4  -  2 )  =  2
253252eqcomi 2442 . . . . . . . . . . . . . . . . 17  |-  2  =  ( 4  -  2 )
254253a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  =  ( 4  -  2 ) )
255254oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( 2  x.  ( y  +  1 ) ) ^
( 4  -  2 ) ) )
256120rpne0d 11024 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
257219a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  ZZ )
258190nn0zi 10663 . . . . . . . . . . . . . . . . 17  |-  4  e.  ZZ
259258a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  4  e.  ZZ )
260147, 256, 257, 259expsubd 12011 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ ( 4  -  2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( 2  x.  ( y  +  1 ) ) ^ 2 ) ) )
261255, 260eqtrd 2470 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( 2  x.  ( y  +  1 ) ) ^ 2 ) ) )
262246eqcomd 2443 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
263262oveq1d 6101 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) )  -  1 ) ^
2 ) )
264261, 263oveq12d 6104 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( ( 2  x.  y
)  +  1 ) ^ 2 ) )  =  ( ( ( ( 2  x.  (
y  +  1 ) ) ^ 4 )  /  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )  / 
( ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ^ 2 ) ) )
265147, 256, 259expclzd 12005 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 4 )  e.  CC )
266148sqcld 11998 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 )  e.  CC )
267166, 168addcld 9397 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
268171nnne0d 10358 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  =/=  0 )
269113nnne0d 10358 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
270165, 267, 268, 269mulne0d 9980 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
271147, 270, 257expne0d 12006 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =/=  0 )
272148, 150, 257expne0d 12006 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 )  =/=  0 )
273265, 161, 266, 271, 272divdiv1d 10130 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( ( 2  x.  ( y  +  1 ) ) ^
4 )  /  (
( 2  x.  (
y  +  1 ) ) ^ 2 ) )  /  ( ( ( 2  x.  (
y  +  1 ) )  -  1 ) ^ 2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  x.  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 ) ) ) )
274147, 148sqmuld 12012 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  x.  ( ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ^ 2 ) ) )
275274eqcomd 2443 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  x.  ( ( ( 2  x.  (
y  +  1 ) )  -  1 ) ^ 2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ) ^
2 ) )
276275oveq2d 6102 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  (
y  +  1 ) ) ^ 2 )  x.  ( ( ( 2  x.  ( y  +  1 ) )  -  1 ) ^
2 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) ) )
277264, 273, 2763eqtrd 2474 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( ( 2  x.  y
)  +  1 ) ^ 2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) ) )
278236, 250, 2773eqtrd 2474 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  ( ( ( 2  x.  (
y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) ) )
279278oveq2d 6102 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) ) ) )
280234, 235, 2793eqtrd 2474 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) ) ) )
281280oveq2d 6102 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) )  x.  ( ( ( 1  /  (
( 2  x.  y
)  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
2 )  /  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ) )  =  ( ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
4 )  /  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 ) ) ) ) )
282164, 232, 2813eqtrd 2474 . . . . . . 7  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( ( ( 2  x.  ( y  +  1 ) ) ^ 2 )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) )  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) ) )  =  ( ( 1  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) )  x.  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
4 )  /  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 ) ) ) ) )
283146, 160, 2823eqtrd 2474 . . . . . 6  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  - 
1 ) )  x.  ( ( 2  x.  k )  /  (
( 2  x.  k
)  +  1 ) ) ) ) `  ( y  +  1 ) ) )  =  ( ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
4 )  /  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 ) ) ) ) )
284 eqidd 2439 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) )  =  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) )
285 simpr 461 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  k  =  ( y  +  1 ) )
286285oveq2d 6102 . . . . . . . . . . . 12  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( 2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
287286oveq1d 6101 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k ) ^
4 )  =  ( ( 2  x.  (
y  +  1 ) ) ^ 4 ) )
288286oveq1d 6101 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k )  - 
1 )  =  ( ( 2  x.  (
y  +  1 ) )  -  1 ) )
289286, 288oveq12d 6104 . . . . . . . . . . . 12  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
290289oveq1d 6101 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 )  =  ( ( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 ) )
291287, 290oveq12d 6104 . . . . . . . . . 10  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) ) )
292147, 148mulcld 9398 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  CC )
293292sqcld 11998 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  e.  CC )
294147, 148, 256, 150mulne0d 9980 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =/=  0 )
295292, 294, 257expne0d 12006 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  =/=  0 )
296265, 293, 295divcld 10099 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) )  e.  CC )
297284, 291, 113, 296fvmptd 5774 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) `  (
y  +  1 ) )  =  ( ( ( 2  x.  (
y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  ( y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) ) ^
2 ) ) )
298297eqcomd 2443 . . . . . . . 8  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) )  =  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) `
 ( y  +  1 ) ) )
299298oveq2d 6102 . . . . . . 7  |-  ( y  e.  NN  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
4 )  /  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 ) ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) `
 ( y  +  1 ) ) ) )
300299oveq2d 6102 . . . . . 6  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) )  x.  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( ( 2  x.  ( y  +  1 ) ) ^
4 )  /  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 ) ) ) )  =  ( ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) `  ( y  +  1 ) ) ) ) )
301 seqp1 11813 . . . . . . . . 9  |-  ( y  e.  ( ZZ>= `  1
)  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  ( y  +  1 ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) `
 ( y  +  1 ) ) ) )
30299, 301syl 16 . . . . . . . 8  |-  ( y  e.  NN  ->  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) `  ( y  +  1 ) )  =  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) `
 ( y  +  1 ) ) ) )
303302eqcomd 2443 . . . . . . 7  |-  ( y  e.  NN  ->  (
(  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) `  ( y  +  1 ) ) )  =  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  ( y  +  1 ) ) )
304303oveq2d 6102 . . . . . 6  |-  ( y  e.  NN  ->  (
( 1  /  (
( 2  x.  (
y  +  1 ) )  +  1 ) )  x.  ( (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `
 y )  x.  ( ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  / 
( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) `  ( y  +  1 ) ) ) )  =  ( ( 1  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  x.  (  seq 1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k
) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  - 
1 ) ) ^
2 ) ) ) ) `  ( y  +  1 ) ) ) )
305283, 300, 3043eqtrd 2474 . . . . 5  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k