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

Theorem wallispi2lem1 27695
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 5695 . . 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 6056 . . . . . 6  |-  ( x  =  1  ->  (
2  x.  x )  =  ( 2  x.  1 ) )
32oveq1d 6063 . . . . 5  |-  ( x  =  1  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
43oveq2d 6064 . . . 4  |-  ( x  =  1  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  1 )  +  1 ) ) )
5 fveq2 5695 . . . 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 6066 . . 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 2426 . 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 5695 . . 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 6056 . . . . . 6  |-  ( x  =  y  ->  (
2  x.  x )  =  ( 2  x.  y ) )
109oveq1d 6063 . . . . 5  |-  ( x  =  y  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  y )  +  1 ) )
1110oveq2d 6064 . . . 4  |-  ( x  =  y  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  y )  +  1 ) ) )
12 fveq2 5695 . . . 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 6066 . . 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 2426 . 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 5695 . . 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 6056 . . . . . 6  |-  ( x  =  ( y  +  1 )  ->  (
2  x.  x )  =  ( 2  x.  ( y  +  1 ) ) )
1716oveq1d 6063 . . . . 5  |-  ( x  =  ( y  +  1 )  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
1817oveq2d 6064 . . . 4  |-  ( x  =  ( y  +  1 )  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
19 fveq2 5695 . . . 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 6066 . . 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 2426 . 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 5695 . . 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 6056 . . . . . 6  |-  ( x  =  N  ->  (
2  x.  x )  =  ( 2  x.  N ) )
2423oveq1d 6063 . . . . 5  |-  ( x  =  N  ->  (
( 2  x.  x
)  +  1 )  =  ( ( 2  x.  N )  +  1 ) )
2524oveq2d 6064 . . . 4  |-  ( x  =  N  ->  (
1  /  ( ( 2  x.  x )  +  1 ) )  =  ( 1  / 
( ( 2  x.  N )  +  1 ) ) )
26 fveq2 5695 . . . 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 6066 . . 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 2426 . 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 10275 . . . 4  |-  1  e.  ZZ
30 seq1 11299 . . . 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 8 . . 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 9975 . . . 4  |-  1  e.  NN
33 oveq2 6056 . . . . . . 7  |-  ( k  =  1  ->  (
2  x.  k )  =  ( 2  x.  1 ) )
3433oveq1d 6063 . . . . . . 7  |-  ( k  =  1  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  1 )  - 
1 ) )
3533, 34oveq12d 6066 . . . . . 6  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  -  1 ) ) )
3633oveq1d 6063 . . . . . . 7  |-  ( k  =  1  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  1 )  +  1 ) )
3733, 36oveq12d 6066 . . . . . 6  |-  ( k  =  1  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )
3835, 37oveq12d 6066 . . . . 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 2412 . . . . 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 6073 . . . . 5  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  e. 
_V
4138, 39, 40fvmpt 5773 . . . 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 8 . . 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 10034 . . . . . . . 8  |-  2  e.  CC
4443mulid1i 9056 . . . . . . 7  |-  ( 2  x.  1 )  =  2
4544oveq1i 6058 . . . . . . . 8  |-  ( ( 2  x.  1 )  -  1 )  =  ( 2  -  1 )
46 2m1e1 10059 . . . . . . . 8  |-  ( 2  -  1 )  =  1
4745, 46eqtri 2432 . . . . . . 7  |-  ( ( 2  x.  1 )  -  1 )  =  1
4844, 47oveq12i 6060 . . . . . 6  |-  ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  - 
1 ) )  =  ( 2  /  1
)
4944oveq1i 6058 . . . . . . . 8  |-  ( ( 2  x.  1 )  +  1 )  =  ( 2  +  1 )
50 2p1e3 10067 . . . . . . . 8  |-  ( 2  +  1 )  =  3
5149, 50eqtri 2432 . . . . . . 7  |-  ( ( 2  x.  1 )  +  1 )  =  3
5244, 51oveq12i 6060 . . . . . 6  |-  ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  +  1 ) )  =  ( 2  /  3
)
5348, 52oveq12i 6060 . . . . 5  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( ( 2  / 
1 )  x.  (
2  /  3 ) )
54 ax-1cn 9012 . . . . . 6  |-  1  e.  CC
55 3cn 10036 . . . . . 6  |-  3  e.  CC
56 ax-1ne0 9023 . . . . . 6  |-  1  =/=  0
57 3ne0 10049 . . . . . 6  |-  3  =/=  0
5843, 54, 43, 55, 56, 57divmuldivi 9738 . . . . 5  |-  ( ( 2  /  1 )  x.  ( 2  / 
3 ) )  =  ( ( 2  x.  2 )  /  (
1  x.  3 ) )
59 2t2e4 10091 . . . . . 6  |-  ( 2  x.  2 )  =  4
6055mulid2i 9057 . . . . . 6  |-  ( 1  x.  3 )  =  3
6159, 60oveq12i 6060 . . . . 5  |-  ( ( 2  x.  2 )  /  ( 1  x.  3 ) )  =  ( 4  /  3
)
6253, 58, 613eqtri 2436 . . . 4  |-  ( ( ( 2  x.  1 )  /  ( ( 2  x.  1 )  -  1 ) )  x.  ( ( 2  x.  1 )  / 
( ( 2  x.  1 )  +  1 ) ) )  =  ( 4  /  3
)
63 4cn 10038 . . . . 5  |-  4  e.  CC
64 divrec2 9659 . . . . 5  |-  ( ( 4  e.  CC  /\  3  e.  CC  /\  3  =/=  0 )  ->  (
4  /  3 )  =  ( ( 1  /  3 )  x.  4 ) )
6563, 55, 57, 64mp3an 1279 . . . 4  |-  ( 4  /  3 )  =  ( ( 1  / 
3 )  x.  4 )
6651eqcomi 2416 . . . . . 6  |-  3  =  ( ( 2  x.  1 )  +  1 )
6766oveq2i 6059 . . . . 5  |-  ( 1  /  3 )  =  ( 1  /  (
( 2  x.  1 )  +  1 ) )
68 seq1 11299 . . . . . . . 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 8 . . . . . . 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 6063 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( 2  x.  k
) ^ 4 )  =  ( ( 2  x.  1 ) ^
4 ) )
7133, 34oveq12d 6066 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) )
7271oveq1d 6063 . . . . . . . . . 10  |-  ( k  =  1  ->  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )
7370, 72oveq12d 6066 . . . . . . . . 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 2412 . . . . . . . . 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 6073 . . . . . . . . 9  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  e. 
_V
7673, 74, 75fvmpt 5773 . . . . . . . 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 8 . . . . . . 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 6058 . . . . . . . . 9  |-  ( ( 2  x.  1 ) ^ 4 )  =  ( 2 ^ 4 )
7944, 47oveq12i 6060 . . . . . . . . . . 11  |-  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) )  =  ( 2  x.  1 )
8079, 44eqtri 2432 . . . . . . . . . 10  |-  ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) )  =  2
8180oveq1i 6058 . . . . . . . . 9  |-  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  -  1 ) ) ^ 2 )  =  ( 2 ^ 2 )
8278, 81oveq12i 6060 . . . . . . . 8  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  =  ( ( 2 ^ 4 )  /  (
2 ^ 2 ) )
83 2exp4 13384 . . . . . . . . . 10  |-  ( 2 ^ 4 )  = ; 1
6
84 sq2 11440 . . . . . . . . . 10  |-  ( 2 ^ 2 )  =  4
8583, 84oveq12i 6060 . . . . . . . . 9  |-  ( ( 2 ^ 4 )  /  ( 2 ^ 2 ) )  =  (; 1 6  /  4
)
86 4t4e16 10419 . . . . . . . . . . 11  |-  ( 4  x.  4 )  = ; 1
6
8786eqcomi 2416 . . . . . . . . . 10  |- ; 1 6  =  ( 4  x.  4 )
8887oveq1i 6058 . . . . . . . . 9  |-  (; 1 6  /  4
)  =  ( ( 4  x.  4 )  /  4 )
89 0re 9055 . . . . . . . . . . 11  |-  0  e.  RR
90 4pos 10050 . . . . . . . . . . 11  |-  0  <  4
9189, 90gtneii 9149 . . . . . . . . . 10  |-  4  =/=  0
9263, 63, 91divcan3i 9724 . . . . . . . . 9  |-  ( ( 4  x.  4 )  /  4 )  =  4
9385, 88, 923eqtri 2436 . . . . . . . 8  |-  ( ( 2 ^ 4 )  /  ( 2 ^ 2 ) )  =  4
9482, 93eqtri 2432 . . . . . . 7  |-  ( ( ( 2  x.  1 ) ^ 4 )  /  ( ( ( 2  x.  1 )  x.  ( ( 2  x.  1 )  - 
1 ) ) ^
2 ) )  =  4
9569, 77, 943eqtri 2436 . . . . . 6  |-  (  seq  1 (  x.  , 
( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
4 )  /  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 ) ) ) ) ` 
1 )  =  4
9695eqcomi 2416 . . . . 5  |-  4  =  (  seq  1
(  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) ) ^ 2 ) ) ) ) `  1
)
9767, 96oveq12i 6060 . . . 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 ) )
9862, 65, 973eqtri 2436 . . 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 ) )
9931, 42, 983eqtri 2436 . 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 ) )
100 elnnuz 10486 . . . . . . 7  |-  ( y  e.  NN  <->  y  e.  ( ZZ>= `  1 )
)
101100biimpi 187 . . . . . 6  |-  ( y  e.  NN  ->  y  e.  ( ZZ>= `  1 )
)
102101adantr 452 . . . . 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 ) )
103 seqp1 11301 . . . . 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 ) ) ) )
104102, 103syl 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 ) ) ) )
105 simpr 448 . . . . 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
) ) )
106105oveq1d 6063 . . . 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 ) ) ) )
107 eqidd 2413 . . . . . . . . 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 ) ) ) ) )
108 oveq2 6056 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
109108oveq1d 6063 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
110108, 109oveq12d 6066 . . . . . . . . . . 11  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  -  1 ) ) )
111108oveq1d 6063 . . . . . . . . . . . 12  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )
112108, 111oveq12d 6066 . . . . . . . . . . 11  |-  ( k  =  ( y  +  1 )  ->  (
( 2  x.  k
)  /  ( ( 2  x.  k )  +  1 ) )  =  ( ( 2  x.  ( y  +  1 ) )  / 
( ( 2  x.  ( y  +  1 ) )  +  1 ) ) )
113110, 112oveq12d 6066 . . . . . . . . . 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 ) ) ) )
114113adantl 453 . . . . . . . . 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 ) ) ) )
115 peano2nn 9976 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  NN )
116 2rp 10581 . . . . . . . . . . . . 13  |-  2  e.  RR+
117116a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  2  e.  RR+ )
118 nnre 9971 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  RR )
119 nnnn0 10192 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  NN0 )
120119nn0ge0d 10241 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  y )
121118, 120ge0p1rpd 10638 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR+ )
122117, 121rpmulcld 10628 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR+ )
123 2re 10033 . . . . . . . . . . . . . . 15  |-  2  e.  RR
124123a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  RR )
125 1re 9054 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
126125a1i 11 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  1  e.  RR )
127118, 126readdcld 9079 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  RR )
128124, 127remulcld 9080 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  RR )
129128, 126resubcld 9429 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR )
130 1lt2 10106 . . . . . . . . . . . . . . 15  |-  1  <  2
131130a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <  2 )
132 nnrp 10585 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  y  e.  RR+ )
133126, 132ltaddrp2d 10642 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  1  <  ( y  +  1 ) )
134124, 127, 131, 133mulgt1d 9911 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  1  <  ( 2  x.  (
y  +  1 ) ) )
135126, 128posdifd 9577 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  <  ( 2  x.  ( y  +  1 ) )  <->  0  <  ( ( 2  x.  (
y  +  1 ) )  -  1 ) ) )
136134, 135mpbid 202 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  0  <  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )
137129, 136elrpd 10610 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  RR+ )
138122, 137rpdivcld 10629 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  RR+ )
139117rpge0d 10616 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  2 )
140 0le1 9515 . . . . . . . . . . . . . . 15  |-  0  <_  1
141140a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  0  <_  1 )
142118, 126, 120, 141addge0d 9566 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  0  <_  ( y  +  1 ) )
143124, 127, 139, 142mulge0d 9567 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  0  <_  ( 2  x.  (
y  +  1 ) ) )
144128, 143ge0p1rpd 10638 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  RR+ )
145122, 144rpdivcld 10629 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  RR+ )
146138, 145rpmulcld 10628 . . . . . . . . 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+ )
147107, 114, 115, 146fvmptd 5777 . . . . . . . 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 ) ) ) )
148147oveq2d 6064 . . . . . . 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 ) ) ) ) )
149128recnd 9078 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  e.  CC )
150129recnd 9078 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  e.  CC )
151144rpcnd 10614 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  e.  CC )
152136gt0ne0d 9555 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =/=  0 )
153144rpne0d 10617 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  +  1 )  =/=  0 )
154149, 150, 149, 151, 152, 153divmuldivd 9795 . . . . . . . . 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 ) ) ) )
155149, 149mulcld 9072 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  e.  CC )
156155, 150, 151, 152, 153divdiv1d 9785 . . . . . . . . 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 ) ) ) )
157149sqvald 11483 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( 2  x.  ( y  +  1 ) )  x.  ( 2  x.  (
y  +  1 ) ) ) )
158157eqcomd 2417 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( 2  x.  ( y  +  1 ) ) )  =  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )
159158oveq1d 6063 . . . . . . . . . 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 ) ) )
160159oveq1d 6063 . . . . . . . . 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 ) ) )
161154, 156, 1603eqtr2d 2450 . . . . . . . 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 ) ) )
162161oveq2d 6064 . . . . . . 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 ) ) ) )
163149sqcld 11484 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  e.  CC )
164163, 150, 152divcld 9754 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 2 )  /  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  CC )
165164, 151, 153divrec2d 9758 . . . . . . . . 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 ) ) ) )
166165oveq2d 6064 . . . . . . . 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 ) ) ) ) )
16743a1i 11 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  2  e.  CC )
168 nncn 9972 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  y  e.  CC )
169167, 168mulcld 9072 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  CC )
17054a1i 11 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  1  e.  CC )
171169, 170addcld 9071 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  CC )
172 2nn 10097 . . . . . . . . . . . . . . 15  |-  2  e.  NN
173172a1i 11 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  2  e.  NN )
174 id 20 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  y  e.  NN )
175173, 174nnmulcld 10011 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
2  x.  y )  e.  NN )
176175peano2nnd 9981 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  e.  NN )
177176nnne0d 10008 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =/=  0 )
178171, 177reccld 9747 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
1  /  ( ( 2  x.  y )  +  1 ) )  e.  CC )
179 eqidd 2413 . . . . . . . . . . . . 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 ) ) ) )
180 oveq2 6056 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  (
2  x.  k )  =  ( 2  x.  x ) )
181180oveq1d 6063 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( 2  x.  k
) ^ 4 )  =  ( ( 2  x.  x ) ^
4 ) )
182180oveq1d 6063 . . . . . . . . . . . . . . . . 17  |-  ( k  =  x  ->  (
( 2  x.  k
)  -  1 )  =  ( ( 2  x.  x )  - 
1 ) )
183180, 182oveq12d 6066 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  (
( 2  x.  k
)  x.  ( ( 2  x.  k )  -  1 ) )  =  ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) )
184183oveq1d 6063 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( ( 2  x.  k )  x.  (
( 2  x.  k
)  -  1 ) ) ^ 2 )  =  ( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  - 
1 ) ) ^
2 ) )
185181, 184oveq12d 6066 . . . . . . . . . . . . . 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 ) ) )
186185adantl 453 . . . . . . . . . . . . 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 ) ) )
187 elfznn 11044 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... y )  ->  x  e.  NN )
188187adantl 453 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  x  e.  NN )
189172a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  e.  NN )
190 id 20 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  e.  NN )
191189, 190nnmulcld 10011 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  NN )
192 4nn0 10204 . . . . . . . . . . . . . . . . . . 19  |-  4  e.  NN0
193192a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  4  e.  NN0 )
194191, 193nnexpcld 11507 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
) ^ 4 )  e.  NN )
195194nncnd 9980 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( 2  x.  x
) ^ 4 )  e.  CC )
19643a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  e.  CC )
197 nncn 9972 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  e.  CC )
198196, 197mulcld 9072 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  CC )
19954a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  1  e.  CC )
200198, 199subcld 9375 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  -  1 )  e.  CC )
201198, 200mulcld 9072 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) )  e.  CC )
202201sqcld 11484 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 )  e.  CC )
203189nnne0d 10008 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  2  =/=  0 )
204 nnne0 9996 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  x  =/=  0 )
205196, 197, 203, 204mulne0d 9638 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
2  x.  x )  =/=  0 )
206125a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  NN  ->  1  e.  RR )
207123a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  2  e.  RR )
208207, 206remulcld 9080 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  1 )  e.  RR )
209 nnre 9971 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  x  e.  RR )
210207, 209remulcld 9080 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  x )  e.  RR )
21144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  (
2  x.  1 )  =  2 )
212130, 211syl5breqr 4216 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  1  <  ( 2  x.  1 ) )
213 2nn0 10202 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  NN0
214213nn0ge0i 10213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <_  2
215214a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  0  <_  2 )
216 nnge1 9990 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  NN  ->  1  <_  x )
217206, 209, 207, 215, 216lemul2ad 9915 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  NN  ->  (
2  x.  1 )  <_  ( 2  x.  x ) )
218206, 208, 210, 212, 217ltletrd 9194 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  NN  ->  1  <  ( 2  x.  x
) )
219206, 218gtned 9172 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  NN  ->  (
2  x.  x )  =/=  1 )
220198, 199, 219subne0d 9384 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  -  1 )  =/=  0 )
221198, 200, 205, 220mulne0d 9638 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  (
( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) )  =/=  0 )
222 2z 10276 . . . . . . . . . . . . . . . . . 18  |-  2  e.  ZZ
223222a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  NN  ->  2  e.  ZZ )
224201, 221, 223expne0d 11492 . . . . . . . . . . . . . . . 16  |-  ( x  e.  NN  ->  (
( ( 2  x.  x )  x.  (
( 2  x.  x
)  -  1 ) ) ^ 2 )  =/=  0 )
225195, 202, 224divcld 9754 . . . . . . . . . . . . . . 15  |-  ( x  e.  NN  ->  (
( ( 2  x.  x ) ^ 4 )  /  ( ( ( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
226187, 225syl 16 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... y )  ->  (
( ( 2  x.  x ) ^ 4 )  /  ( ( ( 2  x.  x
)  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
227226adantl 453 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  x  e.  ( 1 ... y ) )  ->  ( ( ( 2  x.  x ) ^ 4 )  / 
( ( ( 2  x.  x )  x.  ( ( 2  x.  x )  -  1 ) ) ^ 2 ) )  e.  CC )
228179, 186, 188, 227fvmptd 5777 . . . . . . . . . . . 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 ) ) )
229228, 227eqeltrd 2486 . . . . . . . . . . 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 )
230 mulcl 9038 . . . . . . . . . . . 12  |-  ( ( x  e.  CC  /\  w  e.  CC )  ->  ( x  x.  w
)  e.  CC )
231230adantl 453 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  ( x  e.  CC  /\  w  e.  CC ) )  ->  ( x  x.  w )  e.  CC )
232101, 229, 231seqcl 11306 . . . . . . . . . 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 )
233178, 232mulcld 9072 . . . . . . . . 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 )
234151, 153reccld 9747 . . . . . . . . 9  |-  ( y  e.  NN  ->  (
1  /  ( ( 2  x.  ( y  +  1 ) )  +  1 ) )  e.  CC )
235233, 234, 164mul12d 9239 . . . . . . . 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 ) ) ) ) )
236178, 232mulcomd 9073 . . . . . . . . . . 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 ) ) ) )
237236oveq1d 6063 . . . . . . . . . 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 ) ) ) )
238232, 178, 164mulassd 9075 . . . . . . . . . 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 ) ) ) ) )
239170, 171, 163, 150, 177, 152divmuldivd 9795 . . . . . . . . . . . 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 ) ) ) )
240163mulid2d 9070 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
1  x.  ( ( 2  x.  ( y  +  1 ) ) ^ 2 ) )  =  ( ( 2  x.  ( y  +  1 ) ) ^
2 ) )
241167, 168, 170adddid 9076 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  ( 2  x.  1 ) ) )
24244a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN  ->  (
2  x.  1 )  =  2 )
243242oveq2d 6064 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  x.  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
244241, 243eqtrd 2444 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =  ( ( 2  x.  y )  +  2 ) )
245244oveq1d 6063 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( ( 2  x.  y )  +  2 )  - 
1 ) )
246169, 167, 170addsubassd 9395 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  2 )  -  1 )  =  ( ( 2  x.  y )  +  ( 2  -  1 ) ) )
24746a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  ->  (
2  -  1 )  =  1 )
248247oveq2d 6064 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  ( 2  -  1 ) )  =  ( ( 2  x.  y )  +  1 ) )
249245, 246, 2483eqtrd 2448 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  -  1 )  =  ( ( 2  x.  y )  +  1 ) )
250249oveq2d 6064 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  1 ) ) )
251171sqvald 11483 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 ) ^ 2 )  =  ( ( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  y )  +  1 ) ) )
252250, 251eqtr4d 2447 . . . . . . . . . . . . 13  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =  ( ( ( 2  x.  y )  +  1 ) ^
2 ) )
253240, 252oveq12d 6066 . . . . . . . . . . . 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 ) ) )
254 2p2e4 10062 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  +  2 )  =  4
25563, 43, 43, 254subaddrii 9353 . . . . . . . . . . . . . . . . . 18  |-  ( 4  -  2 )  =  2
256255eqcomi 2416 . . . . . . . . . . . . . . . . 17  |-  2  =  ( 4  -  2 )
257256a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  =  ( 4  -  2 ) )
258257oveq2d 6064 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( 2  x.  ( y  +  1 ) ) ^
( 4  -  2 ) ) )
259122rpne0d 10617 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
260222a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  e.  ZZ )
261192nn0zi 10270 . . . . . . . . . . . . . . . . 17  |-  4  e.  ZZ
262261a1i 11 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  4  e.  ZZ )
263149, 259, 260, 262expsubd 11497 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ ( 4  -  2 ) )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( 2  x.  ( y  +  1 ) ) ^ 2 ) ) )
264258, 263eqtrd 2444 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) ) ^ 4 )  / 
( ( 2  x.  ( y  +  1 ) ) ^ 2 ) ) )
265249eqcomd 2417 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
( 2  x.  y
)  +  1 )  =  ( ( 2  x.  ( y  +  1 ) )  - 
1 ) )
266265oveq1d 6063 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  y )  +  1 ) ^ 2 )  =  ( ( ( 2  x.  ( y  +  1 ) )  -  1 ) ^
2 ) )
267264, 266oveq12d 6066 . . . . . . . . . . . . 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 ) ) )
268149, 259, 262expclzd 11491 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 4 )  e.  CC )
269150sqcld 11484 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 )  e.  CC )
270168, 170addcld 9071 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  e.  CC )
271173nnne0d 10008 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  2  =/=  0 )
272115nnne0d 10008 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN  ->  (
y  +  1 )  =/=  0 )
273167, 270, 271, 272mulne0d 9638 . . . . . . . . . . . . . . 15  |-  ( y  e.  NN  ->  (
2  x.  ( y  +  1 ) )  =/=  0 )
274149, 273, 260expne0d 11492 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) ) ^ 2 )  =/=  0 )
275150, 152, 260expne0d 11492 . . . . . . . . . . . . . 14  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  -  1 ) ^ 2 )  =/=  0 )
276268, 163, 269, 274, 275divdiv1d 9785 . . . . . . . . . . . . 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 ) ) ) )
277149, 150sqmuld 11498 . . . . . . . . . . . . . . 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 ) ) )
278277eqcomd 2417 . . . . . . . . . . . . . 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 ) )
279278oveq2d 6064 . . . . . . . . . . . . 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 ) ) )
280267, 276, 2793eqtrd 2448 . . . . . . . . . . . 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 ) ) )
281239, 253, 2803eqtrd 2448 . . . . . . . . . . 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 ) ) )
282281oveq2d 6064 . . . . . . . . . 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 ) ) ) )
283237, 238, 2823eqtrd 2448 . . . . . . . . 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 ) ) ) )
284283oveq2d 6064 . . . . . . . 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 ) ) ) ) )
285166, 235, 2843eqtrd 2448 . . . . . . 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 ) ) ) ) )
286148, 162, 2853eqtrd 2448 . . . . . 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 ) ) ) ) )
287 eqidd 2413 . . . . . . . . . 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 ) ) ) )
288 simpr 448 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  k  =  ( y  +  1 ) )
289288oveq2d 6064 . . . . . . . . . . . 12  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( 2  x.  k )  =  ( 2  x.  ( y  +  1 ) ) )
290289oveq1d 6063 . . . . . . . . . . 11  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k ) ^
4 )  =  ( ( 2  x.  (
y  +  1 ) ) ^ 4 ) )
291289oveq1d 6063 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN  /\  k  =  ( y  +  1 ) )  ->  ( ( 2  x.  k )  - 
1 )  =  ( ( 2  x.  (
y  +  1 ) )  -  1 ) )
292289, 291oveq12d 6066 . . . . . . . . . . . 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 ) ) )
293292oveq1d 6063 . . . . . . . . . . 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 ) )
294290, 293oveq12d 6066 . . . . . . . . . 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 ) ) )
295149, 150mulcld 9072 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  e.  CC )
296295sqcld 11484 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  e.  CC )
297149, 150, 259, 152mulne0d 9638 . . . . . . . . . . . 12  |-  ( y  e.  NN  ->  (
( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) )  =/=  0 )
298295, 297, 260expne0d 11492 . . . . . . . . . . 11  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) )  x.  (
( 2  x.  (
y  +  1 ) )  -  1 ) ) ^ 2 )  =/=  0 )
299268, 296, 298divcld 9754 . . . . . . . . . 10  |-  ( y  e.  NN  ->  (
( ( 2  x.  ( y  +  1 ) ) ^ 4 )  /  ( ( ( 2  x.  (
y  +  1 ) )  x.  ( ( 2  x.  ( y  +  1 ) )  -  1 ) ) ^ 2 ) )  e.  CC )
300287, 294, 115, 299fvmptd 5777 . . . . . . . . 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 ) ) )
301300eqcomd 2417 . . . . . . . 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 ) ) )
302301oveq2d 6064 . . . . . . 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 ) ) ) )
303302oveq2d 6064 . . . . . 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 ) ) ) ) )
304 seqp1 11301 . . . . . . . . 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 ) ) ) )
305101, 304syl 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 ) ) ) )
306305eqcomd 2417 . . . . . . 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 ) ) )
307306oveq2d 6064 . . . . . 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 ) ) ) )
308286, 303, 3073eqtrd 2448 . . . . 5  |-  ( y  e.  NN  ->  (
( ( 1  / 
( ( 2  x.  y )  +  1 ) )  x.  (  seq  1 (  x.  , 
(