Metamath Proof Explorer

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 ) ) )