Metamath Proof Explorer

Theorem wallispi2lem1

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)

Ref Expression
Assertion 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

Step Hyp Ref Expression
1 fveq2 
 |-  ( 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 
 |-  ( x = 1 -> ( 2 x. x ) = ( 2 x. 1 ) )
3 2 oveq1d 
 |-  ( x = 1 -> ( ( 2 x. x ) + 1 ) = ( ( 2 x. 1 ) + 1 ) )
4 3 oveq2d 
 |-  ( x = 1 -> ( 1 / ( ( 2 x. x ) + 1 ) ) = ( 1 / ( ( 2 x. 1 ) + 1 ) ) )
5 fveq2 
 |-  ( 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 ) )
6 4 5 oveq12d 
 |-  ( 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 ) ) )
7 1 6 eqeq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
10 9 oveq1d 
 |-  ( x = y -> ( ( 2 x. x ) + 1 ) = ( ( 2 x. y ) + 1 ) )
11 10 oveq2d 
 |-  ( x = y -> ( 1 / ( ( 2 x. x ) + 1 ) ) = ( 1 / ( ( 2 x. y ) + 1 ) ) )
12 fveq2 
 |-  ( 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 ) )
13 11 12 oveq12d 
 |-  ( 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 ) ) )
14 8 13 eqeq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( x = ( y + 1 ) -> ( 2 x. x ) = ( 2 x. ( y + 1 ) ) )
17 16 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( 2 x. x ) + 1 ) = ( ( 2 x. ( y + 1 ) ) + 1 ) )
18 17 oveq2d 
 |-  ( x = ( y + 1 ) -> ( 1 / ( ( 2 x. x ) + 1 ) ) = ( 1 / ( ( 2 x. ( y + 1 ) ) + 1 ) ) )
19 fveq2 
 |-  ( 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 ) ) )
20 18 19 oveq12d 
 |-  ( 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 ) ) ) )
21 15 20 eqeq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( x = N -> ( 2 x. x ) = ( 2 x. N ) )
24 23 oveq1d 
 |-  ( x = N -> ( ( 2 x. x ) + 1 ) = ( ( 2 x. N ) + 1 ) )
25 24 oveq2d 
 |-  ( x = N -> ( 1 / ( ( 2 x. x ) + 1 ) ) = ( 1 / ( ( 2 x. N ) + 1 ) ) )
26 fveq2 
 |-  ( 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 ) )
27 25 26 oveq12d 
 |-  ( 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 ) ) )
28 22 27 eqeq12d 
 |-  ( 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 
 |-  1 e. ZZ
30 seq1 
 |-  ( 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 ) )
31 29 30 ax-mp 
 |-  ( 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 
 |-  1 e. NN
33 oveq2 
 |-  ( k = 1 -> ( 2 x. k ) = ( 2 x. 1 ) )
34 33 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. 1 ) - 1 ) )
35 33 34 oveq12d 
 |-  ( k = 1 -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. 1 ) / ( ( 2 x. 1 ) - 1 ) ) )
36 33 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. 1 ) + 1 ) )
37 33 36 oveq12d 
 |-  ( k = 1 -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) = ( ( 2 x. 1 ) / ( ( 2 x. 1 ) + 1 ) ) )
38 35 37 oveq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( ( 2 x. 1 ) / ( ( 2 x. 1 ) - 1 ) ) x. ( ( 2 x. 1 ) / ( ( 2 x. 1 ) + 1 ) ) ) e. _V
41 38 39 40 fvmpt 
 |-  ( 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 ) ) ) )
42 32 41 ax-mp 
 |-  ( ( 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 
 |-  ( 2 x. 1 ) = 2
44 43 oveq1i 
 |-  ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 )
45 2m1e1 
 |-  ( 2 - 1 ) = 1
46 44 45 eqtri 
 |-  ( ( 2 x. 1 ) - 1 ) = 1
47 43 46 oveq12i 
 |-  ( ( 2 x. 1 ) / ( ( 2 x. 1 ) - 1 ) ) = ( 2 / 1 )
48 43 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
49 2p1e3 
 |-  ( 2 + 1 ) = 3
50 48 49 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
51 43 50 oveq12i 
 |-  ( ( 2 x. 1 ) / ( ( 2 x. 1 ) + 1 ) ) = ( 2 / 3 )
52 47 51 oveq12i 
 |-  ( ( ( 2 x. 1 ) / ( ( 2 x. 1 ) - 1 ) ) x. ( ( 2 x. 1 ) / ( ( 2 x. 1 ) + 1 ) ) ) = ( ( 2 / 1 ) x. ( 2 / 3 ) )
53 2cn 
 |-  2 e. CC
54 ax-1cn 
 |-  1 e. CC
55 3cn 
 |-  3 e. CC
56 ax-1ne0 
 |-  1 =/= 0
57 3ne0 
 |-  3 =/= 0
58 53 54 53 55 56 57 divmuldivi 
 |-  ( ( 2 / 1 ) x. ( 2 / 3 ) ) = ( ( 2 x. 2 ) / ( 1 x. 3 ) )
59 2t2e4 
 |-  ( 2 x. 2 ) = 4
60 55 mulid2i 
 |-  ( 1 x. 3 ) = 3
61 59 60 oveq12i 
 |-  ( ( 2 x. 2 ) / ( 1 x. 3 ) ) = ( 4 / 3 )
62 52 58 61 3eqtri 
 |-  ( ( ( 2 x. 1 ) / ( ( 2 x. 1 ) - 1 ) ) x. ( ( 2 x. 1 ) / ( ( 2 x. 1 ) + 1 ) ) ) = ( 4 / 3 )
63 4cn 
 |-  4 e. CC
64 divrec2 
 |-  ( ( 4 e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 4 / 3 ) = ( ( 1 / 3 ) x. 4 ) )
65 63 55 57 64 mp3an 
 |-  ( 4 / 3 ) = ( ( 1 / 3 ) x. 4 )
66 50 eqcomi 
 |-  3 = ( ( 2 x. 1 ) + 1 )
67 66 oveq2i 
 |-  ( 1 / 3 ) = ( 1 / ( ( 2 x. 1 ) + 1 ) )
68 seq1 
 |-  ( 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 ) )
69 29 68 ax-mp 
 |-  ( 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 )
70 33 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. 1 ) ^ 4 ) )
71 33 34 oveq12d 
 |-  ( k = 1 -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) )
72 71 oveq1d 
 |-  ( k = 1 -> ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) = ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) )
73 70 72 oveq12d 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( ( 2 x. 1 ) ^ 4 ) / ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) ) e. _V
76 73 74 75 fvmpt 
 |-  ( 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 ) ) )
77 32 76 ax-mp 
 |-  ( ( 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 ) )
78 43 oveq1i 
 |-  ( ( 2 x. 1 ) ^ 4 ) = ( 2 ^ 4 )
79 43 46 oveq12i 
 |-  ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) = ( 2 x. 1 )
80 79 43 eqtri 
 |-  ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) = 2
81 80 oveq1i 
 |-  ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) = ( 2 ^ 2 )
82 78 81 oveq12i 
 |-  ( ( ( 2 x. 1 ) ^ 4 ) / ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) ) = ( ( 2 ^ 4 ) / ( 2 ^ 2 ) )
83 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
84 sq2 
 |-  ( 2 ^ 2 ) = 4
85 83 84 oveq12i 
 |-  ( ( 2 ^ 4 ) / ( 2 ^ 2 ) ) = ( ; 1 6 / 4 )
86 4t4e16 
 |-  ( 4 x. 4 ) = ; 1 6
87 86 eqcomi 
 |-  ; 1 6 = ( 4 x. 4 )
88 87 oveq1i 
 |-  ( ; 1 6 / 4 ) = ( ( 4 x. 4 ) / 4 )
89 4ne0 
 |-  4 =/= 0
90 63 63 89 divcan3i 
 |-  ( ( 4 x. 4 ) / 4 ) = 4
91 85 88 90 3eqtri 
 |-  ( ( 2 ^ 4 ) / ( 2 ^ 2 ) ) = 4
92 82 91 eqtri 
 |-  ( ( ( 2 x. 1 ) ^ 4 ) / ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) ) = 4
93 69 77 92 3eqtri 
 |-  ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` 1 ) = 4
94 93 eqcomi 
 |-  4 = ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` 1 )
95 67 94 oveq12i 
 |-  ( ( 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 ) )
96 62 65 95 3eqtri 
 |-  ( ( ( 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 ) )
97 31 42 96 3eqtri 
 |-  ( 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 
 |-  ( y e. NN <-> y e. ( ZZ>= ` 1 ) )
99 98 biimpi 
 |-  ( y e. NN -> y e. ( ZZ>= ` 1 ) )
100 99 adantr 
 |-  ( ( 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 
 |-  ( 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 ) ) ) )
102 100 101 syl 
 |-  ( ( 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 
 |-  ( ( 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 ) ) )
104 103 oveq1d 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( k = ( y + 1 ) -> ( 2 x. k ) = ( 2 x. ( y + 1 ) ) )
107 106 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. ( y + 1 ) ) - 1 ) )
108 106 107 oveq12d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) )
109 106 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. ( y + 1 ) ) + 1 ) )
110 106 109 oveq12d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) )
111 108 110 oveq12d 
 |-  ( 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 ) ) ) )
112 111 adantl 
 |-  ( ( 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 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
114 2rp 
 |-  2 e. RR+
115 114 a1i 
 |-  ( y e. NN -> 2 e. RR+ )
116 nnre 
 |-  ( y e. NN -> y e. RR )
117 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
118 117 nn0ge0d 
 |-  ( y e. NN -> 0 <_ y )
119 116 118 ge0p1rpd 
 |-  ( y e. NN -> ( y + 1 ) e. RR+ )
120 115 119 rpmulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. RR+ )
121 2re 
 |-  2 e. RR
122 121 a1i 
 |-  ( y e. NN -> 2 e. RR )
123 1red 
 |-  ( y e. NN -> 1 e. RR )
124 116 123 readdcld 
 |-  ( y e. NN -> ( y + 1 ) e. RR )
125 122 124 remulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. RR )
126 125 123 resubcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) e. RR )
127 1lt2 
 |-  1 < 2
128 127 a1i 
 |-  ( y e. NN -> 1 < 2 )
129 nnrp 
 |-  ( y e. NN -> y e. RR+ )
130 123 129 ltaddrp2d 
 |-  ( y e. NN -> 1 < ( y + 1 ) )
131 122 124 128 130 mulgt1d 
 |-  ( y e. NN -> 1 < ( 2 x. ( y + 1 ) ) )
132 123 125 posdifd 
 |-  ( y e. NN -> ( 1 < ( 2 x. ( y + 1 ) ) <-> 0 < ( ( 2 x. ( y + 1 ) ) - 1 ) ) )
133 131 132 mpbid 
 |-  ( y e. NN -> 0 < ( ( 2 x. ( y + 1 ) ) - 1 ) )
134 126 133 elrpd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) e. RR+ )
135 120 134 rpdivcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) e. RR+ )
136 115 rpge0d 
 |-  ( y e. NN -> 0 <_ 2 )
137 0le1 
 |-  0 <_ 1
138 137 a1i 
 |-  ( y e. NN -> 0 <_ 1 )
139 116 123 118 138 addge0d 
 |-  ( y e. NN -> 0 <_ ( y + 1 ) )
140 122 124 136 139 mulge0d 
 |-  ( y e. NN -> 0 <_ ( 2 x. ( y + 1 ) ) )
141 125 140 ge0p1rpd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) e. RR+ )
142 120 141 rpdivcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) e. RR+ )
143 135 142 rpmulcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) e. RR+ )
144 105 112 113 143 fvmptd 
 |-  ( 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 ) ) ) )
145 144 oveq2d 
 |-  ( 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 ) ) ) ) )
146 125 recnd 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. CC )
147 126 recnd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) e. CC )
148 141 rpcnd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) e. CC )
149 133 gt0ne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) =/= 0 )
150 141 rpne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) =/= 0 )
151 146 147 146 148 149 150 divmuldivd 
 |-  ( 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 ) ) ) )
152 146 146 mulcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) e. CC )
153 152 147 148 149 150 divdiv1d 
 |-  ( 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 ) ) ) )
154 146 sqvald 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 2 ) = ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) )
155 154 eqcomd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) = ( ( 2 x. ( y + 1 ) ) ^ 2 ) )
156 155 oveq1d 
 |-  ( 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 ) ) )
157 156 oveq1d 
 |-  ( 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 ) ) )
158 151 153 157 3eqtr2d 
 |-  ( 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 ) ) )
159 158 oveq2d 
 |-  ( 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 ) ) ) )
160 146 sqcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 2 ) e. CC )
161 160 147 149 divcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) ^ 2 ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) e. CC )
162 161 148 150 divrec2d 
 |-  ( 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 ) ) ) )
163 162 oveq2d 
 |-  ( 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 
 |-  ( y e. NN -> 2 e. CC )
165 nncn 
 |-  ( y e. NN -> y e. CC )
166 164 165 mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. CC )
167 1cnd 
 |-  ( y e. NN -> 1 e. CC )
168 166 167 addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. CC )
169 2nn 
 |-  2 e. NN
170 169 a1i 
 |-  ( y e. NN -> 2 e. NN )
171 id 
 |-  ( y e. NN -> y e. NN )
172 170 171 nnmulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. NN )
173 172 peano2nnd 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. NN )
174 173 nnne0d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) =/= 0 )
175 168 174 reccld 
 |-  ( y e. NN -> ( 1 / ( ( 2 x. y ) + 1 ) ) e. CC )
176 eqidd 
 |-  ( ( 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 
 |-  ( k = x -> ( 2 x. k ) = ( 2 x. x ) )
178 177 oveq1d 
 |-  ( k = x -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. x ) ^ 4 ) )
179 177 oveq1d 
 |-  ( k = x -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. x ) - 1 ) )
180 177 179 oveq12d 
 |-  ( k = x -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) )
181 180 oveq1d 
 |-  ( k = x -> ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) = ( ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) ^ 2 ) )
182 178 181 oveq12d 
 |-  ( 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 ) ) )
183 182 adantl 
 |-  ( ( ( 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 
 |-  ( x e. ( 1 ... y ) -> x e. NN )
185 184 adantl 
 |-  ( ( y e. NN /\ x e. ( 1 ... y ) ) -> x e. NN )
186 169 a1i 
 |-  ( x e. NN -> 2 e. NN )
187 id 
 |-  ( x e. NN -> x e. NN )
188 186 187 nnmulcld 
 |-  ( x e. NN -> ( 2 x. x ) e. NN )
189 4nn0 
 |-  4 e. NN0
190 189 a1i 
 |-  ( x e. NN -> 4 e. NN0 )
191 188 190 nnexpcld 
 |-  ( x e. NN -> ( ( 2 x. x ) ^ 4 ) e. NN )
192 191 nncnd 
 |-  ( x e. NN -> ( ( 2 x. x ) ^ 4 ) e. CC )
193 2cnd 
 |-  ( x e. NN -> 2 e. CC )
194 nncn 
 |-  ( x e. NN -> x e. CC )
195 193 194 mulcld 
 |-  ( x e. NN -> ( 2 x. x ) e. CC )
196 1cnd 
 |-  ( x e. NN -> 1 e. CC )
197 195 196 subcld 
 |-  ( x e. NN -> ( ( 2 x. x ) - 1 ) e. CC )
198 195 197 mulcld 
 |-  ( x e. NN -> ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) e. CC )
199 198 sqcld 
 |-  ( x e. NN -> ( ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) ^ 2 ) e. CC )
200 186 nnne0d 
 |-  ( x e. NN -> 2 =/= 0 )
201 nnne0 
 |-  ( x e. NN -> x =/= 0 )
202 193 194 200 201 mulne0d 
 |-  ( x e. NN -> ( 2 x. x ) =/= 0 )
203 1red 
 |-  ( x e. NN -> 1 e. RR )
204 121 a1i 
 |-  ( x e. NN -> 2 e. RR )
205 204 203 remulcld 
 |-  ( x e. NN -> ( 2 x. 1 ) e. RR )
206 nnre 
 |-  ( x e. NN -> x e. RR )
207 204 206 remulcld 
 |-  ( x e. NN -> ( 2 x. x ) e. RR )
208 43 a1i 
 |-  ( x e. NN -> ( 2 x. 1 ) = 2 )
209 127 208 breqtrrid 
 |-  ( x e. NN -> 1 < ( 2 x. 1 ) )
210 0le2 
 |-  0 <_ 2
211 210 a1i 
 |-  ( x e. NN -> 0 <_ 2 )
212 nnge1 
 |-  ( x e. NN -> 1 <_ x )
213 203 206 204 211 212 lemul2ad 
 |-  ( x e. NN -> ( 2 x. 1 ) <_ ( 2 x. x ) )
214 203 205 207 209 213 ltletrd 
 |-  ( x e. NN -> 1 < ( 2 x. x ) )
215 203 214 gtned 
 |-  ( x e. NN -> ( 2 x. x ) =/= 1 )
216 195 196 215 subne0d 
 |-  ( x e. NN -> ( ( 2 x. x ) - 1 ) =/= 0 )
217 195 197 202 216 mulne0d 
 |-  ( x e. NN -> ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) =/= 0 )
218 2z 
 |-  2 e. ZZ
219 218 a1i 
 |-  ( x e. NN -> 2 e. ZZ )
220 198 217 219 expne0d 
 |-  ( x e. NN -> ( ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) ^ 2 ) =/= 0 )
221 192 199 220 divcld 
 |-  ( x e. NN -> ( ( ( 2 x. x ) ^ 4 ) / ( ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) ^ 2 ) ) e. CC )
222 184 221 syl 
 |-  ( x e. ( 1 ... y ) -> ( ( ( 2 x. x ) ^ 4 ) / ( ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) ^ 2 ) ) e. CC )
223 222 adantl 
 |-  ( ( y e. NN /\ x e. ( 1 ... y ) ) -> ( ( ( 2 x. x ) ^ 4 ) / ( ( ( 2 x. x ) x. ( ( 2 x. x ) - 1 ) ) ^ 2 ) ) e. CC )
224 176 183 185 223 fvmptd 
 |-  ( ( 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 ) ) )
225 224 223 eqeltrd 
 |-  ( ( 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 
 |-  ( ( x e. CC /\ w e. CC ) -> ( x x. w ) e. CC )
227 226 adantl 
 |-  ( ( y e. NN /\ ( x e. CC /\ w e. CC ) ) -> ( x x. w ) e. CC )
228 99 225 227 seqcl 
 |-  ( 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 )
229 175 228 mulcld 
 |-  ( 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 )
230 148 150 reccld 
 |-  ( y e. NN -> ( 1 / ( ( 2 x. ( y + 1 ) ) + 1 ) ) e. CC )
231 229 230 161 mul12d 
 |-  ( 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 ) ) ) ) )
232 175 228 mulcomd 
 |-  ( 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 ) ) ) )
233 232 oveq1d 
 |-  ( 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 ) ) ) )
234 228 175 161 mulassd 
 |-  ( 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 ) ) ) ) )
235 167 168 160 147 174 149 divmuldivd 
 |-  ( 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 ) ) ) )
236 160 mulid2d 
 |-  ( y e. NN -> ( 1 x. ( ( 2 x. ( y + 1 ) ) ^ 2 ) ) = ( ( 2 x. ( y + 1 ) ) ^ 2 ) )
237 164 165 167 adddid 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
238 43 a1i 
 |-  ( y e. NN -> ( 2 x. 1 ) = 2 )
239 238 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 2 x. 1 ) ) = ( ( 2 x. y ) + 2 ) )
240 237 239 eqtrd 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + 2 ) )
241 240 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( ( 2 x. y ) + 2 ) - 1 ) )
242 166 164 167 addsubassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 2 ) - 1 ) = ( ( 2 x. y ) + ( 2 - 1 ) ) )
243 45 a1i 
 |-  ( y e. NN -> ( 2 - 1 ) = 1 )
244 243 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 2 - 1 ) ) = ( ( 2 x. y ) + 1 ) )
245 241 242 244 3eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( 2 x. y ) + 1 ) )
246 245 oveq2d 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) = ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 1 ) ) )
247 168 sqvald 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) ^ 2 ) = ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 1 ) ) )
248 246 247 eqtr4d 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) = ( ( ( 2 x. y ) + 1 ) ^ 2 ) )
249 236 248 oveq12d 
 |-  ( 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 
 |-  ( 2 + 2 ) = 4
251 53 53 250 mvlladdi 
 |-  2 = ( 4 - 2 )
252 251 a1i 
 |-  ( y e. NN -> 2 = ( 4 - 2 ) )
253 252 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 2 ) = ( ( 2 x. ( y + 1 ) ) ^ ( 4 - 2 ) ) )
254 120 rpne0d 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 0 )
255 218 a1i 
 |-  ( y e. NN -> 2 e. ZZ )
256 4z 
 |-  4 e. ZZ
257 256 a1i 
 |-  ( y e. NN -> 4 e. ZZ )
258 146 254 255 257 expsubd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ ( 4 - 2 ) ) = ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( 2 x. ( y + 1 ) ) ^ 2 ) ) )
259 253 258 eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 2 ) = ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( 2 x. ( y + 1 ) ) ^ 2 ) ) )
260 245 eqcomd 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) = ( ( 2 x. ( y + 1 ) ) - 1 ) )
261 260 oveq1d 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) ^ 2 ) = ( ( ( 2 x. ( y + 1 ) ) - 1 ) ^ 2 ) )
262 259 261 oveq12d 
 |-  ( 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 ) ) )
263 146 254 257 expclzd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 4 ) e. CC )
264 147 sqcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) - 1 ) ^ 2 ) e. CC )
265 165 167 addcld 
 |-  ( y e. NN -> ( y + 1 ) e. CC )
266 170 nnne0d 
 |-  ( y e. NN -> 2 =/= 0 )
267 113 nnne0d 
 |-  ( y e. NN -> ( y + 1 ) =/= 0 )
268 164 265 266 267 mulne0d 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 0 )
269 146 268 255 expne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 2 ) =/= 0 )
270 147 149 255 expne0d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) - 1 ) ^ 2 ) =/= 0 )
271 263 160 264 269 270 divdiv1d 
 |-  ( 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 ) ) ) )
272 146 147 sqmuld 
 |-  ( 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 ) ) )
273 272 eqcomd 
 |-  ( 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 ) )
274 273 oveq2d 
 |-  ( 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 ) ) )
275 262 271 274 3eqtrd 
 |-  ( 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 ) ) )
276 235 249 275 3eqtrd 
 |-  ( 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 ) ) )
277 276 oveq2d 
 |-  ( 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 ) ) ) )
278 233 234 277 3eqtrd 
 |-  ( 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 ) ) ) )
279 278 oveq2d 
 |-  ( 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 ) ) ) ) )
280 163 231 279 3eqtrd 
 |-  ( 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 ) ) ) ) )
281 145 159 280 3eqtrd 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( y e. NN /\ k = ( y + 1 ) ) -> k = ( y + 1 ) )
284 283 oveq2d 
 |-  ( ( y e. NN /\ k = ( y + 1 ) ) -> ( 2 x. k ) = ( 2 x. ( y + 1 ) ) )
285 284 oveq1d 
 |-  ( ( y e. NN /\ k = ( y + 1 ) ) -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. ( y + 1 ) ) ^ 4 ) )
286 284 oveq1d 
 |-  ( ( y e. NN /\ k = ( y + 1 ) ) -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. ( y + 1 ) ) - 1 ) )
287 284 286 oveq12d 
 |-  ( ( y e. NN /\ k = ( y + 1 ) ) -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) )
288 287 oveq1d 
 |-  ( ( 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 ) )
289 285 288 oveq12d 
 |-  ( ( 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 ) ) )
290 146 147 mulcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) e. CC )
291 290 sqcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) e. CC )
292 146 147 254 149 mulne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) =/= 0 )
293 290 292 255 expne0d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) =/= 0 )
294 263 291 293 divcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) e. CC )
295 282 289 113 294 fvmptd 
 |-  ( 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 ) ) )
296 295 eqcomd 
 |-  ( 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 ) ) )
297 296 oveq2d 
 |-  ( 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 ) ) ) )
298 297 oveq2d 
 |-  ( 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 
 |-  ( 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 ) ) ) )
300 99 299 syl 
 |-  ( 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 ) ) ) )
301 300 eqcomd 
 |-  ( 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 ) ) )
302 301 oveq2d 
 |-  ( 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 ) ) ) )
303 281 298 302 3eqtrd 
 |-  ( 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 + 1 ) ) ) )
304 303 adantr 
 |-  ( ( 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 ) ) ) -> ( ( ( 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 + 1 ) ) ) )
305 102 104 304 3eqtrd 
 |-  ( ( 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 ) ) = ( ( 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 ) ) ) )
306 305 ex 
 |-  ( 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 ) ) = ( ( 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 ) ) ) ) )
307 7 14 21 28 97 306 nnind 
 |-  ( 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 ) ) )