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 43934

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 7337	. . . . . . 7 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
2	1	fveq2d 6823	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
3	1	fvoveq1d 7351	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
4	2, 3	oveq12d 7347	. . . . 5 ⊢ (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5		fveq2 6819	. . . . . . 7 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
6	5	oveq2d 7345	. . . . . 6 ⊢ (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
7	6	oveq2d 7345	. . . . 5 ⊢ (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
8	4, 7	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9		oveq2 7337	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
10	9	fveq2d 6823	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
11	9	fvoveq1d 7351	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
12	10, 11	oveq12d 7347	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13		fveq2 6819	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
14	13	oveq2d 7345	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
15	14	oveq2d 7345	. . . . 5 ⊢ (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
16	12, 15	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17		oveq2 7337	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
18	17	fveq2d 6823	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
19	17	fvoveq1d 7351	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
20	18, 19	oveq12d 7347	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21		fveq2 6819	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
22	21	oveq2d 7345	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
23	22	oveq2d 7345	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
24	20, 23	eqeq12d 2752	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25		oveq2 7337	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
26	25	fveq2d 6823	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
27	25	fvoveq1d 7351	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
28	26, 27	oveq12d 7347	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29		fveq2 6819	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
30	29	oveq2d 7345	. . . . . 6 ⊢ (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
31	30	oveq2d 7345	. . . . 5 ⊢ (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
32	28, 31	eqeq12d 2752	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33		2t1e2 12229	. . . . . . 7 ⊢ (2 · 1) = 2
34	33	fveq2i 6822	. . . . . 6 ⊢ (𝐼‘(2 · 1)) = (𝐼‘2)
35	33	oveq1i 7339	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
36		2p1e3 12208	. . . . . . . 8 ⊢ (2 + 1) = 3
37	35, 36	eqtri 2764	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
38	37	fveq2i 6822	. . . . . 6 ⊢ (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
39	34, 38	oveq12i 7341	. . . . 5 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40		2z 12445	. . . . . . . . 9 ⊢ 2 ∈ ℤ
41		uzid 12690	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
42	40, 41	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ (ℤ_≥‘2)
43		wallispilem4.2	. . . . . . . . . 10 ⊢ 𝐼 = (𝑛 ∈ ℕ₀ ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
44	43	wallispilem2 43932	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
45	44	simp3i 1140	. . . . . . . 8 ⊢ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
46	42, 45	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47		2m1e1 12192	. . . . . . . . 9 ⊢ (2 − 1) = 1
48	47	oveq1i 7339	. . . . . . . 8 ⊢ ((2 − 1) / 2) = (1 / 2)
49		2cn 12141	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
50	49	subidi 11385	. . . . . . . . . 10 ⊢ (2 − 2) = 0
51	50	fveq2i 6822	. . . . . . . . 9 ⊢ (𝐼‘(2 − 2)) = (𝐼‘0)
52	44	simp1i 1138	. . . . . . . . 9 ⊢ (𝐼‘0) = π
53	51, 52	eqtri 2764	. . . . . . . 8 ⊢ (𝐼‘(2 − 2)) = π
54	48, 53	oveq12i 7341	. . . . . . 7 ⊢ (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55		ax-1cn 11022	. . . . . . . . 9 ⊢ 1 ∈ ℂ
56		2cnne0 12276	. . . . . . . . 9 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
57		picn 25714	. . . . . . . . 9 ⊢ π ∈ ℂ
58		div32 11746	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
59	55, 56, 57, 58	mp3an 1460	. . . . . . . 8 ⊢ ((1 / 2) · π) = (1 · (π / 2))
60		2ne0 12170	. . . . . . . . . 10 ⊢ 2 ≠ 0
61	57, 49, 60	divcli 11810	. . . . . . . . 9 ⊢ (π / 2) ∈ ℂ
62	61	mulid2i 11073	. . . . . . . 8 ⊢ (1 · (π / 2)) = (π / 2)
63	59, 62	eqtri 2764	. . . . . . 7 ⊢ ((1 / 2) · π) = (π / 2)
64	46, 54, 63	3eqtri 2768	. . . . . 6 ⊢ (𝐼‘2) = (π / 2)
65		3z 12446	. . . . . . . . 9 ⊢ 3 ∈ ℤ
66		2re 12140	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
67		3re 12146	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
68		2lt3 12238	. . . . . . . . . 10 ⊢ 2 < 3
69	66, 67, 68	ltleii 11191	. . . . . . . . 9 ⊢ 2 ≤ 3
70		eluz2 12681	. . . . . . . . 9 ⊢ (3 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
71	40, 65, 69, 70	mpbir3an 1340	. . . . . . . 8 ⊢ 3 ∈ (ℤ_≥‘2)
72	43	wallispilem2 43932	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
73	72	simp3i 1140	. . . . . . . 8 ⊢ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
74	71, 73	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75		3m1e2 12194	. . . . . . . . . 10 ⊢ (3 − 1) = 2
76	75	eqcomi 2745	. . . . . . . . 9 ⊢ 2 = (3 − 1)
77	76	oveq1i 7339	. . . . . . . 8 ⊢ (2 / 3) = ((3 − 1) / 3)
78		3cn 12147	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
79	78, 49, 55, 36	subaddrii 11403	. . . . . . . . . 10 ⊢ (3 − 2) = 1
80	79	fveq2i 6822	. . . . . . . . 9 ⊢ (𝐼‘(3 − 2)) = (𝐼‘1)
81	44	simp2i 1139	. . . . . . . . 9 ⊢ (𝐼‘1) = 2
82	80, 81	eqtr2i 2765	. . . . . . . 8 ⊢ 2 = (𝐼‘(3 − 2))
83	77, 82	oveq12i 7341	. . . . . . 7 ⊢ ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84		3ne0 12172	. . . . . . . . 9 ⊢ 3 ≠ 0
85	49, 78, 84	divcli 11810	. . . . . . . 8 ⊢ (2 / 3) ∈ ℂ
86	85, 49	mulcomi 11076	. . . . . . 7 ⊢ ((2 / 3) · 2) = (2 · (2 / 3))
87	74, 83, 86	3eqtr2i 2770	. . . . . 6 ⊢ (𝐼‘3) = (2 · (2 / 3))
88	64, 87	oveq12i 7341	. . . . 5 ⊢ ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89		1z 12443	. . . . . . . . 9 ⊢ 1 ∈ ℤ
90		seq1 13827	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
91	89, 90	ax-mp 5	. . . . . . . 8 ⊢ (seq1( · , 𝐹)‘1) = (𝐹‘1)
92		1nn 12077	. . . . . . . . 9 ⊢ 1 ∈ ℕ
93		oveq2 7337	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
94	93, 33	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (2 · 𝑘) = 2)
95	93	oveq1d 7344	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
96	33	oveq1i 7339	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) − 1) = (2 − 1)
97	96, 47	eqtri 2764	. . . . . . . . . . . . . 14 ⊢ ((2 · 1) − 1) = 1
98	95, 97	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
99	94, 98	oveq12d 7347	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
100	49	div1i 11796	. . . . . . . . . . . 12 ⊢ (2 / 1) = 2
101	99, 100	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
102	94	oveq1d 7344	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103	102, 36	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
104	94, 103	oveq12d 7347	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105	101, 104	oveq12d 7347	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106		wallispilem4.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107		ovex 7362	. . . . . . . . . 10 ⊢ (2 · (2 / 3)) ∈ V
108	105, 106, 107	fvmpt 6925	. . . . . . . . 9 ⊢ (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
109	92, 108	ax-mp 5	. . . . . . . 8 ⊢ (𝐹‘1) = (2 · (2 / 3))
110	91, 109	eqtr2i 2765	. . . . . . 7 ⊢ (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111	110	oveq2i 7340	. . . . . 6 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
112	49, 85	mulcli 11075	. . . . . . . . 9 ⊢ (2 · (2 / 3)) ∈ ℂ
113	109, 112	eqeltri 2833	. . . . . . . 8 ⊢ (𝐹‘1) ∈ ℂ
114	91, 113	eqeltri 2833	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ∈ ℂ
115	49, 78, 60, 84	divne0i 11816	. . . . . . . . 9 ⊢ (2 / 3) ≠ 0
116	49, 85, 60, 115	mulne0i 11711	. . . . . . . 8 ⊢ (2 · (2 / 3)) ≠ 0
117	110, 116	eqnetrri 3012	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ≠ 0
118	61, 114, 117	divreci 11813	. . . . . 6 ⊢ ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119	111, 118	eqtri 2764	. . . . 5 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
120	39, 88, 119	3eqtri 2768	. . . 4 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121		oveq2 7337	. . . . . . 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 12144	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
124		nncn 12074	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
125	55	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
126	123, 124, 125	adddid 11092	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127	123	mulid1d 11085	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
128	127	oveq2d 7345	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129	126, 128	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130	129	oveq1d 7344	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131	123, 124	mulcld 11088	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132	131, 123, 125	addsubassd 11445	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
133	47	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 − 1) = 1)
134	133	oveq2d 7345	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135	130, 132, 134	3eqtrd 2780	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136	135	oveq1d 7344	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137	136	oveq1d 7344	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (3 − 1) = 2)
139	138	oveq2d 7345	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
140	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℂ)
141	131, 140, 125	addsubassd 11445	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142	139, 141, 129	3eqtr4d 2786	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143	142	oveq1d 7344	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144	143	oveq1d 7344	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145	137, 144	oveq12d 7347	. . . . . . . . 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 12435	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148	147	peano2zd 12522	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149	146, 148	zmulcld 12525	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
150	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
151		nnre 12073	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152		1red 11069	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
153	151, 152	readdcld 11097	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154		0le2 12168	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 2
155	154	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ 2)
156		nnnn0 12333	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
157	156	nn0ge0d 12389	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158	152, 151	addge02d 11657	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159	157, 158	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160	150, 153, 155, 159	lemulge11d 12005	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
161	40	eluz1i 12683	. . . . . . . . . . . . 13 ⊢ ((2 · (𝑦 + 1)) ∈ (ℤ_≥‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162	149, 160, 161	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ_≥‘2))
163	43, 162	itgsinexp 43821	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164	129	oveq1d 7344	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165	131, 123	pncand 11426	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166	164, 165	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167	166	fveq2d 6823	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168	167	oveq2d 7345	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169	163, 168	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170	129	oveq1d 7344	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171	131, 123, 125	addassd 11090	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
172	36	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 + 1) = 3)
173	172	oveq2d 7345	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174	170, 171, 173	3eqtrd 2780	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175	174	fveq2d 6823	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176	146, 147	zmulcld 12525	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
177	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℤ)
178	176, 177	zaddcld 12523	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179	150, 151	remulcld 11098	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
180	67	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ)
181	179, 180	readdcld 11097	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182		nnge1 12094	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183	150, 151, 155, 182	lemulge11d 12005	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184		0re 11070	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
185		3pos 12171	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
186	184, 67, 185	ltleii 11191	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 3
187	179, 180	addge01d 11656	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188	186, 187	mpbii 232	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189	150, 179, 181, 183, 188	letrd 11225	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
190	40	eluz1i 12683	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑦) + 3) ∈ (ℤ_≥‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191	178, 189, 190	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ_≥‘2))
192	43, 191	itgsinexp 43821	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193	175, 192	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194	169, 193	oveq12d 7347	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195	131, 125	addcld 11087	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196	124, 125	addcld 11087	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197	123, 196	mulcld 11088	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
198	60	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
199		peano2nn 12078	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200	199	nnne0d 12116	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201	123, 196, 198, 200	mulne0d 11720	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202	195, 197, 201	divcld 11844	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203		2nn0 12343	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
204	203	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ₀)
205	204, 156	nn0mulcld 12391	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ₀)
206	43	wallispilem3 43933	. . . . . . . . . . . 12 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℝ⁺)
207	206	rpcnd 12867	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208	205, 207	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209	131, 140	addcld 11087	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210		0red 11071	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ∈ ℝ)
211		2pos 12169	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
212	211	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 2)
213		nngt0 12097	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
214	150, 151, 212, 213	mulgt0d 11223	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215	180, 185	jctir 521	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216		elrp 12825	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℝ⁺ ↔ (3 ∈ ℝ ∧ 0 < 3))
217	215, 216	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ⁺)
218	179, 217	ltaddrpd 12898	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219	210, 179, 181, 214, 218	lttrd 11229	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220	219	gt0ne0d 11632	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221	197, 209, 220	divcld 11844	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222	197, 209, 201, 220	divne0d 11860	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223	178, 146	zsubcld 12524	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224	181, 150	subge0d 11658	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225	189, 224	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226		elnn0z 12425	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227	223, 225, 226	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ₀)
228	43	wallispilem3 43933	. . . . . . . . . . . . 13 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
229	227, 228	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
230	229	rpcnne0d 12874	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231	221, 222, 230	jca31 515	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232		divmuldiv 11768	. . . . . . . . . 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 835	. . . . . . . . 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 2786	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235	131, 140, 123	addsubassd 11445	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
236	79	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (3 − 2) = 1)
237	236	oveq2d 7345	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238	235, 237	eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239	238	fveq2d 6823	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240	239	oveq2d 7345	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241	240	oveq2d 7345	. . . . . . . 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 2776	. . . . . . 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 12715	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
245	244	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘1))
246		seqp1 13829	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247	245, 246	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248		oveq2 7337	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249	248	oveq1d 7344	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250	248, 249	oveq12d 7347	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251	248	oveq1d 7344	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252	248, 251	oveq12d 7347	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253	250, 252	oveq12d 7347	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254	150, 153	remulcld 11098	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255	254, 152	resubcld 11496	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256		1lt2 12237	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
257	256	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < 2)
258		nnrp 12834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
259	152, 258	ltaddrp2d 12899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260	150, 153, 257, 259	mulgt1d 12004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261	152, 260	gtned 11203	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262	197, 125, 261	subne0d 11434	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263	254, 255, 262	redivcld 11896	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264	174, 181	eqeltrd 2837	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265	174, 220	eqnetrd 3008	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266	254, 264, 265	redivcld 11896	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267	263, 266	remulcld 11098	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268	106, 253, 199, 267	fvmptd3 6948	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269	268	oveq2d 7345	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270	247, 269	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271	270	oveq2d 7345	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272	271	oveq2d 7345	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273	135	oveq2d 7345	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274	174	oveq2d 7345	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275	273, 274	oveq12d 7347	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276	275	oveq2d 7345	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277	276	oveq2d 7345	. . . . . . . . . 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 7345	. . . . . . . . 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 13378	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280	279	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281		oveq2 7337	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282	281	oveq1d 7344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283	281, 282	oveq12d 7347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284	281	oveq1d 7344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285	281, 284	oveq12d 7347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286	283, 285	oveq12d 7347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288		2rp 12828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ⁺)
290		nnrp 12834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ⁺)
291	289, 290	rpmulcld 12881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ⁺)
292	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ)
293		nnre 12073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294	292, 293	remulcld 11098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295		1red 11069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 ∈ ℝ)
296	294, 295	resubcld 11496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297		nnge1 12094	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298		nncn 12074	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299	298	mulid2d 11086	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300	295, 292, 290	ltmul1d 12906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301	256, 300	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302	299, 301	eqbrtrrd 5113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303	295, 293, 294, 297, 302	lelttrd 11226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304	295, 294	posdifd 11655	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305	303, 304	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306	296, 305	elrpd 12862	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ⁺)
307	291, 306	rpdivcld 12882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ⁺)
308	154	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 2)
309	290	rpge0d 12869	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310	292, 293, 308, 309	mulge0d 11645	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311	294, 310	ge0p1rpd 12895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ⁺)
312	291, 311	rpdivcld 12882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ⁺)
313	307, 312	rpmulcld 12881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ⁺)
314	106, 286, 287, 313	fvmptd3 6948	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315	314, 313	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) ∈ ℝ⁺)
316	280, 315	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹‘𝑤) ∈ ℝ⁺)
317		rpmulcl 12846	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺) → (𝑤 · 𝑧) ∈ ℝ⁺)
318	317	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺)) → (𝑤 · 𝑧) ∈ ℝ⁺)
319	245, 316, 318	seqcl 13836	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ⁺)
320	319	rpcnne0d 12874	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321	288	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ⁺)
322	151, 157	ge0p1rpd 12895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ⁺)
323	321, 322	rpmulcld 12881	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ⁺)
324	150, 151, 155, 157	mulge0d 11645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325	179, 324	ge0p1rpd 12895	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ⁺)
326	323, 325	rpdivcld 12882	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ⁺)
327	321, 258	rpmulcld 12881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ⁺)
328	327, 217	rpaddcld 12880	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ⁺)
329	323, 328	rpdivcld 12882	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ⁺)
330	326, 329	rpmulcld 12881	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ⁺)
331	330	rpcnne0d 12874	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332		divdiv1 11779	. . . . . . . . . . . . 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 1370	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334	333	eqcomd 2742	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335	334	oveq2d 7345	. . . . . . . . . 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 12867	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338	319	rpne0d 12870	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339	337, 338	reccld 11837	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340	330	rpcnd 12867	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341	330	rpne0d 12870	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342	336, 339, 340, 341	divassd 11879	. . . . . . . . . 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 3009	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344	197, 195, 197, 209, 343, 220	divmuldivd 11885	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345	344	oveq2d 7345	. . . . . . . . . . 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 11088	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347	197, 197	mulcld 11088	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348	195, 209	mulcld 11088	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349	197, 197, 201, 201	mulne0d 11720	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350	195, 209, 343, 220	mulne0d 11720	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351	346, 347, 348, 349, 350	divdiv2d 11876	. . . . . . . . . . . 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 11879	. . . . . . . . . . . 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 2776	. . . . . . . . . . 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 11891	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355	354	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356	355	oveq2d 7345	. . . . . . . . . . 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 2780	. . . . . . . . . 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 2782	. . . . . . . . 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 12311	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361	360, 339	mulcld 11088	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362	202, 221, 222	divcld 11844	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363	361, 362	mulcomd 11089	. . . . . . . . 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 2780	. . . . . . . 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 2776	. . . . . . 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 2786	. . . . 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 12084	. . 3 ⊢ (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370	369	mpteq2ia 5192	. 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 2774	1 ⊢ 𝐺 = 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ≠ wne 2940 class class class wbr 5089 ↦ cmpt 5172 ‘cfv 6473 (class class class)co 7329 ℂcc 10962 ℝcr 10963 0cc0 10964 1c1 10965 + caddc 10967 · cmul 10969 < clt 11102 ≤ cle 11103 − cmin 11298 / cdiv 11725 ℕcn 12066 2c2 12121 3c3 12122 ℕ₀cn0 12326 ℤcz 12412 ℤ_≥cuz 12675 ℝ⁺crp 12823 (,)cioo 13172 ...cfz 13332 seqcseq 13814 ↑cexp 13875 sincsin 15864 πcpi 15867 ∫citg 24880

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5226 ax-sep 5240 ax-nul 5247 ax-pow 5305 ax-pr 5369 ax-un 7642 ax-inf2 9490 ax-cc 10284 ax-cnex 11020 ax-resscn 11021 ax-1cn 11022 ax-icn 11023 ax-addcl 11024 ax-addrcl 11025 ax-mulcl 11026 ax-mulrcl 11027 ax-mulcom 11028 ax-addass 11029 ax-mulass 11030 ax-distr 11031 ax-i2m1 11032 ax-1ne0 11033 ax-1rid 11034 ax-rnegex 11035 ax-rrecex 11036 ax-cnre 11037 ax-pre-lttri 11038 ax-pre-lttrn 11039 ax-pre-ltadd 11040 ax-pre-mulgt0 11041 ax-pre-sup 11042 ax-addf 11043 ax-mulf 11044

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-symdif 4188 df-nul 4269 df-if 4473 df-pw 4548 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4852 df-int 4894 df-iun 4940 df-iin 4941 df-disj 5055 df-br 5090 df-opab 5152 df-mpt 5173 df-tr 5207 df-id 5512 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5569 df-se 5570 df-we 5571 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6232 df-ord 6299 df-on 6300 df-lim 6301 df-suc 6302 df-iota 6425 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478 df-fo 6479 df-f1o 6480 df-fv 6481 df-isom 6482 df-riota 7286 df-ov 7332 df-oprab 7333 df-mpo 7334 df-of 7587 df-ofr 7588 df-om 7773 df-1st 7891 df-2nd 7892 df-supp 8040 df-frecs 8159 df-wrecs 8190 df-recs 8264 df-rdg 8303 df-1o 8359 df-2o 8360 df-oadd 8363 df-omul 8364 df-er 8561 df-map 8680 df-pm 8681 df-ixp 8749 df-en 8797 df-dom 8798 df-sdom 8799 df-fin 8800 df-fsupp 9219 df-fi 9260 df-sup 9291 df-inf 9292 df-oi 9359 df-dju 9750 df-card 9788 df-acn 9791 df-pnf 11104 df-mnf 11105 df-xr 11106 df-ltxr 11107 df-le 11108 df-sub 11300 df-neg 11301 df-div 11726 df-nn 12067 df-2 12129 df-3 12130 df-4 12131 df-5 12132 df-6 12133 df-7 12134 df-8 12135 df-9 12136 df-n0 12327 df-z 12413 df-dec 12531 df-uz 12676 df-q 12782 df-rp 12824 df-xneg 12941 df-xadd 12942 df-xmul 12943 df-ioo 13176 df-ioc 13177 df-ico 13178 df-icc 13179 df-fz 13333 df-fzo 13476 df-fl 13605 df-mod 13683 df-seq 13815 df-exp 13876 df-fac 14081 df-bc 14110 df-hash 14138 df-shft 14869 df-cj 14901 df-re 14902 df-im 14903 df-sqrt 15037 df-abs 15038 df-limsup 15271 df-clim 15288 df-rlim 15289 df-sum 15489 df-ef 15868 df-sin 15870 df-cos 15871 df-pi 15873 df-struct 16937 df-sets 16954 df-slot 16972 df-ndx 16984 df-base 17002 df-ress 17031 df-plusg 17064 df-mulr 17065 df-starv 17066 df-sca 17067 df-vsca 17068 df-ip 17069 df-tset 17070 df-ple 17071 df-ds 17073 df-unif 17074 df-hom 17075 df-cco 17076 df-rest 17222 df-topn 17223 df-0g 17241 df-gsum 17242 df-topgen 17243 df-pt 17244 df-prds 17247 df-xrs 17302 df-qtop 17307 df-imas 17308 df-xps 17310 df-mre 17384 df-mrc 17385 df-acs 17387 df-mgm 18415 df-sgrp 18464 df-mnd 18475 df-submnd 18520 df-mulg 18789 df-cntz 19011 df-cmn 19475 df-psmet 20687 df-xmet 20688 df-met 20689 df-bl 20690 df-mopn 20691 df-fbas 20692 df-fg 20693 df-cnfld 20696 df-top 22141 df-topon 22158 df-topsp 22180 df-bases 22194 df-cld 22268 df-ntr 22269 df-cls 22270 df-nei 22347 df-lp 22385 df-perf 22386 df-cn 22476 df-cnp 22477 df-haus 22564 df-cmp 22636 df-tx 22811 df-hmeo 23004 df-fil 23095 df-fm 23187 df-flim 23188 df-flf 23189 df-xms 23571 df-ms 23572 df-tms 23573 df-cncf 24139 df-ovol 24726 df-vol 24727 df-mbf 24881 df-itg1 24882 df-itg2 24883 df-ibl 24884 df-itg 24885 df-0p 24932 df-limc 25128 df-dv 25129

This theorem is referenced by: wallispilem5 43935

W3C validator