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 birani ⊢ ( ( 𝑦 ∈ ℕ ∧ ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑦 ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) ) → 𝑦 ∈ ( ℤ≥ ‘ 1 ) )
107 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 ) ) ) )
108 106 107 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 ) ) ) )
109 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 ) ) )
110 109 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 ) ) ) )
111 eqidd ⊢ ( 𝑦 ∈ ℕ → ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) )
112 oveq2 ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( 2 · 𝑘 ) = ( 2 · ( 𝑦 + 1 ) ) )
113 112 oveq1d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) ↑ 4 ) = ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) )
114 112 oveq1d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) − 1 ) = ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) )
115 112 114 oveq12d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) )
116 115 oveq1d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) = ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) )
117 113 116 oveq12d ⊢ ( 𝑘 = ( 𝑦 + 1 ) → ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
118 117 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑘 = ( 𝑦 + 1 ) ) → ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
119 peano2nn ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
120 2cnd ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℂ )
121 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
122 1cnd ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℂ )
123 121 122 addcld ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℂ )
124 120 123 mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ∈ ℂ )
125 4nn0 ⊢ 4 ∈ ℕ0
126 125 a1i ⊢ ( 𝑦 ∈ ℕ → 4 ∈ ℕ0 )
127 124 126 expcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) ∈ ℂ )
128 124 122 subcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ∈ ℂ )
129 124 128 mulcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ∈ ℂ )
130 129 sqcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ∈ ℂ )
131 2pos ⊢ 0 < 2
132 131 a1i ⊢ ( 𝑦 ∈ ℕ → 0 < 2 )
133 132 gt0ne0d ⊢ ( 𝑦 ∈ ℕ → 2 ≠ 0 )
134 119 nnne0d ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ≠ 0 )
135 120 123 133 134 mulne0d ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ≠ 0 )
136 1red ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℝ )
137 2re ⊢ 2 ∈ ℝ
138 137 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℝ )
139 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
140 139 136 readdcld ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℝ )
141 1lt2 ⊢ 1 < 2
142 141 a1i ⊢ ( 𝑦 ∈ ℕ → 1 < 2 )
143 nnrp ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ+ )
144 136 143 ltaddrp2d ⊢ ( 𝑦 ∈ ℕ → 1 < ( 𝑦 + 1 ) )
145 138 140 142 144 mulgt1d ⊢ ( 𝑦 ∈ ℕ → 1 < ( 2 · ( 𝑦 + 1 ) ) )
146 136 145 gtned ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) ≠ 1 )
147 124 122 146 subne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ≠ 0 )
148 124 128 135 147 mulne0d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ≠ 0 )
149 2z ⊢ 2 ∈ ℤ
150 149 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℤ )
151 129 148 150 expne0d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ≠ 0 )
152 127 130 151 divcld ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) ∈ ℂ )
153 111 118 119 152 fvmptd ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ ( 𝑦 + 1 ) ) = ( ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) / ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
154 153 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 ) ) ) )
155 nnnn0 ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
156 126 155 nn0mulcld ⊢ ( 𝑦 ∈ ℕ → ( 4 · 𝑦 ) ∈ ℕ0 )
157 120 156 expcld ⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( 4 · 𝑦 ) ) ∈ ℂ )
158 faccl ⊢ ( 𝑦 ∈ ℕ0 → ( ! ‘ 𝑦 ) ∈ ℕ )
159 nncn ⊢ ( ( ! ‘ 𝑦 ) ∈ ℕ → ( ! ‘ 𝑦 ) ∈ ℂ )
160 155 158 159 3syl ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ 𝑦 ) ∈ ℂ )
161 160 126 expcld ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ 𝑦 ) ↑ 4 ) ∈ ℂ )
162 157 161 mulcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) ∈ ℂ )
163 75 a1i ⊢ ( 𝑦 ∈ ℕ → 2 ∈ ℕ0 )
164 163 155 nn0mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℕ0 )
165 faccl ⊢ ( ( 2 · 𝑦 ) ∈ ℕ0 → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℕ )
166 nncn ⊢ ( ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℂ )
167 164 165 166 3syl ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℂ )
168 167 sqcld ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ∈ ℂ )
169 164 165 syl ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ∈ ℕ )
170 169 nnne0d ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 2 · 𝑦 ) ) ≠ 0 )
171 167 170 150 expne0d ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ≠ 0 )
172 162 168 127 130 171 151 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 ) ) ) )
173 120 123 126 mulexpd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) = ( ( 2 ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) )
174 173 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) )
175 120 126 expcld ⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ 4 ) ∈ ℂ )
176 123 126 expcld ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑦 + 1 ) ↑ 4 ) ∈ ℂ )
177 157 161 175 176 mul4d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) )
178 160 123 126 mulexpd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) = ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) )
179 178 eqcomd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) = ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) )
180 179 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) ↑ 4 ) · ( ( 𝑦 + 1 ) ↑ 4 ) ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) )
181 174 177 180 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) ↑ 4 ) ) = ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) )
182 120 121 mulcld ⊢ ( 𝑦 ∈ ℕ → ( 2 · 𝑦 ) ∈ ℂ )
183 182 122 addcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ∈ ℂ )
184 124 183 mulcomd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) = ( ( ( 2 · 𝑦 ) + 1 ) · ( 2 · ( 𝑦 + 1 ) ) ) )
185 184 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) · ( 2 · ( 𝑦 + 1 ) ) ) ) )
186 120 121 122 adddid ⊢ ( 𝑦 ∈ ℕ → ( 2 · ( 𝑦 + 1 ) ) = ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) )
187 186 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) = ( ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) − 1 ) )
188 59 120 eqeltrid ⊢ ( 𝑦 ∈ ℕ → ( 2 · 1 ) ∈ ℂ )
189 182 188 122 addsubassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) − 1 ) = ( ( 2 · 𝑦 ) + ( ( 2 · 1 ) − 1 ) ) )
190 59 a1i ⊢ ( 𝑦 ∈ ℕ → ( 2 · 1 ) = 2 )
191 190 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 1 ) − 1 ) = ( 2 − 1 ) )
192 191 92 eqtrdi ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 1 ) − 1 ) = 1 )
193 192 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( ( 2 · 1 ) − 1 ) ) = ( ( 2 · 𝑦 ) + 1 ) )
194 187 189 193 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) = ( ( 2 · 𝑦 ) + 1 ) )
195 194 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) = ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) )
196 195 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) ) )
197 167 183 124 mulassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) · ( 2 · ( 𝑦 + 1 ) ) ) ) )
198 185 196 197 3eqtr4d ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) = ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) )
199 198 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) ↑ 2 ) = ( ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) )
200 167 129 163 mulexpd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ) ↑ 2 ) = ( ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) )
201 df-2 ⊢ 2 = ( 1 + 1 )
202 201 a1i ⊢ ( 𝑦 ∈ ℕ → 2 = ( 1 + 1 ) )
203 202 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( ( 2 · 𝑦 ) + ( 1 + 1 ) ) )
204 182 122 122 addassd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) = ( ( 2 · 𝑦 ) + ( 1 + 1 ) ) )
205 203 204 eqtr4d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) )
206 205 fveq2d ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) = ( ! ‘ ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) )
207 62 a1i ⊢ ( 𝑦 ∈ ℕ → 1 ∈ ℕ0 )
208 164 207 nn0addcld ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 1 ) ∈ ℕ0 )
209 facp1 ⊢ ( ( ( 2 · 𝑦 ) + 1 ) ∈ ℕ0 → ( ! ‘ ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) )
210 208 209 syl ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) )
211 facp1 ⊢ ( ( 2 · 𝑦 ) ∈ ℕ0 → ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) )
212 164 211 syl ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) = ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) )
213 202 eqcomd ⊢ ( 𝑦 ∈ ℕ → ( 1 + 1 ) = 2 )
214 213 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + ( 1 + 1 ) ) = ( ( 2 · 𝑦 ) + 2 ) )
215 213 201 59 3eqtr4g ⊢ ( 𝑦 ∈ ℕ → 2 = ( 2 · 1 ) )
216 215 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( ( 2 · 𝑦 ) + ( 2 · 1 ) ) )
217 216 186 eqtr4d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 · 𝑦 ) + 2 ) = ( 2 · ( 𝑦 + 1 ) ) )
218 204 214 217 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) = ( 2 · ( 𝑦 + 1 ) ) )
219 212 218 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑦 ) + 1 ) ) · ( ( ( 2 · 𝑦 ) + 1 ) + 1 ) ) = ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) )
220 206 210 219 3eqtrrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) = ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) )
221 220 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( ! ‘ ( 2 · 𝑦 ) ) · ( ( 2 · 𝑦 ) + 1 ) ) · ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) )
222 199 200 221 3eqtr3d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) · ( ( ( 2 · ( 𝑦 + 1 ) ) · ( ( 2 · ( 𝑦 + 1 ) ) − 1 ) ) ↑ 2 ) ) = ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) )
223 181 222 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 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 ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 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 ⊢ ( 𝑦 ∈ ℕ → 4 = ( 4 · 1 ) )
226 225 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( ( 4 · 𝑦 ) + 4 ) = ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) )
227 226 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 4 · 𝑦 ) + 4 ) ) = ( 2 ↑ ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) ) )
228 120 126 156 expaddd ⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 4 · 𝑦 ) + 4 ) ) = ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) )
229 81 a1i ⊢ ( 𝑦 ∈ ℕ → 4 ∈ ℂ )
230 229 121 122 adddid ⊢ ( 𝑦 ∈ ℕ → ( 4 · ( 𝑦 + 1 ) ) = ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) )
231 230 eqcomd ⊢ ( 𝑦 ∈ ℕ → ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) = ( 4 · ( 𝑦 + 1 ) ) )
232 231 oveq2d ⊢ ( 𝑦 ∈ ℕ → ( 2 ↑ ( ( 4 · 𝑦 ) + ( 4 · 1 ) ) ) = ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) )
233 227 228 232 3eqtr3d ⊢ ( 𝑦 ∈ ℕ → ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) = ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) )
234 facp1 ⊢ ( 𝑦 ∈ ℕ0 → ( ! ‘ ( 𝑦 + 1 ) ) = ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) )
235 155 234 syl ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( 𝑦 + 1 ) ) = ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) )
236 235 eqcomd ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) = ( ! ‘ ( 𝑦 + 1 ) ) )
237 236 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) = ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) )
238 233 237 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) = ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) )
239 217 fveq2d ⊢ ( 𝑦 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) = ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) )
240 239 oveq1d ⊢ ( 𝑦 ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) = ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) )
241 238 240 oveq12d ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( 2 ↑ 4 ) ) · ( ( ( ! ‘ 𝑦 ) · ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( ( 2 · 𝑦 ) + 2 ) ) ↑ 2 ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) )
242 154 224 241 3eqtrd ⊢ ( 𝑦 ∈ ℕ → ( ( ( ( 2 ↑ ( 4 · 𝑦 ) ) · ( ( ! ‘ 𝑦 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑦 ) ) ↑ 2 ) ) · ( ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ‘ ( 𝑦 + 1 ) ) ) = ( ( ( 2 ↑ ( 4 · ( 𝑦 + 1 ) ) ) · ( ( ! ‘ ( 𝑦 + 1 ) ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · ( 𝑦 + 1 ) ) ) ↑ 2 ) ) )
243 242 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 ) ) )
244 108 110 243 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 ) ) )
245 244 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 ) ) ) )
246 11 22 33 44 104 245 nnind ⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑁 ) = ( ( ( 2 ↑ ( 4 · 𝑁 ) ) · ( ( ! ‘ 𝑁 ) ↑ 4 ) ) / ( ( ! ‘ ( 2 · 𝑁 ) ) ↑ 2 ) ) )