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 43503

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 6756	. . 3 ⊢ (𝑥 = 1 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1))
2		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 1 → (4 · 𝑥) = (4 · 1))
3	2	oveq2d 7271	. . . . 5 ⊢ (𝑥 = 1 → (2↑(4 · 𝑥)) = (2↑(4 · 1)))
4		fveq2 6756	. . . . . 6 ⊢ (𝑥 = 1 → (!‘𝑥) = (!‘1))
5	4	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 1 → ((!‘𝑥)↑4) = ((!‘1)↑4))
6	3, 5	oveq12d 7273	. . . 4 ⊢ (𝑥 = 1 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · 1)) · ((!‘1)↑4)))
7		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
8	7	fveq2d 6760	. . . . 5 ⊢ (𝑥 = 1 → (!‘(2 · 𝑥)) = (!‘(2 · 1)))
9	8	oveq1d 7270	. . . 4 ⊢ (𝑥 = 1 → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · 1))↑2))
10	6, 9	oveq12d 7273	. . 3 ⊢ (𝑥 = 1 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2)))
11	1, 10	eqeq12d 2754	. 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 6756	. . 3 ⊢ (𝑥 = 𝑦 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦))
13		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 𝑦 → (4 · 𝑥) = (4 · 𝑦))
14	13	oveq2d 7271	. . . . 5 ⊢ (𝑥 = 𝑦 → (2↑(4 · 𝑥)) = (2↑(4 · 𝑦)))
15		fveq2 6756	. . . . . 6 ⊢ (𝑥 = 𝑦 → (!‘𝑥) = (!‘𝑦))
16	15	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 𝑦 → ((!‘𝑥)↑4) = ((!‘𝑦)↑4))
17	14, 16	oveq12d 7273	. . . 4 ⊢ (𝑥 = 𝑦 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)))
18		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
19	18	fveq2d 6760	. . . . 5 ⊢ (𝑥 = 𝑦 → (!‘(2 · 𝑥)) = (!‘(2 · 𝑦)))
20	19	oveq1d 7270	. . . 4 ⊢ (𝑥 = 𝑦 → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · 𝑦))↑2))
21	17, 20	oveq12d 7273	. . 3 ⊢ (𝑥 = 𝑦 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)))
22	12, 21	eqeq12d 2754	. 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 6756	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)))
24		oveq2 7263	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (4 · 𝑥) = (4 · (𝑦 + 1)))
25	24	oveq2d 7271	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (2↑(4 · 𝑥)) = (2↑(4 · (𝑦 + 1))))
26		fveq2 6756	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (!‘𝑥) = (!‘(𝑦 + 1)))
27	26	oveq1d 7270	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((!‘𝑥)↑4) = ((!‘(𝑦 + 1))↑4))
28	25, 27	oveq12d 7273	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)))
29		oveq2 7263	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
30	29	fveq2d 6760	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (!‘(2 · 𝑥)) = (!‘(2 · (𝑦 + 1))))
31	30	oveq1d 7270	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · (𝑦 + 1)))↑2))
32	28, 31	oveq12d 7273	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
33	23, 32	eqeq12d 2754	. 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 6756	. . 3 ⊢ (𝑥 = 𝑁 → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑥) = (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁))
35		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 𝑁 → (4 · 𝑥) = (4 · 𝑁))
36	35	oveq2d 7271	. . . . 5 ⊢ (𝑥 = 𝑁 → (2↑(4 · 𝑥)) = (2↑(4 · 𝑁)))
37		fveq2 6756	. . . . . 6 ⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁))
38	37	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 𝑁 → ((!‘𝑥)↑4) = ((!‘𝑁)↑4))
39	36, 38	oveq12d 7273	. . . 4 ⊢ (𝑥 = 𝑁 → ((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) = ((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)))
40		oveq2 7263	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2 · 𝑥) = (2 · 𝑁))
41	40	fveq2d 6760	. . . . 5 ⊢ (𝑥 = 𝑁 → (!‘(2 · 𝑥)) = (!‘(2 · 𝑁)))
42	41	oveq1d 7270	. . . 4 ⊢ (𝑥 = 𝑁 → ((!‘(2 · 𝑥))↑2) = ((!‘(2 · 𝑁))↑2))
43	39, 42	oveq12d 7273	. . 3 ⊢ (𝑥 = 𝑁 → (((2↑(4 · 𝑥)) · ((!‘𝑥)↑4)) / ((!‘(2 · 𝑥))↑2)) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2)))
44	34, 43	eqeq12d 2754	. 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 12280	. . . 4 ⊢ 1 ∈ ℤ
46		seq1 13662	. . . 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 11914	. . . 4 ⊢ 1 ∈ ℕ
49		oveq2 7263	. . . . . . 7 ⊢ (𝑘 = 1 → (2 · 𝑘) = (2 · 1))
50	49	oveq1d 7270	. . . . . 6 ⊢ (𝑘 = 1 → ((2 · 𝑘)↑4) = ((2 · 1)↑4))
51	49	oveq1d 7270	. . . . . . . 8 ⊢ (𝑘 = 1 → ((2 · 𝑘) − 1) = ((2 · 1) − 1))
52	49, 51	oveq12d 7273	. . . . . . 7 ⊢ (𝑘 = 1 → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · 1) · ((2 · 1) − 1)))
53	52	oveq1d 7270	. . . . . 6 ⊢ (𝑘 = 1 → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · 1) · ((2 · 1) − 1))↑2))
54	50, 53	oveq12d 7273	. . . . 5 ⊢ (𝑘 = 1 → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)))
55		eqid 2738	. . . . 5 ⊢ (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))
56		ovex 7288	. . . . 5 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) ∈ V
57	54, 55, 56	fvmpt 6857	. . . 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 12066	. . . . . 6 ⊢ (2 · 1) = 2
60	59	oveq1i 7265	. . . . 5 ⊢ ((2 · 1)↑4) = (2↑4)
61		2exp4 16714	. . . . . . 7 ⊢ (2↑4) = ;16
62		1nn0 12179	. . . . . . . 8 ⊢ 1 ∈ ℕ₀
63		6nn0 12184	. . . . . . . 8 ⊢ 6 ∈ ℕ₀
64		0nn0 12178	. . . . . . . 8 ⊢ 0 ∈ ℕ₀
65		1t1e1 12065	. . . . . . . . . 10 ⊢ (1 · 1) = 1
66	65	oveq1i 7265	. . . . . . . . 9 ⊢ ((1 · 1) + 0) = (1 + 0)
67		1p0e1 12027	. . . . . . . . 9 ⊢ (1 + 0) = 1
68	66, 67	eqtri 2766	. . . . . . . 8 ⊢ ((1 · 1) + 0) = 1
69		6cn 11994	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
70	69	mulid1i 10910	. . . . . . . . 9 ⊢ (6 · 1) = 6
71	63	dec0h 12388	. . . . . . . . 9 ⊢ 6 = ;06
72	70, 71	eqtri 2766	. . . . . . . 8 ⊢ (6 · 1) = ;06
73	62, 62, 63, 61, 63, 64, 68, 72	decmul1c 12431	. . . . . . 7 ⊢ ((2↑4) · 1) = ;16
74	61, 73	eqtr4i 2769	. . . . . 6 ⊢ (2↑4) = ((2↑4) · 1)
75		2nn0 12180	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
76		2t2e4 12067	. . . . . . . . 9 ⊢ (2 · 2) = 4
77		sq1 13840	. . . . . . . . 9 ⊢ (1↑2) = 1
78	62, 75, 76, 77, 65	numexp2x 16708	. . . . . . . 8 ⊢ (1↑4) = 1
79	78	eqcomi 2747	. . . . . . 7 ⊢ 1 = (1↑4)
80	79	oveq2i 7266	. . . . . 6 ⊢ ((2↑4) · 1) = ((2↑4) · (1↑4))
81		4cn 11988	. . . . . . . . . 10 ⊢ 4 ∈ ℂ
82	81	mulid1i 10910	. . . . . . . . 9 ⊢ (4 · 1) = 4
83	82	eqcomi 2747	. . . . . . . 8 ⊢ 4 = (4 · 1)
84	83	oveq2i 7266	. . . . . . 7 ⊢ (2↑4) = (2↑(4 · 1))
85		fac1 13919	. . . . . . . . 9 ⊢ (!‘1) = 1
86	85	eqcomi 2747	. . . . . . . 8 ⊢ 1 = (!‘1)
87	86	oveq1i 7265	. . . . . . 7 ⊢ (1↑4) = ((!‘1)↑4)
88	84, 87	oveq12i 7267	. . . . . 6 ⊢ ((2↑4) · (1↑4)) = ((2↑(4 · 1)) · ((!‘1)↑4))
89	74, 80, 88	3eqtri 2770	. . . . 5 ⊢ (2↑4) = ((2↑(4 · 1)) · ((!‘1)↑4))
90	60, 89	eqtri 2766	. . . 4 ⊢ ((2 · 1)↑4) = ((2↑(4 · 1)) · ((!‘1)↑4))
91	59	oveq1i 7265	. . . . . . . 8 ⊢ ((2 · 1) − 1) = (2 − 1)
92		2m1e1 12029	. . . . . . . 8 ⊢ (2 − 1) = 1
93	91, 92	eqtri 2766	. . . . . . 7 ⊢ ((2 · 1) − 1) = 1
94	93	oveq2i 7266	. . . . . 6 ⊢ ((2 · 1) · ((2 · 1) − 1)) = ((2 · 1) · 1)
95	59	oveq1i 7265	. . . . . . 7 ⊢ ((2 · 1) · 1) = (2 · 1)
96	95, 59	eqtri 2766	. . . . . 6 ⊢ ((2 · 1) · 1) = 2
97	59	fveq2i 6759	. . . . . . . 8 ⊢ (!‘(2 · 1)) = (!‘2)
98		fac2 13921	. . . . . . . 8 ⊢ (!‘2) = 2
99	97, 98	eqtri 2766	. . . . . . 7 ⊢ (!‘(2 · 1)) = 2
100	99	eqcomi 2747	. . . . . 6 ⊢ 2 = (!‘(2 · 1))
101	94, 96, 100	3eqtri 2770	. . . . 5 ⊢ ((2 · 1) · ((2 · 1) − 1)) = (!‘(2 · 1))
102	101	oveq1i 7265	. . . 4 ⊢ (((2 · 1) · ((2 · 1) − 1))↑2) = ((!‘(2 · 1))↑2)
103	90, 102	oveq12i 7267	. . 3 ⊢ (((2 · 1)↑4) / (((2 · 1) · ((2 · 1) − 1))↑2)) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2))
104	47, 58, 103	3eqtri 2770	. 2 ⊢ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘1) = (((2↑(4 · 1)) · ((!‘1)↑4)) / ((!‘(2 · 1))↑2))
105		elnnuz 12551	. . . . . . 7 ⊢ (𝑦 ∈ ℕ ↔ 𝑦 ∈ (ℤ_≥‘1))
106	105	biimpi 215	. . . . . 6 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘1))
107	106	adantr 480	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2))) → 𝑦 ∈ (ℤ_≥‘1))
108		seqp1 13664	. . . . 5 ⊢ (𝑦 ∈ (ℤ_≥‘1) → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘(𝑦 + 1)) = ((seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑦) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))))
109	107, 108	syl 17	. . . 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))))
110		simpr 484	. . . . 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)))
111	110	oveq1d 7270	. . . 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))))
112		eqidd 2739	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))) = (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))
113		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑦 + 1) → (2 · 𝑘) = (2 · (𝑦 + 1)))
114	113	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘)↑4) = ((2 · (𝑦 + 1))↑4))
115	113	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) − 1) = ((2 · (𝑦 + 1)) − 1))
116	113, 115	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑦 + 1) → ((2 · 𝑘) · ((2 · 𝑘) − 1)) = ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))
117	116	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2) = (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))
118	114, 117	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑘 = (𝑦 + 1) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
119	118	adantl 481	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 𝑘 = (𝑦 + 1)) → (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
120		peano2nn 11915	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
121		2cnd 11981	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℂ)
122		nncn 11911	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
123		1cnd 10901	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℂ)
124	122, 123	addcld 10925	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
125	121, 124	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
126		4nn0 12182	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
127	126	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 4 ∈ ℕ₀)
128	125, 127	expcld 13792	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) ∈ ℂ)
129	125, 123	subcld 11262	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ∈ ℂ)
130	125, 129	mulcld 10926	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ∈ ℂ)
131	130	sqcld 13790	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ∈ ℂ)
132		2pos 12006	. . . . . . . . . . . . . 14 ⊢ 0 < 2
133	132	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 0 < 2)
134	133	gt0ne0d 11469	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 2 ≠ 0)
135	120	nnne0d 11953	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ≠ 0)
136	121, 124, 134, 135	mulne0d 11557	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 0)
137		1red 10907	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℝ)
138		2re 11977	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
139	138	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℝ)
140		nnre 11910	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
141	140, 137	readdcld 10935	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℝ)
142		1lt2 12074	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
143	142	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 < 2)
144		nnrp 12670	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
145	137, 144	ltaddrp2d 12735	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 1 < (𝑦 + 1))
146	139, 141, 143, 145	mulgt1d 11841	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 < (2 · (𝑦 + 1)))
147	137, 146	gtned 11040	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ≠ 1)
148	125, 123, 147	subne0d 11271	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) ≠ 0)
149	125, 129, 136, 148	mulne0d 11557	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) ≠ 0)
150		2z 12282	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
151	150	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℤ)
152	130, 149, 151	expne0d 13798	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2) ≠ 0)
153	128, 131, 152	divcld 11681	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) ∈ ℂ)
154	112, 119, 120, 153	fvmptd 6864	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1)) = (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
155	154	oveq2d 7271	. . . . . 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))))
156		nnnn0 12170	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
157	127, 156	nn0mulcld 12228	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (4 · 𝑦) ∈ ℕ₀)
158	121, 157	expcld 13792	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑(4 · 𝑦)) ∈ ℂ)
159		faccl 13925	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ₀ → (!‘𝑦) ∈ ℕ)
160		nncn 11911	. . . . . . . . . . 11 ⊢ ((!‘𝑦) ∈ ℕ → (!‘𝑦) ∈ ℂ)
161	156, 159, 160	3syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (!‘𝑦) ∈ ℂ)
162	161, 127	expcld 13792	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((!‘𝑦)↑4) ∈ ℂ)
163	158, 162	mulcld 10926	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) ∈ ℂ)
164	75	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 2 ∈ ℕ₀)
165	164, 156	nn0mulcld 12228	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℕ₀)
166		faccl 13925	. . . . . . . . . 10 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (!‘(2 · 𝑦)) ∈ ℕ)
167		nncn 11911	. . . . . . . . . 10 ⊢ ((!‘(2 · 𝑦)) ∈ ℕ → (!‘(2 · 𝑦)) ∈ ℂ)
168	165, 166, 167	3syl 18	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (!‘(2 · 𝑦)) ∈ ℂ)
169	168	sqcld 13790	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦))↑2) ∈ ℂ)
170	165, 166	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (!‘(2 · 𝑦)) ∈ ℕ)
171	170	nnne0d 11953	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (!‘(2 · 𝑦)) ≠ 0)
172	168, 171, 151	expne0d 13798	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦))↑2) ≠ 0)
173	163, 169, 128, 131, 172, 152	divmuldivd 11722	. . . . . . 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))))
174	121, 124, 127	mulexpd 13807	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1))↑4) = ((2↑4) · ((𝑦 + 1)↑4)))
175	174	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) = (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2↑4) · ((𝑦 + 1)↑4))))
176	121, 127	expcld 13792	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (2↑4) ∈ ℂ)
177	124, 127	expcld 13792	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((𝑦 + 1)↑4) ∈ ℂ)
178	158, 162, 176, 177	mul4d 11117	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2↑4) · ((𝑦 + 1)↑4))) = (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦)↑4) · ((𝑦 + 1)↑4))))
179	161, 124, 127	mulexpd 13807	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((!‘𝑦) · (𝑦 + 1))↑4) = (((!‘𝑦)↑4) · ((𝑦 + 1)↑4)))
180	179	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((!‘𝑦)↑4) · ((𝑦 + 1)↑4)) = (((!‘𝑦) · (𝑦 + 1))↑4))
181	180	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦)↑4) · ((𝑦 + 1)↑4))) = (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)))
182	175, 178, 181	3eqtrd 2782	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) = (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)))
183	121, 122	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
184	183, 123	addcld 10925	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℂ)
185	125, 184	mulcomd 10927	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1)) = (((2 · 𝑦) + 1) · (2 · (𝑦 + 1))))
186	185	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1))) = ((!‘(2 · 𝑦)) · (((2 · 𝑦) + 1) · (2 · (𝑦 + 1)))))
187	121, 122, 123	adddid 10930	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
188	187	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = (((2 · 𝑦) + (2 · 1)) − 1))
189	59, 121	eqeltrid 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (2 · 1) ∈ ℂ)
190	183, 189, 123	addsubassd 11282	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + (2 · 1)) − 1) = ((2 · 𝑦) + ((2 · 1) − 1)))
191	59	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (2 · 1) = 2)
192	191	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → ((2 · 1) − 1) = (2 − 1))
193	192, 92	eqtrdi 2795	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → ((2 · 1) − 1) = 1)
194	193	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + ((2 · 1) − 1)) = ((2 · 𝑦) + 1))
195	188, 190, 194	3eqtrd 2782	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) − 1) = ((2 · 𝑦) + 1))
196	195	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)) = ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1)))
197	196	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))) = ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · 𝑦) + 1))))
198	168, 184, 125	mulassd 10929	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))) = ((!‘(2 · 𝑦)) · (((2 · 𝑦) + 1) · (2 · (𝑦 + 1)))))
199	186, 197, 198	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))) = (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))))
200	199	oveq1d 7270	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))↑2) = ((((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1)))↑2))
201	168, 130, 164	mulexpd 13807	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1)))↑2) = (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)))
202		df-2 11966	. . . . . . . . . . . . . . 15 ⊢ 2 = (1 + 1)
203	202	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 2 = (1 + 1))
204	203	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = ((2 · 𝑦) + (1 + 1)))
205	183, 123, 123	addassd 10928	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) + 1) = ((2 · 𝑦) + (1 + 1)))
206	204, 205	eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = (((2 · 𝑦) + 1) + 1))
207	206	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (!‘((2 · 𝑦) + 2)) = (!‘(((2 · 𝑦) + 1) + 1)))
208	62	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → 1 ∈ ℕ₀)
209	165, 208	nn0addcld 12227	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℕ₀)
210		facp1 13920	. . . . . . . . . . . 12 ⊢ (((2 · 𝑦) + 1) ∈ ℕ₀ → (!‘(((2 · 𝑦) + 1) + 1)) = ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1)))
211	209, 210	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (!‘(((2 · 𝑦) + 1) + 1)) = ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1)))
212		facp1 13920	. . . . . . . . . . . . 13 ⊢ ((2 · 𝑦) ∈ ℕ₀ → (!‘((2 · 𝑦) + 1)) = ((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)))
213	165, 212	syl 17	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (!‘((2 · 𝑦) + 1)) = ((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)))
214	203	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (1 + 1) = 2)
215	214	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + (1 + 1)) = ((2 · 𝑦) + 2))
216	214, 202, 59	3eqtr4g 2804	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 2 = (2 · 1))
217	216	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = ((2 · 𝑦) + (2 · 1)))
218	217, 187	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((2 · 𝑦) + 2) = (2 · (𝑦 + 1)))
219	205, 215, 218	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) + 1) = (2 · (𝑦 + 1)))
220	213, 219	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → ((!‘((2 · 𝑦) + 1)) · (((2 · 𝑦) + 1) + 1)) = (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))))
221	207, 211, 220	3eqtrrd 2783	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1))) = (!‘((2 · 𝑦) + 2)))
222	221	oveq1d 7270	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((((!‘(2 · 𝑦)) · ((2 · 𝑦) + 1)) · (2 · (𝑦 + 1)))↑2) = ((!‘((2 · 𝑦) + 2))↑2))
223	200, 201, 222	3eqtr3d 2786	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2)) = ((!‘((2 · 𝑦) + 2))↑2))
224	182, 223	oveq12d 7273	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) · ((2 · (𝑦 + 1))↑4)) / (((!‘(2 · 𝑦))↑2) · (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 · 𝑦) + 2))↑2)))
225	173, 224	eqtrd 2778	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · (((2 · (𝑦 + 1))↑4) / (((2 · (𝑦 + 1)) · ((2 · (𝑦 + 1)) − 1))↑2))) = ((((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 · 𝑦) + 2))↑2)))
226	83	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → 4 = (4 · 1))
227	226	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((4 · 𝑦) + 4) = ((4 · 𝑦) + (4 · 1)))
228	227	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑((4 · 𝑦) + 4)) = (2↑((4 · 𝑦) + (4 · 1))))
229	121, 127, 157	expaddd 13794	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑((4 · 𝑦) + 4)) = ((2↑(4 · 𝑦)) · (2↑4)))
230	81	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → 4 ∈ ℂ)
231	230, 122, 123	adddid 10930	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ → (4 · (𝑦 + 1)) = ((4 · 𝑦) + (4 · 1)))
232	231	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → ((4 · 𝑦) + (4 · 1)) = (4 · (𝑦 + 1)))
233	232	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (2↑((4 · 𝑦) + (4 · 1))) = (2↑(4 · (𝑦 + 1))))
234	228, 229, 233	3eqtr3d 2786	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((2↑(4 · 𝑦)) · (2↑4)) = (2↑(4 · (𝑦 + 1))))
235		facp1 13920	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℕ₀ → (!‘(𝑦 + 1)) = ((!‘𝑦) · (𝑦 + 1)))
236	156, 235	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (!‘(𝑦 + 1)) = ((!‘𝑦) · (𝑦 + 1)))
237	236	eqcomd 2744	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → ((!‘𝑦) · (𝑦 + 1)) = (!‘(𝑦 + 1)))
238	237	oveq1d 7270	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (((!‘𝑦) · (𝑦 + 1))↑4) = ((!‘(𝑦 + 1))↑4))
239	234, 238	oveq12d 7273	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) = ((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)))
240	218	fveq2d 6760	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (!‘((2 · 𝑦) + 2)) = (!‘(2 · (𝑦 + 1))))
241	240	oveq1d 7270	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((!‘((2 · 𝑦) + 2))↑2) = ((!‘(2 · (𝑦 + 1)))↑2))
242	239, 241	oveq12d 7273	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · (2↑4)) · (((!‘𝑦) · (𝑦 + 1))↑4)) / ((!‘((2 · 𝑦) + 2))↑2)) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
243	155, 225, 242	3eqtrd 2782	. . . . 5 ⊢ (𝑦 ∈ ℕ → ((((2↑(4 · 𝑦)) · ((!‘𝑦)↑4)) / ((!‘(2 · 𝑦))↑2)) · ((𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2)))‘(𝑦 + 1))) = (((2↑(4 · (𝑦 + 1))) · ((!‘(𝑦 + 1))↑4)) / ((!‘(2 · (𝑦 + 1)))↑2)))
244	243	adantr 480	. . . 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)))
245	109, 111, 244	3eqtrd 2782	. . 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)))
246	245	ex 412	. 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))))
247	11, 22, 33, 44, 104, 246	nnind 11921	1 ⊢ (𝑁 ∈ ℕ → (seq1( · , (𝑘 ∈ ℕ ↦ (((2 · 𝑘)↑4) / (((2 · 𝑘) · ((2 · 𝑘) − 1))↑2))))‘𝑁) = (((2↑(4 · 𝑁)) · ((!‘𝑁)↑4)) / ((!‘(2 · 𝑁))↑2)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2108 class class class wbr 5070 ↦ cmpt 5153 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 − cmin 11135 / cdiv 11562 ℕcn 11903 2c2 11958 4c4 11960 6c6 11962 ℕ₀cn0 12163 ℤcz 12249 cdc 12366 ℤ_≥cuz 12511 seqcseq 13649 ↑cexp 13710 !cfa 13915

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-fac 13916

This theorem is referenced by: wallispi2 43504

W3C validator