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

Metamath Proof Explorer

Theorem wallispilem4

Proof