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

Theorem wallispi2lem1 31738
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 5852 . . 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 6285 . . . . . 6  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
32oveq1d 6292 . . . . 5  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43oveq2d 6293 . . . 4  |-  ( x  =  1  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  1 )  +  1 ) ) )
5 fveq2 5852 . . . 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 6295 . . 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 2463 . 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 5852 . . 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 6285 . . . . . 6  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
109oveq1d 6292 . . . . 5  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1110oveq2d 6293 . . . 4  |-  ( x  =  y  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  y )  +  1 ) ) )
12 fveq2 5852 . . . 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 6295 . . 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 2463 . 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 5852 . . 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 6285 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
1716oveq1d 6292 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
1817oveq2d 6293 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
19 fveq2 5852 . . . 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 6295 . . 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 2463 . 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 5852 . . 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 6285 . . . . . 6  |-  ( x  =  N  ->  (
2  x.  x )  =  ( 2  x.  N ) )
2423oveq1d 6292 . . . . 5  |-  ( x  =  N  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  N )  +  1 ) )
2524oveq2d 6293 . . . 4  |-  ( x  =  N  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  N )  +  1 ) ) )
26 fveq2 5852 . . . 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 6295 . . 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 2463 . 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 10895 . . . 4  |-  1  e.  ZZ
30 seq1 12094 . . . 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 10548 . . . 4  |-  1  e.  NN
33 oveq2 6285 . . . . . . 7  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
3433oveq1d 6292 . . . . . . 7  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
3533, 34oveq12d 6295 . . . . . 6  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  -  1 ) ) )
3633oveq1d 6292 . . . . . . 7  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
3733, 36oveq12d 6295 . . . . . 6  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )
3835, 37oveq12d 6295 . . . . 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 2441 . . . . 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 6305 . . . . 5  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  e. 
_V
4138, 39, 40fvmpt 5937 . . . 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 2t1e2 10685 . . . . . . 7  |-  ( 2  x.  1 )  =  2
4443oveq1i 6287 . . . . . . . 8  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
45 2m1e1 10651 . . . . . . . 8  |-  ( 2  -  1 )  =  1
4644, 45eqtri 2470 . . . . . . 7  |-  ( ( 2  x.  1 )  -  1 )  =  1
4743, 46oveq12i 6289 . . . . . 6  |-  ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  - 
1 ) )  =  ( 2  /  1
)
4843oveq1i 6287 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
49 2p1e3 10660 . . . . . . . 8  |-  ( 2  +  1 )  =  3
5048, 49eqtri 2470 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
5143, 50oveq12i 6289 . . . . . 6  |-  ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  +  1 ) )  =  ( 2  /  3
)
5247, 51oveq12i 6289 . . . . 5  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( ( 2  / 
1 )  x.  (
2  /  3 ) )
53 2cn 10607 . . . . . 6  |-  2  e.  CC
54 ax-1cn 9548 . . . . . 6  |-  1  e.  CC
55 3cn 10611 . . . . . 6  |-  3  e.  CC
56 ax-1ne0 9559 . . . . . 6  |-  1  =/=  0
57 3ne0 10631 . . . . . 6  |-  3  =/=  0
5853, 54, 53, 55, 56, 57divmuldivi 10305 . . . . 5  |-  ( ( 2  /  1 )  x.  ( 2  / 
3 ) )  =  ( ( 2  x.  2 )  /  (
1  x.  3 ) )
59 2t2e4 10686 . . . . . 6  |-  ( 2  x.  2 )  =  4
6055mulid2i 9597 . . . . . 6  |-  ( 1  x.  3 )  =  3
6159, 60oveq12i 6289 . . . . 5  |-  ( ( 2  x.  2 )  /  ( 1  x.  3 ) )  =  ( 4  /  3
)
6252, 58, 613eqtri 2474 . . . 4  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( 4  /  3
)
63 4cn 10614 . . . . 5  |-  4  e.  CC
64 divrec2 10225 . . . . 5  |-  ( ( 4  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )  ->  (
4  /  3 )  =  ( ( 1  /  3 )  x.  4 ) )
6563, 55, 57, 64mp3an 1323 . . . 4  |-  ( 4  /  3 )  =  ( ( 1  / 
3 )  x.  4 )
6650eqcomi 2454 . . . . . 6  |-  3  =  ( ( 2  x.  1 )  +  1 )
6766oveq2i 6288 . . . . 5  |-  ( 1  /  3 )  =  ( 1  /  (
( 2  x.  1 )  +  1 ) )
68 seq1 12094 . . . . . . . 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 6292 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( 2  x.  k
) ^ 4 )  =  ( ( 2  x.  1 ) ^
4 ) )
7133, 34oveq12d 6295 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) )
7271oveq1d 6292 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )
7370, 72oveq12d 6295 . . . . . . . . 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 2441 . . . . . . . . 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 6305 . . . . . . . . 9  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  e. 
_V
7673, 74, 75fvmpt 5937 . . . . . . . 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 ) )
7843oveq1i 6287 . . . . . . . . 9  |-  ( ( 2  x.  1 ) ^ 4 )  =  ( 2 ^ 4 )
7943, 46oveq12i 6289 . . . . . . . . . . 11  |-  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) )  =  ( 2  x.  1 )
8079, 43eqtri 2470 . . . . . . . . . 10  |-  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) )  =  2
8180oveq1i 6287 . . . . . . . . 9  |-  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) ^ 2 )  =  ( 2 ^ 2 )
8278, 81oveq12i 6289 . . . . . . . 8  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  =  ( ( 2 ^ 4 )  /  (
2 ^ 2 ) )
83 2exp4 14443 . . . . . . . . . 10  |-  ( 2 ^ 4 )  = ; 1
6
84 sq2 12238 . . . . . . . . . 10  |-  ( 2 ^ 2 )  =  4
8583, 84oveq12i 6289 . . . . . . . . 9  |-  ( ( 2 ^ 4 )  /  ( 2 ^ 2 ) )  =  (; 1 6  /  4
)
86 4t4e16 11052 . . . . . . . . . . 11  |-  ( 4  x.  4 )  = ; 1
6
8786eqcomi 2454 . . . . . . . . . 10  |- ; 1 6  =  ( 4  x.  4 )
8887oveq1i 6287 . . . . . . . . 9  |-  (; 1 6  /  4
)  =  ( ( 4  x.  4 )  /  4 )
89 4ne0 10633 . . . . . . . . . 10  |-  4  =/=  0
9063, 63, 89divcan3i 10291 . . . . . . . . 9  |-  ( ( 4  x.  4 )  /  4 )  =  4
9185, 88, 903eqtri 2474 . . . . . . . 8  |-  ( ( 2 ^ 4 )  /  ( 2 ^ 2 ) )  =  4
9282, 91eqtri 2470 . . . . . . 7  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  =  4
9369, 77, 923eqtri 2474 . . . . . 6  |-  (  seq 1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 )  =  4
9493eqcomi 2454 . . . . 5  |-  4  =  (  seq 1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  1
)
9567, 94oveq12i 6289 . . . 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 2474 . . 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 2474 . 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 11121 . . . . . . 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 12096 . . . . 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 6292 . . . 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 2442 . . . . . . . . 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 6285 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
107106oveq1d 6292 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
108106, 107oveq12d 6295 . . . . . . . . . . 11  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
109106oveq1d 6292 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
110106, 109oveq12d 6295 . . . . . . . . . . 11  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
111108, 110oveq12d 6295 . . . . . . . . . 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 10549 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
114 2rp 11229 . . . . . . . . . . . . 13  |-  2  e.  RR+
115114a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  e.  RR+ )
116 nnre 10544 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  RR )
117 nnnn0 10803 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  NN0 )
118117nn0ge0d 10856 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  y )
119116, 118ge0p1rpd 11286 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
120115, 119rpmulcld 11276 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
121 2re 10606 . . . . . . . . . . . . . . 15  |-  2  e.  RR
122121a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  RR )
123 1red 9609 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  e.  RR )
124116, 123readdcld 9621 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
125122, 124remulcld 9622 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
126125, 123resubcld 9988 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
127 1lt2 10703 . . . . . . . . . . . . . . 15  |-  1  <  2
128127a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <  2 )
129 nnrp 11233 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  RR+ )
130123, 129ltaddrp2d 11290 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
131122, 124, 128, 130mulgt1d 10483 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  1  <  ( 2  x.  (
y  +  1 ) ) )
132123, 125posdifd 10140 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  <  ( 2  x.  ( y  +  1 ) )  <->  0  <  ( ( 2  x.  (
y  +  1 ) )  -  1 ) ) )
133131, 132mpbid 210 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  0  <  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )
134126, 133elrpd 11258 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR+ )
135120, 134rpdivcld 11277 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR+ )
136115rpge0d 11264 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  2 )
137 0le1 10077 . . . . . . . . . . . . . . 15  |-  0  <_  1
138137a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  1 )
139116, 123, 118, 138addge0d 10129 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  ( y  +  1 ) )
140122, 124, 136, 139mulge0d 10130 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  (
y  +  1 ) ) )
141125, 140ge0p1rpd 11286 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR+ )
142120, 141rpdivcld 11277 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR+ )
143135, 142rpmulcld 11276 . . . . . . . . 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+ )
144105, 112, 113, 143fvmptd 5942 . . . . . . . 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 ) ) ) )
145144oveq2d 6293 . . . . . . 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 ) ) ) ) )
146125recnd 9620 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
147126recnd 9620 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  CC )
148141rpcnd 11262 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  CC )
149133gt0ne0d 10118 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
150141rpne0d 11265 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
151146, 147, 146, 148, 149, 150divmuldivd 10362 . . . . . . . . 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 ) ) ) )
152146, 146mulcld 9614 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
153152, 147, 148, 149, 150divdiv1d 10352 . . . . . . . . 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 ) ) ) )
154146sqvald 12281 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  (
y  +  1 ) ) ) )
155154eqcomd 2449 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  =  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )
156155oveq1d 6292 . . . . . . . . . 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 ) ) )
157156oveq1d 6292 . . . . . . . . 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 ) ) )
158151, 153, 1573eqtr2d 2488 . . . . . . . 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 ) ) )
159158oveq2d 6293 . . . . . . 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 ) ) ) )
160146sqcld 12282 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  e.  CC )
161160, 147, 149divcld 10321 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  CC )
162161, 148, 150divrec2d 10325 . . . . . . . . 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 ) ) ) )
163162oveq2d 6293 . . . . . . . 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 ) ) ) ) )
164 2cnd 10609 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  e.  CC )
165 nncn 10545 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  CC )
166164, 165mulcld 9614 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
167 1cnd 9610 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  1  e.  CC )
168166, 167addcld 9613 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
169 2nn 10694 . . . . . . . . . . . . . . 15  |-  2  e.  NN
170169a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  NN )
171 id 22 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  NN )
172170, 171nnmulcld 10584 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN )
173172peano2nnd 10554 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  NN )
174173nnne0d 10581 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
175168, 174reccld 10314 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
1  /  ( ( 2  x.  y )  +  1 ) )  e.  CC )
176 eqidd 2442 . . . . . . . . . . . . 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 ) ) ) )
177 oveq2 6285 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  (
2  x.  k )  =  ( 2  x.  x ) )
178177oveq1d 6292 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( 2  x.  k
) ^ 4 )  =  ( ( 2  x.  x ) ^
4 ) )
179177oveq1d 6292 . . . . . . . . . . . . . . . . 17  |-  ( k  =  x  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  x )  - 
1 ) )
180177, 179oveq12d 6295 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  (
( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) )
181180oveq1d 6292 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  - 
1 ) ) ^
2 ) )
182178, 181oveq12d 6295 . . . . . . . . . . . . . 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 ) ) )
183182adantl 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 ) ) )
184 elfznn 11718 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... y )  ->  x  e.  NN )
185184adantl 466 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  x  e.  NN )
186169a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  e.  NN )
187 id 22 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  e.  NN )
188186, 187nnmulcld 10584 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  NN )
189 4nn0 10815 . . . . . . . . . . . . . . . . . . 19  |-  4  e.  NN0
190189a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  4  e.  NN0 )
191188, 190nnexpcld 12305 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
) ^ 4 )  e.  NN )
192191nncnd 10553 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( 2  x.  x
) ^ 4 )  e.  CC )
193 2cnd 10609 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  e.  CC )
194 nncn 10545 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  e.  CC )
195193, 194mulcld 9614 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  CC )
196 1cnd 9610 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  1  e.  CC )
197195, 196subcld 9931 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  -  1 )  e.  CC )
198195, 197mulcld 9614 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) )  e.  CC )
199198sqcld 12282 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 )  e.  CC )
200186nnne0d 10581 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  =/=  0 )
201 nnne0 10569 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  =/=  0 )
202193, 194, 200, 201mulne0d 10202 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  =/=  0 )
203 1red 9609 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  NN  ->  1  e.  RR )
204121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  2  e.  RR )
205204, 203remulcld 9622 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  1 )  e.  RR )
206 nnre 10544 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  x  e.  RR )
207204, 206remulcld 9622 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  RR )
20843a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  (
2  x.  1 )  =  2 )
209127, 208syl5breqr 4469 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  1  <  ( 2  x.  1 ) )
210 0le2 10627 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <_  2
211210a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  0  <_  2 )
212 nnge1 10563 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  1  <_  x )
213203, 206, 204, 211, 212lemul2ad 10487 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  1 )  <_  ( 2  x.  x ) )
214203, 205, 207, 209, 213ltletrd 9740 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  NN  ->  1  <  ( 2  x.  x
) )
215203, 214gtned 9718 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  (
2  x.  x )  =/=  1 )
216195, 196, 215subne0d 9940 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  -  1 )  =/=  0 )
217195, 197, 202, 216mulne0d 10202 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) )  =/=  0 )
218 2z 10897 . . . . . . . . . . . . . . . . . 18  |-  2  e.  ZZ
219218a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  2  e.  ZZ )
220198, 217, 219expne0d 12290 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 )  =/=  0 )
221192, 199, 220divcld 10321 . . . . . . . . . . . . . . 15  |-  ( x  e.  NN  ->  (
( ( 2  x.  x ) ^ 4 )  /  ( ( ( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
222184, 221syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... y )  ->  (
( ( 2  x.  x ) ^ 4 )  /  ( ( ( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
223222adantl 466 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  ( ( ( 2  x.  x ) ^ 4 )  / 
( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
224176, 183, 185, 223fvmptd 5942 . . . . . . . . . . . 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 ) ) )
225224, 223eqeltrd 2529 . . . . . . . . . . 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 )
226 mulcl 9574 . . . . . . . . . . . 12  |-  ( ( x  e.  CC  /\  w  e.  CC )  ->  ( x  x.  w
)  e.  CC )
227226adantl 466 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  ( x  e.  CC  /\  w  e.  CC ) )  ->  ( x  x.  w )  e.  CC )
22899, 225, 227seqcl 12101 . . . . . . . . . 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 )
229175, 228mulcld 9614 . . . . . . . . 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 )
230148, 150reccld 10314 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
1  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  CC )
231229, 230, 161mul12d 9787 . . . . . . . 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 ) ) ) ) )
232175, 228mulcomd 9615 . . . . . . . . . . 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 ) ) ) )
233232oveq1d 6292 . . . . . . . . . 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 ) ) ) )
234228, 175, 161mulassd 9617 . . . . . . . . . 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 ) ) ) ) )
235167, 168, 160, 147, 174, 149divmuldivd 10362 . . . . . . . . . . . 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 ) ) ) )
236160mulid2d 9612 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  x.  ( ( 2  x.  ( y  +  1 ) ) ^ 2 ) )  =  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )
237164, 165, 167adddid 9618 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
23843a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
239238oveq2d 6293 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
240237, 239eqtrd 2482 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
241240oveq1d 6292 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
242166, 164, 167addsubassd 9951 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
24345a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  -  1 )  =  1 )
244243oveq2d 6293 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
245241, 242, 2443eqtrd 2486 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
246245oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  1 ) ) )
247168sqvald 12281 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 ) ^ 2 )  =  ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  1 ) ) )
248246, 247eqtr4d 2485 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  y )  +  1 ) ^
2 ) )
249236, 248oveq12d 6295 . . . . . . . . . . . 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 ) ) )
250 2p2e4 10654 . . . . . . . . . . . . . . . . . 18  |-  ( 2  +  2 )  =  4
25153, 53, 250mvlladdi 9837 . . . . . . . . . . . . . . . . 17  |-  2  =  ( 4  -  2 )
252251a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  =  ( 4  -  2 ) )
253252oveq2d 6293 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( 2  x.  ( y  +  1 ) ) ^
( 4  -  2 ) ) )
254120rpne0d 11265 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
255218a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  ZZ )
256189nn0zi 10890 . . . . . . . . . . . . . . . . 17  |-  4  e.  ZZ
257256a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  4  e.  ZZ )
258146, 254, 255, 257expsubd 12295 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ ( 4  -  2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( 2  x.  ( y  +  1 ) ) ^ 2 ) ) )
259253, 258eqtrd 2482 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( 2  x.  ( y  +  1 ) ) ^ 2 ) ) )
260245eqcomd 2449 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
261260oveq1d 6292 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) )  -  1 ) ^
2 ) )
262259, 261oveq12d 6295 . . . . . . . . . . . . 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 ) ) )
263146, 254, 257expclzd 12289 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 4 )  e.  CC )
264147sqcld 12282 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 )  e.  CC )
265165, 167addcld 9613 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
266170nnne0d 10581 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  =/=  0 )
267113nnne0d 10581 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
268164, 265, 266, 267mulne0d 10202 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
269146, 268, 255expne0d 12290 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =/=  0 )
270147, 149, 255expne0d 12290 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 )  =/=  0 )
271263, 160, 264, 269, 270divdiv1d 10352 . . . . . . . . . . . . 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 ) ) ) )
272146, 147sqmuld 12296 . . . . . . . . . . . . . . 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 ) ) )
273272eqcomd 2449 . . . . . . . . . . . . . 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 ) )
274273oveq2d 6293 . . . . . . . . . . . . 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 ) ) )
275262, 271, 2743eqtrd 2486 . . . . . . . . . . . 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 ) ) )
276235, 249, 2753eqtrd 2486 . . . . . . . . . . 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 ) ) )
277276oveq2d 6293 . . . . . . . . . 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 ) ) ) )
278233, 234, 2773eqtrd 2486 . . . . . . . . 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 ) ) ) )
279278oveq2d 6293 . . . . . . . 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 ) ) ) ) )
280163, 231, 2793eqtrd 2486 . . . . . . 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 ) ) ) ) )
281145, 159, 2803eqtrd 2486 . . . . . 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 ) ) ) ) )
282 eqidd 2442 . . . . . . . . . 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 ) ) ) )
283 simpr 461 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  k  =  ( y  +  1 ) )
284283oveq2d 6293 . . . . . . . . . . . 12  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( 2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
285284oveq1d 6292 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k ) ^
4 )  =  ( ( 2  x.  (
y  +  1 ) ) ^ 4 ) )
286284oveq1d 6292 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k )  - 
1 )  =  ( ( 2  x.  (
y  +  1 ) )  -  1 ) )
287284, 286oveq12d 6295 . . . . . . . . . . . 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 ) ) )
288287oveq1d 6292 . . . . . . . . . . 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 ) )
289285, 288oveq12d 6295 . . . . . . . . . 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 ) ) )
290146, 147mulcld 9614 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  CC )
291290sqcld 12282 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  e.  CC )
292146, 147, 254, 149mulne0d 10202 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =/=  0 )
293290, 292, 255expne0d 12290 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  =/=  0 )
294263, 291, 293divcld 10321 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) )  e.  CC )
295282, 289, 113, 294fvmptd 5942 . . . . . . . . 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 ) ) )
296295eqcomd 2449 . . . . . . . 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 ) ) )
297296oveq2d 6293 . . . . . . 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 ) ) ) )
298297oveq2d 6293 . . . . . 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 ) ) ) ) )
299 seqp1 12096 . . . . . . . . 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 ) ) ) )
30099, 299syl 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 ) ) ) )
301300eqcomd 2449 . . . . . . 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 ) ) )
302301oveq2d 6293 . . . . . 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 ) ) ) )
303281, 298, 3023eqtrd 2486 . . . . 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
)  -  1 ) ) ^ 2 ) ) ) ) `  y ) )  x.  ( ( k  e.  NN  |->  ( ( (