Theorem wallispilem4 44770

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 ↦ ∫(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 7413	. . . . . . 7 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
2	1	fveq2d 6892	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
3	1	fvoveq1d 7427	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
4	2, 3	oveq12d 7423	. . . . 5 ⊢ (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5		fveq2 6888	. . . . . . 7 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
6	5	oveq2d 7421	. . . . . 6 ⊢ (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
7	6	oveq2d 7421	. . . . 5 ⊢ (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
8	4, 7	eqeq12d 2748	. . . 4 ⊢ (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9		oveq2 7413	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
10	9	fveq2d 6892	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
11	9	fvoveq1d 7427	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
12	10, 11	oveq12d 7423	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13		fveq2 6888	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
14	13	oveq2d 7421	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
15	14	oveq2d 7421	. . . . 5 ⊢ (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
16	12, 15	eqeq12d 2748	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17		oveq2 7413	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
18	17	fveq2d 6892	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
19	17	fvoveq1d 7427	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
20	18, 19	oveq12d 7423	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21		fveq2 6888	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
22	21	oveq2d 7421	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
23	22	oveq2d 7421	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
24	20, 23	eqeq12d 2748	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25		oveq2 7413	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
26	25	fveq2d 6892	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
27	25	fvoveq1d 7427	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
28	26, 27	oveq12d 7423	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29		fveq2 6888	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
30	29	oveq2d 7421	. . . . . 6 ⊢ (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
31	30	oveq2d 7421	. . . . 5 ⊢ (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
32	28, 31	eqeq12d 2748	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33		2t1e2 12371	. . . . . . 7 ⊢ (2 · 1) = 2
34	33	fveq2i 6891	. . . . . 6 ⊢ (𝐼‘(2 · 1)) = (𝐼‘2)
35	33	oveq1i 7415	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
36		2p1e3 12350	. . . . . . . 8 ⊢ (2 + 1) = 3
37	35, 36	eqtri 2760	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
38	37	fveq2i 6891	. . . . . 6 ⊢ (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
39	34, 38	oveq12i 7417	. . . . 5 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40		2z 12590	. . . . . . . . 9 ⊢ 2 ∈ ℤ
41		uzid 12833	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ≥‘2))
42	40, 41	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ (ℤ≥‘2)
43		wallispilem4.2	. . . . . . . . . 10 ⊢ 𝐼 = (𝑛 ∈ ℕ0 ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
44	43	wallispilem2 44768	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
45	44	simp3i 1141	. . . . . . . 8 ⊢ (2 ∈ (ℤ≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
46	42, 45	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47		2m1e1 12334	. . . . . . . . 9 ⊢ (2 − 1) = 1
48	47	oveq1i 7415	. . . . . . . 8 ⊢ ((2 − 1) / 2) = (1 / 2)
49		2cn 12283	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
50	49	subidi 11527	. . . . . . . . . 10 ⊢ (2 − 2) = 0
51	50	fveq2i 6891	. . . . . . . . 9 ⊢ (𝐼‘(2 − 2)) = (𝐼‘0)
52	44	simp1i 1139	. . . . . . . . 9 ⊢ (𝐼‘0) = π
53	51, 52	eqtri 2760	. . . . . . . 8 ⊢ (𝐼‘(2 − 2)) = π
54	48, 53	oveq12i 7417	. . . . . . 7 ⊢ (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55		ax-1cn 11164	. . . . . . . . 9 ⊢ 1 ∈ ℂ
56		2cnne0 12418	. . . . . . . . 9 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
57		picn 25960	. . . . . . . . 9 ⊢ π ∈ ℂ
58		div32 11888	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
59	55, 56, 57, 58	mp3an 1461	. . . . . . . 8 ⊢ ((1 / 2) · π) = (1 · (π / 2))
60		2ne0 12312	. . . . . . . . . 10 ⊢ 2 ≠ 0
61	57, 49, 60	divcli 11952	. . . . . . . . 9 ⊢ (π / 2) ∈ ℂ
62	61	mullidi 11215	. . . . . . . 8 ⊢ (1 · (π / 2)) = (π / 2)
63	59, 62	eqtri 2760	. . . . . . 7 ⊢ ((1 / 2) · π) = (π / 2)
64	46, 54, 63	3eqtri 2764	. . . . . 6 ⊢ (𝐼‘2) = (π / 2)
65		3z 12591	. . . . . . . . 9 ⊢ 3 ∈ ℤ
66		2re 12282	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
67		3re 12288	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
68		2lt3 12380	. . . . . . . . . 10 ⊢ 2 < 3
69	66, 67, 68	ltleii 11333	. . . . . . . . 9 ⊢ 2 ≤ 3
70		eluz2 12824	. . . . . . . . 9 ⊢ (3 ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
71	40, 65, 69, 70	mpbir3an 1341	. . . . . . . 8 ⊢ 3 ∈ (ℤ≥‘2)
72	43	wallispilem2 44768	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
73	72	simp3i 1141	. . . . . . . 8 ⊢ (3 ∈ (ℤ≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
74	71, 73	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75		3m1e2 12336	. . . . . . . . . 10 ⊢ (3 − 1) = 2
76	75	eqcomi 2741	. . . . . . . . 9 ⊢ 2 = (3 − 1)
77	76	oveq1i 7415	. . . . . . . 8 ⊢ (2 / 3) = ((3 − 1) / 3)
78		3cn 12289	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
79	78, 49, 55, 36	subaddrii 11545	. . . . . . . . . 10 ⊢ (3 − 2) = 1
80	79	fveq2i 6891	. . . . . . . . 9 ⊢ (𝐼‘(3 − 2)) = (𝐼‘1)
81	44	simp2i 1140	. . . . . . . . 9 ⊢ (𝐼‘1) = 2
82	80, 81	eqtr2i 2761	. . . . . . . 8 ⊢ 2 = (𝐼‘(3 − 2))
83	77, 82	oveq12i 7417	. . . . . . 7 ⊢ ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84		3ne0 12314	. . . . . . . . 9 ⊢ 3 ≠ 0
85	49, 78, 84	divcli 11952	. . . . . . . 8 ⊢ (2 / 3) ∈ ℂ
86	85, 49	mulcomi 11218	. . . . . . 7 ⊢ ((2 / 3) · 2) = (2 · (2 / 3))
87	74, 83, 86	3eqtr2i 2766	. . . . . 6 ⊢ (𝐼‘3) = (2 · (2 / 3))
88	64, 87	oveq12i 7417	. . . . 5 ⊢ ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89		1z 12588	. . . . . . . . 9 ⊢ 1 ∈ ℤ
90		seq1 13975	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
91	89, 90	ax-mp 5	. . . . . . . 8 ⊢ (seq1( · , 𝐹)‘1) = (𝐹‘1)
92		1nn 12219	. . . . . . . . 9 ⊢ 1 ∈ ℕ
93		oveq2 7413	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
94	93, 33	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (2 · 𝑘) = 2)
95	93	oveq1d 7420	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
96	33	oveq1i 7415	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) − 1) = (2 − 1)
97	96, 47	eqtri 2760	. . . . . . . . . . . . . 14 ⊢ ((2 · 1) − 1) = 1
98	95, 97	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
99	94, 98	oveq12d 7423	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
100	49	div1i 11938	. . . . . . . . . . . 12 ⊢ (2 / 1) = 2
101	99, 100	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
102	94	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103	102, 36	eqtrdi 2788	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
104	94, 103	oveq12d 7423	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105	101, 104	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106		wallispilem4.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107		ovex 7438	. . . . . . . . . 10 ⊢ (2 · (2 / 3)) ∈ V
108	105, 106, 107	fvmpt 6995	. . . . . . . . 9 ⊢ (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
109	92, 108	ax-mp 5	. . . . . . . 8 ⊢ (𝐹‘1) = (2 · (2 / 3))
110	91, 109	eqtr2i 2761	. . . . . . 7 ⊢ (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111	110	oveq2i 7416	. . . . . 6 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
112	49, 85	mulcli 11217	. . . . . . . . 9 ⊢ (2 · (2 / 3)) ∈ ℂ
113	109, 112	eqeltri 2829	. . . . . . . 8 ⊢ (𝐹‘1) ∈ ℂ
114	91, 113	eqeltri 2829	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ∈ ℂ
115	49, 78, 60, 84	divne0i 11958	. . . . . . . . 9 ⊢ (2 / 3) ≠ 0
116	49, 85, 60, 115	mulne0i 11853	. . . . . . . 8 ⊢ (2 · (2 / 3)) ≠ 0
117	110, 116	eqnetrri 3012	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ≠ 0
118	61, 114, 117	divreci 11955	. . . . . 6 ⊢ ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119	111, 118	eqtri 2760	. . . . 5 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
120	39, 88, 119	3eqtri 2764	. . . 4 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121		oveq2 7413	. . . . . . 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 12286	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
124		nncn 12216	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
125	55	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
126	123, 124, 125	adddid 11234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127	123	mulridd 11227	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
128	127	oveq2d 7421	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129	126, 128	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130	129	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131	123, 124	mulcld 11230	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132	131, 123, 125	addsubassd 11587	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
133	47	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 − 1) = 1)
134	133	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135	130, 132, 134	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136	135	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137	136	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (3 − 1) = 2)
139	138	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
140	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℂ)
141	131, 140, 125	addsubassd 11587	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142	139, 141, 129	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143	142	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144	143	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145	137, 144	oveq12d 7423	. . . . . . . . 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 12575	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148	147	peano2zd 12665	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149	146, 148	zmulcld 12668	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
150	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
151		nnre 12215	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152		1red 11211	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
153	151, 152	readdcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154		0le2 12310	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 2
155	154	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ 2)
156		nnnn0 12475	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
157	156	nn0ge0d 12531	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158	152, 151	addge02d 11799	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159	157, 158	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160	150, 153, 155, 159	lemulge11d 12147	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
161	40	eluz1i 12826	. . . . . . . . . . . . 13 ⊢ ((2 · (𝑦 + 1)) ∈ (ℤ≥‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162	149, 160, 161	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ≥‘2))
163	43, 162	itgsinexp 44657	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164	129	oveq1d 7420	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165	131, 123	pncand 11568	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166	164, 165	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167	166	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168	167	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169	163, 168	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170	129	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171	131, 123, 125	addassd 11232	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
172	36	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 + 1) = 3)
173	172	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174	170, 171, 173	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175	174	fveq2d 6892	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176	146, 147	zmulcld 12668	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
177	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℤ)
178	176, 177	zaddcld 12666	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179	150, 151	remulcld 11240	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
180	67	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ)
181	179, 180	readdcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182		nnge1 12236	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183	150, 151, 155, 182	lemulge11d 12147	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184		0re 11212	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
185		3pos 12313	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
186	184, 67, 185	ltleii 11333	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 3
187	179, 180	addge01d 11798	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188	186, 187	mpbii 232	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189	150, 179, 181, 183, 188	letrd 11367	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
190	40	eluz1i 12826	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑦) + 3) ∈ (ℤ≥‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191	178, 189, 190	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ≥‘2))
192	43, 191	itgsinexp 44657	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193	175, 192	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194	169, 193	oveq12d 7423	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195	131, 125	addcld 11229	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196	124, 125	addcld 11229	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197	123, 196	mulcld 11230	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
198	60	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
199		peano2nn 12220	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200	199	nnne0d 12258	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201	123, 196, 198, 200	mulne0d 11862	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202	195, 197, 201	divcld 11986	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203		2nn0 12485	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ0
204	203	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ0)
205	204, 156	nn0mulcld 12533	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ0)
206	43	wallispilem3 44769	. . . . . . . . . . . 12 ⊢ ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℝ+)
207	206	rpcnd 13014	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ ℕ0 → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208	205, 207	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209	131, 140	addcld 11229	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210		0red 11213	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ∈ ℝ)
211		2pos 12311	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
212	211	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 2)
213		nngt0 12239	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
214	150, 151, 212, 213	mulgt0d 11365	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215	180, 185	jctir 521	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216		elrp 12972	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℝ+ ↔ (3 ∈ ℝ ∧ 0 < 3))
217	215, 216	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ+)
218	179, 217	ltaddrpd 13045	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219	210, 179, 181, 214, 218	lttrd 11371	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220	219	gt0ne0d 11774	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221	197, 209, 220	divcld 11986	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222	197, 209, 201, 220	divne0d 12002	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223	178, 146	zsubcld 12667	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224	181, 150	subge0d 11800	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225	189, 224	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226		elnn0z 12567	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227	223, 225, 226	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ0)
228	43	wallispilem3 44769	. . . . . . . . . . . . 13 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ0 → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
229	227, 228	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ+)
230	229	rpcnne0d 13021	. . . . . . . . . . 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 11910	. . . . . . . . . 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 836	. . . . . . . . 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 2782	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235	131, 140, 123	addsubassd 11587	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
236	79	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (3 − 2) = 1)
237	236	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238	235, 237	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239	238	fveq2d 6892	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240	239	oveq2d 7421	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241	240	oveq2d 7421	. . . . . . . 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 2772	. . . . . . 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 12862	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ≥‘1))
245	244	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ≥‘1))
246		seqp1 13977	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247	245, 246	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248		oveq2 7413	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249	248	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250	248, 249	oveq12d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251	248	oveq1d 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252	248, 251	oveq12d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253	250, 252	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254	150, 153	remulcld 11240	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255	254, 152	resubcld 11638	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256		1lt2 12379	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
257	256	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < 2)
258		nnrp 12981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
259	152, 258	ltaddrp2d 13046	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260	150, 153, 257, 259	mulgt1d 12146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261	152, 260	gtned 11345	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262	197, 125, 261	subne0d 11576	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263	254, 255, 262	redivcld 12038	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264	174, 181	eqeltrd 2833	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265	174, 220	eqnetrd 3008	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266	254, 264, 265	redivcld 12038	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267	263, 266	remulcld 11240	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268	106, 253, 199, 267	fvmptd3 7018	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269	268	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270	247, 269	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271	270	oveq2d 7421	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272	271	oveq2d 7421	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273	135	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274	174	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275	273, 274	oveq12d 7423	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276	275	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277	276	oveq2d 7421	. . . . . . . . . 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 7421	. . . . . . . . 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 13526	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280	279	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281		oveq2 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282	281	oveq1d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283	281, 282	oveq12d 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284	281	oveq1d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285	281, 284	oveq12d 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286	283, 285	oveq12d 7423	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288		2rp 12975	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ+
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ+)
290		nnrp 12981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ+)
291	289, 290	rpmulcld 13028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ+)
292	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ)
293		nnre 12215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294	292, 293	remulcld 11240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295		1red 11211	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 ∈ ℝ)
296	294, 295	resubcld 11638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297		nnge1 12236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298		nncn 12216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299	298	mullidd 11228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300	295, 292, 290	ltmul1d 13053	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301	256, 300	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302	299, 301	eqbrtrrd 5171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303	295, 293, 294, 297, 302	lelttrd 11368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304	295, 294	posdifd 11797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305	303, 304	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306	296, 305	elrpd 13009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ+)
307	291, 306	rpdivcld 13029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ+)
308	154	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 2)
309	290	rpge0d 13016	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310	292, 293, 308, 309	mulge0d 11787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311	294, 310	ge0p1rpd 13042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ+)
312	291, 311	rpdivcld 13029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ+)
313	307, 312	rpmulcld 13028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ+)
314	106, 286, 287, 313	fvmptd3 7018	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315	314, 313	eqeltrd 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) ∈ ℝ+)
316	280, 315	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹‘𝑤) ∈ ℝ+)
317		rpmulcl 12993	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+) → (𝑤 · 𝑧) ∈ ℝ+)
318	317	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+)) → (𝑤 · 𝑧) ∈ ℝ+)
319	245, 316, 318	seqcl 13984	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ+)
320	319	rpcnne0d 13021	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321	288	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ+)
322	151, 157	ge0p1rpd 13042	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ+)
323	321, 322	rpmulcld 13028	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ+)
324	150, 151, 155, 157	mulge0d 11787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325	179, 324	ge0p1rpd 13042	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ+)
326	323, 325	rpdivcld 13029	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ+)
327	321, 258	rpmulcld 13028	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ+)
328	327, 217	rpaddcld 13027	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ+)
329	323, 328	rpdivcld 13029	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ+)
330	326, 329	rpmulcld 13028	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ+)
331	330	rpcnne0d 13021	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332		divdiv1 11921	. . . . . . . . . . . . 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 1371	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334	333	eqcomd 2738	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335	334	oveq2d 7421	. . . . . . . . . 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 13014	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338	319	rpne0d 13017	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339	337, 338	reccld 11979	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340	330	rpcnd 13014	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341	330	rpne0d 13017	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342	336, 339, 340, 341	divassd 12021	. . . . . . . . . 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 12027	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345	344	oveq2d 7421	. . . . . . . . . . 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 11230	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347	197, 197	mulcld 11230	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348	195, 209	mulcld 11230	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349	197, 197, 201, 201	mulne0d 11862	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350	195, 209, 343, 220	mulne0d 11862	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351	346, 347, 348, 349, 350	divdiv2d 12018	. . . . . . . . . . . 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 12021	. . . . . . . . . . . 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 2772	. . . . . . . . . . 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 12033	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355	354	eqcomd 2738	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356	355	oveq2d 7421	. . . . . . . . . . 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 2776	. . . . . . . . . 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 2778	. . . . . . . . 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 12453	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361	360, 339	mulcld 11230	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362	202, 221, 222	divcld 11986	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363	361, 362	mulcomd 11231	. . . . . . . . 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 2776	. . . . . . . 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 2772	. . . . . . 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 2782	. . . . 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 12226	. . 3 ⊢ (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370	369	mpteq2ia 5250	. 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 2770	1 ⊢ 𝐺 = 𝐻

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ≠ wne 2940   class class class wbr 5147   ↦ cmpt 5230  ‘cfv 6540  (class class class)co 7405  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244   ≤ cle 11245   − cmin 11440   / cdiv 11867  ℕcn 12208  2c2 12263  3c3 12264  ℕ₀cn0 12468  ℤcz 12554  ℤ_≥cuz 12818  ℝ⁺crp 12970  (,)cioo 13320  ...cfz 13480  seqcseq 13962  ↑cexp 14023  sincsin 16003  πcpi 16006  ∫citg 25126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cc 10426  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-symdif 4241  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19644  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-mopn 20932  df-fbas 20933  df-fg 20934  df-cnfld 20937  df-top 22387  df-topon 22404  df-topsp 22426  df-bases 22440  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-lp 22631  df-perf 22632  df-cn 22722  df-cnp 22723  df-haus 22810  df-cmp 22882  df-tx 23057  df-hmeo 23250  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-xms 23817  df-ms 23818  df-tms 23819  df-cncf 24385  df-ovol 24972  df-vol 24973  df-mbf 25127  df-itg1 25128  df-itg2 25129  df-ibl 25130  df-itg 25131  df-0p 25178  df-limc 25374  df-dv 25375

This theorem is referenced by:  wallispilem5  44771