wallispi2lem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wallispi2lem1		Structured version Visualization version GIF version

Theorem wallispi2lem1 43502

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.)

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

Proof of Theorem wallispi2lem1 Dummy variables 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6756	. . 3 ⊢ (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1))
2		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
3	2	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 1 → ((2 · 𝑥) + 1) = ((2 · 1) + 1))
4	3	oveq2d 7271	. . . 4 ⊢ (𝑥 = 1 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 1) + 1)))
5		fveq2 6756	. . . 4 ⊢ (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
6	4, 5	oveq12d 7273	. . 3 ⊢ (𝑥 = 1 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)))
7	1, 6	eqeq12d 2754	. 2 ⊢ (𝑥 = 1 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))))
8		fveq2 6756	. . 3 ⊢ (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦))
9		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
10	9	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 𝑦 → ((2 · 𝑥) + 1) = ((2 · 𝑦) + 1))
11	10	oveq2d 7271	. . . 4 ⊢ (𝑥 = 𝑦 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑦) + 1)))
12		fveq2 6756	. . . 4 ⊢ (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
13	11, 12	oveq12d 7273	. . 3 ⊢ (𝑥 = 𝑦 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
14	8, 13	eqeq12d 2754	. 2 ⊢ (𝑥 = 𝑦 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))))
15		fveq2 6756	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)))
16		oveq2 7263	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
17	16	oveq1d 7270	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((2 · 𝑥) + 1) = ((2 · (𝑦 + 1)) + 1))
18	17	oveq2d 7271	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · (𝑦 + 1)) + 1)))
19		fveq2 6756	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
20	18, 19	oveq12d 7273	. . 3 ⊢ (𝑥 = (𝑦 + 1) → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
21	15, 20	eqeq12d 2754	. 2 ⊢ (𝑥 = (𝑦 + 1) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))))
22		fveq2 6756	. . 3 ⊢ (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁))
23		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
24	23	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2 · 𝑥) + 1) = ((2 · 𝑁) + 1))
25	24	oveq2d 7271	. . . 4 ⊢ (𝑥 = 𝑁 → (1 / ((2 · 𝑥) + 1)) = (1 / ((2 · 𝑁) + 1)))
26		fveq2 6756	. . . 4 ⊢ (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
27	25, 26	oveq12d 7273	. . 3 ⊢ (𝑥 = 𝑁 → ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))
28	22, 27	eqeq12d 2754	. 2 ⊢ (𝑥 = 𝑁 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑥) = ((1 / ((2 · 𝑥) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))))
29		1z 12280	. . . 4 ⊢ 1 ∈ ℤ
30		seq1 13662	. . . 4 ⊢ (1 ∈ ℤ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1))
31	29, 30	ax-mp 5	. . 3 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1)
32		1nn 11914	. . . 4 ⊢ 1 ∈ ℕ
33		oveq2 7263	. . . . . . 7 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
34	33	oveq1d 7270	. . . . . . 7 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
35	33, 34	oveq12d 7273	. . . . . 6 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 1) / ((2 · 1) − 1)))
36	33	oveq1d 7270	. . . . . . 7 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = ((2 · 1) + 1))
37	33, 36	oveq12d 7273	. . . . . 6 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 1) / ((2 · 1) + 1)))
38	35, 37	oveq12d 7273	. . . . 5 ⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
39		eqid 2738	. . . . 5 ⊢ (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
40		ovex 7288	. . . . 5 ⊢ (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) ∈ V
41	38, 39, 40	fvmpt 6857	. . . 4 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))))
42	32, 41	ax-mp 5	. . 3 ⊢ ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘1) = (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1)))
43		2t1e2 12066	. . . . . . 7 ⊢ (2 · 1) = 2
44	43	oveq1i 7265	. . . . . . . 8 ⊢ ((2 · 1) − 1) = (2 − 1)
45		2m1e1 12029	. . . . . . . 8 ⊢ (2 − 1) = 1
46	44, 45	eqtri 2766	. . . . . . 7 ⊢ ((2 · 1) − 1) = 1
47	43, 46	oveq12i 7267	. . . . . 6 ⊢ ((2 · 1) / ((2 · 1) − 1)) = (2 / 1)
48	43	oveq1i 7265	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
49		2p1e3 12045	. . . . . . . 8 ⊢ (2 + 1) = 3
50	48, 49	eqtri 2766	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
51	43, 50	oveq12i 7267	. . . . . 6 ⊢ ((2 · 1) / ((2 · 1) + 1)) = (2 / 3)
52	47, 51	oveq12i 7267	. . . . 5 ⊢ (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((2 / 1) · (2 / 3))
53		2cn 11978	. . . . . 6 ⊢ 2 ∈ ℂ
54		ax-1cn 10860	. . . . . 6 ⊢ 1 ∈ ℂ
55		3cn 11984	. . . . . 6 ⊢ 3 ∈ ℂ
56		ax-1ne0 10871	. . . . . 6 ⊢ 1 ≠ 0
57		3ne0 12009	. . . . . 6 ⊢ 3 ≠ 0
58	53, 54, 53, 55, 56, 57	divmuldivi 11665	. . . . 5 ⊢ ((2 / 1) · (2 / 3)) = ((2 · 2) / (1 · 3))
59		2t2e4 12067	. . . . . 6 ⊢ (2 · 2) = 4
60	55	mulid2i 10911	. . . . . 6 ⊢ (1 · 3) = 3
61	59, 60	oveq12i 7267	. . . . 5 ⊢ ((2 · 2) / (1 · 3)) = (4 / 3)
62	52, 58, 61	3eqtri 2770	. . . 4 ⊢ (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = (4 / 3)
63		4cn 11988	. . . . 5 ⊢ 4 ∈ ℂ
64		divrec2 11580	. . . . 5 ⊢ ((4 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (4 / 3) = ((1 / 3) · 4))
65	63, 55, 57, 64	mp3an 1459	. . . 4 ⊢ (4 / 3) = ((1 / 3) · 4)
66	50	eqcomi 2747	. . . . . 6 ⊢ 3 = ((2 · 1) + 1)
67	66	oveq2i 7266	. . . . 5 ⊢ (1 / 3) = (1 / ((2 · 1) + 1))
68		seq1 13662	. . . . . . . 8 ⊢ (1 ∈ ℤ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1))
69	29, 68	ax-mp 5	. . . . . . 7 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1)
70	33	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
71	33, 34	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
72	71	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
73	70, 72	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
74		eqid 2738	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
75		ovex 7288	. . . . . . . . 9 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
76	73, 74, 75	fvmpt 6857	. . . . . . . 8 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
77	32, 76	ax-mp 5	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2))
78	43	oveq1i 7265	. . . . . . . . 9 ⊢ ((2 · 1)↑4) = (2↑4)
79	43, 46	oveq12i 7267	. . . . . . . . . . 11 ⊢ ((2 · 1) · ((2 · 1) − 1)) = (2 · 1)
80	79, 43	eqtri 2766	. . . . . . . . . 10 ⊢ ((2 · 1) · ((2 · 1) − 1)) = 2
81	80	oveq1i 7265	. . . . . . . . 9 ⊢ (((2 · 1) · ((2 · 1) − 1))↑2) = (2↑2)
82	78, 81	oveq12i 7267	. . . . . . . 8 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = ((2↑4) / (2↑2))
83		2exp4 16714	. . . . . . . . . 10 ⊢ (2↑4) = ;16
84		sq2 13842	. . . . . . . . . 10 ⊢ (2↑2) = 4
85	83, 84	oveq12i 7267	. . . . . . . . 9 ⊢ ((2↑4) / (2↑2)) = (;16 / 4)
86		4t4e16 12465	. . . . . . . . . . 11 ⊢ (4 · 4) = ;16
87	86	eqcomi 2747	. . . . . . . . . 10 ⊢ ;16 = (4 · 4)
88	87	oveq1i 7265	. . . . . . . . 9 ⊢ (;16 / 4) = ((4 · 4) / 4)
89		4ne0 12011	. . . . . . . . . 10 ⊢ 4 ≠ 0
90	63, 63, 89	divcan3i 11651	. . . . . . . . 9 ⊢ ((4 · 4) / 4) = 4
91	85, 88, 90	3eqtri 2770	. . . . . . . 8 ⊢ ((2↑4) / (2↑2)) = 4
92	82, 91	eqtri 2766	. . . . . . 7 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = 4
93	69, 77, 92	3eqtri 2770	. . . . . 6 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = 4
94	93	eqcomi 2747	. . . . 5 ⊢ 4 = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1)
95	67, 94	oveq12i 7267	. . . 4 ⊢ ((1 / 3) · 4) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
96	62, 65, 95	3eqtri 2770	. . 3 ⊢ (((2 · 1) / ((2 · 1) − 1)) · ((2 · 1) / ((2 · 1) + 1))) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
97	31, 42, 96	3eqtri 2770	. 2 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘1) = ((1 / ((2 · 1) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
98		elnnuz 12551	. . . . . . 7 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
99	98	biimpi 215	. . . . . 6 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘1))
100	99	adantr 480	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → 𝑦 ∈ (ℤ_≥‘1))
101		seqp1 13664	. . . . 5 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))))
102	100, 101	syl 17	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))))
103		simpr 484	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)))
104	103	oveq1d 7270	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))))
105		eqidd 2739	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))
106		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
107	106	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
108	106, 107	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
109	106	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
110	106, 109	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
111	108, 110	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
112	111	adantl 481	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
113		peano2nn 11915	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
114		2rp 12664	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ⁺
115	114	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ⁺)
116		nnre 11910	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
117		nnnn0 12170	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
118	117	nn0ge0d 12226	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 ≤ 𝑦)
119	116, 118	ge0p1rpd 12731	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ⁺)
120	115, 119	rpmulcld 12717	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ⁺)
121		2re 11977	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
122	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
123		1red 10907	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
124	116, 123	readdcld 10935	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
125	122, 124	remulcld 10936	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
126	125, 123	resubcld 11333	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
127		1lt2 12074	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
128	127	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 < 2)
129		nnrp 12670	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
130	123, 129	ltaddrp2d 12735	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
131	122, 124, 128, 130	mulgt1d 11841	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
132	123, 125	posdifd 11492	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (1 < (2 · (𝑦 + 1)) ↔ 0 < ((2 · (𝑦 + 1)) − 1)))
133	131, 132	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 0 < ((2 · (𝑦 + 1)) − 1))
134	126, 133	elrpd 12698	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ⁺)
135	120, 134	rpdivcld 12718	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ⁺)
136	115	rpge0d 12705	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 ≤ 2)
137		0le1 11428	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
138	137	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ 1)
139	116, 123, 118, 138	addge0d 11481	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 ≤ (𝑦 + 1))
140	122, 124, 136, 139	mulge0d 11482	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 0 ≤ (2 · (𝑦 + 1)))
141	125, 140	ge0p1rpd 12731	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ⁺)
142	120, 141	rpdivcld 12718	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ⁺)
143	135, 142	rpmulcld 12717	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ⁺)
144	105, 112, 113, 143	fvmptd 6864	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
145	144	oveq2d 7271	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
146	125	recnd 10934	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
147	126	recnd 10934	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
148	141	rpcnd 12703	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℂ)
149	133	gt0ne0d 11469	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
150	141	rpne0d 12706	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
151	146, 147, 146, 148, 149, 150	divmuldivd 11722	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
152	146, 146	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
153	152, 147, 148, 149, 150	divdiv1d 11712	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · (𝑦 + 1)) − 1) · ((2 · (𝑦 + 1)) + 1))))
154	146	sqvald 13789	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))
155	154	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) = ((2 · (𝑦 + 1))↑2))
156	155	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) = (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))
157	156	oveq1d 7270	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
158	151, 153, 157	3eqtr2d 2784	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)))
159	158	oveq2d 7271	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1))))
160	146	sqcld 13790	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ∈ ℂ)
161	160, 147, 149	divcld 11681	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
162	161, 148, 150	divrec2d 11685	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
163	162	oveq2d 7271	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1))) = (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))))
164		2cnd 11981	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
165		nncn 11911	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
166	164, 165	mulcld 10926	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
167		1cnd 10901	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
168	166, 167	addcld 10925	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
169		2nn 11976	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
170	169	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ)
171		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ)
172	170, 171	nnmulcld 11956	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ)
173	172	peano2nnd 11920	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ)
174	173	nnne0d 11953	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
175	168, 174	reccld 11674	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (1 / ((2 · 𝑦) + 1)) ∈ ℂ)
176		eqidd 2739	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
177		oveq2 7263	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
178	177	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → ((2 · 𝑘)↑4) = ((2 · 𝑥)↑4))
179	177	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑥 → ((2 · 𝑘) − 1) = ((2 · 𝑥) − 1))
180	177, 179	oveq12d 7273	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 𝑥) · ((2 · 𝑥) − 1)))
181	180	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2))
182	178, 181	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
183	182	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) ∧ 𝑘 = 𝑥) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
184		elfznn 13214	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...𝑦) → 𝑥 ∈ ℕ)
185	184	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → 𝑥 ∈ ℕ)
186	169	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℕ)
187		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
188	186, 187	nnmulcld 11956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℕ)
189		4nn0 12182	. . . . . . . . . . . . . . . . . . 19 ⊢ 4 ∈ ℕ₀
190	189	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → 4 ∈ ℕ₀)
191	188, 190	nnexpcld 13888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℕ)
192	191	nncnd 11919	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → ((2 · 𝑥)↑4) ∈ ℂ)
193		2cnd 11981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℂ)
194		nncn 11911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
195	193, 194	mulcld 10926	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℂ)
196		1cnd 10901	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 1 ∈ ℂ)
197	195, 196	subcld 11262	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ∈ ℂ)
198	195, 197	mulcld 10926	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ∈ ℂ)
199	198	sqcld 13790	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ∈ ℂ)
200	186	nnne0d 11953	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 2 ≠ 0)
201		nnne0 11937	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0)
202	193, 194, 200, 201	mulne0d 11557	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 0)
203		1red 10907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℕ → 1 ∈ ℝ)
204	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℝ)
205	204, 203	remulcld 10936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℕ → (2 · 1) ∈ ℝ)
206		nnre 11910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
207	204, 206	remulcld 10936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℕ → (2 · 𝑥) ∈ ℝ)
208	43	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → (2 · 1) = 2)
209	127, 208	breqtrrid 5108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℕ → 1 < (2 · 1))
210		0le2 12005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ≤ 2
211	210	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 0 ≤ 2)
212		nnge1 11931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 1 ≤ 𝑥)
213	203, 206, 204, 211, 212	lemul2ad 11845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℕ → (2 · 1) ≤ (2 · 𝑥))
214	203, 205, 207, 209, 213	ltletrd 11065	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℕ → 1 < (2 · 𝑥))
215	203, 214	gtned 11040	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℕ → (2 · 𝑥) ≠ 1)
216	195, 196, 215	subne0d 11271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → ((2 · 𝑥) − 1) ≠ 0)
217	195, 197, 202, 216	mulne0d 11557	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → ((2 · 𝑥) · ((2 · 𝑥) − 1)) ≠ 0)
218		2z 12282	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℤ
219	218	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℤ)
220	198, 217, 219	expne0d 13798	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2) ≠ 0)
221	192, 199, 220	divcld 11681	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℕ → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
222	184, 221	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...𝑦) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
223	222	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)) ∈ ℂ)
224	176, 183, 185, 223	fvmptd 6864	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) = (((2 · 𝑥)↑4) / (((2 · 𝑥) · ((2 · 𝑥) − 1))↑2)))
225	224, 223	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑥 ∈ (1...𝑦)) → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘𝑥) ∈ ℂ)
226		mulcl 10886	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥 · 𝑤) ∈ ℂ)
227	226	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → (𝑥 · 𝑤) ∈ ℂ)
228	99, 225, 227	seqcl 13671	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) ∈ ℂ)
229	175, 228	mulcld 10926	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) ∈ ℂ)
230	148, 150	reccld 11674	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (1 / ((2 · (𝑦 + 1)) + 1)) ∈ ℂ)
231	229, 230, 161	mul12d 11114	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((1 / ((2 · (𝑦 + 1)) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))))
232	175, 228	mulcomd 10927	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))))
233	232	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))))
234	228, 175, 161	mulassd 10929	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (1 / ((2 · 𝑦) + 1))) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))))
235	167, 168, 160, 147, 174, 149	divmuldivd 11722	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))))
236	160	mulid2d 10924	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (1 · ((2 · (𝑦 + 1))↑2)) = ((2 · (𝑦 + 1))↑2))
237	164, 165, 167	adddid 10930	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
238	43	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
239	238	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
240	237, 239	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
241	240	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
242	166, 164, 167	addsubassd 11282	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
243	45	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 − 1) = 1)
244	243	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
245	241, 242, 244	3eqtrd 2782	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
246	245	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
247	168	sqvald 13789	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · 𝑦) + 1) · ((2 · 𝑦) + 1)))
248	246, 247	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1)) = (((2 · 𝑦) + 1)↑2))
249	236, 248	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 · ((2 · (𝑦 + 1))↑2)) / (((2 · 𝑦) + 1) · ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)))
250		2p2e4 12038	. . . . . . . . . . . . . . . . . 18 ⊢ (2 + 2) = 4
251	53, 53, 250	mvlladdi 11169	. . . . . . . . . . . . . . . . 17 ⊢ 2 = (4 − 2)
252	251	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 = (4 − 2))
253	252	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = ((2 · (𝑦 + 1))↑(4 − 2)))
254	120	rpne0d 12706	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
255	218	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℤ)
256		4z 12284	. . . . . . . . . . . . . . . . 17 ⊢ 4 ∈ ℤ
257	256	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 4 ∈ ℤ)
258	146, 254, 255, 257	expsubd 13803	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑(4 − 2)) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
259	253, 258	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) = (((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)))
260	245	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) = ((2 · (𝑦 + 1)) − 1))
261	260	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1)↑2) = (((2 · (𝑦 + 1)) − 1)↑2))
262	259, 261	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)))
263	146, 254, 257	expclzd 13797	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
264	147	sqcld 13790	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ∈ ℂ)
265	165, 167	addcld 10925	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
266	170	nnne0d 11953	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
267	113	nnne0d 11953	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
268	164, 265, 266, 267	mulne0d 11557	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
269	146, 268, 255	expne0d 13798	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑2) ≠ 0)
270	147, 149, 255	expne0d 13798	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1)↑2) ≠ 0)
271	263, 160, 264, 269, 270	divdiv1d 11712	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1))↑4) / ((2 · (𝑦 + 1))↑2)) / (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))))
272	146, 147	sqmuld 13804	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) = (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)))
273	272	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2)) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
274	273	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1))↑2) · (((2 · (𝑦 + 1)) − 1)↑2))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
275	262, 271, 274	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑2) / (((2 · 𝑦) + 1)↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
276	235, 249, 275	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
277	276	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((1 / ((2 · 𝑦) + 1)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))))
278	233, 234, 277	3eqtrd 2782	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))))
279	278	oveq2d 7271	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · (𝑦 + 1)) + 1)) · (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · (((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))))
280	163, 231, 279	3eqtrd 2782	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((((2 · (𝑦 + 1))↑2) / ((2 · (𝑦 + 1)) − 1)) / ((2 · (𝑦 + 1)) + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))))
281	145, 159, 280	3eqtrd 2782	. . . . . 6 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))))
282		eqidd 2739	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
283		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → 𝑘 = (𝑦 + 1))
284	283	oveq2d 7271	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (2 · 𝑘) = (2 · (𝑦 + 1)))
285	284	oveq1d 7270	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
286	284	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
287	284, 286	oveq12d 7273	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
288	287	oveq1d 7270	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
289	285, 288	oveq12d 7273	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
290	146, 147	mulcld 10926	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
291	290	sqcld 13790	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
292	146, 147, 254, 149	mulne0d 11557	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
293	290, 292, 255	expne0d 13798	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
294	263, 291, 293	divcld 11681	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
295	282, 289, 113, 294	fvmptd 6864	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
296	295	eqcomd 2744	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))
297	296	oveq2d 7271	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
298	297	oveq2d 7271	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))))
299		seqp1 13664	. . . . . . . . 9 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
300	99, 299	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
301	300	eqcomd 2744	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
302	301	oveq2d 7271	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((1 / ((2 · (𝑦 + 1)) + 1)) · ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
303	281, 298, 302	3eqtrd 2782	. . . . 5 ⊢ (𝑦 ∈ ℕ → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
304	303	adantr 480	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))‘(𝑦 + 1))) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
305	102, 104, 304	3eqtrd 2782	. . 3 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1))))
306	305	ex 412	. 2 ⊢ (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑦) = ((1 / ((2 · 𝑦) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦)) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘(𝑦 + 1)) = ((1 / ((2 · (𝑦 + 1)) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))))
307	7, 14, 21, 28, 97, 306	nnind 11921	1 ⊢ (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1)))))‘𝑁) = ((1 / ((2 · 𝑁) + 1)) · (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 class class class wbr 5070 ↦ cmpt 5153 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 − cmin 11135 / cdiv 11562 ℕcn 11903 2c2 11958 3c3 11959 4c4 11960 6c6 11962 ℕ₀cn0 12163 ℤcz 12249 cdc 12366 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 seqcseq 13649 ↑cexp 13710

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-rp 12660 df-fz 13169 df-seq 13650 df-exp 13711

This theorem is referenced by: wallispi2 43504

W3C validator