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 mulridi 
 |-  ( 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 mulridi 
 |-  ( 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 birani 
 |-  ( ( 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 ) )
107 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 ) ) ) )
108 106 107 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 ) ) ) )
109 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 ) ) )
110 109 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 ) ) ) )
111 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 ) ) ) )
112 oveq2 
 |-  ( k = ( y + 1 ) -> ( 2 x. k ) = ( 2 x. ( y + 1 ) ) )
113 112 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) ^ 4 ) = ( ( 2 x. ( y + 1 ) ) ^ 4 ) )
114 112 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. ( y + 1 ) ) - 1 ) )
115 112 114 oveq12d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) )
116 115 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) = ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) )
117 113 116 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 ) ) )
118 117 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 ) ) )
119 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
120 2cnd 
 |-  ( y e. NN -> 2 e. CC )
121 nncn 
 |-  ( y e. NN -> y e. CC )
122 1cnd 
 |-  ( y e. NN -> 1 e. CC )
123 121 122 addcld 
 |-  ( y e. NN -> ( y + 1 ) e. CC )
124 120 123 mulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. CC )
125 4nn0 
 |-  4 e. NN0
126 125 a1i 
 |-  ( y e. NN -> 4 e. NN0 )
127 124 126 expcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 4 ) e. CC )
128 124 122 subcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) e. CC )
129 124 128 mulcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) e. CC )
130 129 sqcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) e. CC )
131 2pos 
 |-  0 < 2
132 131 a1i 
 |-  ( y e. NN -> 0 < 2 )
133 132 gt0ne0d 
 |-  ( y e. NN -> 2 =/= 0 )
134 119 nnne0d 
 |-  ( y e. NN -> ( y + 1 ) =/= 0 )
135 120 123 133 134 mulne0d 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 0 )
136 1red 
 |-  ( y e. NN -> 1 e. RR )
137 2re 
 |-  2 e. RR
138 137 a1i 
 |-  ( y e. NN -> 2 e. RR )
139 nnre 
 |-  ( y e. NN -> y e. RR )
140 139 136 readdcld 
 |-  ( y e. NN -> ( y + 1 ) e. RR )
141 1lt2 
 |-  1 < 2
142 141 a1i 
 |-  ( y e. NN -> 1 < 2 )
143 nnrp 
 |-  ( y e. NN -> y e. RR+ )
144 136 143 ltaddrp2d 
 |-  ( y e. NN -> 1 < ( y + 1 ) )
145 138 140 142 144 mulgt1d 
 |-  ( y e. NN -> 1 < ( 2 x. ( y + 1 ) ) )
146 136 145 gtned 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 1 )
147 124 122 146 subne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) =/= 0 )
148 124 128 135 147 mulne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) =/= 0 )
149 2z 
 |-  2 e. ZZ
150 149 a1i 
 |-  ( y e. NN -> 2 e. ZZ )
151 129 148 150 expne0d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) =/= 0 )
152 127 130 151 divcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) ^ 4 ) / ( ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) ^ 2 ) ) e. CC )
153 111 118 119 152 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 ) ) )
154 153 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 ) ) ) )
155 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
156 126 155 nn0mulcld 
 |-  ( y e. NN -> ( 4 x. y ) e. NN0 )
157 120 156 expcld 
 |-  ( y e. NN -> ( 2 ^ ( 4 x. y ) ) e. CC )
158 faccl 
 |-  ( y e. NN0 -> ( ! ` y ) e. NN )
159 nncn 
 |-  ( ( ! ` y ) e. NN -> ( ! ` y ) e. CC )
160 155 158 159 3syl 
 |-  ( y e. NN -> ( ! ` y ) e. CC )
161 160 126 expcld 
 |-  ( y e. NN -> ( ( ! ` y ) ^ 4 ) e. CC )
162 157 161 mulcld 
 |-  ( y e. NN -> ( ( 2 ^ ( 4 x. y ) ) x. ( ( ! ` y ) ^ 4 ) ) e. CC )
163 75 a1i 
 |-  ( y e. NN -> 2 e. NN0 )
164 163 155 nn0mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. NN0 )
165 faccl 
 |-  ( ( 2 x. y ) e. NN0 -> ( ! ` ( 2 x. y ) ) e. NN )
166 nncn 
 |-  ( ( ! ` ( 2 x. y ) ) e. NN -> ( ! ` ( 2 x. y ) ) e. CC )
167 164 165 166 3syl 
 |-  ( y e. NN -> ( ! ` ( 2 x. y ) ) e. CC )
168 167 sqcld 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) ^ 2 ) e. CC )
169 164 165 syl 
 |-  ( y e. NN -> ( ! ` ( 2 x. y ) ) e. NN )
170 169 nnne0d 
 |-  ( y e. NN -> ( ! ` ( 2 x. y ) ) =/= 0 )
171 167 170 150 expne0d 
 |-  ( y e. NN -> ( ( ! ` ( 2 x. y ) ) ^ 2 ) =/= 0 )
172 162 168 127 130 171 151 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 ) ) ) )
173 120 123 126 mulexpd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) ^ 4 ) = ( ( 2 ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) )
174 173 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 ) ) ) )
175 120 126 expcld 
 |-  ( y e. NN -> ( 2 ^ 4 ) e. CC )
176 123 126 expcld 
 |-  ( y e. NN -> ( ( y + 1 ) ^ 4 ) e. CC )
177 157 161 175 176 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 ) ) ) )
178 160 123 126 mulexpd 
 |-  ( y e. NN -> ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) = ( ( ( ! ` y ) ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) )
179 178 eqcomd 
 |-  ( y e. NN -> ( ( ( ! ` y ) ^ 4 ) x. ( ( y + 1 ) ^ 4 ) ) = ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) )
180 179 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 ) ) )
181 174 177 180 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 ) ) )
182 120 121 mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. CC )
183 182 122 addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. CC )
184 124 183 mulcomd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. y ) + 1 ) ) = ( ( ( 2 x. y ) + 1 ) x. ( 2 x. ( y + 1 ) ) ) )
185 184 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 ) ) ) ) )
186 120 121 122 adddid 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
187 186 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( ( 2 x. y ) + ( 2 x. 1 ) ) - 1 ) )
188 59 120 eqeltrid 
 |-  ( y e. NN -> ( 2 x. 1 ) e. CC )
189 182 188 122 addsubassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + ( 2 x. 1 ) ) - 1 ) = ( ( 2 x. y ) + ( ( 2 x. 1 ) - 1 ) ) )
190 59 a1i 
 |-  ( y e. NN -> ( 2 x. 1 ) = 2 )
191 190 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 ) )
192 191 92 eqtrdi 
 |-  ( y e. NN -> ( ( 2 x. 1 ) - 1 ) = 1 )
193 192 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( ( 2 x. 1 ) - 1 ) ) = ( ( 2 x. y ) + 1 ) )
194 187 189 193 3eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( 2 x. y ) + 1 ) )
195 194 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) x. ( ( 2 x. y ) + 1 ) ) )
196 195 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 ) ) ) )
197 167 183 124 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 ) ) ) ) )
198 185 196 197 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 ) ) ) )
199 198 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 ) )
200 167 129 163 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 ) ) )
201 df-2 
 |-  2 = ( 1 + 1 )
202 201 a1i 
 |-  ( y e. NN -> 2 = ( 1 + 1 ) )
203 202 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
204 182 122 122 addassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
205 203 204 eqtr4d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( ( ( 2 x. y ) + 1 ) + 1 ) )
206 205 fveq2d 
 |-  ( y e. NN -> ( ! ` ( ( 2 x. y ) + 2 ) ) = ( ! ` ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
207 62 a1i 
 |-  ( y e. NN -> 1 e. NN0 )
208 164 207 nn0addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. NN0 )
209 facp1 
 |-  ( ( ( 2 x. y ) + 1 ) e. NN0 -> ( ! ` ( ( ( 2 x. y ) + 1 ) + 1 ) ) = ( ( ! ` ( ( 2 x. y ) + 1 ) ) x. ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
210 208 209 syl 
 |-  ( y e. NN -> ( ! ` ( ( ( 2 x. y ) + 1 ) + 1 ) ) = ( ( ! ` ( ( 2 x. y ) + 1 ) ) x. ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
211 facp1 
 |-  ( ( 2 x. y ) e. NN0 -> ( ! ` ( ( 2 x. y ) + 1 ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) )
212 164 211 syl 
 |-  ( y e. NN -> ( ! ` ( ( 2 x. y ) + 1 ) ) = ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) )
213 202 eqcomd 
 |-  ( y e. NN -> ( 1 + 1 ) = 2 )
214 213 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 1 + 1 ) ) = ( ( 2 x. y ) + 2 ) )
215 213 201 59 3eqtr4g 
 |-  ( y e. NN -> 2 = ( 2 x. 1 ) )
216 215 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
217 216 186 eqtr4d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 2 ) = ( 2 x. ( y + 1 ) ) )
218 204 214 217 3eqtrd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( 2 x. ( y + 1 ) ) )
219 212 218 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 ) ) ) )
220 206 210 219 3eqtrrd 
 |-  ( y e. NN -> ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) = ( ! ` ( ( 2 x. y ) + 2 ) ) )
221 220 oveq1d 
 |-  ( y e. NN -> ( ( ( ( ! ` ( 2 x. y ) ) x. ( ( 2 x. y ) + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ^ 2 ) = ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) )
222 199 200 221 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 ) )
223 181 222 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 ) ) )
224 172 223 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 ) ) )
225 83 a1i 
 |-  ( y e. NN -> 4 = ( 4 x. 1 ) )
226 225 oveq2d 
 |-  ( y e. NN -> ( ( 4 x. y ) + 4 ) = ( ( 4 x. y ) + ( 4 x. 1 ) ) )
227 226 oveq2d 
 |-  ( y e. NN -> ( 2 ^ ( ( 4 x. y ) + 4 ) ) = ( 2 ^ ( ( 4 x. y ) + ( 4 x. 1 ) ) ) )
228 120 126 156 expaddd 
 |-  ( y e. NN -> ( 2 ^ ( ( 4 x. y ) + 4 ) ) = ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) )
229 81 a1i 
 |-  ( y e. NN -> 4 e. CC )
230 229 121 122 adddid 
 |-  ( y e. NN -> ( 4 x. ( y + 1 ) ) = ( ( 4 x. y ) + ( 4 x. 1 ) ) )
231 230 eqcomd 
 |-  ( y e. NN -> ( ( 4 x. y ) + ( 4 x. 1 ) ) = ( 4 x. ( y + 1 ) ) )
232 231 oveq2d 
 |-  ( y e. NN -> ( 2 ^ ( ( 4 x. y ) + ( 4 x. 1 ) ) ) = ( 2 ^ ( 4 x. ( y + 1 ) ) ) )
233 227 228 232 3eqtr3d 
 |-  ( y e. NN -> ( ( 2 ^ ( 4 x. y ) ) x. ( 2 ^ 4 ) ) = ( 2 ^ ( 4 x. ( y + 1 ) ) ) )
234 facp1 
 |-  ( y e. NN0 -> ( ! ` ( y + 1 ) ) = ( ( ! ` y ) x. ( y + 1 ) ) )
235 155 234 syl 
 |-  ( y e. NN -> ( ! ` ( y + 1 ) ) = ( ( ! ` y ) x. ( y + 1 ) ) )
236 235 eqcomd 
 |-  ( y e. NN -> ( ( ! ` y ) x. ( y + 1 ) ) = ( ! ` ( y + 1 ) ) )
237 236 oveq1d 
 |-  ( y e. NN -> ( ( ( ! ` y ) x. ( y + 1 ) ) ^ 4 ) = ( ( ! ` ( y + 1 ) ) ^ 4 ) )
238 233 237 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 ) ) )
239 217 fveq2d 
 |-  ( y e. NN -> ( ! ` ( ( 2 x. y ) + 2 ) ) = ( ! ` ( 2 x. ( y + 1 ) ) ) )
240 239 oveq1d 
 |-  ( y e. NN -> ( ( ! ` ( ( 2 x. y ) + 2 ) ) ^ 2 ) = ( ( ! ` ( 2 x. ( y + 1 ) ) ) ^ 2 ) )
241 238 240 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 ) ) )
242 154 224 241 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 ) ) )
243 242 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 ) ) )
244 108 110 243 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 ) ) )
245 244 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 ) ) ) )
246 11 22 33 44 104 245 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 ) ) )