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 45722

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 7421	. . . . . . 7 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
2	1	fveq2d 6894	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
3	1	fvoveq1d 7435	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
4	2, 3	oveq12d 7431	. . . . 5 ⊢ (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5		fveq2 6890	. . . . . . 7 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
6	5	oveq2d 7429	. . . . . 6 ⊢ (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
7	6	oveq2d 7429	. . . . 5 ⊢ (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
8	4, 7	eqeq12d 2742	. . . 4 ⊢ (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9		oveq2 7421	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
10	9	fveq2d 6894	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
11	9	fvoveq1d 7435	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
12	10, 11	oveq12d 7431	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13		fveq2 6890	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
14	13	oveq2d 7429	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
15	14	oveq2d 7429	. . . . 5 ⊢ (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
16	12, 15	eqeq12d 2742	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17		oveq2 7421	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
18	17	fveq2d 6894	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
19	17	fvoveq1d 7435	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
20	18, 19	oveq12d 7431	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21		fveq2 6890	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
22	21	oveq2d 7429	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
23	22	oveq2d 7429	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
24	20, 23	eqeq12d 2742	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25		oveq2 7421	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
26	25	fveq2d 6894	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
27	25	fvoveq1d 7435	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
28	26, 27	oveq12d 7431	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29		fveq2 6890	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
30	29	oveq2d 7429	. . . . . 6 ⊢ (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
31	30	oveq2d 7429	. . . . 5 ⊢ (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
32	28, 31	eqeq12d 2742	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33		2t1e2 12418	. . . . . . 7 ⊢ (2 · 1) = 2
34	33	fveq2i 6893	. . . . . 6 ⊢ (𝐼‘(2 · 1)) = (𝐼‘2)
35	33	oveq1i 7423	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
36		2p1e3 12397	. . . . . . . 8 ⊢ (2 + 1) = 3
37	35, 36	eqtri 2754	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
38	37	fveq2i 6893	. . . . . 6 ⊢ (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
39	34, 38	oveq12i 7425	. . . . 5 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40		2z 12637	. . . . . . . . 9 ⊢ 2 ∈ ℤ
41		uzid 12880	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
42	40, 41	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ (ℤ_≥‘2)
43		wallispilem4.2	. . . . . . . . . 10 ⊢ 𝐼 = (𝑛 ∈ ℕ₀ ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
44	43	wallispilem2 45720	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
45	44	simp3i 1138	. . . . . . . 8 ⊢ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
46	42, 45	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47		2m1e1 12381	. . . . . . . . 9 ⊢ (2 − 1) = 1
48	47	oveq1i 7423	. . . . . . . 8 ⊢ ((2 − 1) / 2) = (1 / 2)
49		2cn 12330	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
50	49	subidi 11569	. . . . . . . . . 10 ⊢ (2 − 2) = 0
51	50	fveq2i 6893	. . . . . . . . 9 ⊢ (𝐼‘(2 − 2)) = (𝐼‘0)
52	44	simp1i 1136	. . . . . . . . 9 ⊢ (𝐼‘0) = π
53	51, 52	eqtri 2754	. . . . . . . 8 ⊢ (𝐼‘(2 − 2)) = π
54	48, 53	oveq12i 7425	. . . . . . 7 ⊢ (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55		ax-1cn 11204	. . . . . . . . 9 ⊢ 1 ∈ ℂ
56		2cnne0 12465	. . . . . . . . 9 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
57		picn 26481	. . . . . . . . 9 ⊢ π ∈ ℂ
58		div32 11931	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
59	55, 56, 57, 58	mp3an 1458	. . . . . . . 8 ⊢ ((1 / 2) · π) = (1 · (π / 2))
60		2ne0 12359	. . . . . . . . . 10 ⊢ 2 ≠ 0
61	57, 49, 60	divcli 11998	. . . . . . . . 9 ⊢ (π / 2) ∈ ℂ
62	61	mullidi 11257	. . . . . . . 8 ⊢ (1 · (π / 2)) = (π / 2)
63	59, 62	eqtri 2754	. . . . . . 7 ⊢ ((1 / 2) · π) = (π / 2)
64	46, 54, 63	3eqtri 2758	. . . . . 6 ⊢ (𝐼‘2) = (π / 2)
65		3z 12638	. . . . . . . . 9 ⊢ 3 ∈ ℤ
66		2re 12329	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
67		3re 12335	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
68		2lt3 12427	. . . . . . . . . 10 ⊢ 2 < 3
69	66, 67, 68	ltleii 11375	. . . . . . . . 9 ⊢ 2 ≤ 3
70		eluz2 12871	. . . . . . . . 9 ⊢ (3 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
71	40, 65, 69, 70	mpbir3an 1338	. . . . . . . 8 ⊢ 3 ∈ (ℤ_≥‘2)
72	43	wallispilem2 45720	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
73	72	simp3i 1138	. . . . . . . 8 ⊢ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
74	71, 73	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75		3m1e2 12383	. . . . . . . . . 10 ⊢ (3 − 1) = 2
76	75	eqcomi 2735	. . . . . . . . 9 ⊢ 2 = (3 − 1)
77	76	oveq1i 7423	. . . . . . . 8 ⊢ (2 / 3) = ((3 − 1) / 3)
78		3cn 12336	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
79	78, 49, 55, 36	subaddrii 11587	. . . . . . . . . 10 ⊢ (3 − 2) = 1
80	79	fveq2i 6893	. . . . . . . . 9 ⊢ (𝐼‘(3 − 2)) = (𝐼‘1)
81	44	simp2i 1137	. . . . . . . . 9 ⊢ (𝐼‘1) = 2
82	80, 81	eqtr2i 2755	. . . . . . . 8 ⊢ 2 = (𝐼‘(3 − 2))
83	77, 82	oveq12i 7425	. . . . . . 7 ⊢ ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84		3ne0 12361	. . . . . . . . 9 ⊢ 3 ≠ 0
85	49, 78, 84	divcli 11998	. . . . . . . 8 ⊢ (2 / 3) ∈ ℂ
86	85, 49	mulcomi 11260	. . . . . . 7 ⊢ ((2 / 3) · 2) = (2 · (2 / 3))
87	74, 83, 86	3eqtr2i 2760	. . . . . 6 ⊢ (𝐼‘3) = (2 · (2 / 3))
88	64, 87	oveq12i 7425	. . . . 5 ⊢ ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89		1z 12635	. . . . . . . . 9 ⊢ 1 ∈ ℤ
90		seq1 14025	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
91	89, 90	ax-mp 5	. . . . . . . 8 ⊢ (seq1( · , 𝐹)‘1) = (𝐹‘1)
92		1nn 12266	. . . . . . . . 9 ⊢ 1 ∈ ℕ
93		oveq2 7421	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
94	93, 33	eqtrdi 2782	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (2 · 𝑘) = 2)
95	93	oveq1d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
96	33	oveq1i 7423	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) − 1) = (2 − 1)
97	96, 47	eqtri 2754	. . . . . . . . . . . . . 14 ⊢ ((2 · 1) − 1) = 1
98	95, 97	eqtrdi 2782	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
99	94, 98	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
100	49	div1i 11984	. . . . . . . . . . . 12 ⊢ (2 / 1) = 2
101	99, 100	eqtrdi 2782	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
102	94	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103	102, 36	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
104	94, 103	oveq12d 7431	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105	101, 104	oveq12d 7431	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106		wallispilem4.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107		ovex 7446	. . . . . . . . . 10 ⊢ (2 · (2 / 3)) ∈ V
108	105, 106, 107	fvmpt 6998	. . . . . . . . 9 ⊢ (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
109	92, 108	ax-mp 5	. . . . . . . 8 ⊢ (𝐹‘1) = (2 · (2 / 3))
110	91, 109	eqtr2i 2755	. . . . . . 7 ⊢ (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111	110	oveq2i 7424	. . . . . 6 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
112	49, 85	mulcli 11259	. . . . . . . . 9 ⊢ (2 · (2 / 3)) ∈ ℂ
113	109, 112	eqeltri 2822	. . . . . . . 8 ⊢ (𝐹‘1) ∈ ℂ
114	91, 113	eqeltri 2822	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ∈ ℂ
115	49, 78, 60, 84	divne0i 12004	. . . . . . . . 9 ⊢ (2 / 3) ≠ 0
116	49, 85, 60, 115	mulne0i 11895	. . . . . . . 8 ⊢ (2 · (2 / 3)) ≠ 0
117	110, 116	eqnetrri 3002	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ≠ 0
118	61, 114, 117	divreci 12001	. . . . . 6 ⊢ ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119	111, 118	eqtri 2754	. . . . 5 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
120	39, 88, 119	3eqtri 2758	. . . 4 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121		oveq2 7421	. . . . . . 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 480	. . . . . 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 12333	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
124		nncn 12263	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
125	55	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
126	123, 124, 125	adddid 11276	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127	123	mulridd 11269	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
128	127	oveq2d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129	126, 128	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130	129	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131	123, 124	mulcld 11272	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132	131, 123, 125	addsubassd 11629	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
133	47	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 − 1) = 1)
134	133	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135	130, 132, 134	3eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136	135	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137	136	oveq1d 7428	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (3 − 1) = 2)
139	138	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
140	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℂ)
141	131, 140, 125	addsubassd 11629	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142	139, 141, 129	3eqtr4d 2776	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143	142	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144	143	oveq1d 7428	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145	137, 144	oveq12d 7431	. . . . . . . . 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 12622	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148	147	peano2zd 12712	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149	146, 148	zmulcld 12715	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
150	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
151		nnre 12262	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152		1red 11253	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
153	151, 152	readdcld 11281	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154		0le2 12357	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 2
155	154	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ 2)
156		nnnn0 12522	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
157	156	nn0ge0d 12578	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158	152, 151	addge02d 11841	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159	157, 158	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160	150, 153, 155, 159	lemulge11d 12194	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
161	40	eluz1i 12873	. . . . . . . . . . . . 13 ⊢ ((2 · (𝑦 + 1)) ∈ (ℤ_≥‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162	149, 160, 161	sylanbrc 581	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ_≥‘2))
163	43, 162	itgsinexp 45609	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164	129	oveq1d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165	131, 123	pncand 11610	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166	164, 165	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167	166	fveq2d 6894	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168	167	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169	163, 168	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170	129	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171	131, 123, 125	addassd 11274	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
172	36	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 + 1) = 3)
173	172	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174	170, 171, 173	3eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175	174	fveq2d 6894	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176	146, 147	zmulcld 12715	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
177	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℤ)
178	176, 177	zaddcld 12713	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179	150, 151	remulcld 11282	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
180	67	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ)
181	179, 180	readdcld 11281	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182		nnge1 12283	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183	150, 151, 155, 182	lemulge11d 12194	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184		0re 11254	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
185		3pos 12360	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
186	184, 67, 185	ltleii 11375	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 3
187	179, 180	addge01d 11840	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188	186, 187	mpbii 232	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189	150, 179, 181, 183, 188	letrd 11409	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
190	40	eluz1i 12873	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑦) + 3) ∈ (ℤ_≥‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191	178, 189, 190	sylanbrc 581	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ_≥‘2))
192	43, 191	itgsinexp 45609	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193	175, 192	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194	169, 193	oveq12d 7431	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195	131, 125	addcld 11271	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196	124, 125	addcld 11271	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197	123, 196	mulcld 11272	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
198	60	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
199		peano2nn 12267	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200	199	nnne0d 12305	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201	123, 196, 198, 200	mulne0d 11904	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202	195, 197, 201	divcld 12032	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203		2nn0 12532	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
204	203	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ₀)
205	204, 156	nn0mulcld 12580	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ₀)
206	43	wallispilem3 45721	. . . . . . . . . . . 12 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℝ⁺)
207	206	rpcnd 13063	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208	205, 207	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209	131, 140	addcld 11271	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210		0red 11255	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ∈ ℝ)
211		2pos 12358	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
212	211	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 2)
213		nngt0 12286	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
214	150, 151, 212, 213	mulgt0d 11407	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215	180, 185	jctir 519	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216		elrp 13021	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℝ⁺ ↔ (3 ∈ ℝ ∧ 0 < 3))
217	215, 216	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ⁺)
218	179, 217	ltaddrpd 13094	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219	210, 179, 181, 214, 218	lttrd 11413	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220	219	gt0ne0d 11816	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221	197, 209, 220	divcld 12032	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222	197, 209, 201, 220	divne0d 12048	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223	178, 146	zsubcld 12714	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224	181, 150	subge0d 11842	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225	189, 224	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226		elnn0z 12614	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227	223, 225, 226	sylanbrc 581	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ₀)
228	43	wallispilem3 45721	. . . . . . . . . . . . 13 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
229	227, 228	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
230	229	rpcnne0d 13070	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0))
231	221, 222, 230	jca31 513	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ ∧ ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0) ∧ ((𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℂ ∧ (𝐼‘(((2 · 𝑦) + 3) − 2)) ≠ 0)))
232		divmuldiv 11956	. . . . . . . . . 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 2776	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235	131, 140, 123	addsubassd 11629	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
236	79	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (3 − 2) = 1)
237	236	oveq2d 7429	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238	235, 237	eqtrd 2766	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239	238	fveq2d 6894	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240	239	oveq2d 7429	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241	240	oveq2d 7429	. . . . . . . 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 2766	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1)))))
243	242	adantr 479	. . . . . 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 12909	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
245	244	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘1))
246		seqp1 14027	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247	245, 246	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248		oveq2 7421	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249	248	oveq1d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250	248, 249	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251	248	oveq1d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252	248, 251	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253	250, 252	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254	150, 153	remulcld 11282	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255	254, 152	resubcld 11680	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256		1lt2 12426	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
257	256	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < 2)
258		nnrp 13030	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
259	152, 258	ltaddrp2d 13095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260	150, 153, 257, 259	mulgt1d 12193	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261	152, 260	gtned 11387	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262	197, 125, 261	subne0d 11618	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263	254, 255, 262	redivcld 12084	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264	174, 181	eqeltrd 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265	174, 220	eqnetrd 2998	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266	254, 264, 265	redivcld 12084	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267	263, 266	remulcld 11282	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268	106, 253, 199, 267	fvmptd3 7021	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269	268	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270	247, 269	eqtrd 2766	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271	270	oveq2d 7429	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272	271	oveq2d 7429	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273	135	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274	174	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275	273, 274	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276	275	oveq2d 7429	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277	276	oveq2d 7429	. . . . . . . . . 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 7429	. . . . . . . . 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 13575	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280	279	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281		oveq2 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282	281	oveq1d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283	281, 282	oveq12d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284	281	oveq1d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285	281, 284	oveq12d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286	283, 285	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288		2rp 13024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ⁺)
290		nnrp 13030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ⁺)
291	289, 290	rpmulcld 13077	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ⁺)
292	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ)
293		nnre 12262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294	292, 293	remulcld 11282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295		1red 11253	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 ∈ ℝ)
296	294, 295	resubcld 11680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297		nnge1 12283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298		nncn 12263	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299	298	mullidd 11270	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300	295, 292, 290	ltmul1d 13102	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301	256, 300	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302	299, 301	eqbrtrrd 5167	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303	295, 293, 294, 297, 302	lelttrd 11410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304	295, 294	posdifd 11839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305	303, 304	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306	296, 305	elrpd 13058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ⁺)
307	291, 306	rpdivcld 13078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ⁺)
308	154	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 2)
309	290	rpge0d 13065	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310	292, 293, 308, 309	mulge0d 11829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311	294, 310	ge0p1rpd 13091	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ⁺)
312	291, 311	rpdivcld 13078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ⁺)
313	307, 312	rpmulcld 13077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ⁺)
314	106, 286, 287, 313	fvmptd3 7021	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315	314, 313	eqeltrd 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) ∈ ℝ⁺)
316	280, 315	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹‘𝑤) ∈ ℝ⁺)
317		rpmulcl 13042	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺) → (𝑤 · 𝑧) ∈ ℝ⁺)
318	317	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺)) → (𝑤 · 𝑧) ∈ ℝ⁺)
319	245, 316, 318	seqcl 14033	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ⁺)
320	319	rpcnne0d 13070	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321	288	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ⁺)
322	151, 157	ge0p1rpd 13091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ⁺)
323	321, 322	rpmulcld 13077	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ⁺)
324	150, 151, 155, 157	mulge0d 11829	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325	179, 324	ge0p1rpd 13091	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ⁺)
326	323, 325	rpdivcld 13078	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ⁺)
327	321, 258	rpmulcld 13077	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ⁺)
328	327, 217	rpaddcld 13076	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ⁺)
329	323, 328	rpdivcld 13078	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ⁺)
330	326, 329	rpmulcld 13077	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ⁺)
331	330	rpcnne0d 13070	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332		divdiv1 11967	. . . . . . . . . . . . 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 1368	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334	333	eqcomd 2732	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335	334	oveq2d 7429	. . . . . . . . . 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 13063	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338	319	rpne0d 13066	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339	337, 338	reccld 12025	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340	330	rpcnd 13063	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341	330	rpne0d 13066	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342	336, 339, 340, 341	divassd 12067	. . . . . . . . . 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 2999	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344	197, 195, 197, 209, 343, 220	divmuldivd 12073	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345	344	oveq2d 7429	. . . . . . . . . . 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 11272	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347	197, 197	mulcld 11272	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348	195, 209	mulcld 11272	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349	197, 197, 201, 201	mulne0d 11904	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350	195, 209, 343, 220	mulne0d 11904	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351	346, 347, 348, 349, 350	divdiv2d 12064	. . . . . . . . . . . 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 12067	. . . . . . . . . . . 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 2766	. . . . . . . . . . 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 12079	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355	354	eqcomd 2732	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356	355	oveq2d 7429	. . . . . . . . . . 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 2770	. . . . . . . . . 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 2772	. . . . . . . . 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 12500	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361	360, 339	mulcld 11272	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362	202, 221, 222	divcld 12032	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363	361, 362	mulcomd 11273	. . . . . . . . 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 2770	. . . . . . . 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 2766	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
366	365	adantr 479	. . . . . 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 2776	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
368	367	ex 411	. . . 4 ⊢ (𝑦 ∈ ℕ → (((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
369	8, 16, 24, 32, 120, 368	nnind 12273	. . 3 ⊢ (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370	369	mpteq2ia 5246	. 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 2764	1 ⊢ 𝐺 = 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ≠ wne 2930 class class class wbr 5143 ↦ cmpt 5226 ‘cfv 6543 (class class class)co 7413 ℂcc 11144 ℝcr 11145 0cc0 11146 1c1 11147 + caddc 11149 · cmul 11151 < clt 11286 ≤ cle 11287 − cmin 11482 / cdiv 11909 ℕcn 12255 2c2 12310 3c3 12311 ℕ₀cn0 12515 ℤcz 12601 ℤ_≥cuz 12865 ℝ⁺crp 13019 (,)cioo 13369 ...cfz 13529 seqcseq 14012 ↑cexp 14072 sincsin 16057 πcpi 16060 ∫citg 25632

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7735 ax-inf2 9674 ax-cc 10466 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-pre-sup 11224 ax-addf 11225

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3966 df-symdif 4241 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4906 df-int 4947 df-iun 4995 df-iin 4996 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6302 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-ofr 7680 df-om 7866 df-1st 7992 df-2nd 7993 df-supp 8164 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-omul 8490 df-er 8723 df-map 8846 df-pm 8847 df-ixp 8916 df-en 8964 df-dom 8965 df-sdom 8966 df-fin 8967 df-fsupp 9396 df-fi 9444 df-sup 9475 df-inf 9476 df-oi 9543 df-dju 9934 df-card 9972 df-acn 9975 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11484 df-neg 11485 df-div 11910 df-nn 12256 df-2 12318 df-3 12319 df-4 12320 df-5 12321 df-6 12322 df-7 12323 df-8 12324 df-9 12325 df-n0 12516 df-z 12602 df-dec 12721 df-uz 12866 df-q 12976 df-rp 13020 df-xneg 13137 df-xadd 13138 df-xmul 13139 df-ioo 13373 df-ioc 13374 df-ico 13375 df-icc 13376 df-fz 13530 df-fzo 13673 df-fl 13803 df-mod 13881 df-seq 14013 df-exp 14073 df-fac 14283 df-bc 14312 df-hash 14340 df-shft 15064 df-cj 15096 df-re 15097 df-im 15098 df-sqrt 15232 df-abs 15233 df-limsup 15465 df-clim 15482 df-rlim 15483 df-sum 15683 df-ef 16061 df-sin 16063 df-cos 16064 df-pi 16066 df-struct 17141 df-sets 17158 df-slot 17176 df-ndx 17188 df-base 17206 df-ress 17235 df-plusg 17271 df-mulr 17272 df-starv 17273 df-sca 17274 df-vsca 17275 df-ip 17276 df-tset 17277 df-ple 17278 df-ds 17280 df-unif 17281 df-hom 17282 df-cco 17283 df-rest 17429 df-topn 17430 df-0g 17448 df-gsum 17449 df-topgen 17450 df-pt 17451 df-prds 17454 df-xrs 17509 df-qtop 17514 df-imas 17515 df-xps 17517 df-mre 17591 df-mrc 17592 df-acs 17594 df-mgm 18625 df-sgrp 18704 df-mnd 18720 df-submnd 18766 df-mulg 19055 df-cntz 19304 df-cmn 19773 df-psmet 21328 df-xmet 21329 df-met 21330 df-bl 21331 df-mopn 21332 df-fbas 21333 df-fg 21334 df-cnfld 21337 df-top 22881 df-topon 22898 df-topsp 22920 df-bases 22934 df-cld 23008 df-ntr 23009 df-cls 23010 df-nei 23087 df-lp 23125 df-perf 23126 df-cn 23216 df-cnp 23217 df-haus 23304 df-cmp 23376 df-tx 23551 df-hmeo 23744 df-fil 23835 df-fm 23927 df-flim 23928 df-flf 23929 df-xms 24311 df-ms 24312 df-tms 24313 df-cncf 24883 df-ovol 25478 df-vol 25479 df-mbf 25633 df-itg1 25634 df-itg2 25635 df-ibl 25636 df-itg 25637 df-0p 25684 df-limc 25880 df-dv 25881

This theorem is referenced by: wallispilem5 45723

W3C validator