Metamath Proof Explorer

Theorem wallispilem4

Description: F maps to explicit expression for the ratio of two consecutive values of I . (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses wallispilem4.1 
|- F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
wallispilem4.2 
|- I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` z ) ^ n ) _d z )
wallispilem4.3 
|- G = ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )
wallispilem4.4 
|- H = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
Assertion wallispilem4 
|- G = H

Proof

Step Hyp Ref Expression
1 wallispilem4.1 
 |-  F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )
2 wallispilem4.2 
 |-  I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` z ) ^ n ) _d z )
3 wallispilem4.3 
 |-  G = ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )
4 wallispilem4.4 
 |-  H = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
5 oveq2 
 |-  ( x = 1 -> ( 2 x. x ) = ( 2 x. 1 ) )
6 5 fveq2d 
 |-  ( x = 1 -> ( I ` ( 2 x. x ) ) = ( I ` ( 2 x. 1 ) ) )
7 5 fvoveq1d 
 |-  ( x = 1 -> ( I ` ( ( 2 x. x ) + 1 ) ) = ( I ` ( ( 2 x. 1 ) + 1 ) ) )
8 6 7 oveq12d 
 |-  ( x = 1 -> ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( I ` ( 2 x. 1 ) ) / ( I ` ( ( 2 x. 1 ) + 1 ) ) ) )
9 fveq2 
 |-  ( x = 1 -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` 1 ) )
10 9 oveq2d 
 |-  ( x = 1 -> ( 1 / ( seq 1 ( x. , F ) ` x ) ) = ( 1 / ( seq 1 ( x. , F ) ` 1 ) ) )
11 10 oveq2d 
 |-  ( x = 1 -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` 1 ) ) ) )
12 8 11 eqeq12d 
 |-  ( x = 1 -> ( ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) <-> ( ( I ` ( 2 x. 1 ) ) / ( I ` ( ( 2 x. 1 ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` 1 ) ) ) ) )
13 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
14 13 fveq2d 
 |-  ( x = y -> ( I ` ( 2 x. x ) ) = ( I ` ( 2 x. y ) ) )
15 13 fvoveq1d 
 |-  ( x = y -> ( I ` ( ( 2 x. x ) + 1 ) ) = ( I ` ( ( 2 x. y ) + 1 ) ) )
16 14 15 oveq12d 
 |-  ( x = y -> ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) )
17 fveq2 
 |-  ( x = y -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` y ) )
18 17 oveq2d 
 |-  ( x = y -> ( 1 / ( seq 1 ( x. , F ) ` x ) ) = ( 1 / ( seq 1 ( x. , F ) ` y ) ) )
19 18 oveq2d 
 |-  ( x = y -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) )
20 16 19 eqeq12d 
 |-  ( x = y -> ( ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) <-> ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
21 oveq2 
 |-  ( x = ( y + 1 ) -> ( 2 x. x ) = ( 2 x. ( y + 1 ) ) )
22 21 fveq2d 
 |-  ( x = ( y + 1 ) -> ( I ` ( 2 x. x ) ) = ( I ` ( 2 x. ( y + 1 ) ) ) )
23 21 fvoveq1d 
 |-  ( x = ( y + 1 ) -> ( I ` ( ( 2 x. x ) + 1 ) ) = ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) )
24 22 23 oveq12d 
 |-  ( x = ( y + 1 ) -> ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) )
25 fveq2 
 |-  ( x = ( y + 1 ) -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` ( y + 1 ) ) )
26 25 oveq2d 
 |-  ( x = ( y + 1 ) -> ( 1 / ( seq 1 ( x. , F ) ` x ) ) = ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) )
27 26 oveq2d 
 |-  ( x = ( y + 1 ) -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) )
28 24 27 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) <-> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) ) )
29 oveq2 
 |-  ( x = n -> ( 2 x. x ) = ( 2 x. n ) )
30 29 fveq2d 
 |-  ( x = n -> ( I ` ( 2 x. x ) ) = ( I ` ( 2 x. n ) ) )
31 29 fvoveq1d 
 |-  ( x = n -> ( I ` ( ( 2 x. x ) + 1 ) ) = ( I ` ( ( 2 x. n ) + 1 ) ) )
32 30 31 oveq12d 
 |-  ( x = n -> ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )
33 fveq2 
 |-  ( x = n -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` n ) )
34 33 oveq2d 
 |-  ( x = n -> ( 1 / ( seq 1 ( x. , F ) ` x ) ) = ( 1 / ( seq 1 ( x. , F ) ` n ) ) )
35 34 oveq2d 
 |-  ( x = n -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
36 32 35 eqeq12d 
 |-  ( x = n -> ( ( ( I ` ( 2 x. x ) ) / ( I ` ( ( 2 x. x ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` x ) ) ) <-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) ) )
37 2t1e2 
 |-  ( 2 x. 1 ) = 2
38 37 fveq2i 
 |-  ( I ` ( 2 x. 1 ) ) = ( I ` 2 )
39 37 oveq1i 
 |-  ( ( 2 x. 1 ) + 1 ) = ( 2 + 1 )
40 2p1e3 
 |-  ( 2 + 1 ) = 3
41 39 40 eqtri 
 |-  ( ( 2 x. 1 ) + 1 ) = 3
42 41 fveq2i 
 |-  ( I ` ( ( 2 x. 1 ) + 1 ) ) = ( I ` 3 )
43 38 42 oveq12i 
 |-  ( ( I ` ( 2 x. 1 ) ) / ( I ` ( ( 2 x. 1 ) + 1 ) ) ) = ( ( I ` 2 ) / ( I ` 3 ) )
44 2z 
 |-  2 e. ZZ
45 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
46 44 45 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
47 2 wallispilem2 
 |-  ( ( I ` 0 ) = _pi /\ ( I ` 1 ) = 2 /\ ( 2 e. ( ZZ>= ` 2 ) -> ( I ` 2 ) = ( ( ( 2 - 1 ) / 2 ) x. ( I ` ( 2 - 2 ) ) ) ) )
48 47 simp3i 
 |-  ( 2 e. ( ZZ>= ` 2 ) -> ( I ` 2 ) = ( ( ( 2 - 1 ) / 2 ) x. ( I ` ( 2 - 2 ) ) ) )
49 46 48 ax-mp 
 |-  ( I ` 2 ) = ( ( ( 2 - 1 ) / 2 ) x. ( I ` ( 2 - 2 ) ) )
50 2m1e1 
 |-  ( 2 - 1 ) = 1
51 50 oveq1i 
 |-  ( ( 2 - 1 ) / 2 ) = ( 1 / 2 )
52 2cn 
 |-  2 e. CC
53 52 subidi 
 |-  ( 2 - 2 ) = 0
54 53 fveq2i 
 |-  ( I ` ( 2 - 2 ) ) = ( I ` 0 )
55 47 simp1i 
 |-  ( I ` 0 ) = _pi
56 54 55 eqtri 
 |-  ( I ` ( 2 - 2 ) ) = _pi
57 51 56 oveq12i 
 |-  ( ( ( 2 - 1 ) / 2 ) x. ( I ` ( 2 - 2 ) ) ) = ( ( 1 / 2 ) x. _pi )
58 ax-1cn 
 |-  1 e. CC
59 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
60 picn 
 |-  _pi e. CC
61 div32 
 |-  ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ _pi e. CC ) -> ( ( 1 / 2 ) x. _pi ) = ( 1 x. ( _pi / 2 ) ) )
62 58 59 60 61 mp3an 
 |-  ( ( 1 / 2 ) x. _pi ) = ( 1 x. ( _pi / 2 ) )
63 2ne0 
 |-  2 =/= 0
64 60 52 63 divcli 
 |-  ( _pi / 2 ) e. CC
65 64 mullidi 
 |-  ( 1 x. ( _pi / 2 ) ) = ( _pi / 2 )
66 62 65 eqtri 
 |-  ( ( 1 / 2 ) x. _pi ) = ( _pi / 2 )
67 49 57 66 3eqtri 
 |-  ( I ` 2 ) = ( _pi / 2 )
68 3z 
 |-  3 e. ZZ
69 2re 
 |-  2 e. RR
70 3re 
 |-  3 e. RR
71 2lt3 
 |-  2 < 3
72 69 70 71 ltleii 
 |-  2 <_ 3
73 eluz2 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 3 e. ZZ /\ 2 <_ 3 ) )
74 44 68 72 73 mpbir3an 
 |-  3 e. ( ZZ>= ` 2 )
75 2 wallispilem2 
 |-  ( ( I ` 0 ) = _pi /\ ( I ` 1 ) = 2 /\ ( 3 e. ( ZZ>= ` 2 ) -> ( I ` 3 ) = ( ( ( 3 - 1 ) / 3 ) x. ( I ` ( 3 - 2 ) ) ) ) )
76 75 simp3i 
 |-  ( 3 e. ( ZZ>= ` 2 ) -> ( I ` 3 ) = ( ( ( 3 - 1 ) / 3 ) x. ( I ` ( 3 - 2 ) ) ) )
77 74 76 ax-mp 
 |-  ( I ` 3 ) = ( ( ( 3 - 1 ) / 3 ) x. ( I ` ( 3 - 2 ) ) )
78 3m1e2 
 |-  ( 3 - 1 ) = 2
79 78 eqcomi 
 |-  2 = ( 3 - 1 )
80 79 oveq1i 
 |-  ( 2 / 3 ) = ( ( 3 - 1 ) / 3 )
81 3cn 
 |-  3 e. CC
82 81 52 58 40 subaddrii 
 |-  ( 3 - 2 ) = 1
83 82 fveq2i 
 |-  ( I ` ( 3 - 2 ) ) = ( I ` 1 )
84 47 simp2i 
 |-  ( I ` 1 ) = 2
85 83 84 eqtr2i 
 |-  2 = ( I ` ( 3 - 2 ) )
86 80 85 oveq12i 
 |-  ( ( 2 / 3 ) x. 2 ) = ( ( ( 3 - 1 ) / 3 ) x. ( I ` ( 3 - 2 ) ) )
87 3ne0 
 |-  3 =/= 0
88 52 81 87 divcli 
 |-  ( 2 / 3 ) e. CC
89 88 52 mulcomi 
 |-  ( ( 2 / 3 ) x. 2 ) = ( 2 x. ( 2 / 3 ) )
90 77 86 89 3eqtr2i 
 |-  ( I ` 3 ) = ( 2 x. ( 2 / 3 ) )
91 67 90 oveq12i 
 |-  ( ( I ` 2 ) / ( I ` 3 ) ) = ( ( _pi / 2 ) / ( 2 x. ( 2 / 3 ) ) )
92 1z 
 |-  1 e. ZZ
93 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 ) )
94 92 93 ax-mp 
 |-  ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 )
95 1nn 
 |-  1 e. NN
96 oveq2 
 |-  ( k = 1 -> ( 2 x. k ) = ( 2 x. 1 ) )
97 96 37 eqtrdi 
 |-  ( k = 1 -> ( 2 x. k ) = 2 )
98 96 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. 1 ) - 1 ) )
99 37 oveq1i 
 |-  ( ( 2 x. 1 ) - 1 ) = ( 2 - 1 )
100 99 50 eqtri 
 |-  ( ( 2 x. 1 ) - 1 ) = 1
101 98 100 eqtrdi 
 |-  ( k = 1 -> ( ( 2 x. k ) - 1 ) = 1 )
102 97 101 oveq12d 
 |-  ( k = 1 -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = ( 2 / 1 ) )
103 52 div1i 
 |-  ( 2 / 1 ) = 2
104 102 103 eqtrdi 
 |-  ( k = 1 -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = 2 )
105 97 oveq1d 
 |-  ( k = 1 -> ( ( 2 x. k ) + 1 ) = ( 2 + 1 ) )
106 105 40 eqtrdi 
 |-  ( k = 1 -> ( ( 2 x. k ) + 1 ) = 3 )
107 97 106 oveq12d 
 |-  ( k = 1 -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) = ( 2 / 3 ) )
108 104 107 oveq12d 
 |-  ( k = 1 -> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) = ( 2 x. ( 2 / 3 ) ) )
109 ovex 
 |-  ( 2 x. ( 2 / 3 ) ) e. _V
110 108 1 109 fvmpt 
 |-  ( 1 e. NN -> ( F ` 1 ) = ( 2 x. ( 2 / 3 ) ) )
111 95 110 ax-mp 
 |-  ( F ` 1 ) = ( 2 x. ( 2 / 3 ) )
112 94 111 eqtr2i 
 |-  ( 2 x. ( 2 / 3 ) ) = ( seq 1 ( x. , F ) ` 1 )
113 112 oveq2i 
 |-  ( ( _pi / 2 ) / ( 2 x. ( 2 / 3 ) ) ) = ( ( _pi / 2 ) / ( seq 1 ( x. , F ) ` 1 ) )
114 52 88 mulcli 
 |-  ( 2 x. ( 2 / 3 ) ) e. CC
115 111 114 eqeltri 
 |-  ( F ` 1 ) e. CC
116 94 115 eqeltri 
 |-  ( seq 1 ( x. , F ) ` 1 ) e. CC
117 52 81 63 87 divne0i 
 |-  ( 2 / 3 ) =/= 0
118 52 88 63 117 mulne0i 
 |-  ( 2 x. ( 2 / 3 ) ) =/= 0
119 112 118 eqnetrri 
 |-  ( seq 1 ( x. , F ) ` 1 ) =/= 0
120 64 116 119 divreci 
 |-  ( ( _pi / 2 ) / ( seq 1 ( x. , F ) ` 1 ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` 1 ) ) )
121 113 120 eqtri 
 |-  ( ( _pi / 2 ) / ( 2 x. ( 2 / 3 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` 1 ) ) )
122 43 91 121 3eqtri 
 |-  ( ( I ` ( 2 x. 1 ) ) / ( I ` ( ( 2 x. 1 ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` 1 ) ) )
123 oveq2 
 |-  ( ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) -> ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
124 123 adantl 
 |-  ( ( y e. NN /\ ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) -> ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
125 2cnd 
 |-  ( y e. NN -> 2 e. CC )
126 nncn 
 |-  ( y e. NN -> y e. CC )
127 58 a1i 
 |-  ( y e. NN -> 1 e. CC )
128 125 126 127 adddid 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
129 125 mulridd 
 |-  ( y e. NN -> ( 2 x. 1 ) = 2 )
130 129 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 2 x. 1 ) ) = ( ( 2 x. y ) + 2 ) )
131 128 130 eqtrd 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + 2 ) )
132 131 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( ( 2 x. y ) + 2 ) - 1 ) )
133 125 126 mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. CC )
134 133 125 127 addsubassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 2 ) - 1 ) = ( ( 2 x. y ) + ( 2 - 1 ) ) )
135 50 a1i 
 |-  ( y e. NN -> ( 2 - 1 ) = 1 )
136 135 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 2 - 1 ) ) = ( ( 2 x. y ) + 1 ) )
137 132 134 136 3eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) = ( ( 2 x. y ) + 1 ) )
138 137 oveq1d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) = ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) )
139 138 oveq1d 
 |-  ( y e. NN -> ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) = ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) )
140 78 a1i 
 |-  ( y e. NN -> ( 3 - 1 ) = 2 )
141 140 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 3 - 1 ) ) = ( ( 2 x. y ) + 2 ) )
142 81 a1i 
 |-  ( y e. NN -> 3 e. CC )
143 133 142 127 addsubassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 3 ) - 1 ) = ( ( 2 x. y ) + ( 3 - 1 ) ) )
144 141 143 131 3eqtr4d 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 3 ) - 1 ) = ( 2 x. ( y + 1 ) ) )
145 144 oveq1d 
 |-  ( y e. NN -> ( ( ( ( 2 x. y ) + 3 ) - 1 ) / ( ( 2 x. y ) + 3 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) )
146 145 oveq1d 
 |-  ( y e. NN -> ( ( ( ( ( 2 x. y ) + 3 ) - 1 ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) = ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) )
147 139 146 oveq12d 
 |-  ( y e. NN -> ( ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) / ( ( ( ( ( 2 x. y ) + 3 ) - 1 ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) )
148 44 a1i 
 |-  ( y e. NN -> 2 e. ZZ )
149 nnz 
 |-  ( y e. NN -> y e. ZZ )
150 149 peano2zd 
 |-  ( y e. NN -> ( y + 1 ) e. ZZ )
151 148 150 zmulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. ZZ )
152 69 a1i 
 |-  ( y e. NN -> 2 e. RR )
153 nnre 
 |-  ( y e. NN -> y e. RR )
154 1red 
 |-  ( y e. NN -> 1 e. RR )
155 153 154 readdcld 
 |-  ( y e. NN -> ( y + 1 ) e. RR )
156 0le2 
 |-  0 <_ 2
157 156 a1i 
 |-  ( y e. NN -> 0 <_ 2 )
158 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
159 158 nn0ge0d 
 |-  ( y e. NN -> 0 <_ y )
160 154 153 addge02d 
 |-  ( y e. NN -> ( 0 <_ y <-> 1 <_ ( y + 1 ) ) )
161 159 160 mpbid 
 |-  ( y e. NN -> 1 <_ ( y + 1 ) )
162 152 155 157 161 lemulge11d 
 |-  ( y e. NN -> 2 <_ ( 2 x. ( y + 1 ) ) )
163 44 eluz1i 
 |-  ( ( 2 x. ( y + 1 ) ) e. ( ZZ>= ` 2 ) <-> ( ( 2 x. ( y + 1 ) ) e. ZZ /\ 2 <_ ( 2 x. ( y + 1 ) ) ) )
164 151 162 163 sylanbrc 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. ( ZZ>= ` 2 ) )
165 2 164 itgsinexp 
 |-  ( y e. NN -> ( I ` ( 2 x. ( y + 1 ) ) ) = ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( ( 2 x. ( y + 1 ) ) - 2 ) ) ) )
166 131 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 2 ) = ( ( ( 2 x. y ) + 2 ) - 2 ) )
167 133 125 pncand 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 2 ) - 2 ) = ( 2 x. y ) )
168 166 167 eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 2 ) = ( 2 x. y ) )
169 168 fveq2d 
 |-  ( y e. NN -> ( I ` ( ( 2 x. ( y + 1 ) ) - 2 ) ) = ( I ` ( 2 x. y ) ) )
170 169 oveq2d 
 |-  ( y e. NN -> ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( ( 2 x. ( y + 1 ) ) - 2 ) ) ) = ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) )
171 165 170 eqtrd 
 |-  ( y e. NN -> ( I ` ( 2 x. ( y + 1 ) ) ) = ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) )
172 131 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) = ( ( ( 2 x. y ) + 2 ) + 1 ) )
173 133 125 127 addassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 2 ) + 1 ) = ( ( 2 x. y ) + ( 2 + 1 ) ) )
174 40 a1i 
 |-  ( y e. NN -> ( 2 + 1 ) = 3 )
175 174 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 2 + 1 ) ) = ( ( 2 x. y ) + 3 ) )
176 172 173 175 3eqtrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) = ( ( 2 x. y ) + 3 ) )
177 176 fveq2d 
 |-  ( y e. NN -> ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) = ( I ` ( ( 2 x. y ) + 3 ) ) )
178 148 149 zmulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. ZZ )
179 68 a1i 
 |-  ( y e. NN -> 3 e. ZZ )
180 178 179 zaddcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 3 ) e. ZZ )
181 152 153 remulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. RR )
182 70 a1i 
 |-  ( y e. NN -> 3 e. RR )
183 181 182 readdcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 3 ) e. RR )
184 nnge1 
 |-  ( y e. NN -> 1 <_ y )
185 152 153 157 184 lemulge11d 
 |-  ( y e. NN -> 2 <_ ( 2 x. y ) )
186 0re 
 |-  0 e. RR
187 3pos 
 |-  0 < 3
188 186 70 187 ltleii 
 |-  0 <_ 3
189 181 182 addge01d 
 |-  ( y e. NN -> ( 0 <_ 3 <-> ( 2 x. y ) <_ ( ( 2 x. y ) + 3 ) ) )
190 188 189 mpbii 
 |-  ( y e. NN -> ( 2 x. y ) <_ ( ( 2 x. y ) + 3 ) )
191 152 181 183 185 190 letrd 
 |-  ( y e. NN -> 2 <_ ( ( 2 x. y ) + 3 ) )
192 44 eluz1i 
 |-  ( ( ( 2 x. y ) + 3 ) e. ( ZZ>= ` 2 ) <-> ( ( ( 2 x. y ) + 3 ) e. ZZ /\ 2 <_ ( ( 2 x. y ) + 3 ) ) )
193 180 191 192 sylanbrc 
 |-  ( y e. NN -> ( ( 2 x. y ) + 3 ) e. ( ZZ>= ` 2 ) )
194 2 193 itgsinexp 
 |-  ( y e. NN -> ( I ` ( ( 2 x. y ) + 3 ) ) = ( ( ( ( ( 2 x. y ) + 3 ) - 1 ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) )
195 177 194 eqtrd 
 |-  ( y e. NN -> ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) = ( ( ( ( ( 2 x. y ) + 3 ) - 1 ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) )
196 171 195 oveq12d 
 |-  ( y e. NN -> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 x. ( y + 1 ) ) - 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) / ( ( ( ( ( 2 x. y ) + 3 ) - 1 ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) )
197 133 127 addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. CC )
198 126 127 addcld 
 |-  ( y e. NN -> ( y + 1 ) e. CC )
199 125 198 mulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. CC )
200 63 a1i 
 |-  ( y e. NN -> 2 =/= 0 )
201 peano2nn 
 |-  ( y e. NN -> ( y + 1 ) e. NN )
202 201 nnne0d 
 |-  ( y e. NN -> ( y + 1 ) =/= 0 )
203 125 198 200 202 mulne0d 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 0 )
204 197 199 203 divcld 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) e. CC )
205 2nn0 
 |-  2 e. NN0
206 205 a1i 
 |-  ( y e. NN -> 2 e. NN0 )
207 206 158 nn0mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. NN0 )
208 2 wallispilem3 
 |-  ( ( 2 x. y ) e. NN0 -> ( I ` ( 2 x. y ) ) e. RR+ )
209 208 rpcnd 
 |-  ( ( 2 x. y ) e. NN0 -> ( I ` ( 2 x. y ) ) e. CC )
210 207 209 syl 
 |-  ( y e. NN -> ( I ` ( 2 x. y ) ) e. CC )
211 133 142 addcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 3 ) e. CC )
212 0red 
 |-  ( y e. NN -> 0 e. RR )
213 2pos 
 |-  0 < 2
214 213 a1i 
 |-  ( y e. NN -> 0 < 2 )
215 nngt0 
 |-  ( y e. NN -> 0 < y )
216 152 153 214 215 mulgt0d 
 |-  ( y e. NN -> 0 < ( 2 x. y ) )
217 182 187 jctir 
 |-  ( y e. NN -> ( 3 e. RR /\ 0 < 3 ) )
218 elrp 
 |-  ( 3 e. RR+ <-> ( 3 e. RR /\ 0 < 3 ) )
219 217 218 sylibr 
 |-  ( y e. NN -> 3 e. RR+ )
220 181 219 ltaddrpd 
 |-  ( y e. NN -> ( 2 x. y ) < ( ( 2 x. y ) + 3 ) )
221 212 181 183 216 220 lttrd 
 |-  ( y e. NN -> 0 < ( ( 2 x. y ) + 3 ) )
222 221 gt0ne0d 
 |-  ( y e. NN -> ( ( 2 x. y ) + 3 ) =/= 0 )
223 199 211 222 divcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) e. CC )
224 199 211 203 222 divne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) =/= 0 )
225 180 148 zsubcld 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 3 ) - 2 ) e. ZZ )
226 183 152 subge0d 
 |-  ( y e. NN -> ( 0 <_ ( ( ( 2 x. y ) + 3 ) - 2 ) <-> 2 <_ ( ( 2 x. y ) + 3 ) ) )
227 191 226 mpbird 
 |-  ( y e. NN -> 0 <_ ( ( ( 2 x. y ) + 3 ) - 2 ) )
228 elnn0z 
 |-  ( ( ( ( 2 x. y ) + 3 ) - 2 ) e. NN0 <-> ( ( ( ( 2 x. y ) + 3 ) - 2 ) e. ZZ /\ 0 <_ ( ( ( 2 x. y ) + 3 ) - 2 ) ) )
229 225 227 228 sylanbrc 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 3 ) - 2 ) e. NN0 )
230 2 wallispilem3 
 |-  ( ( ( ( 2 x. y ) + 3 ) - 2 ) e. NN0 -> ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) e. RR+ )
231 229 230 syl 
 |-  ( y e. NN -> ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) e. RR+ )
232 231 rpcnne0d 
 |-  ( y e. NN -> ( ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) e. CC /\ ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) =/= 0 ) )
233 223 224 232 jca31 
 |-  ( y e. NN -> ( ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) e. CC /\ ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) =/= 0 ) /\ ( ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) e. CC /\ ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) =/= 0 ) ) )
234 divmuldiv 
 |-  ( ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) e. CC /\ ( I ` ( 2 x. y ) ) e. CC ) /\ ( ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) e. CC /\ ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) =/= 0 ) /\ ( ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) e. CC /\ ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) =/= 0 ) ) ) -> ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) )
235 204 210 233 234 syl21anc 
 |-  ( y e. NN -> ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) x. ( I ` ( 2 x. y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) x. ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) )
236 147 196 235 3eqtr4d 
 |-  ( y e. NN -> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) )
237 133 142 125 addsubassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 3 ) - 2 ) = ( ( 2 x. y ) + ( 3 - 2 ) ) )
238 82 a1i 
 |-  ( y e. NN -> ( 3 - 2 ) = 1 )
239 238 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 3 - 2 ) ) = ( ( 2 x. y ) + 1 ) )
240 237 239 eqtrd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 3 ) - 2 ) = ( ( 2 x. y ) + 1 ) )
241 240 fveq2d 
 |-  ( y e. NN -> ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) = ( I ` ( ( 2 x. y ) + 1 ) ) )
242 241 oveq2d 
 |-  ( y e. NN -> ( ( I ` ( 2 x. y ) ) / ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) = ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) )
243 242 oveq2d 
 |-  ( y e. NN -> ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( ( 2 x. y ) + 3 ) - 2 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) ) )
244 236 243 eqtrd 
 |-  ( y e. NN -> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) ) )
245 244 adantr 
 |-  ( ( y e. NN /\ ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) -> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) ) )
246 elnnuz 
 |-  ( y e. NN <-> y e. ( ZZ>= ` 1 ) )
247 246 biimpi 
 |-  ( y e. NN -> y e. ( ZZ>= ` 1 ) )
248 seqp1 
 |-  ( y e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , F ) ` ( y + 1 ) ) = ( ( seq 1 ( x. , F ) ` y ) x. ( F ` ( y + 1 ) ) ) )
249 247 248 syl 
 |-  ( y e. NN -> ( seq 1 ( x. , F ) ` ( y + 1 ) ) = ( ( seq 1 ( x. , F ) ` y ) x. ( F ` ( y + 1 ) ) ) )
250 oveq2 
 |-  ( k = ( y + 1 ) -> ( 2 x. k ) = ( 2 x. ( y + 1 ) ) )
251 250 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. ( y + 1 ) ) - 1 ) )
252 250 251 oveq12d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) )
253 250 oveq1d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. ( y + 1 ) ) + 1 ) )
254 250 253 oveq12d 
 |-  ( k = ( y + 1 ) -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) )
255 252 254 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 ) ) ) )
256 152 155 remulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. RR )
257 256 154 resubcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) e. RR )
258 1lt2 
 |-  1 < 2
259 258 a1i 
 |-  ( y e. NN -> 1 < 2 )
260 nnrp 
 |-  ( y e. NN -> y e. RR+ )
261 154 260 ltaddrp2d 
 |-  ( y e. NN -> 1 < ( y + 1 ) )
262 152 155 259 261 mulgt1d 
 |-  ( y e. NN -> 1 < ( 2 x. ( y + 1 ) ) )
263 154 262 gtned 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) =/= 1 )
264 199 127 263 subne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) - 1 ) =/= 0 )
265 256 257 264 redivcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) e. RR )
266 176 183 eqeltrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) e. RR )
267 176 222 eqnetrd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) + 1 ) =/= 0 )
268 256 266 267 redivcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) e. RR )
269 265 268 remulcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) e. RR )
270 1 255 201 269 fvmptd3 
 |-  ( y e. NN -> ( F ` ( y + 1 ) ) = ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) )
271 270 oveq2d 
 |-  ( y e. NN -> ( ( seq 1 ( x. , F ) ` y ) x. ( F ` ( y + 1 ) ) ) = ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) )
272 249 271 eqtrd 
 |-  ( y e. NN -> ( seq 1 ( x. , F ) ` ( y + 1 ) ) = ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) )
273 272 oveq2d 
 |-  ( y e. NN -> ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) = ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) ) )
274 273 oveq2d 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) ) ) )
275 137 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) )
276 176 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) = ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) )
277 275 276 oveq12d 
 |-  ( 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 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) )
278 277 oveq2d 
 |-  ( y e. NN -> ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) = ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) )
279 278 oveq2d 
 |-  ( y e. NN -> ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) ) = ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) )
280 279 oveq2d 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) ) )
281 elfznn 
 |-  ( w e. ( 1 ... y ) -> w e. NN )
282 281 adantl 
 |-  ( ( y e. NN /\ w e. ( 1 ... y ) ) -> w e. NN )
283 oveq2 
 |-  ( k = w -> ( 2 x. k ) = ( 2 x. w ) )
284 283 oveq1d 
 |-  ( k = w -> ( ( 2 x. k ) - 1 ) = ( ( 2 x. w ) - 1 ) )
285 283 284 oveq12d 
 |-  ( k = w -> ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) = ( ( 2 x. w ) / ( ( 2 x. w ) - 1 ) ) )
286 283 oveq1d 
 |-  ( k = w -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. w ) + 1 ) )
287 283 286 oveq12d 
 |-  ( k = w -> ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) = ( ( 2 x. w ) / ( ( 2 x. w ) + 1 ) ) )
288 285 287 oveq12d 
 |-  ( k = w -> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) = ( ( ( 2 x. w ) / ( ( 2 x. w ) - 1 ) ) x. ( ( 2 x. w ) / ( ( 2 x. w ) + 1 ) ) ) )
289 id 
 |-  ( w e. NN -> w e. NN )
290 2rp 
 |-  2 e. RR+
291 290 a1i 
 |-  ( w e. NN -> 2 e. RR+ )
292 nnrp 
 |-  ( w e. NN -> w e. RR+ )
293 291 292 rpmulcld 
 |-  ( w e. NN -> ( 2 x. w ) e. RR+ )
294 69 a1i 
 |-  ( w e. NN -> 2 e. RR )
295 nnre 
 |-  ( w e. NN -> w e. RR )
296 294 295 remulcld 
 |-  ( w e. NN -> ( 2 x. w ) e. RR )
297 1red 
 |-  ( w e. NN -> 1 e. RR )
298 296 297 resubcld 
 |-  ( w e. NN -> ( ( 2 x. w ) - 1 ) e. RR )
299 nnge1 
 |-  ( w e. NN -> 1 <_ w )
300 nncn 
 |-  ( w e. NN -> w e. CC )
301 300 mullidd 
 |-  ( w e. NN -> ( 1 x. w ) = w )
302 297 294 292 ltmul1d 
 |-  ( w e. NN -> ( 1 < 2 <-> ( 1 x. w ) < ( 2 x. w ) ) )
303 258 302 mpbii 
 |-  ( w e. NN -> ( 1 x. w ) < ( 2 x. w ) )
304 301 303 eqbrtrrd 
 |-  ( w e. NN -> w < ( 2 x. w ) )
305 297 295 296 299 304 lelttrd 
 |-  ( w e. NN -> 1 < ( 2 x. w ) )
306 297 296 posdifd 
 |-  ( w e. NN -> ( 1 < ( 2 x. w ) <-> 0 < ( ( 2 x. w ) - 1 ) ) )
307 305 306 mpbid 
 |-  ( w e. NN -> 0 < ( ( 2 x. w ) - 1 ) )
308 298 307 elrpd 
 |-  ( w e. NN -> ( ( 2 x. w ) - 1 ) e. RR+ )
309 293 308 rpdivcld 
 |-  ( w e. NN -> ( ( 2 x. w ) / ( ( 2 x. w ) - 1 ) ) e. RR+ )
310 156 a1i 
 |-  ( w e. NN -> 0 <_ 2 )
311 292 rpge0d 
 |-  ( w e. NN -> 0 <_ w )
312 294 295 310 311 mulge0d 
 |-  ( w e. NN -> 0 <_ ( 2 x. w ) )
313 296 312 ge0p1rpd 
 |-  ( w e. NN -> ( ( 2 x. w ) + 1 ) e. RR+ )
314 293 313 rpdivcld 
 |-  ( w e. NN -> ( ( 2 x. w ) / ( ( 2 x. w ) + 1 ) ) e. RR+ )
315 309 314 rpmulcld 
 |-  ( w e. NN -> ( ( ( 2 x. w ) / ( ( 2 x. w ) - 1 ) ) x. ( ( 2 x. w ) / ( ( 2 x. w ) + 1 ) ) ) e. RR+ )
316 1 288 289 315 fvmptd3 
 |-  ( w e. NN -> ( F ` w ) = ( ( ( 2 x. w ) / ( ( 2 x. w ) - 1 ) ) x. ( ( 2 x. w ) / ( ( 2 x. w ) + 1 ) ) ) )
317 316 315 eqeltrd 
 |-  ( w e. NN -> ( F ` w ) e. RR+ )
318 282 317 syl 
 |-  ( ( y e. NN /\ w e. ( 1 ... y ) ) -> ( F ` w ) e. RR+ )
319 rpmulcl 
 |-  ( ( w e. RR+ /\ z e. RR+ ) -> ( w x. z ) e. RR+ )
320 319 adantl 
 |-  ( ( y e. NN /\ ( w e. RR+ /\ z e. RR+ ) ) -> ( w x. z ) e. RR+ )
321 247 318 320 seqcl 
 |-  ( y e. NN -> ( seq 1 ( x. , F ) ` y ) e. RR+ )
322 321 rpcnne0d 
 |-  ( y e. NN -> ( ( seq 1 ( x. , F ) ` y ) e. CC /\ ( seq 1 ( x. , F ) ` y ) =/= 0 ) )
323 290 a1i 
 |-  ( y e. NN -> 2 e. RR+ )
324 153 159 ge0p1rpd 
 |-  ( y e. NN -> ( y + 1 ) e. RR+ )
325 323 324 rpmulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. RR+ )
326 152 153 157 159 mulge0d 
 |-  ( y e. NN -> 0 <_ ( 2 x. y ) )
327 181 326 ge0p1rpd 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. RR+ )
328 325 327 rpdivcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) e. RR+ )
329 323 260 rpmulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. RR+ )
330 329 219 rpaddcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 3 ) e. RR+ )
331 325 330 rpdivcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) e. RR+ )
332 328 331 rpmulcld 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) e. RR+ )
333 332 rpcnne0d 
 |-  ( y e. NN -> ( ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) e. CC /\ ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) =/= 0 ) )
334 divdiv1 
 |-  ( ( 1 e. CC /\ ( ( seq 1 ( x. , F ) ` y ) e. CC /\ ( seq 1 ( x. , F ) ` y ) =/= 0 ) /\ ( ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) e. CC /\ ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) =/= 0 ) ) -> ( ( 1 / ( seq 1 ( x. , F ) ` y ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) = ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) )
335 127 322 333 334 syl3anc 
 |-  ( y e. NN -> ( ( 1 / ( seq 1 ( x. , F ) ` y ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) = ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) )
336 335 eqcomd 
 |-  ( y e. NN -> ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) = ( ( 1 / ( seq 1 ( x. , F ) ` y ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) )
337 336 oveq2d 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) ) = ( ( _pi / 2 ) x. ( ( 1 / ( seq 1 ( x. , F ) ` y ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) )
338 64 a1i 
 |-  ( y e. NN -> ( _pi / 2 ) e. CC )
339 321 rpcnd 
 |-  ( y e. NN -> ( seq 1 ( x. , F ) ` y ) e. CC )
340 321 rpne0d 
 |-  ( y e. NN -> ( seq 1 ( x. , F ) ` y ) =/= 0 )
341 339 340 reccld 
 |-  ( y e. NN -> ( 1 / ( seq 1 ( x. , F ) ` y ) ) e. CC )
342 332 rpcnd 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) e. CC )
343 332 rpne0d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) =/= 0 )
344 338 341 342 343 divassd 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) = ( ( _pi / 2 ) x. ( ( 1 / ( seq 1 ( x. , F ) ` y ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) )
345 137 264 eqnetrrd 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) =/= 0 )
346 199 197 199 211 345 222 divmuldivd 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) = ( ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) / ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) ) )
347 346 oveq2d 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) = ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) / ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) ) ) )
348 338 341 mulcld 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) e. CC )
349 199 199 mulcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) e. CC )
350 197 211 mulcld 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) e. CC )
351 199 199 203 203 mulne0d 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) =/= 0 )
352 197 211 345 222 mulne0d 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) =/= 0 )
353 348 349 350 351 352 divdiv2d 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) / ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) ) ) = ( ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) )
354 348 350 349 351 divassd 
 |-  ( y e. NN -> ( ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) = ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) ) )
355 353 354 eqtrd 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) / ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) ) ) = ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) ) )
356 197 199 199 211 203 222 203 divdivdivd 
 |-  ( y e. NN -> ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) = ( ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) )
357 356 eqcomd 
 |-  ( y e. NN -> ( ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) = ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) )
358 357 oveq2d 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) x. ( ( 2 x. y ) + 3 ) ) / ( ( 2 x. ( y + 1 ) ) x. ( 2 x. ( y + 1 ) ) ) ) ) = ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) )
359 347 355 358 3eqtrd 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) / ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) = ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) )
360 337 344 359 3eqtr2d 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) ) ) = ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) )
361 60 a1i 
 |-  ( y e. NN -> _pi e. CC )
362 361 halfcld 
 |-  ( y e. NN -> ( _pi / 2 ) e. CC )
363 362 341 mulcld 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) e. CC )
364 204 223 224 divcld 
 |-  ( y e. NN -> ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) e. CC )
365 363 364 mulcomd 
 |-  ( y e. NN -> ( ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) x. ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
366 280 360 365 3eqtrd 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( ( seq 1 ( x. , F ) ` y ) x. ( ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) - 1 ) ) x. ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
367 274 366 eqtrd 
 |-  ( y e. NN -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
368 367 adantr 
 |-  ( ( y e. NN /\ ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) -> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) = ( ( ( ( ( 2 x. y ) + 1 ) / ( 2 x. ( y + 1 ) ) ) / ( ( 2 x. ( y + 1 ) ) / ( ( 2 x. y ) + 3 ) ) ) x. ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) )
369 124 245 368 3eqtr4d 
 |-  ( ( y e. NN /\ ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) ) -> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) )
370 369 ex 
 |-  ( y e. NN -> ( ( ( I ` ( 2 x. y ) ) / ( I ` ( ( 2 x. y ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` y ) ) ) -> ( ( I ` ( 2 x. ( y + 1 ) ) ) / ( I ` ( ( 2 x. ( y + 1 ) ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` ( y + 1 ) ) ) ) ) )
371 12 20 28 36 122 370 nnind 
 |-  ( n e. NN -> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) = ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
372 371 mpteq2ia 
 |-  ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN |-> ( ( _pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )
373 372 3 4 3eqtr4i 
 |-  G = H