Theorem wallispi2lem2

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)

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 1 → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 1 ) )
2		oveq2	⊢ ( 𝑥 = 1 → ( 4 · 𝑥 ) = ( 4 · 1 ) )
3	2	oveq2d	⊢ ( 𝑥 = 1 → ( 2 ↑ ( 4 · 𝑥 ) ) = ( 2 ↑ ( 4 · 1 ) ) )
4		fveq2	⊢ ( 𝑥 = 1 → ( ! ‘ 𝑥 ) = ( ! ‘ 1 ) )
5	4	oveq1d	⊢ ( 𝑥 = 1 → ( ( ! ‘ 𝑥 ) ↑ 4 ) = ( ( ! ‘ 1 ) ↑ 4 ) )
6	3 5	oveq12d	⊢ ( 𝑥 = 1 → ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) = ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) ) )
7		oveq2	⊢ ( 𝑥 = 1 → ( 2 · 𝑥 ) = ( 2 · 1 ) )
8	7	fveq2d	⊢ ( 𝑥 = 1 → ( ! ‘ ( 2 · 𝑥 ) ) = ( ! ‘ ( 2 · 1 ) ) )
9	8	oveq1d	⊢ ( 𝑥 = 1 → ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · 1 ) ) ↑ 2 ) )
10	6 9	oveq12d	⊢ ( 𝑥 = 1 → ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 1 ) ) ↑ 2 ) ) )
11	1 10	eqeq12d	⊢ ( 𝑥 = 1 → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) ↔ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 1 ) = ( ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 1 ) ) ↑ 2 ) ) ) )
12		fveq2	⊢ ( 𝑥 = 𝑦 → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) )
13		oveq2	⊢ ( 𝑥 = 𝑦 → ( 4 · 𝑥 ) = ( 4 · 𝑦 ) )
14	13	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 2 ↑ ( 4 · 𝑥 ) ) = ( 2 ↑ ( 4 · 𝑦 ) ) )
15		fveq2	⊢ ( 𝑥 = 𝑦 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑦 ) )
16	15	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( ! ‘ 𝑥 ) ↑ 4 ) = ( ( ! ‘ 𝑦 ) ↑ 4 ) )
17	14 16	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) = ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) )
18		oveq2	⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
19	18	fveq2d	⊢ ( 𝑥 = 𝑦 → ( ! ‘ ( 2 · 𝑥 ) ) = ( ! ‘ ( 2 · 𝑦 ) ) )
20	19	oveq1d	⊢ ( 𝑥 = 𝑦 → ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) )
21	17 20	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) )
22	12 21	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) ↔ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) )
23		fveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ ( 𝑦 + 1 ) ) )
24		oveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 4 · 𝑥 ) = ( 4 · ( 𝑦 + 1 ) ) )
25	24	oveq2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 2 ↑ ( 4 · 𝑥 ) ) = ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) )
26		fveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ! ‘ 𝑥 ) = ( ! ‘ ( 𝑦 + 1 ) ) )
27	26	oveq1d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ! ‘ 𝑥 ) ↑ 4 ) = ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) )
28	25 27	oveq12d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) = ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) )
29		oveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 2 · 𝑥 ) = ( 2 · ( 𝑦 + 1 ) ) )
30	29	fveq2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ! ‘ ( 2 · 𝑥 ) ) = ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) )
31	30	oveq1d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) )
32	28 31	oveq12d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) )
33	23 32	eqeq12d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) ↔ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) ) )
34		fveq2	⊢ ( 𝑥 = 𝑁 → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑁 ) )
35		oveq2	⊢ ( 𝑥 = 𝑁 → ( 4 · 𝑥 ) = ( 4 · 𝑁 ) )
36	35	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 2 ↑ ( 4 · 𝑥 ) ) = ( 2 ↑ ( 4 · 𝑁 ) ) )
37		fveq2	⊢ ( 𝑥 = 𝑁 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑁 ) )
38	37	oveq1d	⊢ ( 𝑥 = 𝑁 → ( ( ! ‘ 𝑥 ) ↑ 4 ) = ( ( ! ‘ 𝑁 ) ↑ 4 ) )
39	36 38	oveq12d	⊢ ( 𝑥 = 𝑁 → ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) = ( ( 2 ↑ ( 4 · 𝑁 ) ) · ( ( ! ‘ 𝑁 ) ↑ 4 ) ) )
40		oveq2	⊢ ( 𝑥 = 𝑁 → ( 2 · 𝑥 ) = ( 2 · 𝑁 ) )
41	40	fveq2d	⊢ ( 𝑥 = 𝑁 → ( ! ‘ ( 2 · 𝑥 ) ) = ( ! ‘ ( 2 · 𝑁 ) ) )
42	41	oveq1d	⊢ ( 𝑥 = 𝑁 → ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) ↑ 2 ) )
43	39 42	oveq12d	⊢ ( 𝑥 = 𝑁 → ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · 𝑁 ) ) · ( ( ! ‘ 𝑁 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑁 ) ) ↑ 2 ) ) )
44	34 43	eqeq12d	⊢ ( 𝑥 = 𝑁 → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑥 ) = ( ( ( 2 ↑ ( 4 · 𝑥 ) ) · ( ( ! ‘ 𝑥 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑥 ) ) ↑ 2 ) ) ↔ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑁 ) = ( ( ( 2 ↑ ( 4 · 𝑁 ) ) · ( ( ! ‘ 𝑁 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑁 ) ) ↑ 2 ) ) ) )
45		1z	⊢ 1 ∈ ℤ
46		seq1	⊢ ( 1 ∈ ℤ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 1 ) )
47	45 46	ax-mp	⊢ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 1 )
48		1nn	⊢ 1 ∈ ℕ
49		oveq2	⊢ ( 𝑘 = 1 → ( 2 · 𝑘 ) = ( 2 · 1 ) )
50	49	oveq1d	⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) ↑ 4 ) = ( ( 2 · 1 ) ↑ 4 ) )
51	49	oveq1d	⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · 1 ) − 1 ) )
52	49 51	oveq12d	⊢ ( 𝑘 = 1 → ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) = ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) )
53	52	oveq1d	⊢ ( 𝑘 = 1 → ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) = ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) )
54	50 53	oveq12d	⊢ ( 𝑘 = 1 → ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 · 1 ) ↑ 4 ) / ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) ) )
55		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) )
56		ovex	⊢ ( ( ( 2 · 1 ) ↑ 4 ) / ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) ) ∈ V
57	54 55 56	fvmpt	⊢ ( 1 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 1 ) = ( ( ( 2 · 1 ) ↑ 4 ) / ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) ) )
58	48 57	ax-mp	⊢ ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ 1 ) = ( ( ( 2 · 1 ) ↑ 4 ) / ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) )
59		2t1e2	⊢ ( 2 · 1 ) = 2
60	59	oveq1i	⊢ ( ( 2 · 1 ) ↑ 4 ) = ( 2 ↑ 4 )
61		2exp4	⊢ ( 2 ↑ 4 ) = ; 1 6
62		1nn0	⊢ 1 ∈ ℕ0
63		6nn0	⊢ 6 ∈ ℕ0
64		0nn0	⊢ 0 ∈ ℕ0
65		1t1e1	⊢ ( 1 · 1 ) = 1
66	65	oveq1i	⊢ ( ( 1 · 1 ) + 0 ) = ( 1 + 0 )
67		1p0e1	⊢ ( 1 + 0 ) = 1
68	66 67	eqtri	⊢ ( ( 1 · 1 ) + 0 ) = 1
69		6cn	⊢ 6 ∈ ℂ
70	69	mulridi	⊢ ( 6 · 1 ) = 6
71	63	dec0h	⊢ 6 = ; 0 6
72	70 71	eqtri	⊢ ( 6 · 1 ) = ; 0 6
73	62 62 63 61 63 64 68 72	decmul1c	⊢ ( ( 2 ↑ 4 ) · 1 ) = ; 1 6
74	61 73	eqtr4i	⊢ ( 2 ↑ 4 ) = ( ( 2 ↑ 4 ) · 1 )
75		2nn0	⊢ 2 ∈ ℕ0
76		2t2e4	⊢ ( 2 · 2 ) = 4
77		sq1	⊢ ( 1 ↑ 2 ) = 1
78	62 75 76 77 65	numexp2x	⊢ ( 1 ↑ 4 ) = 1
79	78	eqcomi	⊢ 1 = ( 1 ↑ 4 )
80	79	oveq2i	⊢ ( ( 2 ↑ 4 ) · 1 ) = ( ( 2 ↑ 4 ) · ( 1 ↑ 4 ) )
81		4cn	⊢ 4 ∈ ℂ
82	81	mulridi	⊢ ( 4 · 1 ) = 4
83	82	eqcomi	⊢ 4 = ( 4 · 1 )
84	83	oveq2i	⊢ ( 2 ↑ 4 ) = ( 2 ↑ ( 4 · 1 ) )
85		fac1	⊢ ( ! ‘ 1 ) = 1
86	85	eqcomi	⊢ 1 = ( ! ‘ 1 )
87	86	oveq1i	⊢ ( 1 ↑ 4 ) = ( ( ! ‘ 1 ) ↑ 4 )
88	84 87	oveq12i	⊢ ( ( 2 ↑ 4 ) · ( 1 ↑ 4 ) ) = ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) )
89	74 80 88	3eqtri	⊢ ( 2 ↑ 4 ) = ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) )
90	60 89	eqtri	⊢ ( ( 2 · 1 ) ↑ 4 ) = ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) )
91	59	oveq1i	⊢ ( ( 2 · 1 ) − 1 ) = ( 2 − 1 )
92		2m1e1	⊢ ( 2 − 1 ) = 1
93	91 92	eqtri	⊢ ( ( 2 · 1 ) − 1 ) = 1
94	93	oveq2i	⊢ ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) = ( ( 2 · 1 ) · 1 )
95	59	oveq1i	⊢ ( ( 2 · 1 ) · 1 ) = ( 2 · 1 )
96	95 59	eqtri	⊢ ( ( 2 · 1 ) · 1 ) = 2
97	59	fveq2i	⊢ ( ! ‘ ( 2 · 1 ) ) = ( ! ‘ 2 )
98		fac2	⊢ ( ! ‘ 2 ) = 2
99	97 98	eqtri	⊢ ( ! ‘ ( 2 · 1 ) ) = 2
100	99	eqcomi	⊢ 2 = ( ! ‘ ( 2 · 1 ) )
101	94 96 100	3eqtri	⊢ ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) = ( ! ‘ ( 2 · 1 ) )
102	101	oveq1i	⊢ ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · 1 ) ) ↑ 2 )
103	90 102	oveq12i	⊢ ( ( ( 2 · 1 ) ↑ 4 ) / ( ( ( 2 · 1 ) · ( ( 2 · 1 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 1 ) ) ↑ 2 ) )
104	47 58 103	3eqtri	⊢ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 1 ) = ( ( ( 2 ↑ ( 4 · 1 ) ) · ( ( ! ‘ 1 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 1 ) ) ↑ 2 ) )
105		elnnuz	⊢ ( 𝑦 ∈ ℕ ↔ 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
106	105	biimpi	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
107	106	adantr	⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
108		seqp1	⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) · ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ ( 𝑦 + 1 ) ) ) )
109	107 108	syl	⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) · ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ ( 𝑦 + 1 ) ) ) )
110		simpr	⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) )
111	110	oveq1d	⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 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	⊢ ( 𝑦 ∈ ℕ → ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) )
113		oveq2	⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( 2 · 𝑘 ) = ( 2 · ( 𝑦 + 1 ) ) )
114	113	oveq1d	⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) ↑ 4 ) = ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) )
115	113	oveq1d	⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) )
116	113 115	oveq12d	⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) )
117	116	oveq1d	⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) = ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) )
118	114 117	oveq12d	⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
119	118	adantl	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑘 = ( 𝑦 + 1 ) ) → ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
120		peano2nn	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
121		2cnd	⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℂ )
122		nncn	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
123		1cnd	⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℂ )
124	122 123	addcld	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℂ )
125	121 124	mulcld	⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ℂ )
126		4nn0	⊢ 4 ∈ ℕ0
127	126	a1i	⊢ ( 𝑦 ∈ ℕ → 4 ∈ ℕ0 )
128	125 127	expcld	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) ∈ ℂ )
129	125 123	subcld	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ∈ ℂ )
130	125 129	mulcld	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ∈ ℂ )
131	130	sqcld	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ∈ ℂ )
132		2pos	⊢ 0 < 2
133	132	a1i	⊢ ( 𝑦 ∈ ℕ → 0 < 2 )
134	133	gt0ne0d	⊢ ( 𝑦 ∈ ℕ → 2 ≠ 0 )
135	120	nnne0d	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ≠ 0 )
136	121 124 134 135	mulne0d	⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ≠ 0 )
137		1red	⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℝ )
138		2re	⊢ 2 ∈ ℝ
139	138	a1i	⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℝ )
140		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
141	140 137	readdcld	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℝ )
142		1lt2	⊢ 1 < 2
143	142	a1i	⊢ ( 𝑦 ∈ ℕ → 1 < 2 )
144		nnrp	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ+ )
145	137 144	ltaddrp2d	⊢ ( 𝑦 ∈ ℕ → 1 < ( 𝑦 + 1 ) )
146	139 141 143 145	mulgt1d	⊢ ( 𝑦 ∈ ℕ → 1 < ( 2 · ( 𝑦 + 1 ) ) )
147	137 146	gtned	⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ≠ 1 )
148	125 123 147	subne0d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ≠ 0 )
149	125 129 136 148	mulne0d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ≠ 0 )
150		2z	⊢ 2 ∈ ℤ
151	150	a1i	⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℤ )
152	130 149 151	expne0d	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ≠ 0 )
153	128 131 152	divcld	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) ∈ ℂ )
154	112 119 120 153	fvmptd	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
155	154	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 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	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
157	127 156	nn0mulcld	⊢ ( 𝑦 ∈ ℕ → ( 4 · 𝑦 ) ∈ ℕ0 )
158	121 157	expcld	⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( 4 · 𝑦 ) ) ∈ ℂ )
159		faccl	⊢ ( 𝑦 ∈ ℕ0 → ( ! ‘ 𝑦 ) ∈ ℕ )
160		nncn	⊢ ( ( ! ‘ 𝑦 ) ∈ ℕ → ( ! ‘ 𝑦 ) ∈ ℂ )
161	156 159 160	3syl	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ 𝑦 ) ∈ ℂ )
162	161 127	expcld	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ 𝑦 ) ↑ 4 ) ∈ ℂ )
163	158 162	mulcld	⊢ ( 𝑦 ∈ ℕ → ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) ∈ ℂ )
164	75	a1i	⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℕ0 )
165	164 156	nn0mulcld	⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℕ0 )
166		faccl	⊢ ( ( 2 · 𝑦 ) ∈ ℕ0 → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℕ )
167		nncn	⊢ ( ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℂ )
168	165 166 167	3syl	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℂ )
169	168	sqcld	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ∈ ℂ )
170	165 166	syl	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℕ )
171	170	nnne0d	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ≠ 0 )
172	168 171 151	expne0d	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ≠ 0 )
173	163 169 128 131 172 152	divmuldivd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 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	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) = ( ( 2 ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) )
175	174	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) )
176	121 127	expcld	⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ 4 ) ∈ ℂ )
177	124 127	expcld	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑦 + 1 ) ↑ 4 ) ∈ ℂ )
178	158 162 176 177	mul4d	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) )
179	161 124 127	mulexpd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) = ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) )
180	179	eqcomd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) = ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) )
181	180	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) )
182	175 178 181	3eqtrd	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) )
183	121 122	mulcld	⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℂ )
184	183 123	addcld	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ∈ ℂ )
185	125 184	mulcomd	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) = ( ( ( 2 · 𝑦 ) + 1 ) · ( 2 · ( 𝑦 + 1 ) ) ) )
186	185	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) · ( 2 · ( 𝑦 + 1 ) ) ) ) )
187	121 122 123	adddid	⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) = ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) )
188	187	oveq1d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) = ( ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) − 1 ) )
189	59 121	eqeltrid	⊢ ( 𝑦 ∈ ℕ → ( 2 · 1 ) ∈ ℂ )
190	183 189 123	addsubassd	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) − 1 ) = ( ( 2 · 𝑦 ) + ( ( 2 · 1 ) − 1 ) ) )
191	59	a1i	⊢ ( 𝑦 ∈ ℕ → ( 2 · 1 ) = 2 )
192	191	oveq1d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 1 ) − 1 ) = ( 2 − 1 ) )
193	192 92	eqtrdi	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 1 ) − 1 ) = 1 )
194	193	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( ( 2 · 1 ) − 1 ) ) = ( ( 2 · 𝑦 ) + 1 ) )
195	188 190 194	3eqtrd	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) = ( ( 2 · 𝑦 ) + 1 ) )
196	195	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) )
197	196	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) ) )
198	168 184 125	mulassd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) · ( 2 · ( 𝑦 + 1 ) ) ) ) )
199	186 197 198	3eqtr4d	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) = ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) )
200	199	oveq1d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) ↑ 2 ) = ( ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) )
201	168 130 164	mulexpd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) ↑ 2 ) = ( ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
202		df-2	⊢ 2 = ( 1 + 1 )
203	202	a1i	⊢ ( 𝑦 ∈ ℕ → 2 = ( 1 + 1 ) )
204	203	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( ( 2 · 𝑦 ) + ( 1 + 1 ) ) )
205	183 123 123	addassd	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) = ( ( 2 · 𝑦 ) + ( 1 + 1 ) ) )
206	204 205	eqtr4d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) )
207	206	fveq2d	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) = ( ! ‘ ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) )
208	62	a1i	⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℕ0 )
209	165 208	nn0addcld	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ∈ ℕ0 )
210		facp1	⊢ ( ( ( 2 · 𝑦 ) + 1 ) ∈ ℕ0 → ( ! ‘ ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) )
211	209 210	syl	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) )
212		facp1	⊢ ( ( 2 · 𝑦 ) ∈ ℕ0 → ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) )
213	165 212	syl	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) )
214	203	eqcomd	⊢ ( 𝑦 ∈ ℕ → ( 1 + 1 ) = 2 )
215	214	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 1 + 1 ) ) = ( ( 2 · 𝑦 ) + 2 ) )
216	214 202 59	3eqtr4g	⊢ ( 𝑦 ∈ ℕ → 2 = ( 2 · 1 ) )
217	216	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) )
218	217 187	eqtr4d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( 2 · ( 𝑦 + 1 ) ) )
219	205 215 218	3eqtrd	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) = ( 2 · ( 𝑦 + 1 ) ) )
220	213 219	oveq12d	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) = ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) )
221	207 211 220	3eqtrrd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) = ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) )
222	221	oveq1d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) )
223	200 201 222	3eqtr3d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) )
224	182 223	oveq12d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 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	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 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	⊢ ( 𝑦 ∈ ℕ → 4 = ( 4 · 1 ) )
227	226	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( ( 4 · 𝑦 ) + 4 ) = ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) )
228	227	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 4 · 𝑦 ) + 4 ) ) = ( 2 ↑ ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) ) )
229	121 127 157	expaddd	⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 4 · 𝑦 ) + 4 ) ) = ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) )
230	81	a1i	⊢ ( 𝑦 ∈ ℕ → 4 ∈ ℂ )
231	230 122 123	adddid	⊢ ( 𝑦 ∈ ℕ → ( 4 · ( 𝑦 + 1 ) ) = ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) )
232	231	eqcomd	⊢ ( 𝑦 ∈ ℕ → ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) = ( 4 · ( 𝑦 + 1 ) ) )
233	232	oveq2d	⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) ) = ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) )
234	228 229 233	3eqtr3d	⊢ ( 𝑦 ∈ ℕ → ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) = ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) )
235		facp1	⊢ ( 𝑦 ∈ ℕ0 → ( ! ‘ ( 𝑦 + 1 ) ) = ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) )
236	156 235	syl	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 𝑦 + 1 ) ) = ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) )
237	236	eqcomd	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) = ( ! ‘ ( 𝑦 + 1 ) ) )
238	237	oveq1d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) = ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) )
239	234 238	oveq12d	⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) = ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) )
240	218	fveq2d	⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) = ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) )
241	240	oveq1d	⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) )
242	239 241	oveq12d	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) )
243	155 225 242	3eqtrd	⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) · ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ ( 𝑦 + 1 ) ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) )
244	243	adantr	⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 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	⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) )
246	245	ex	⊢ ( 𝑦 ∈ ℕ → ( ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) ) )
247	11 22 33 44 104 246	nnind	⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑁 ) = ( ( ( 2 ↑ ( 4 · 𝑁 ) ) · ( ( ! ‘ 𝑁 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑁 ) ) ↑ 2 ) ) )