wallispilem4 - Mathbox for Glauco Siliprandi

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

Theorem wallispilem4 46511

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

**Hypotheses**
Ref	Expression
wallispilem4.1	⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
wallispilem4.2	⊢ 𝐼 = (𝑛 ∈ ℕ₀ ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
wallispilem4.3	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
wallispilem4.4	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))

**Assertion**
Ref	Expression
wallispilem4	⊢ 𝐺 = 𝐻

Distinct variable groups: 𝑧,𝑛 𝑧,𝐹 Allowed substitution hints: 𝐹(𝑘,𝑛) 𝐺(𝑧,𝑘,𝑛) 𝐻(𝑧,𝑘,𝑛) 𝐼(𝑧,𝑘,𝑛)

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

Step	Hyp	Ref	Expression
1		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
2	1	fveq2d 6831	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
3	1	fvoveq1d 7378	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
4	2, 3	oveq12d 7374	. . . . 5 ⊢ (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5		fveq2 6827	. . . . . . 7 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
6	5	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
7	6	oveq2d 7372	. . . . 5 ⊢ (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
8	4, 7	eqeq12d 2755	. . . 4 ⊢ (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
10	9	fveq2d 6831	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
11	9	fvoveq1d 7378	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
12	10, 11	oveq12d 7374	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13		fveq2 6827	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
14	13	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
15	14	oveq2d 7372	. . . . 5 ⊢ (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
16	12, 15	eqeq12d 2755	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
18	17	fveq2d 6831	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
19	17	fvoveq1d 7378	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
20	18, 19	oveq12d 7374	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21		fveq2 6827	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
22	21	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
23	22	oveq2d 7372	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
24	20, 23	eqeq12d 2755	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
26	25	fveq2d 6831	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
27	25	fvoveq1d 7378	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
28	26, 27	oveq12d 7374	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29		fveq2 6827	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
30	29	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
31	30	oveq2d 7372	. . . . 5 ⊢ (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
32	28, 31	eqeq12d 2755	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33		2t1e2 12330	. . . . . . 7 ⊢ (2 · 1) = 2
34	33	fveq2i 6830	. . . . . 6 ⊢ (𝐼‘(2 · 1)) = (𝐼‘2)
35	33	oveq1i 7366	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
36		2p1e3 12309	. . . . . . . 8 ⊢ (2 + 1) = 3
37	35, 36	eqtri 2762	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
38	37	fveq2i 6830	. . . . . 6 ⊢ (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
39	34, 38	oveq12i 7368	. . . . 5 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40		2z 12550	. . . . . . . . 9 ⊢ 2 ∈ ℤ
41		uzid 12794	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
42	40, 41	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ (ℤ_≥‘2)
43		wallispilem4.2	. . . . . . . . . 10 ⊢ 𝐼 = (𝑛 ∈ ℕ₀ ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
44	43	wallispilem2 46509	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
45	44	simp3i 1147	. . . . . . . 8 ⊢ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
46	42, 45	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47		2m1e1 12293	. . . . . . . . 9 ⊢ (2 − 1) = 1
48	47	oveq1i 7366	. . . . . . . 8 ⊢ ((2 − 1) / 2) = (1 / 2)
49		2cn 12247	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
50	49	subidi 11456	. . . . . . . . . 10 ⊢ (2 − 2) = 0
51	50	fveq2i 6830	. . . . . . . . 9 ⊢ (𝐼‘(2 − 2)) = (𝐼‘0)
52	44	simp1i 1145	. . . . . . . . 9 ⊢ (𝐼‘0) = π
53	51, 52	eqtri 2762	. . . . . . . 8 ⊢ (𝐼‘(2 − 2)) = π
54	48, 53	oveq12i 7368	. . . . . . 7 ⊢ (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55		ax-1cn 11087	. . . . . . . . 9 ⊢ 1 ∈ ℂ
56		2cnne0 12377	. . . . . . . . 9 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
57		picn 26440	. . . . . . . . 9 ⊢ π ∈ ℂ
58		div32 11820	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
59	55, 56, 57, 58	mp3an 1469	. . . . . . . 8 ⊢ ((1 / 2) · π) = (1 · (π / 2))
60		2ne0 12276	. . . . . . . . . 10 ⊢ 2 ≠ 0
61	57, 49, 60	divcli 11888	. . . . . . . . 9 ⊢ (π / 2) ∈ ℂ
62	61	mullidi 11141	. . . . . . . 8 ⊢ (1 · (π / 2)) = (π / 2)
63	59, 62	eqtri 2762	. . . . . . 7 ⊢ ((1 / 2) · π) = (π / 2)
64	46, 54, 63	3eqtri 2766	. . . . . 6 ⊢ (𝐼‘2) = (π / 2)
65		3z 12551	. . . . . . . . 9 ⊢ 3 ∈ ℤ
66		2re 12246	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
67		3re 12252	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
68		2lt3 12339	. . . . . . . . . 10 ⊢ 2 < 3
69	66, 67, 68	ltleii 11260	. . . . . . . . 9 ⊢ 2 ≤ 3
70		eluz2 12785	. . . . . . . . 9 ⊢ (3 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
71	40, 65, 69, 70	mpbir3an 1348	. . . . . . . 8 ⊢ 3 ∈ (ℤ_≥‘2)
72	43	wallispilem2 46509	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
73	72	simp3i 1147	. . . . . . . 8 ⊢ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
74	71, 73	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75		3m1e2 12295	. . . . . . . . . 10 ⊢ (3 − 1) = 2
76	75	eqcomi 2748	. . . . . . . . 9 ⊢ 2 = (3 − 1)
77	76	oveq1i 7366	. . . . . . . 8 ⊢ (2 / 3) = ((3 − 1) / 3)
78		3cn 12253	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
79	78, 49, 55, 36	subaddrii 11474	. . . . . . . . . 10 ⊢ (3 − 2) = 1
80	79	fveq2i 6830	. . . . . . . . 9 ⊢ (𝐼‘(3 − 2)) = (𝐼‘1)
81	44	simp2i 1146	. . . . . . . . 9 ⊢ (𝐼‘1) = 2
82	80, 81	eqtr2i 2763	. . . . . . . 8 ⊢ 2 = (𝐼‘(3 − 2))
83	77, 82	oveq12i 7368	. . . . . . 7 ⊢ ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84		3ne0 12278	. . . . . . . . 9 ⊢ 3 ≠ 0
85	49, 78, 84	divcli 11888	. . . . . . . 8 ⊢ (2 / 3) ∈ ℂ
86	85, 49	mulcomi 11144	. . . . . . 7 ⊢ ((2 / 3) · 2) = (2 · (2 / 3))
87	74, 83, 86	3eqtr2i 2768	. . . . . 6 ⊢ (𝐼‘3) = (2 · (2 / 3))
88	64, 87	oveq12i 7368	. . . . 5 ⊢ ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89		1z 12548	. . . . . . . . 9 ⊢ 1 ∈ ℤ
90		seq1 13967	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
91	89, 90	ax-mp 5	. . . . . . . 8 ⊢ (seq1( · , 𝐹)‘1) = (𝐹‘1)
92		1nn 12176	. . . . . . . . 9 ⊢ 1 ∈ ℕ
93		oveq2 7364	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
94	93, 33	eqtrdi 2790	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (2 · 𝑘) = 2)
95	93	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
96	33	oveq1i 7366	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) − 1) = (2 − 1)
97	96, 47	eqtri 2762	. . . . . . . . . . . . . 14 ⊢ ((2 · 1) − 1) = 1
98	95, 97	eqtrdi 2790	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
99	94, 98	oveq12d 7374	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
100	49	div1i 11874	. . . . . . . . . . . 12 ⊢ (2 / 1) = 2
101	99, 100	eqtrdi 2790	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
102	94	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103	102, 36	eqtrdi 2790	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
104	94, 103	oveq12d 7374	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105	101, 104	oveq12d 7374	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106		wallispilem4.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107		ovex 7389	. . . . . . . . . 10 ⊢ (2 · (2 / 3)) ∈ V
108	105, 106, 107	fvmpt 6935	. . . . . . . . 9 ⊢ (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
109	92, 108	ax-mp 5	. . . . . . . 8 ⊢ (𝐹‘1) = (2 · (2 / 3))
110	91, 109	eqtr2i 2763	. . . . . . 7 ⊢ (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111	110	oveq2i 7367	. . . . . 6 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
112	49, 85	mulcli 11143	. . . . . . . . 9 ⊢ (2 · (2 / 3)) ∈ ℂ
113	109, 112	eqeltri 2835	. . . . . . . 8 ⊢ (𝐹‘1) ∈ ℂ
114	91, 113	eqeltri 2835	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ∈ ℂ
115	49, 78, 60, 84	divne0i 11894	. . . . . . . . 9 ⊢ (2 / 3) ≠ 0
116	49, 85, 60, 115	mulne0i 11784	. . . . . . . 8 ⊢ (2 · (2 / 3)) ≠ 0
117	110, 116	eqnetrri 3005	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ≠ 0
118	61, 114, 117	divreci 11891	. . . . . 6 ⊢ ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119	111, 118	eqtri 2762	. . . . 5 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
120	39, 88, 119	3eqtri 2766	. . . 4 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121		oveq2 7364	. . . . . . 7 ⊢ (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
122	121	adantl 482	. . . . . 6 ⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
123		2cnd 12250	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
124		nncn 12173	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
125	55	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
126	123, 124, 125	adddid 11160	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127	123	mulridd 11153	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
128	127	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129	126, 128	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130	129	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131	123, 124	mulcld 11156	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132	131, 123, 125	addsubassd 11516	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
133	47	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 − 1) = 1)
134	133	oveq2d 7372	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135	130, 132, 134	3eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136	135	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137	136	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (3 − 1) = 2)
139	138	oveq2d 7372	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
140	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℂ)
141	131, 140, 125	addsubassd 11516	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142	139, 141, 129	3eqtr4d 2784	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143	142	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144	143	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145	137, 144	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
146	40	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℤ)
147		nnz 12536	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148	147	peano2zd 12627	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149	146, 148	zmulcld 12630	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
150	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
151		nnre 12172	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152		1red 11136	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
153	151, 152	readdcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154		0le2 12274	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 2
155	154	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ 2)
156		nnnn0 12435	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
157	156	nn0ge0d 12492	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158	152, 151	addge02d 11730	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159	157, 158	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160	150, 153, 155, 159	lemulge11d 12084	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
161	40	eluz1i 12787	. . . . . . . . . . . . 13 ⊢ ((2 · (𝑦 + 1)) ∈ (ℤ_≥‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162	149, 160, 161	sylanbrc 589	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ_≥‘2))
163	43, 162	itgsinexp 46398	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164	129	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165	131, 123	pncand 11497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166	164, 165	eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167	166	fveq2d 6831	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168	167	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169	163, 168	eqtrd 2774	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170	129	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171	131, 123, 125	addassd 11158	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
172	36	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 + 1) = 3)
173	172	oveq2d 7372	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174	170, 171, 173	3eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175	174	fveq2d 6831	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176	146, 147	zmulcld 12630	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
177	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℤ)
178	176, 177	zaddcld 12628	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179	150, 151	remulcld 11166	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
180	67	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ)
181	179, 180	readdcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182		nnge1 12196	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183	150, 151, 155, 182	lemulge11d 12084	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184		0re 11137	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
185		3pos 12277	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
186	184, 67, 185	ltleii 11260	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 3
187	179, 180	addge01d 11729	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188	186, 187	mpbii 234	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189	150, 179, 181, 183, 188	letrd 11294	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
190	40	eluz1i 12787	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑦) + 3) ∈ (ℤ_≥‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191	178, 189, 190	sylanbrc 589	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ_≥‘2))
192	43, 191	itgsinexp 46398	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193	175, 192	eqtrd 2774	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194	169, 193	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195	131, 125	addcld 11155	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196	124, 125	addcld 11155	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197	123, 196	mulcld 11156	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
198	60	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
199		peano2nn 12177	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200	199	nnne0d 12218	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201	123, 196, 198, 200	mulne0d 11793	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202	195, 197, 201	divcld 11922	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203		2nn0 12445	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
204	203	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ₀)
205	204, 156	nn0mulcld 12494	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ₀)
206	43	wallispilem3 46510	. . . . . . . . . . . 12 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℝ⁺)
207	206	rpcnd 12979	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208	205, 207	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209	131, 140	addcld 11155	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210		0red 11138	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ∈ ℝ)
211		2pos 12275	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
212	211	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 2)
213		nngt0 12199	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
214	150, 151, 212, 213	mulgt0d 11292	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215	180, 185	jctir 525	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216		elrp 12935	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℝ⁺ ↔ (3 ∈ ℝ ∧ 0 < 3))
217	215, 216	sylibr 235	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ⁺)
218	179, 217	ltaddrpd 13010	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219	210, 179, 181, 214, 218	lttrd 11298	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220	219	gt0ne0d 11705	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221	197, 209, 220	divcld 11922	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222	197, 209, 201, 220	divne0d 11938	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223	178, 146	zsubcld 12629	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224	181, 150	subge0d 11731	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225	189, 224	mpbird 258	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226		elnn0z 12528	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227	223, 225, 226	sylanbrc 589	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ₀)
228	43	wallispilem3 46510	. . . . . . . . . . . . 13 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
229	227, 228	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
230	229	rpcnne0d 12986	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231	221, 222, 230	jca31 519	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232		divmuldiv 11846	. . . . . . . . . 10 ⊢ ((((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ ∧ (𝐼‘(2 · 𝑦)) ∈ ℂ) ∧ ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))) → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
233	202, 208, 231, 232	syl21anc 843	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
234	145, 194, 233	3eqtr4d 2784	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235	131, 140, 123	addsubassd 11516	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
236	79	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (3 − 2) = 1)
237	236	oveq2d 7372	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238	235, 237	eqtrd 2774	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239	238	fveq2d 6831	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240	239	oveq2d 7372	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241	240	oveq2d 7372	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
242	234, 241	eqtrd 2774	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
243	242	adantr 481	. . . . . 6 ⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
244		elnnuz 12819	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
245	244	biimpi 217	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘1))
246		seqp1 13969	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247	245, 246	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248		oveq2 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249	248	oveq1d 7371	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250	248, 249	oveq12d 7374	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251	248	oveq1d 7371	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252	248, 251	oveq12d 7374	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253	250, 252	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254	150, 153	remulcld 11166	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255	254, 152	resubcld 11569	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256		1lt2 12338	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
257	256	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < 2)
258		nnrp 12945	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
259	152, 258	ltaddrp2d 13011	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260	150, 153, 257, 259	mulgt1d 12083	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261	152, 260	gtned 11272	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262	197, 125, 261	subne0d 11505	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263	254, 255, 262	redivcld 11974	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264	174, 181	eqeltrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265	174, 220	eqnetrd 3001	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266	254, 264, 265	redivcld 11974	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267	263, 266	remulcld 11166	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268	106, 253, 199, 267	fvmptd3 6959	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269	268	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270	247, 269	eqtrd 2774	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271	270	oveq2d 7372	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272	271	oveq2d 7372	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273	135	oveq2d 7372	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274	174	oveq2d 7372	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275	273, 274	oveq12d 7374	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276	275	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277	276	oveq2d 7372	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
278	277	oveq2d 7372	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))))
279		elfznn 13498	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280	279	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281		oveq2 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282	281	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283	281, 282	oveq12d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284	281	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285	281, 284	oveq12d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286	283, 285	oveq12d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288		2rp 12938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ⁺)
290		nnrp 12945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ⁺)
291	289, 290	rpmulcld 12993	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ⁺)
292	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ)
293		nnre 12172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294	292, 293	remulcld 11166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295		1red 11136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 ∈ ℝ)
296	294, 295	resubcld 11569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297		nnge1 12196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298		nncn 12173	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299	298	mullidd 11154	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300	295, 292, 290	ltmul1d 13018	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301	256, 300	mpbii 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302	299, 301	eqbrtrrd 5096	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303	295, 293, 294, 297, 302	lelttrd 11295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304	295, 294	posdifd 11728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305	303, 304	mpbid 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306	296, 305	elrpd 12974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ⁺)
307	291, 306	rpdivcld 12994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ⁺)
308	154	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 2)
309	290	rpge0d 12981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310	292, 293, 308, 309	mulge0d 11718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311	294, 310	ge0p1rpd 13007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ⁺)
312	291, 311	rpdivcld 12994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ⁺)
313	307, 312	rpmulcld 12993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ⁺)
314	106, 286, 287, 313	fvmptd3 6959	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315	314, 313	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) ∈ ℝ⁺)
316	280, 315	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹‘𝑤) ∈ ℝ⁺)
317		rpmulcl 12958	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺) → (𝑤 · 𝑧) ∈ ℝ⁺)
318	317	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺)) → (𝑤 · 𝑧) ∈ ℝ⁺)
319	245, 316, 318	seqcl 13975	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ⁺)
320	319	rpcnne0d 12986	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321	288	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ⁺)
322	151, 157	ge0p1rpd 13007	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ⁺)
323	321, 322	rpmulcld 12993	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ⁺)
324	150, 151, 155, 157	mulge0d 11718	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325	179, 324	ge0p1rpd 13007	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ⁺)
326	323, 325	rpdivcld 12994	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ⁺)
327	321, 258	rpmulcld 12993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ⁺)
328	327, 217	rpaddcld 12992	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ⁺)
329	323, 328	rpdivcld 12994	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ⁺)
330	326, 329	rpmulcld 12993	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ⁺)
331	330	rpcnne0d 12986	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332		divdiv1 11857	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0) ∧ ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)) → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
333	125, 320, 331, 332	syl3anc 1379	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334	333	eqcomd 2745	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335	334	oveq2d 7372	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = ((π / 2) · ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
336	61	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
337	319	rpcnd 12979	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338	319	rpne0d 12982	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339	337, 338	reccld 11915	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340	330	rpcnd 12979	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341	330	rpne0d 12982	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342	336, 339, 340, 341	divassd 11957	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = ((π / 2) · ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
343	135, 262	eqnetrrd 3002	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344	197, 195, 197, 209, 343, 220	divmuldivd 11963	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345	344	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))))
346	336, 339	mulcld 11156	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347	197, 197	mulcld 11156	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348	195, 209	mulcld 11156	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349	197, 197, 201, 201	mulne0d 11793	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350	195, 209, 343, 220	mulne0d 11793	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351	346, 347, 348, 349, 350	divdiv2d 11954	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))) = ((((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
352	346, 348, 347, 349	divassd 11957	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))))
353	351, 352	eqtrd 2774	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))))
354	195, 197, 197, 209, 201, 220, 201	divdivdivd 11969	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355	354	eqcomd 2745	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356	355	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
357	345, 353, 356	3eqtrd 2778	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
358	335, 342, 357	3eqtr2d 2780	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))) = (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
359	57	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → π ∈ ℂ)
360	359	halfcld 12413	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361	360, 339	mulcld 11156	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362	202, 221, 222	divcld 11922	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363	361, 362	mulcomd 11157	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) · ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
364	278, 358, 363	3eqtrd 2778	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
365	272, 364	eqtrd 2774	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
366	365	adantr 481	. . . . . 6 ⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
367	122, 243, 366	3eqtr4d 2784	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
368	367	ex 413	. . . 4 ⊢ (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
369	8, 16, 24, 32, 120, 368	nnind 12183	. . 3 ⊢ (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370	369	mpteq2ia 5167	. 2 ⊢ (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
371		wallispilem4.3	. 2 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
372		wallispilem4.4	. 2 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
373	370, 371, 372	3eqtr4i 2772	1 ⊢ 𝐺 = 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 class class class wbr 5072 ↦ cmpt 5153 ‘cfv 6485 (class class class)co 7356 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 < clt 11170 ≤ cle 11171 − cmin 11368 / cdiv 11798 ℕcn 12165 2c2 12227 3c3 12228 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ℝ⁺crp 12933 (,)cioo 13289 ...cfz 13452 seqcseq 13954 ↑cexp 14014 sincsin 16019 πcpi 16022 ∫citg 25603

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cc 10348 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-symdif 4181 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-disj 5040 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-ofr 7621 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-omul 8400 df-er 8633 df-map 8765 df-pm 8766 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9816 df-card 9854 df-acn 9857 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ioc 13294 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-mod 13820 df-seq 13955 df-exp 14015 df-fac 14227 df-bc 14256 df-hash 14284 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15424 df-clim 15441 df-rlim 15442 df-sum 15640 df-ef 16023 df-sin 16025 df-cos 16026 df-pi 16028 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-rest 17376 df-topn 17377 df-0g 17395 df-gsum 17396 df-topgen 17397 df-pt 17398 df-prds 17401 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-mulg 19035 df-cntz 19283 df-cmn 19748 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-fbas 21344 df-fg 21345 df-cnfld 21348 df-top 22877 df-topon 22894 df-topsp 22916 df-bases 22929 df-cld 23002 df-ntr 23003 df-cls 23004 df-nei 23081 df-lp 23119 df-perf 23120 df-cn 23210 df-cnp 23211 df-haus 23298 df-cmp 23370 df-tx 23545 df-hmeo 23738 df-fil 23829 df-fm 23921 df-flim 23922 df-flf 23923 df-xms 24303 df-ms 24304 df-tms 24305 df-cncf 24863 df-ovol 25449 df-vol 25450 df-mbf 25604 df-itg1 25605 df-itg2 25606 df-ibl 25607 df-itg 25608 df-0p 25655 df-limc 25851 df-dv 25852

This theorem is referenced by: wallispilem5 46512

W3C validator