wallispi2lem2 - Mathbox for Glauco Siliprandi

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

Theorem wallispi2lem2 46769

Description: Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.)

**Assertion**
Ref	Expression
wallispi2lem2	⊢ (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2)))

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

Step	Hyp	Ref	Expression
1		fveq2 6883	. . 3 ⊢ (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
2		oveq2 7420	. . . . . 6 ⊢ (𝑥 = 1 → (4 · 𝑥) = (4 · 1))
3	2	oveq2d 7428	. . . . 5 ⊢ (𝑥 = 1 → (2↑(4 · 𝑥)) = (2↑(4 · 1)))
4		fveq2 6883	. . . . . 6 ⊢ (𝑥 = 1 → (!‘𝑥) = (!‘1))
5	4	oveq1d 7427	. . . . 5 ⊢ (𝑥 = 1 → ((!‘𝑥)↑4) = ((!‘1)↑4))
6	3, 5	oveq12d 7430	. . . 4 ⊢ (𝑥 = 1 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · 1)) · ((!‘1)↑4)))
7		oveq2 7420	. . . . . 6 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
8	7	fveq2d 6887	. . . . 5 ⊢ (𝑥 = 1 → (!‘(2 · 𝑥)) = (!‘(2 · 1)))
9	8	oveq1d 7427	. . . 4 ⊢ (𝑥 = 1 → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · 1))↑2))
10	6, 9	oveq12d 7430	. . 3 ⊢ (𝑥 = 1 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2)))
11	1, 10	eqeq12d 2779	. 2 ⊢ (𝑥 = 1 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2))))
12		fveq2 6883	. . 3 ⊢ (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
13		oveq2 7420	. . . . . 6 ⊢ (𝑥 = 𝑦 → (4 · 𝑥) = (4 · 𝑦))
14	13	oveq2d 7428	. . . . 5 ⊢ (𝑥 = 𝑦 → (2↑(4 · 𝑥)) = (2↑(4 · 𝑦)))
15		fveq2 6883	. . . . . 6 ⊢ (𝑥 = 𝑦 → (!‘𝑥) = (!‘𝑦))
16	15	oveq1d 7427	. . . . 5 ⊢ (𝑥 = 𝑦 → ((!‘𝑥)↑4) = ((!‘𝑦)↑4))
17	14, 16	oveq12d 7430	. . . 4 ⊢ (𝑥 = 𝑦 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)))
18		oveq2 7420	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
19	18	fveq2d 6887	. . . . 5 ⊢ (𝑥 = 𝑦 → (!‘(2 · 𝑥)) = (!‘(2 · 𝑦)))
20	19	oveq1d 7427	. . . 4 ⊢ (𝑥 = 𝑦 → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · 𝑦))↑2))
21	17, 20	oveq12d 7430	. . 3 ⊢ (𝑥 = 𝑦 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)))
22	12, 21	eqeq12d 2779	. 2 ⊢ (𝑥 = 𝑦 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))))
23		fveq2 6883	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
24		oveq2 7420	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (4 · 𝑥) = (4 · (𝑦 + 1)))
25	24	oveq2d 7428	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (2↑(4 · 𝑥)) = (2↑(4 · (𝑦 + 1))))
26		fveq2 6883	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (!‘𝑥) = (!‘(𝑦 + 1)))
27	26	oveq1d 7427	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((!‘𝑥)↑4) = ((!‘(𝑦 + 1))↑4))
28	25, 27	oveq12d 7430	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)))
29		oveq2 7420	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
30	29	fveq2d 6887	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (!‘(2 · 𝑥)) = (!‘(2 · (𝑦 + 1))))
31	30	oveq1d 7427	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · (𝑦 + 1)))↑2))
32	28, 31	oveq12d 7430	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
33	23, 32	eqeq12d 2779	. 2 ⊢ (𝑥 = (𝑦 + 1) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2))))
34		fveq2 6883	. . 3 ⊢ (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
35		oveq2 7420	. . . . . 6 ⊢ (𝑥 = 𝑁 → (4 · 𝑥) = (4 · 𝑁))
36	35	oveq2d 7428	. . . . 5 ⊢ (𝑥 = 𝑁 → (2↑(4 · 𝑥)) = (2↑(4 · 𝑁)))
37		fveq2 6883	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
38	37	oveq1d 7427	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥)↑4) = ((!‘𝑁)↑4))
39	36, 38	oveq12d 7430	. . . 4 ⊢ (𝑥 = 𝑁 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)))
40		oveq2 7420	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
41	40	fveq2d 6887	. . . . 5 ⊢ (𝑥 = 𝑁 → (!‘(2 · 𝑥)) = (!‘(2 · 𝑁)))
42	41	oveq1d 7427	. . . 4 ⊢ (𝑥 = 𝑁 → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · 𝑁))↑2))
43	39, 42	oveq12d 7430	. . 3 ⊢ (𝑥 = 𝑁 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2)))
44	34, 43	eqeq12d 2779	. 2 ⊢ (𝑥 = 𝑁 → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) ↔ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2))))
45		1z 12625	. . . 4 ⊢ 1 ∈ ℤ
46		seq1 14052	. . . 4 ⊢ (1 ∈ ℤ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1))
47	45, 46	ax-mp 5	. . 3 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1)
48		1nn 12245	. . . 4 ⊢ 1 ∈ ℕ
49		oveq2 7420	. . . . . . 7 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
50	49	oveq1d 7427	. . . . . 6 ⊢ (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
51	49	oveq1d 7427	. . . . . . . 8 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
52	49, 51	oveq12d 7430	. . . . . . 7 ⊢ (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
53	52	oveq1d 7427	. . . . . 6 ⊢ (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
54	50, 53	oveq12d 7430	. . . . 5 ⊢ (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
55		eqid 2763	. . . . 5 ⊢ (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
56		ovex 7445	. . . . 5 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
57	54, 55, 56	fvmpt 6991	. . . 4 ⊢ (1 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
58	48, 57	ax-mp 5	. . 3 ⊢ ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘1) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2))
59		2t1e2 12404	. . . . . 6 ⊢ (2 · 1) = 2
60	59	oveq1i 7422	. . . . 5 ⊢ ((2 · 1)↑4) = (2↑4)
61		2exp4 17145	. . . . . . 7 ⊢ (2↑4) = ;16
62		1nn0 12521	. . . . . . . 8 ⊢ 1 ∈ ℕ₀
63		6nn0 12526	. . . . . . . 8 ⊢ 6 ∈ ℕ₀
64		0nn0 12520	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
65		1t1e1 12403	. . . . . . . . . 10 ⊢ (1 · 1) = 1
66	65	oveq1i 7422	. . . . . . . . 9 ⊢ ((1 · 1) + 0) = (1 + 0)
67		1p0e1 12364	. . . . . . . . 9 ⊢ (1 + 0) = 1
68	66, 67	eqtri 2786	. . . . . . . 8 ⊢ ((1 · 1) + 0) = 1
69		6cn 12333	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
70	69	mulridi 11214	. . . . . . . . 9 ⊢ (6 · 1) = 6
71	63	dec0h 12739	. . . . . . . . 9 ⊢ 6 = ;06
72	70, 71	eqtri 2786	. . . . . . . 8 ⊢ (6 · 1) = ;06
73	62, 62, 63, 61, 63, 64, 68, 72	decmul1c 12782	. . . . . . 7 ⊢ ((2↑4) · 1) = ;16
74	61, 73	eqtr4i 2789	. . . . . 6 ⊢ (2↑4) = ((2↑4) · 1)
75		2nn0 12522	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
76		2t2e4 12405	. . . . . . . . 9 ⊢ (2 · 2) = 4
77		sq1 14233	. . . . . . . . 9 ⊢ (1↑2) = 1
78	62, 75, 76, 77, 65	numexp2x 17139	. . . . . . . 8 ⊢ (1↑4) = 1
79	78	eqcomi 2772	. . . . . . 7 ⊢ 1 = (1↑4)
80	79	oveq2i 7423	. . . . . 6 ⊢ ((2↑4) · 1) = ((2↑4) · (1↑4))
81		4cn 12327	. . . . . . . . . 10 ⊢ 4 ∈ ℂ
82	81	mulridi 11214	. . . . . . . . 9 ⊢ (4 · 1) = 4
83	82	eqcomi 2772	. . . . . . . 8 ⊢ 4 = (4 · 1)
84	83	oveq2i 7423	. . . . . . 7 ⊢ (2↑4) = (2↑(4 · 1))
85		fac1 14315	. . . . . . . . 9 ⊢ (!‘1) = 1
86	85	eqcomi 2772	. . . . . . . 8 ⊢ 1 = (!‘1)
87	86	oveq1i 7422	. . . . . . 7 ⊢ (1↑4) = ((!‘1)↑4)
88	84, 87	oveq12i 7424	. . . . . 6 ⊢ ((2↑4) · (1↑4)) = ((2↑(4 · 1)) · ((!‘1)↑4))
89	74, 80, 88	3eqtri 2790	. . . . 5 ⊢ (2↑4) = ((2↑(4 · 1)) · ((!‘1)↑4))
90	60, 89	eqtri 2786	. . . 4 ⊢ ((2 · 1)↑4) = ((2↑(4 · 1)) · ((!‘1)↑4))
91	59	oveq1i 7422	. . . . . . . 8 ⊢ ((2 · 1) − 1) = (2 − 1)
92		2m1e1 12366	. . . . . . . 8 ⊢ (2 − 1) = 1
93	91, 92	eqtri 2786	. . . . . . 7 ⊢ ((2 · 1) − 1) = 1
94	93	oveq2i 7423	. . . . . 6 ⊢ ((2 · 1) · ((2 · 1) − 1)) = ((2 · 1) · 1)
95	59	oveq1i 7422	. . . . . . 7 ⊢ ((2 · 1) · 1) = (2 · 1)
96	95, 59	eqtri 2786	. . . . . 6 ⊢ ((2 · 1) · 1) = 2
97	59	fveq2i 6886	. . . . . . . 8 ⊢ (!‘(2 · 1)) = (!‘2)
98		fac2 14317	. . . . . . . 8 ⊢ (!‘2) = 2
99	97, 98	eqtri 2786	. . . . . . 7 ⊢ (!‘(2 · 1)) = 2
100	99	eqcomi 2772	. . . . . 6 ⊢ 2 = (!‘(2 · 1))
101	94, 96, 100	3eqtri 2790	. . . . 5 ⊢ ((2 · 1) · ((2 · 1) − 1)) = (!‘(2 · 1))
102	101	oveq1i 7422	. . . 4 ⊢ (((2 · 1) · ((2 · 1) − 1))↑2) = ((!‘(2 · 1))↑2)
103	90, 102	oveq12i 7424	. . 3 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2))
104	47, 58, 103	3eqtri 2790	. 2 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2))
105		elnnuz 12903	. . . . . 6 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
106	105	birani 508	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → 𝑦 ∈ (ℤ_≥‘1))
107		seqp1 14054	. . . . 5 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
108	106, 107	syl 18	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
109		simpr 489	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)))
110	109	oveq1d 7427	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
111		eqidd 2764	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
112		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
113	112	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
114	112	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
115	112, 114	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
116	115	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
117	113, 116	oveq12d 7430	. . . . . . . . 9 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
118	117	adantl 486	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
119		peano2nn 12246	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
120		2cnd 12320	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
121		nncn 12242	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
122		1cnd 11203	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
123	121, 122	addcld 11229	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
124	120, 123	mulcld 11230	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
125		4nn0 12524	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
126	125	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 4 ∈ ℕ₀)
127	124, 126	expcld 14184	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
128	124, 122	subcld 11570	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
129	124, 128	mulcld 11230	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
130	129	sqcld 14182	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
131		2pos 12346	. . . . . . . . . . . . . 14 ⊢ 0 < 2
132	131	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < 2)
133	132	gt0ne0d 11779	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
134	119	nnne0d 12287	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
135	120, 123, 133, 134	mulne0d 11867	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
136		1red 11210	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
137		2re 12316	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
138	137	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
139		nnre 12241	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
140	139, 136	readdcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
141		1lt2 12414	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
142	141	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 < 2)
143		nnrp 13029	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
144	136, 143	ltaddrp2d 13095	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
145	138, 140, 142, 144	mulgt1d 12152	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
146	136, 145	gtned 11346	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
147	124, 122, 146	subne0d 11579	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
148	124, 128, 135, 147	mulne0d 11867	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
149		2z 12627	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
150	149	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℤ)
151	129, 148, 150	expne0d 14190	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
152	127, 130, 151	divcld 11992	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
153	111, 118, 119, 152	fvmptd 6999	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
154	153	oveq2d 7428	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))))
155		nnnn0 12512	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
156	126, 155	nn0mulcld 12571	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (4 · 𝑦) ∈ ℕ₀)
157	120, 156	expcld 14184	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑(4 · 𝑦)) ∈ ℂ)
158		faccl 14321	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ₀ → (!‘𝑦) ∈ ℕ)
159		nncn 12242	. . . . . . . . . . 11 ⊢ ((!‘𝑦) ∈ ℕ → (!‘𝑦) ∈ ℂ)
160	155, 158, 159	3syl 19	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (!‘𝑦) ∈ ℂ)
161	160, 126	expcld 14184	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((!‘𝑦)↑4) ∈ ℂ)
162	157, 161	mulcld 11230	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) ∈ ℂ)
163	75	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ₀)
164	163, 155	nn0mulcld 12571	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ₀)
165		faccl 14321	. . . . . . . . . 10 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (!‘(2 · 𝑦)) ∈ ℕ)
166		nncn 12242	. . . . . . . . . 10 ⊢ ((!‘(2 · 𝑦)) ∈ ℕ → (!‘(2 · 𝑦)) ∈ ℂ)
167	164, 165, 166	3syl 19	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (!‘(2 · 𝑦)) ∈ ℂ)
168	167	sqcld 14182	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦))↑2) ∈ ℂ)
169	164, 165	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (!‘(2 · 𝑦)) ∈ ℕ)
170	169	nnne0d 12287	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (!‘(2 · 𝑦)) ≠ 0)
171	167, 170, 150	expne0d 14190	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦))↑2) ≠ 0)
172	162, 168, 127, 130, 171, 151	divmuldivd 12033	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) / (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))))
173	120, 123, 126	mulexpd 14199	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) = ((2↑4) · ((𝑦 + 1)↑4)))
174	173	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2↑4) · ((𝑦 + 1)↑4))))
175	120, 126	expcld 14184	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2↑4) ∈ ℂ)
176	123, 126	expcld 14184	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((𝑦 + 1)↑4) ∈ ℂ)
177	157, 161, 175, 176	mul4d 11423	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2↑4) · ((𝑦 + 1)↑4))) = (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦)↑4) · ((𝑦 + 1)↑4))))
178	160, 123, 126	mulexpd 14199	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((!‘𝑦) · (𝑦 + 1))↑4) = (((!‘𝑦)↑4) · ((𝑦 + 1)↑4)))
179	178	eqcomd 2769	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((!‘𝑦)↑4) · ((𝑦 + 1)↑4)) = (((!‘𝑦) · (𝑦 + 1))↑4))
180	179	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦)↑4) · ((𝑦 + 1)↑4))) = (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)))
181	174, 177, 180	3eqtrd 2802	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) = (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)))
182	120, 121	mulcld 11230	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
183	182, 122	addcld 11229	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
184	124, 183	mulcomd 11231	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1)) = (((2 · 𝑦) + 1) · (2 · (𝑦 + 1))))
185	184	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1))) = ((!‘(2 · 𝑦)) · (((2 · 𝑦) + 1) · (2 · (𝑦 + 1)))))
186	120, 121, 122	adddid 11234	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
187	186	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + (2 · 1)) − 1))
188	59, 120	eqeltrid 2867	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · 1) ∈ ℂ)
189	182, 188, 122	addsubassd 11590	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + (2 · 1)) − 1) = ((2 · 𝑦) + ((2 · 1) − 1)))
190	59	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
191	190	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 1) − 1) = (2 − 1))
192	191, 92	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 1) − 1) = 1)
193	192	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + ((2 · 1) − 1)) = ((2 · 𝑦) + 1))
194	187, 189, 193	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
195	194	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1)))
196	195	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))) = ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1))))
197	167, 183, 124	mulassd 11233	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))) = ((!‘(2 · 𝑦)) · (((2 · 𝑦) + 1) · (2 · (𝑦 + 1)))))
198	185, 196, 197	3eqtr4d 2808	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))) = (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))))
199	198	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))↑2) = ((((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1)))↑2))
200	167, 129, 163	mulexpd 14199	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))↑2) = (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
201		df-2 12304	. . . . . . . . . . . . . . 15 ⊢ 2 = (1 + 1)
202	201	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 = (1 + 1))
203	202	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = ((2 · 𝑦) + (1 + 1)))
204	182, 122, 122	addassd 11232	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) + 1) = ((2 · 𝑦) + (1 + 1)))
205	203, 204	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = (((2 · 𝑦) + 1) + 1))
206	205	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (!‘((2 · 𝑦) + 2)) = (!‘(((2 · 𝑦) + 1) + 1)))
207	62	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℕ₀)
208	164, 207	nn0addcld 12570	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ₀)
209		facp1 14316	. . . . . . . . . . . 12 ⊢ (((2 · 𝑦) + 1) ∈ ℕ₀ → (!‘(((2 · 𝑦) + 1) + 1)) = ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1)))
210	208, 209	syl 18	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (!‘(((2 · 𝑦) + 1) + 1)) = ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1)))
211		facp1 14316	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (!‘((2 · 𝑦) + 1)) = ((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)))
212	164, 211	syl 18	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (!‘((2 · 𝑦) + 1)) = ((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)))
213	202	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (1 + 1) = 2)
214	213	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (1 + 1)) = ((2 · 𝑦) + 2))
215	213, 201, 59	3eqtr4g 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 2 = (2 · 1))
216	215	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = ((2 · 𝑦) + (2 · 1)))
217	216, 186	eqtr4d 2801	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = (2 · (𝑦 + 1)))
218	204, 214, 217	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) + 1) = (2 · (𝑦 + 1)))
219	212, 218	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1)) = (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))))
220	206, 210, 219	3eqtrrd 2803	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))) = (!‘((2 · 𝑦) + 2)))
221	220	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1)))↑2) = ((!‘((2 · 𝑦) + 2))↑2))
222	199, 200, 221	3eqtr3d 2806	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((!‘((2 · 𝑦) + 2))↑2))
223	181, 222	oveq12d 7430	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) / (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 · 𝑦) + 2))↑2)))
224	172, 223	eqtrd 2798	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 · 𝑦) + 2))↑2)))
225	83	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 4 = (4 · 1))
226	225	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((4 · 𝑦) + 4) = ((4 · 𝑦) + (4 · 1)))
227	226	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑((4 · 𝑦) + 4)) = (2↑((4 · 𝑦) + (4 · 1))))
228	120, 126, 156	expaddd 14186	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑((4 · 𝑦) + 4)) = ((2↑(4 · 𝑦)) · (2↑4)))
229	81	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 4 ∈ ℂ)
230	229, 121, 122	adddid 11234	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (4 · (𝑦 + 1)) = ((4 · 𝑦) + (4 · 1)))
231	230	eqcomd 2769	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((4 · 𝑦) + (4 · 1)) = (4 · (𝑦 + 1)))
232	231	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑((4 · 𝑦) + (4 · 1))) = (2↑(4 · (𝑦 + 1))))
233	227, 228, 232	3eqtr3d 2806	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((2↑(4 · 𝑦)) · (2↑4)) = (2↑(4 · (𝑦 + 1))))
234		facp1 14316	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ₀ → (!‘(𝑦 + 1)) = ((!‘𝑦) · (𝑦 + 1)))
235	155, 234	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (!‘(𝑦 + 1)) = ((!‘𝑦) · (𝑦 + 1)))
236	235	eqcomd 2769	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((!‘𝑦) · (𝑦 + 1)) = (!‘(𝑦 + 1)))
237	236	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((!‘𝑦) · (𝑦 + 1))↑4) = ((!‘(𝑦 + 1))↑4))
238	233, 237	oveq12d 7430	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) = ((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)))
239	217	fveq2d 6887	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (!‘((2 · 𝑦) + 2)) = (!‘(2 · (𝑦 + 1))))
240	239	oveq1d 7427	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((!‘((2 · 𝑦) + 2))↑2) = ((!‘(2 · (𝑦 + 1)))↑2))
241	238, 240	oveq12d 7430	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 · 𝑦) + 2))↑2)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
242	154, 224, 241	3eqtrd 2802	. . . . 5 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
243	242	adantr 485	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
244	108, 110, 243	3eqtrd 2802	. . 3 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
245	244	ex 417	. 2 ⊢ (𝑦 ∈ ℕ → ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2))))
246	11, 22, 33, 44, 104, 245	nnind 12252	1 ⊢ (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 class class class wbr 5110 ↦ cmpt 5193 ‘cfv 6538 (class class class)co 7412 ℂcc 11099 ℝcr 11100 0cc0 11101 1c1 11102 + caddc 11104 · cmul 11106 < clt 11244 − cmin 11442 / cdiv 11872 ℕcn 12234 2c2 12296 4c4 12298 6c6 12300 ℕ₀cn0 12505 ℤcz 12592 cdc 12712 ℤ_≥cuz 12863 seqcseq 14039 ↑cexp 14099 !cfa 14311

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-5 12307 df-6 12308 df-7 12309 df-8 12310 df-9 12311 df-n0 12506 df-z 12593 df-dec 12713 df-uz 12864 df-rp 13018 df-seq 14040 df-exp 14100 df-fac 14312

This theorem is referenced by: wallispi2 46770

W3C validator