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	$⊢ N \in ℕ \to seq 1 (\times (k \in ℕ ⟼ (\frac{2 k}{2 k - 1}) (\frac{2 k}{2 k + 1}))) (N) = (\frac{1}{2 \cdot N + 1}) seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (N)$

Proof

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

Metamath Proof Explorer

Theorem wallispi2lem1

Proof