Theorem wallispi2lem1

Description: An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017)

	Ref	Expression
Assertion	wallispi2lem1	⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) ‘ 𝑁 ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑁 ) ) )

Proof

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