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 41917

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 7031	. . . . . . 7 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
2	1	fveq2d 6549	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 1)))
3	1	fvoveq1d 7045	. . . . . 6 ⊢ (𝑥 = 1 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 1) + 1)))
4	2, 3	oveq12d 7041	. . . . 5 ⊢ (𝑥 = 1 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))))
5		fveq2 6545	. . . . . . 7 ⊢ (𝑥 = 1 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘1))
6	5	oveq2d 7039	. . . . . 6 ⊢ (𝑥 = 1 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘1)))
7	6	oveq2d 7039	. . . . 5 ⊢ (𝑥 = 1 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1))))
8	4, 7	eqeq12d 2812	. . . 4 ⊢ (𝑥 = 1 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))))
9		oveq2 7031	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
10	9	fveq2d 6549	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑦)))
11	9	fvoveq1d 7045	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑦) + 1)))
12	10, 11	oveq12d 7041	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
13		fveq2 6545	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑦))
14	13	oveq2d 7039	. . . . . 6 ⊢ (𝑥 = 𝑦 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑦)))
15	14	oveq2d 7039	. . . . 5 ⊢ (𝑥 = 𝑦 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))))
16	12, 15	eqeq12d 2812	. . . 4 ⊢ (𝑥 = 𝑦 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦)))))
17		oveq2 7031	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
18	17	fveq2d 6549	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · (𝑦 + 1))))
19	17	fvoveq1d 7045	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · (𝑦 + 1)) + 1)))
20	18, 19	oveq12d 7041	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))))
21		fveq2 6545	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑦 + 1)))
22	21	oveq2d 7039	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))
23	22	oveq2d 7039	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))))
24	20, 23	eqeq12d 2812	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1))))))
25		oveq2 7031	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
26	25	fveq2d 6549	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘(2 · 𝑥)) = (𝐼‘(2 · 𝑛)))
27	25	fvoveq1d 7045	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝐼‘((2 · 𝑥) + 1)) = (𝐼‘((2 · 𝑛) + 1)))
28	26, 27	oveq12d 7041	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))))
29		fveq2 6545	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑛))
30	29	oveq2d 7039	. . . . . 6 ⊢ (𝑥 = 𝑛 → (1 / (seq1( · , 𝐹)‘𝑥)) = (1 / (seq1( · , 𝐹)‘𝑛)))
31	30	oveq2d 7039	. . . . 5 ⊢ (𝑥 = 𝑛 → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
32	28, 31	eqeq12d 2812	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝐼‘(2 · 𝑥)) / (𝐼‘((2 · 𝑥) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑥))) ↔ ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛)))))
33		2t1e2 11654	. . . . . . 7 ⊢ (2 · 1) = 2
34	33	fveq2i 6548	. . . . . 6 ⊢ (𝐼‘(2 · 1)) = (𝐼‘2)
35	33	oveq1i 7033	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
36		2p1e3 11633	. . . . . . . 8 ⊢ (2 + 1) = 3
37	35, 36	eqtri 2821	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
38	37	fveq2i 6548	. . . . . 6 ⊢ (𝐼‘((2 · 1) + 1)) = (𝐼‘3)
39	34, 38	oveq12i 7035	. . . . 5 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((𝐼‘2) / (𝐼‘3))
40		2z 11868	. . . . . . . . 9 ⊢ 2 ∈ ℤ
41		uzid 12112	. . . . . . . . 9 ⊢ (2 ∈ ℤ → 2 ∈ (ℤ_≥‘2))
42	40, 41	ax-mp 5	. . . . . . . 8 ⊢ 2 ∈ (ℤ_≥‘2)
43		wallispilem4.2	. . . . . . . . . 10 ⊢ 𝐼 = (𝑛 ∈ ℕ₀ ↦ ∫(0(,)π)((sin‘𝑧)↑𝑛) d𝑧)
44	43	wallispilem2 41915	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))))
45	44	simp3i 1134	. . . . . . . 8 ⊢ (2 ∈ (ℤ_≥‘2) → (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2))))
46	42, 45	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘2) = (((2 − 1) / 2) · (𝐼‘(2 − 2)))
47		2m1e1 11617	. . . . . . . . 9 ⊢ (2 − 1) = 1
48	47	oveq1i 7033	. . . . . . . 8 ⊢ ((2 − 1) / 2) = (1 / 2)
49		2cn 11566	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
50	49	subidi 10811	. . . . . . . . . 10 ⊢ (2 − 2) = 0
51	50	fveq2i 6548	. . . . . . . . 9 ⊢ (𝐼‘(2 − 2)) = (𝐼‘0)
52	44	simp1i 1132	. . . . . . . . 9 ⊢ (𝐼‘0) = π
53	51, 52	eqtri 2821	. . . . . . . 8 ⊢ (𝐼‘(2 − 2)) = π
54	48, 53	oveq12i 7035	. . . . . . 7 ⊢ (((2 − 1) / 2) · (𝐼‘(2 − 2))) = ((1 / 2) · π)
55		ax-1cn 10448	. . . . . . . . 9 ⊢ 1 ∈ ℂ
56		2cnne0 11701	. . . . . . . . 9 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
57		picn 24732	. . . . . . . . 9 ⊢ π ∈ ℂ
58		div32 11172	. . . . . . . . 9 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ π ∈ ℂ) → ((1 / 2) · π) = (1 · (π / 2)))
59	55, 56, 57, 58	mp3an 1453	. . . . . . . 8 ⊢ ((1 / 2) · π) = (1 · (π / 2))
60		2ne0 11595	. . . . . . . . . 10 ⊢ 2 ≠ 0
61	57, 49, 60	divcli 11236	. . . . . . . . 9 ⊢ (π / 2) ∈ ℂ
62	61	mulid2i 10499	. . . . . . . 8 ⊢ (1 · (π / 2)) = (π / 2)
63	59, 62	eqtri 2821	. . . . . . 7 ⊢ ((1 / 2) · π) = (π / 2)
64	46, 54, 63	3eqtri 2825	. . . . . 6 ⊢ (𝐼‘2) = (π / 2)
65		3z 11869	. . . . . . . . 9 ⊢ 3 ∈ ℤ
66		2re 11565	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
67		3re 11571	. . . . . . . . . 10 ⊢ 3 ∈ ℝ
68		2lt3 11663	. . . . . . . . . 10 ⊢ 2 < 3
69	66, 67, 68	ltleii 10616	. . . . . . . . 9 ⊢ 2 ≤ 3
70		eluz2 12103	. . . . . . . . 9 ⊢ (3 ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ≤ 3))
71	40, 65, 69, 70	mpbir3an 1334	. . . . . . . 8 ⊢ 3 ∈ (ℤ_≥‘2)
72	43	wallispilem2 41915	. . . . . . . . 9 ⊢ ((𝐼‘0) = π ∧ (𝐼‘1) = 2 ∧ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))))
73	72	simp3i 1134	. . . . . . . 8 ⊢ (3 ∈ (ℤ_≥‘2) → (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2))))
74	71, 73	ax-mp 5	. . . . . . 7 ⊢ (𝐼‘3) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
75		3m1e2 11619	. . . . . . . . . 10 ⊢ (3 − 1) = 2
76	75	eqcomi 2806	. . . . . . . . 9 ⊢ 2 = (3 − 1)
77	76	oveq1i 7033	. . . . . . . 8 ⊢ (2 / 3) = ((3 − 1) / 3)
78		3cn 11572	. . . . . . . . . . 11 ⊢ 3 ∈ ℂ
79	78, 49, 55, 36	subaddrii 10829	. . . . . . . . . 10 ⊢ (3 − 2) = 1
80	79	fveq2i 6548	. . . . . . . . 9 ⊢ (𝐼‘(3 − 2)) = (𝐼‘1)
81	44	simp2i 1133	. . . . . . . . 9 ⊢ (𝐼‘1) = 2
82	80, 81	eqtr2i 2822	. . . . . . . 8 ⊢ 2 = (𝐼‘(3 − 2))
83	77, 82	oveq12i 7035	. . . . . . 7 ⊢ ((2 / 3) · 2) = (((3 − 1) / 3) · (𝐼‘(3 − 2)))
84		3ne0 11597	. . . . . . . . 9 ⊢ 3 ≠ 0
85	49, 78, 84	divcli 11236	. . . . . . . 8 ⊢ (2 / 3) ∈ ℂ
86	85, 49	mulcomi 10502	. . . . . . 7 ⊢ ((2 / 3) · 2) = (2 · (2 / 3))
87	74, 83, 86	3eqtr2i 2827	. . . . . 6 ⊢ (𝐼‘3) = (2 · (2 / 3))
88	64, 87	oveq12i 7035	. . . . 5 ⊢ ((𝐼‘2) / (𝐼‘3)) = ((π / 2) / (2 · (2 / 3)))
89		1z 11866	. . . . . . . . 9 ⊢ 1 ∈ ℤ
90		seq1 13236	. . . . . . . . 9 ⊢ (1 ∈ ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1))
91	89, 90	ax-mp 5	. . . . . . . 8 ⊢ (seq1( · , 𝐹)‘1) = (𝐹‘1)
92		1nn 11503	. . . . . . . . 9 ⊢ 1 ∈ ℕ
93		oveq2 7031	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
94	93, 33	syl6eq 2849	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (2 · 𝑘) = 2)
95	93	oveq1d 7038	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
96	33	oveq1i 7033	. . . . . . . . . . . . . . 15 ⊢ ((2 · 1) − 1) = (2 − 1)
97	96, 47	eqtri 2821	. . . . . . . . . . . . . 14 ⊢ ((2 · 1) − 1) = 1
98	95, 97	syl6eq 2849	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = 1)
99	94, 98	oveq12d 7041	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = (2 / 1))
100	49	div1i 11222	. . . . . . . . . . . 12 ⊢ (2 / 1) = 2
101	99, 100	syl6eq 2849	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = 2)
102	94	oveq1d 7038	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = (2 + 1))
103	102, 36	syl6eq 2849	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((2 · 𝑘) + 1) = 3)
104	94, 103	oveq12d 7041	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = (2 / 3))
105	101, 104	oveq12d 7041	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (2 · (2 / 3)))
106		wallispilem4.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))))
107		ovex 7055	. . . . . . . . . 10 ⊢ (2 · (2 / 3)) ∈ V
108	105, 106, 107	fvmpt 6642	. . . . . . . . 9 ⊢ (1 ∈ ℕ → (𝐹‘1) = (2 · (2 / 3)))
109	92, 108	ax-mp 5	. . . . . . . 8 ⊢ (𝐹‘1) = (2 · (2 / 3))
110	91, 109	eqtr2i 2822	. . . . . . 7 ⊢ (2 · (2 / 3)) = (seq1( · , 𝐹)‘1)
111	110	oveq2i 7034	. . . . . 6 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) / (seq1( · , 𝐹)‘1))
112	49, 85	mulcli 10501	. . . . . . . . 9 ⊢ (2 · (2 / 3)) ∈ ℂ
113	109, 112	eqeltri 2881	. . . . . . . 8 ⊢ (𝐹‘1) ∈ ℂ
114	91, 113	eqeltri 2881	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ∈ ℂ
115	49, 78, 60, 84	divne0i 11242	. . . . . . . . 9 ⊢ (2 / 3) ≠ 0
116	49, 85, 60, 115	mulne0i 11137	. . . . . . . 8 ⊢ (2 · (2 / 3)) ≠ 0
117	110, 116	eqnetrri 3057	. . . . . . 7 ⊢ (seq1( · , 𝐹)‘1) ≠ 0
118	61, 114, 117	divreci 11239	. . . . . 6 ⊢ ((π / 2) / (seq1( · , 𝐹)‘1)) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
119	111, 118	eqtri 2821	. . . . 5 ⊢ ((π / 2) / (2 · (2 / 3))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
120	39, 88, 119	3eqtri 2825	. . . 4 ⊢ ((𝐼‘(2 · 1)) / (𝐼‘((2 · 1) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘1)))
121		oveq2 7031	. . . . . . 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 11569	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
124		nncn 11500	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
125	55	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
126	123, 124, 125	adddid 10518	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
127	123	mulid1d 10511	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
128	127	oveq2d 7039	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + 2))
129	126, 128	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + 2))
130	129	oveq1d 7038	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + 2) − 1))
131	123, 124	mulcld 10514	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
132	131, 123, 125	addsubassd 10871	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 1) = ((2 · 𝑦) + (2 − 1)))
133	47	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 − 1) = 1)
134	133	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 − 1)) = ((2 · 𝑦) + 1))
135	130, 132, 134	3eqtrd 2837	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
136	135	oveq1d 7038	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) = (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))))
137	136	oveq1d 7038	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
138	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (3 − 1) = 2)
139	138	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 1)) = ((2 · 𝑦) + 2))
140	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℂ)
141	131, 140, 125	addsubassd 10871	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = ((2 · 𝑦) + (3 − 1)))
142	139, 141, 129	3eqtr4d 2843	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 1) = (2 · (𝑦 + 1)))
143	142	oveq1d 7038	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
144	143	oveq1d 7038	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
145	137, 144	oveq12d 7041	. . . . . . . . 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 11858	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
148	147	peano2zd 11944	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
149	146, 148	zmulcld 11947	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℤ)
150	66	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
151		nnre 11499	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
152		1red 10495	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
153	151, 152	readdcld 10523	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
154		0le2 11593	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 2
155	154	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ 2)
156		nnnn0 11758	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
157	156	nn0ge0d 11812	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 ≤ 𝑦)
158	152, 151	addge02d 11083	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 𝑦 ↔ 1 ≤ (𝑦 + 1)))
159	157, 158	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 ≤ (𝑦 + 1))
160	150, 153, 155, 159	lemulge11d 11431	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · (𝑦 + 1)))
161	40	eluz1i 12105	. . . . . . . . . . . . 13 ⊢ ((2 · (𝑦 + 1)) ∈ (ℤ_≥‘2) ↔ ((2 · (𝑦 + 1)) ∈ ℤ ∧ 2 ≤ (2 · (𝑦 + 1))))
162	149, 160, 161	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ (ℤ_≥‘2))
163	43, 162	itgsinexp 41803	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))))
164	129	oveq1d 7038	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (((2 · 𝑦) + 2) − 2))
165	131, 123	pncand 10852	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) − 2) = (2 · 𝑦))
166	164, 165	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 2) = (2 · 𝑦))
167	166	fveq2d 6549	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) − 2)) = (𝐼‘(2 · 𝑦)))
168	167	oveq2d 7039	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘((2 · (𝑦 + 1)) − 2))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
169	163, 168	eqtrd 2833	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · (𝑦 + 1))) = ((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))))
170	129	oveq1d 7038	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = (((2 · 𝑦) + 2) + 1))
171	131, 123, 125	addassd 10516	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 2) + 1) = ((2 · 𝑦) + (2 + 1)))
172	36	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 + 1) = 3)
173	172	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (2 + 1)) = ((2 · 𝑦) + 3))
174	170, 171, 173	3eqtrd 2837	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) = ((2 · 𝑦) + 3))
175	174	fveq2d 6549	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (𝐼‘((2 · 𝑦) + 3)))
176	146, 147	zmulcld 11947	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
177	65	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℤ)
178	176, 177	zaddcld 11945	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℤ)
179	150, 151	remulcld 10524	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
180	67	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ)
181	179, 180	readdcld 10523	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ)
182		nnge1 11519	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
183	150, 151, 155, 182	lemulge11d 11431	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
184		0re 10496	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
185		3pos 11596	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
186	184, 67, 185	ltleii 10616	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 3
187	179, 180	addge01d 11082	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ 3 ↔ (2 · 𝑦) ≤ ((2 · 𝑦) + 3)))
188	186, 187	mpbii 234	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ≤ ((2 · 𝑦) + 3))
189	150, 179, 181, 183, 188	letrd 10650	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 2 ≤ ((2 · 𝑦) + 3))
190	40	eluz1i 12105	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑦) + 3) ∈ (ℤ_≥‘2) ↔ (((2 · 𝑦) + 3) ∈ ℤ ∧ 2 ≤ ((2 · 𝑦) + 3)))
191	178, 189, 190	sylanbrc 583	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ (ℤ_≥‘2))
192	43, 191	itgsinexp 41803	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · 𝑦) + 3)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
193	175, 192	eqtrd 2833	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘((2 · (𝑦 + 1)) + 1)) = (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2))))
194	169, 193	oveq12d 7041	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · (𝑦 + 1)) − 1) / (2 · (𝑦 + 1))) · (𝐼‘(2 · 𝑦))) / (((((2 · 𝑦) + 3) − 1) / ((2 · 𝑦) + 3)) · (𝐼‘(((2 · 𝑦) + 3) − 2)))))
195	131, 125	addcld 10513	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
196	124, 125	addcld 10513	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
197	123, 196	mulcld 10514	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
198	60	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
199		peano2nn 11504	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
200	199	nnne0d 11541	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
201	123, 196, 198, 200	mulne0d 11146	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
202	195, 197, 201	divcld 11270	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) ∈ ℂ)
203		2nn0 11768	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
204	203	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ₀)
205	204, 156	nn0mulcld 11814	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ₀)
206	43	wallispilem3 41916	. . . . . . . . . . . 12 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℝ⁺)
207	206	rpcnd 12287	. . . . . . . . . . 11 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
208	205, 207	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(2 · 𝑦)) ∈ ℂ)
209	131, 140	addcld 10513	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℂ)
210		0red 10497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ∈ ℝ)
211		2pos 11594	. . . . . . . . . . . . . . . 16 ⊢ 0 < 2
212	211	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 2)
213		nngt0 11522	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
214	150, 151, 212, 213	mulgt0d 10648	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 < (2 · 𝑦))
215	180, 185	jctir 521	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (3 ∈ ℝ ∧ 0 < 3))
216		elrp 12245	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℝ⁺ ↔ (3 ∈ ℝ ∧ 0 < 3))
217	215, 216	sylibr 235	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 3 ∈ ℝ⁺)
218	179, 217	ltaddrpd 12318	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) < ((2 · 𝑦) + 3))
219	210, 179, 181, 214, 218	lttrd 10654	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < ((2 · 𝑦) + 3))
220	219	gt0ne0d 11058	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ≠ 0)
221	197, 209, 220	divcld 11270	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℂ)
222	197, 209, 201, 220	divne0d 11286	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ≠ 0)
223	178, 146	zsubcld 11946	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℤ)
224	181, 150	subge0d 11084	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (0 ≤ (((2 · 𝑦) + 3) − 2) ↔ 2 ≤ ((2 · 𝑦) + 3)))
225	189, 224	mpbird 258	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 0 ≤ (((2 · 𝑦) + 3) − 2))
226		elnn0z 11848	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ ↔ ((((2 · 𝑦) + 3) − 2) ∈ ℤ ∧ 0 ≤ (((2 · 𝑦) + 3) − 2)))
227	223, 225, 226	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) ∈ ℕ₀)
228	43	wallispilem3 41916	. . . . . . . . . . . . 13 ⊢ ((((2 · 𝑦) + 3) − 2) ∈ ℕ₀ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
229	227, 228	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) ∈ ℝ⁺)
230	229	rpcnne0d 12294	. . . . . . . . . . 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 11194	. . . . . . . . . 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 834	. . . . . . . . 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 2843	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · (𝑦 + 1))) / (𝐼‘((2 · (𝑦 + 1)) + 1))) = (((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) · ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2)))))
235	131, 140, 123	addsubassd 10871	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + (3 − 2)))
236	79	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (3 − 2) = 1)
237	236	oveq2d 7039	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (3 − 2)) = ((2 · 𝑦) + 1))
238	235, 237	eqtrd 2833	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 3) − 2) = ((2 · 𝑦) + 1))
239	238	fveq2d 6549	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝐼‘(((2 · 𝑦) + 3) − 2)) = (𝐼‘((2 · 𝑦) + 1)))
240	239	oveq2d 7039	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((𝐼‘(2 · 𝑦)) / (𝐼‘(((2 · 𝑦) + 3) − 2))) = ((𝐼‘(2 · 𝑦)) / (𝐼‘((2 · 𝑦) + 1))))
241	240	oveq2d 7039	. . . . . . . 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 2833	. . . . . . 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 12135	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
245	244	biimpi 217	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘1))
246		seqp1 13238	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
247	245, 246	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))))
248		oveq2 7031	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
249	248	oveq1d 7038	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
250	248, 249	oveq12d 7041	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)))
251	248	oveq1d 7038	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) + 1) = ((2 · (𝑦 + 1)) + 1))
252	248, 251	oveq12d 7041	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))
253	250, 252	oveq12d 7041	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
254	150, 153	remulcld 10524	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ)
255	254, 152	resubcld 10922	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℝ)
256		1lt2 11662	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 2
257	256	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < 2)
258		nnrp 12254	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
259	152, 258	ltaddrp2d 12319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
260	150, 153, 257, 259	mulgt1d 11430	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
261	152, 260	gtned 10628	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
262	197, 125, 261	subne0d 10860	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
263	254, 255, 262	redivcld 11322	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) ∈ ℝ)
264	174, 181	eqeltrd 2885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ∈ ℝ)
265	174, 220	eqnetrd 3053	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) + 1) ≠ 0)
266	254, 264, 265	redivcld 11322	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) ∈ ℝ)
267	263, 266	remulcld 10524	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) ∈ ℝ)
268	106, 253, 199, 267	fvmptd3 6664	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝐹‘(𝑦 + 1)) = (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))
269	268	oveq2d 7039	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (𝐹‘(𝑦 + 1))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
270	247, 269	eqtrd 2833	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘(𝑦 + 1)) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))
271	270	oveq2d 7039	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘(𝑦 + 1))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))))))
272	271	oveq2d 7039	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘(𝑦 + 1)))) = ((π / 2) · (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))))))
273	135	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)))
274	174	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)) = ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))
275	273, 274	oveq12d 7041	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1))) = (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
276	275	oveq2d 7039	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) − 1)) · ((2 · (𝑦 + 1)) / ((2 · (𝑦 + 1)) + 1)))) = ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
277	276	oveq2d 7039	. . . . . . . . . 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 7039	. . . . . . . . 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 12790	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (1...𝑦) → 𝑤 ∈ ℕ)
280	279	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → 𝑤 ∈ ℕ)
281		oveq2 7031	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → (2 · 𝑘) = (2 · 𝑤))
282	281	oveq1d 7038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) − 1) = ((2 · 𝑤) − 1))
283	281, 282	oveq12d 7041	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) − 1)) = ((2 · 𝑤) / ((2 · 𝑤) − 1)))
284	281	oveq1d 7038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) + 1) = ((2 · 𝑤) + 1))
285	281, 284	oveq12d 7041	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑤 → ((2 · 𝑘) / ((2 · 𝑘) + 1)) = ((2 · 𝑤) / ((2 · 𝑤) + 1)))
286	283, 285	oveq12d 7041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑤 → (((2 · 𝑘) / ((2 · 𝑘) − 1)) · ((2 · 𝑘) / ((2 · 𝑘) + 1))) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
287		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℕ)
288		2rp 12248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
289	288	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ⁺)
290		nnrp 12254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ⁺)
291	289, 290	rpmulcld 12301	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ⁺)
292	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 2 ∈ ℝ)
293		nnre 11499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℝ)
294	292, 293	remulcld 10524	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (2 · 𝑤) ∈ ℝ)
295		1red 10495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 ∈ ℝ)
296	294, 295	resubcld 10922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ)
297		nnge1 11519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 1 ≤ 𝑤)
298		nncn 11500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
299	298	mulid2d 10512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) = 𝑤)
300	295, 292, 290	ltmul1d 12326	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ ℕ → (1 < 2 ↔ (1 · 𝑤) < (2 · 𝑤)))
301	256, 300	mpbii 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℕ → (1 · 𝑤) < (2 · 𝑤))
302	299, 301	eqbrtrrd 4992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℕ → 𝑤 < (2 · 𝑤))
303	295, 293, 294, 297, 302	lelttrd 10651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 1 < (2 · 𝑤))
304	295, 294	posdifd 11081	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → (1 < (2 · 𝑤) ↔ 0 < ((2 · 𝑤) − 1)))
305	303, 304	mpbid 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 < ((2 · 𝑤) − 1))
306	296, 305	elrpd 12282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) − 1) ∈ ℝ⁺)
307	291, 306	rpdivcld 12302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) − 1)) ∈ ℝ⁺)
308	154	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 2)
309	290	rpge0d 12289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℕ → 0 ≤ 𝑤)
310	292, 293, 308, 309	mulge0d 11071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℕ → 0 ≤ (2 · 𝑤))
311	294, 310	ge0p1rpd 12315	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) + 1) ∈ ℝ⁺)
312	291, 311	rpdivcld 12302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ℕ → ((2 · 𝑤) / ((2 · 𝑤) + 1)) ∈ ℝ⁺)
313	307, 312	rpmulcld 12301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℕ → (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))) ∈ ℝ⁺)
314	106, 286, 287, 313	fvmptd3 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) = (((2 · 𝑤) / ((2 · 𝑤) − 1)) · ((2 · 𝑤) / ((2 · 𝑤) + 1))))
315	314, 313	eqeltrd 2885	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℕ → (𝐹‘𝑤) ∈ ℝ⁺)
316	280, 315	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ (1...𝑦)) → (𝐹‘𝑤) ∈ ℝ⁺)
317		rpmulcl 12266	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺) → (𝑤 · 𝑧) ∈ ℝ⁺)
318	317	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ (𝑤 ∈ ℝ⁺ ∧ 𝑧 ∈ ℝ⁺)) → (𝑤 · 𝑧) ∈ ℝ⁺)
319	245, 316, 318	seqcl 13244	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℝ⁺)
320	319	rpcnne0d 12294	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((seq1( · , 𝐹)‘𝑦) ∈ ℂ ∧ (seq1( · , 𝐹)‘𝑦) ≠ 0))
321	288	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ⁺)
322	151, 157	ge0p1rpd 12315	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ⁺)
323	321, 322	rpmulcld 12301	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℝ⁺)
324	150, 151, 155, 157	mulge0d 11071	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → 0 ≤ (2 · 𝑦))
325	179, 324	ge0p1rpd 12315	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ⁺)
326	323, 325	rpdivcld 12302	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) ∈ ℝ⁺)
327	321, 258	rpmulcld 12301	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ⁺)
328	327, 217	rpaddcld 12300	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 3) ∈ ℝ⁺)
329	323, 328	rpdivcld 12302	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)) ∈ ℝ⁺)
330	326, 329	rpmulcld 12301	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℝ⁺)
331	330	rpcnne0d 12294	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ ∧ (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0))
332		divdiv1 11205	. . . . . . . . . . . . 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 1364	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))) = (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))))
334	333	eqcomd 2803	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / ((seq1( · , 𝐹)‘𝑦) · (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))) = ((1 / (seq1( · , 𝐹)‘𝑦)) / (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3)))))
335	334	oveq2d 7039	. . . . . . . . . 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 12287	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ∈ ℂ)
338	319	rpne0d 12290	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (seq1( · , 𝐹)‘𝑦) ≠ 0)
339	337, 338	reccld 11263	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (1 / (seq1( · , 𝐹)‘𝑦)) ∈ ℂ)
340	330	rpcnd 12287	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
341	330	rpne0d 12290	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ≠ 0)
342	336, 339, 340, 341	divassd 11305	. . . . . . . . . 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 3054	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ≠ 0)
344	197, 195, 197, 209, 343, 220	divmuldivd 11311	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) / ((2 · 𝑦) + 1)) · ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = (((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) / (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3))))
345	344	oveq2d 7039	. . . . . . . . . . 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 10514	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
347	197, 197	mulcld 10514	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ∈ ℂ)
348	195, 209	mulcld 10514	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ∈ ℂ)
349	197, 197, 201, 201	mulne0d 11146	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1))) ≠ 0)
350	195, 209, 343, 220	mulne0d 11146	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) ≠ 0)
351	346, 347, 348, 349, 350	divdiv2d 11302	. . . . . . . . . . . 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 11305	. . . . . . . . . . . 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 2833	. . . . . . . . . . 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 11317	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) = ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))))
355	354	eqcomd 2803	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) · ((2 · 𝑦) + 3)) / ((2 · (𝑦 + 1)) · (2 · (𝑦 + 1)))) = ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))))
356	355	oveq2d 7039	. . . . . . . . . . 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 2837	. . . . . . . . . 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 2839	. . . . . . . . 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 11736	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (π / 2) ∈ ℂ)
361	360, 339	mulcld 10514	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑦))) ∈ ℂ)
362	202, 221, 222	divcld 11270	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((((2 · 𝑦) + 1) / (2 · (𝑦 + 1))) / ((2 · (𝑦 + 1)) / ((2 · 𝑦) + 3))) ∈ ℂ)
363	361, 362	mulcomd 10515	. . . . . . . . 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 2837	. . . . . . . 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 2833	. . . . . . 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 2843	. . . . 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 11510	. . 3 ⊢ (𝑛 ∈ ℕ → ((𝐼‘(2 · 𝑛)) / (𝐼‘((2 · 𝑛) + 1))) = ((π / 2) · (1 / (seq1( · , 𝐹)‘𝑛))))
370	369	mpteq2ia 5058	. 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 2831	1 ⊢ 𝐺 = 𝐻

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ≠ wne 2986 class class class wbr 4968 ↦ cmpt 5047 ‘cfv 6232 (class class class)co 7023 ℂcc 10388 ℝcr 10389 0cc0 10390 1c1 10391 + caddc 10393 · cmul 10395 < clt 10528 ≤ cle 10529 − cmin 10723 / cdiv 11151 ℕcn 11492 2c2 11546 3c3 11547 ℕ₀cn0 11751 ℤcz 11835 ℤ_≥cuz 12097 ℝ⁺crp 12243 (,)cioo 12592 ...cfz 12746 seqcseq 13223 ↑cexp 13283 sincsin 15254 πcpi 15257 ∫citg 23906

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-inf2 8957 ax-cc 9710 ax-cnex 10446 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 ax-pre-sup 10468 ax-addf 10469 ax-mulf 10470

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-fal 1538 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-symdif 4145 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-int 4789 df-iun 4833 df-iin 4834 df-disj 4937 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-se 5410 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-isom 6241 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-of 7274 df-ofr 7275 df-om 7444 df-1st 7552 df-2nd 7553 df-supp 7689 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-1o 7960 df-2o 7961 df-oadd 7964 df-omul 7965 df-er 8146 df-map 8265 df-pm 8266 df-ixp 8318 df-en 8365 df-dom 8366 df-sdom 8367 df-fin 8368 df-fsupp 8687 df-fi 8728 df-sup 8759 df-inf 8760 df-oi 8827 df-dju 9183 df-card 9221 df-acn 9224 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-div 11152 df-nn 11493 df-2 11554 df-3 11555 df-4 11556 df-5 11557 df-6 11558 df-7 11559 df-8 11560 df-9 11561 df-n0 11752 df-z 11836 df-dec 11953 df-uz 12098 df-q 12202 df-rp 12244 df-xneg 12361 df-xadd 12362 df-xmul 12363 df-ioo 12596 df-ioc 12597 df-ico 12598 df-icc 12599 df-fz 12747 df-fzo 12888 df-fl 13016 df-mod 13092 df-seq 13224 df-exp 13284 df-fac 13488 df-bc 13517 df-hash 13545 df-shft 14264 df-cj 14296 df-re 14297 df-im 14298 df-sqrt 14432 df-abs 14433 df-limsup 14666 df-clim 14683 df-rlim 14684 df-sum 14881 df-ef 15258 df-sin 15260 df-cos 15261 df-pi 15263 df-struct 16318 df-ndx 16319 df-slot 16320 df-base 16322 df-sets 16323 df-ress 16324 df-plusg 16411 df-mulr 16412 df-starv 16413 df-sca 16414 df-vsca 16415 df-ip 16416 df-tset 16417 df-ple 16418 df-ds 16420 df-unif 16421 df-hom 16422 df-cco 16423 df-rest 16529 df-topn 16530 df-0g 16548 df-gsum 16549 df-topgen 16550 df-pt 16551 df-prds 16554 df-xrs 16608 df-qtop 16613 df-imas 16614 df-xps 16616 df-mre 16690 df-mrc 16691 df-acs 16693 df-mgm 17685 df-sgrp 17727 df-mnd 17738 df-submnd 17779 df-mulg 17986 df-cntz 18192 df-cmn 18639 df-psmet 20223 df-xmet 20224 df-met 20225 df-bl 20226 df-mopn 20227 df-fbas 20228 df-fg 20229 df-cnfld 20232 df-top 21190 df-topon 21207 df-topsp 21229 df-bases 21242 df-cld 21315 df-ntr 21316 df-cls 21317 df-nei 21394 df-lp 21432 df-perf 21433 df-cn 21523 df-cnp 21524 df-haus 21611 df-cmp 21683 df-tx 21858 df-hmeo 22051 df-fil 22142 df-fm 22234 df-flim 22235 df-flf 22236 df-xms 22617 df-ms 22618 df-tms 22619 df-cncf 23173 df-ovol 23752 df-vol 23753 df-mbf 23907 df-itg1 23908 df-itg2 23909 df-ibl 23910 df-itg 23911 df-0p 23958 df-limc 24151 df-dv 24152

This theorem is referenced by: wallispilem5 41918

W3C validator