Metamath Proof Explorer

Theorem wallispi2lem2

Description: Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Assertion wallispi2lem2 
|- ( N e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` N ) = ( ( ( 2 ^ ( 4 x. N ) ) x. ( ( ! ` N ) ^ 4 ) ) / ( ( ! ` ( 2 x. N ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 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 ) )
2 oveq2 
 |-  ( x = 1 -> ( 4 x. x ) = ( 4 x. 1 ) )
3 2 oveq2d 
 |-  ( x = 1 -> ( 2 ^ ( 4 x. x ) ) = ( 2 ^ ( 4 x. 1 ) ) )
4 fveq2 
 |-  ( x = 1 -> ( ! ` x ) = ( ! ` 1 ) )
5 4 oveq1d 
 |-  ( x = 1 -> ( ( ! ` x ) ^ 4 ) = ( ( ! ` 1 ) ^ 4 ) )
6 3 5 oveq12d 
 |-  ( x = 1 -> ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) = ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) ) )
7 oveq2 
 |-  ( x = 1 -> ( 2 x. x ) = ( 2 x. 1 ) )
8 7 fveq2d 
 |-  ( x = 1 -> ( ! ` ( 2 x. x ) ) = ( ! ` ( 2 x. 1 ) ) )
9 8 oveq1d 
 |-  ( x = 1 -> ( ( ! ` ( 2 x. x ) ) ^ 2 ) = ( ( ! ` ( 2 x. 1 ) ) ^ 2 ) )
10 6 9 oveq12d 
 |-  ( x = 1 -> ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) = ( ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) ) / ( ( ! ` ( 2 x. 1 ) ) ^ 2 ) ) )
11 1 10 eqeq12d 
 |-  ( x = 1 -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` x ) = ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) <-> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` 1 ) = ( ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) ) / ( ( ! ` ( 2 x. 1 ) ) ^ 2 ) ) ) )
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 oveq2 
 |-  ( x = y -> ( 4 x. x ) = ( 4 x. y ) )
14 13 oveq2d 
 |-  ( x = y -> ( 2 ^ ( 4 x. x ) ) = ( 2 ^ ( 4 x. y ) ) )
15 fveq2 
 |-  ( x = y -> ( ! ` x ) = ( ! ` y ) )
16 15 oveq1d 
 |-  ( x = y -> ( ( ! ` x ) ^ 4 ) = ( ( ! ` y ) ^ 4 ) )
17 14 16 oveq12d 
 |-  ( x = y -> ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) = ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) )
18 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
19 18 fveq2d 
 |-  ( x = y -> ( ! ` ( 2 x. x ) ) = ( ! ` ( 2 x. y ) ) )
20 19 oveq1d 
 |-  ( x = y -> ( ( ! ` ( 2 x. x ) ) ^ 2 ) = ( ( ! ` ( 2 x. y ) ) ^ 2 ) )
21 17 20 oveq12d 
 |-  ( x = y -> ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) )
22 12 21 eqeq12d 
 |-  ( x = y -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` x ) = ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) <-> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) ) )
23 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 ) ) )
24 oveq2 
 |-  ( x = ( y + 1 ) -> ( 4 x. x ) = ( 4 x. ( y + 1 ) ) )
25 24 oveq2d 
 |-  ( x = ( y + 1 ) -> ( 2 ^ ( 4 x. x ) ) = ( 2 ^ ( 4 x. ( y + 1 ) ) ) )
26 fveq2 
 |-  ( x = ( y + 1 ) -> ( ! ` x ) = ( ! ` ( y + 1 ) ) )
27 26 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( ! ` x ) ^ 4 ) = ( ( ! ` ( y + 1 ) ) ^ 4 ) )
28 25 27 oveq12d 
 |-  ( x = ( y + 1 ) -> ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) = ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) )
29 oveq2 
 |-  ( x = ( y + 1 ) -> ( 2 x. x ) = ( 2 x. ( y + 1 ) ) )
30 29 fveq2d 
 |-  ( x = ( y + 1 ) -> ( ! ` ( 2 x. x ) ) = ( ! ` ( 2 x. ( y + 1 ) ) ) )
31 30 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( ! ` ( 2 x. x ) ) ^ 2 ) = ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) )
32 28 31 oveq12d 
 |-  ( x = ( y + 1 ) -> ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) )
33 23 32 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` x ) = ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) <-> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` ( y + 1 ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) ) )
34 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 ) )
35 oveq2 
 |-  ( x = N -> ( 4 x. x ) = ( 4 x. N ) )
36 35 oveq2d 
 |-  ( x = N -> ( 2 ^ ( 4 x. x ) ) = ( 2 ^ ( 4 x. N ) ) )
37 fveq2 
 |-  ( x = N -> ( ! ` x ) = ( ! ` N ) )
38 37 oveq1d 
 |-  ( x = N -> ( ( ! ` x ) ^ 4 ) = ( ( ! ` N ) ^ 4 ) )
39 36 38 oveq12d 
 |-  ( x = N -> ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) = ( ( 2 ^ ( 4 x. N ) ) x. ( ( ! ` N ) ^ 4 ) ) )
40 oveq2 
 |-  ( x = N -> ( 2 x. x ) = ( 2 x. N ) )
41 40 fveq2d 
 |-  ( x = N -> ( ! ` ( 2 x. x ) ) = ( ! ` ( 2 x. N ) ) )
42 41 oveq1d 
 |-  ( x = N -> ( ( ! ` ( 2 x. x ) ) ^ 2 ) = ( ( ! ` ( 2 x. N ) ) ^ 2 ) )
43 39 42 oveq12d 
 |-  ( x = N -> ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) = ( ( ( 2 ^ ( 4 x. N ) ) x. ( ( ! ` N ) ^ 4 ) ) / ( ( ! ` ( 2 x. N ) ) ^ 2 ) ) )
44 34 43 eqeq12d 
 |-  ( x = N -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` x ) = ( ( ( 2 ^ ( 4 x. x ) ) x. ( ( ! ` x ) ^ 4 ) ) / ( ( ! ` ( 2 x. x ) ) ^ 2 ) ) <-> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` N ) = ( ( ( 2 ^ ( 4 x. N ) ) x. ( ( ! ` N ) ^ 4 ) ) / ( ( ! ` ( 2 x. N ) ) ^ 2 ) ) ) )
45 1z 
 |-  1 e. ZZ
46 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 ) )
47 45 46 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 )
48 1nn 
 |-  1 e. NN
49 oveq2 
 |-  ( k = 1 -> ( 2 x. k ) = ( 2 x. 1 ) )
50 49 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. 1 ) ^ 4 ) )
51 49 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. 1 ) - 1 ) )
52 49 51 oveq12d 
 |-  ( k = 1 -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) )
53 52 oveq1d 
 |-  ( k = 1 -> ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) = ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) )
54 50 53 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 ) ) )
55 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 ) ) )
56 ovex 
 |-  ( ( ( 2 x. 1 ) ^ 4 ) / ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) ) e. _V
57 54 55 56 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 ) ) )
58 48 57 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 ) )
59 2t1e2 
 |-  ( 2 x. 1 ) = 2
60 59 oveq1i 
 |-  ( ( 2 x. 1 ) ^ 4 ) = ( 2 ^ 4 )
61 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
62 1nn0 
 |-  1 e. NN0
63 6nn0 
 |-  6 e. NN0
64 0nn0 
 |-  0 e. NN0
65 1t1e1 
 |-  ( 1 x. 1 ) = 1
66 65 oveq1i 
 |-  ( ( 1 x. 1 ) + 0 ) = ( 1 + 0 )
67 1p0e1 
 |-  ( 1 + 0 ) = 1
68 66 67 eqtri 
 |-  ( ( 1 x. 1 ) + 0 ) = 1
69 6cn 
 |-  6 e. CC
70 69 mulid1i 
 |-  ( 6 x. 1 ) = 6
71 63 dec0h 
 |-  6 = ; 0 6
72 70 71 eqtri 
 |-  ( 6 x. 1 ) = ; 0 6
73 62 62 63 61 63 64 68 72 decmul1c 
 |-  ( ( 2 ^ 4 ) x. 1 ) = ; 1 6
74 61 73 eqtr4i 
 |-  ( 2 ^ 4 ) = ( ( 2 ^ 4 ) x. 1 )
75 2nn0 
 |-  2 e. NN0
76 2t2e4 
 |-  ( 2 x. 2 ) = 4
77 sq1 
 |-  ( 1 ^ 2 ) = 1
78 62 75 76 77 65 numexp2x 
 |-  ( 1 ^ 4 ) = 1
79 78 eqcomi 
 |-  1 = ( 1 ^ 4 )
80 79 oveq2i 
 |-  ( ( 2 ^ 4 ) x. 1 ) = ( ( 2 ^ 4 ) x. ( 1 ^ 4 ) )
81 4cn 
 |-  4 e. CC
82 81 mulid1i 
 |-  ( 4 x. 1 ) = 4
83 82 eqcomi 
 |-  4 = ( 4 x. 1 )
84 83 oveq2i 
 |-  ( 2 ^ 4 ) = ( 2 ^ ( 4 x. 1 ) )
85 fac1 
 |-  ( ! ` 1 ) = 1
86 85 eqcomi 
 |-  1 = ( ! ` 1 )
87 86 oveq1i 
 |-  ( 1 ^ 4 ) = ( ( ! ` 1 ) ^ 4 )
88 84 87 oveq12i 
 |-  ( ( 2 ^ 4 ) x. ( 1 ^ 4 ) ) = ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) )
89 74 80 88 3eqtri 
 |-  ( 2 ^ 4 ) = ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) )
90 60 89 eqtri 
 |-  ( ( 2 x. 1 ) ^ 4 ) = ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) )
91 59 oveq1i 
 |-  ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 )
92 2m1e1 
 |-  ( 2 - 1 ) = 1
93 91 92 eqtri 
 |-  ( ( 2 x. 1 ) - 1 ) = 1
94 93 oveq2i 
 |-  ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) = ( ( 2 x. 1 ) x. 1 )
95 59 oveq1i 
 |-  ( ( 2 x. 1 ) x. 1 ) = ( 2 x. 1 )
96 95 59 eqtri 
 |-  ( ( 2 x. 1 ) x. 1 ) = 2
97 59 fveq2i 
 |-  ( ! ` ( 2 x. 1 ) ) = ( ! ` 2 )
98 fac2 
 |-  ( ! ` 2 ) = 2
99 97 98 eqtri 
 |-  ( ! ` ( 2 x. 1 ) ) = 2
100 99 eqcomi 
 |-  2 = ( ! ` ( 2 x. 1 ) )
101 94 96 100 3eqtri 
 |-  ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) = ( ! ` ( 2 x. 1 ) )
102 101 oveq1i 
 |-  ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) = ( ( ! ` ( 2 x. 1 ) ) ^ 2 )
103 90 102 oveq12i 
 |-  ( ( ( 2 x. 1 ) ^ 4 ) / ( ( ( 2 x. 1 ) x. ( ( 2 x. 1 ) - 1 ) ) ^ 2 ) ) = ( ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) ) / ( ( ! ` ( 2 x. 1 ) ) ^ 2 ) )
104 47 58 103 3eqtri 
 |-  ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` 1 ) = ( ( ( 2 ^ ( 4 x. 1 ) ) x. ( ( ! ` 1 ) ^ 4 ) ) / ( ( ! ` ( 2 x. 1 ) ) ^ 2 ) )
105 elnnuz 
 |-  ( y e. NN <-> y e. ( ZZ>= ` 1 ) )
106 105 biimpi 
 |-  ( y e. NN -> y e. ( ZZ>= ` 1 ) )
107 106 adantr 
 |-  ( ( y e. NN /\ ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) ) -> y e. ( ZZ>= ` 1 ) )
108 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 ) ) ) )
109 107 108 syl 
 |-  ( ( y e. NN /\ ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) ) -> ( 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 ) ) ) )
110 simpr 
 |-  ( ( y e. NN /\ ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) ) -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) )
111 110 oveq1d 
 |-  ( ( y e. NN /\ ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 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 ) ) ) = ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` ( y + 1 ) ) ) )
112 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 ) ) ) )
113 oveq2 
 |-  ( k = ( y + 1 ) -> ( 2 x. k ) = ( 2 x. ( y + 1 ) ) )
114 113 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. ( y + 1 ) ) ^ 4 ) )
115 113 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. ( y + 1 ) ) - 1 ) )
116 113 115 oveq12d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) )
117 116 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) = ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) )
118 114 117 oveq12d 
 |-  ( 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 ) ) )
119 118 adantl 
 |-  ( ( 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 ) ) )
120 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
121 2cnd 
 |-  ( y e. NN -> 2 e. CC )
122 nncn 
 |-  ( y e. NN -> y e. CC )
123 1cnd 
 |-  ( y e. NN -> 1 e. CC )
124 122 123 addcld 
 |-  ( y e. NN -> ( y + 1 ) e. CC )
125 121 124 mulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. CC )
126 4nn0 
 |-  4 e. NN0
127 126 a1i 
 |-  ( y e. NN -> 4 e. NN0 )
128 125 127 expcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 4 ) e. CC )
129 125 123 subcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) e. CC )
130 125 129 mulcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) e. CC )
131 130 sqcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) e. CC )
132 2pos 
 |-  0 < 2
133 132 a1i 
 |-  ( y e. NN -> 0 < 2 )
134 133 gt0ne0d 
 |-  ( y e. NN -> 2 =/= 0 )
135 120 nnne0d 
 |-  ( y e. NN -> ( y + 1 ) =/= 0 )
136 121 124 134 135 mulne0d 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 0 )
137 1red 
 |-  ( y e. NN -> 1 e. RR )
138 2re 
 |-  2 e. RR
139 138 a1i 
 |-  ( y e. NN -> 2 e. RR )
140 nnre 
 |-  ( y e. NN -> y e. RR )
141 140 137 readdcld 
 |-  ( y e. NN -> ( y + 1 ) e. RR )
142 1lt2 
 |-  1 < 2
143 142 a1i 
 |-  ( y e. NN -> 1 < 2 )
144 nnrp 
 |-  ( y e. NN -> y e. RR+ )
145 137 144 ltaddrp2d 
 |-  ( y e. NN -> 1 < ( y + 1 ) )
146 139 141 143 145 mulgt1d 
 |-  ( y e. NN -> 1 < ( 2 x. ( y + 1 ) ) )
147 137 146 gtned 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 1 )
148 125 123 147 subne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) =/= 0 )
149 125 129 136 148 mulne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) =/= 0 )
150 2z 
 |-  2 e. ZZ
151 150 a1i 
 |-  ( y e. NN -> 2 e. ZZ )
152 130 149 151 expne0d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) =/= 0 )
153 128 131 152 divcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) e. CC )
154 112 119 120 153 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 ) ) )
155 154 oveq2d 
 |-  ( y e. NN -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` ( y + 1 ) ) ) = ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) ) )
156 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
157 127 156 nn0mulcld 
 |-  ( y e. NN -> ( 4 x. y ) e. NN0 )
158 121 157 expcld 
 |-  ( y e. NN -> ( 2 ^ ( 4 x. y ) ) e. CC )
159 faccl 
 |-  ( y e. NN0 -> ( ! ` y ) e. NN )
160 nncn 
 |-  ( ( ! ` y ) e. NN -> ( ! ` y ) e. CC )
161 156 159 160 3syl 
 |-  ( y e. NN -> ( ! ` y ) e. CC )
162 161 127 expcld 
 |-  ( y e. NN -> ( ( ! ` y ) ^ 4 ) e. CC )
163 158 162 mulcld 
 |-  ( y e. NN -> ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) e. CC )
164 75 a1i 
 |-  ( y e. NN -> 2 e. NN0 )
165 164 156 nn0mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. NN0 )
166 faccl 
 |-  ( ( 2 x. y ) e. NN0 -> ( ! ` ( 2 x. y ) ) e. NN )
167 nncn 
 |-  ( ( ! ` ( 2 x. y ) ) e. NN -> ( ! ` ( 2 x. y ) ) e. CC )
168 165 166 167 3syl 
 |-  ( y e. NN -> ( ! ` ( 2 x. y ) ) e. CC )
169 168 sqcld 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) ^ 2 ) e. CC )
170 165 166 syl 
 |-  ( y e. NN -> ( ! ` ( 2 x. y ) ) e. NN )
171 170 nnne0d 
 |-  ( y e. NN -> ( ! ` ( 2 x. y ) ) =/= 0 )
172 168 171 151 expne0d 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) ^ 2 ) =/= 0 )
173 163 169 128 131 172 152 divmuldivd 
 |-  ( y e. NN -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) ) = ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) x. ( ( 2 x. ( y + 1 ) ) ^ 4 ) ) / ( ( ( ! ` ( 2 x. y ) ) ^ 2 ) x. ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) ) )
174 121 124 127 mulexpd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 4 ) = ( ( 2 ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) )
175 174 oveq2d 
 |-  ( y e. NN -> ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) x. ( ( 2 x. ( y + 1 ) ) ^ 4 ) ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) x. ( ( 2 ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) ) )
176 121 127 expcld 
 |-  ( y e. NN -> ( 2 ^ 4 ) e. CC )
177 124 127 expcld 
 |-  ( y e. NN -> ( ( y + 1 ) ^ 4 ) e. CC )
178 158 162 176 177 mul4d 
 |-  ( y e. NN -> ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) x. ( ( 2 ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) ) )
179 161 124 127 mulexpd 
 |-  ( y e. NN -> ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) = ( ( ( ! ` y ) ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) )
180 179 eqcomd 
 |-  ( y e. NN -> ( ( ( ! ` y ) ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) = ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) )
181 180 oveq2d 
 |-  ( y e. NN -> ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) ) )
182 175 178 181 3eqtrd 
 |-  ( y e. NN -> ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) x. ( ( 2 x. ( y + 1 ) ) ^ 4 ) ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) ) )
183 121 122 mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. CC )
184 183 123 addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. CC )
185 125 184 mulcomd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. y ) + 1 ) ) = ( ( ( 2 x. y ) + 1 ) x. ( 2 x. ( y + 1 ) ) ) )
186 185 oveq2d 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. y ) + 1 ) ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( ( 2 x. y ) + 1 ) x. ( 2 x. ( y + 1 ) ) ) ) )
187 121 122 123 adddid 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
188 187 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( ( 2 x. y ) + ( 2 x. 1 ) ) - 1 ) )
189 59 121 eqeltrid 
 |-  ( y e. NN -> ( 2 x. 1 ) e. CC )
190 183 189 123 addsubassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + ( 2 x. 1 ) ) - 1 ) = ( ( 2 x. y ) + ( ( 2 x. 1 ) - 1 ) ) )
191 59 a1i 
 |-  ( y e. NN -> ( 2 x. 1 ) = 2 )
192 191 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 ) )
193 192 92 eqtrdi 
 |-  ( y e. NN -> ( ( 2 x. 1 ) - 1 ) = 1 )
194 193 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( ( 2 x. 1 ) - 1 ) ) = ( ( 2 x. y ) + 1 ) )
195 188 190 194 3eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( 2 x. y ) + 1 ) )
196 195 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. y ) + 1 ) ) )
197 196 oveq2d 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. y ) + 1 ) ) ) )
198 168 184 125 mulassd 
 |-  ( y e. NN -> ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( ( 2 x. y ) + 1 ) x. ( 2 x. ( y + 1 ) ) ) ) )
199 186 197 198 3eqtr4d 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ) = ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) )
200 199 oveq1d 
 |-  ( y e. NN -> ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ) ^ 2 ) = ( ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ^ 2 ) )
201 168 130 164 mulexpd 
 |-  ( y e. NN -> ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ) ^ 2 ) = ( ( ( ! ` ( 2 x. y ) ) ^ 2 ) x. ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) )
202 df-2 
 |-  2 = ( 1 + 1 )
203 202 a1i 
 |-  ( y e. NN -> 2 = ( 1 + 1 ) )
204 203 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
205 183 123 123 addassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
206 204 205 eqtr4d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( ( ( 2 x. y ) + 1 ) + 1 ) )
207 206 fveq2d 
 |-  ( y e. NN -> ( ! ` ( ( 2 x. y ) + 2 ) ) = ( ! ` ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
208 62 a1i 
 |-  ( y e. NN -> 1 e. NN0 )
209 165 208 nn0addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. NN0 )
210 facp1 
 |-  ( ( ( 2 x. y ) + 1 ) e. NN0 -> ( ! ` ( ( ( 2 x. y ) + 1 ) + 1 ) ) = ( ( ! ` ( ( 2 x. y ) + 1 ) ) x. ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
211 209 210 syl 
 |-  ( y e. NN -> ( ! ` ( ( ( 2 x. y ) + 1 ) + 1 ) ) = ( ( ! ` ( ( 2 x. y ) + 1 ) ) x. ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
212 facp1 
 |-  ( ( 2 x. y ) e. NN0 -> ( ! ` ( ( 2 x. y ) + 1 ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) )
213 165 212 syl 
 |-  ( y e. NN -> ( ! ` ( ( 2 x. y ) + 1 ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) )
214 203 eqcomd 
 |-  ( y e. NN -> ( 1 + 1 ) = 2 )
215 214 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 1 + 1 ) ) = ( ( 2 x. y ) + 2 ) )
216 214 202 59 3eqtr4g 
 |-  ( y e. NN -> 2 = ( 2 x. 1 ) )
217 216 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
218 217 187 eqtr4d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( 2 x. ( y + 1 ) ) )
219 205 215 218 3eqtrd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( 2 x. ( y + 1 ) ) )
220 213 219 oveq12d 
 |-  ( y e. NN -> ( ( ! ` ( ( 2 x. y ) + 1 ) ) x. ( ( ( 2 x. y ) + 1 ) + 1 ) ) = ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) )
221 207 211 220 3eqtrrd 
 |-  ( y e. NN -> ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) = ( ! ` ( ( 2 x. y ) + 2 ) ) )
222 221 oveq1d 
 |-  ( y e. NN -> ( ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ^ 2 ) = ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) )
223 200 201 222 3eqtr3d 
 |-  ( y e. NN -> ( ( ( ! ` ( 2 x. y ) ) ^ 2 ) x. ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) = ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) )
224 182 223 oveq12d 
 |-  ( y e. NN -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) x. ( ( 2 x. ( y + 1 ) ) ^ 4 ) ) / ( ( ( ! ` ( 2 x. y ) ) ^ 2 ) x. ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) ) = ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) ) )
225 173 224 eqtrd 
 |-  ( y e. NN -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) ) = ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) ) )
226 83 a1i 
 |-  ( y e. NN -> 4 = ( 4 x. 1 ) )
227 226 oveq2d 
 |-  ( y e. NN -> ( ( 4 x. y ) + 4 ) = ( ( 4 x. y ) + ( 4 x. 1 ) ) )
228 227 oveq2d 
 |-  ( y e. NN -> ( 2 ^ ( ( 4 x. y ) + 4 ) ) = ( 2 ^ ( ( 4 x. y ) + ( 4 x. 1 ) ) ) )
229 121 127 157 expaddd 
 |-  ( y e. NN -> ( 2 ^ ( ( 4 x. y ) + 4 ) ) = ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) )
230 81 a1i 
 |-  ( y e. NN -> 4 e. CC )
231 230 122 123 adddid 
 |-  ( y e. NN -> ( 4 x. ( y + 1 ) ) = ( ( 4 x. y ) + ( 4 x. 1 ) ) )
232 231 eqcomd 
 |-  ( y e. NN -> ( ( 4 x. y ) + ( 4 x. 1 ) ) = ( 4 x. ( y + 1 ) ) )
233 232 oveq2d 
 |-  ( y e. NN -> ( 2 ^ ( ( 4 x. y ) + ( 4 x. 1 ) ) ) = ( 2 ^ ( 4 x. ( y + 1 ) ) ) )
234 228 229 233 3eqtr3d 
 |-  ( y e. NN -> ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) = ( 2 ^ ( 4 x. ( y + 1 ) ) ) )
235 facp1 
 |-  ( y e. NN0 -> ( ! ` ( y + 1 ) ) = ( ( ! ` y ) x. ( y + 1 ) ) )
236 156 235 syl 
 |-  ( y e. NN -> ( ! ` ( y + 1 ) ) = ( ( ! ` y ) x. ( y + 1 ) ) )
237 236 eqcomd 
 |-  ( y e. NN -> ( ( ! ` y ) x. ( y + 1 ) ) = ( ! ` ( y + 1 ) ) )
238 237 oveq1d 
 |-  ( y e. NN -> ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) = ( ( ! ` ( y + 1 ) ) ^ 4 ) )
239 234 238 oveq12d 
 |-  ( y e. NN -> ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) ) = ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) )
240 218 fveq2d 
 |-  ( y e. NN -> ( ! ` ( ( 2 x. y ) + 2 ) ) = ( ! ` ( 2 x. ( y + 1 ) ) ) )
241 240 oveq1d 
 |-  ( y e. NN -> ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) = ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) )
242 239 241 oveq12d 
 |-  ( y e. NN -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) x. ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) )
243 155 225 242 3eqtrd 
 |-  ( y e. NN -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` ( y + 1 ) ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) )
244 243 adantr 
 |-  ( ( y e. NN /\ ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) ) -> ( ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) x. ( ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ` ( y + 1 ) ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) )
245 109 111 244 3eqtrd 
 |-  ( ( y e. NN /\ ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) ) -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` ( y + 1 ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) )
246 245 ex 
 |-  ( y e. NN -> ( ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` y ) = ( ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) / ( ( ! ` ( 2 x. y ) ) ^ 2 ) ) -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` ( y + 1 ) ) = ( ( ( 2 ^ ( 4 x. ( y + 1 ) ) ) x. ( ( ! ` ( y + 1 ) ) ^ 4 ) ) / ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) ) ) )
247 11 22 33 44 104 246 nnind 
 |-  ( N e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` N ) = ( ( ( 2 ^ ( 4 x. N ) ) x. ( ( ! ` N ) ^ 4 ) ) / ( ( ! ` ( 2 x. N ) ) ^ 2 ) ) )