# Metamath Proof Explorer

## Theorem wallispi2lem1

Description: An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Assertion wallispi2lem1 ${⊢}{N}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({N}\right)=\left(\frac{1}{2\cdot {N}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{x}=1\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left(1\right)$
2 oveq2 ${⊢}{x}=1\to 2{x}=2\cdot 1$
3 2 oveq1d ${⊢}{x}=1\to 2{x}+1=2\cdot 1+1$
4 3 oveq2d ${⊢}{x}=1\to \frac{1}{2{x}+1}=\frac{1}{2\cdot 1+1}$
5 fveq2 ${⊢}{x}=1\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)$
6 4 5 oveq12d ${⊢}{x}=1\to \left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=\left(\frac{1}{2\cdot 1+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)$
7 1 6 eqeq12d ${⊢}{x}=1\to \left(seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=\left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)↔seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left(1\right)=\left(\frac{1}{2\cdot 1+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)\right)$
8 fveq2 ${⊢}{x}={y}\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)$
9 oveq2 ${⊢}{x}={y}\to 2{x}=2{y}$
10 9 oveq1d ${⊢}{x}={y}\to 2{x}+1=2{y}+1$
11 10 oveq2d ${⊢}{x}={y}\to \frac{1}{2{x}+1}=\frac{1}{2{y}+1}$
12 fveq2 ${⊢}{x}={y}\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)$
13 11 12 oveq12d ${⊢}{x}={y}\to \left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)$
14 8 13 eqeq12d ${⊢}{x}={y}\to \left(seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=\left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)↔seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)$
15 fveq2 ${⊢}{x}={y}+1\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}+1\right)$
16 oveq2 ${⊢}{x}={y}+1\to 2{x}=2\left({y}+1\right)$
17 16 oveq1d ${⊢}{x}={y}+1\to 2{x}+1=2\left({y}+1\right)+1$
18 17 oveq2d ${⊢}{x}={y}+1\to \frac{1}{2{x}+1}=\frac{1}{2\left({y}+1\right)+1}$
19 fveq2 ${⊢}{x}={y}+1\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
20 18 19 oveq12d ${⊢}{x}={y}+1\to \left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
21 15 20 eqeq12d ${⊢}{x}={y}+1\to \left(seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=\left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)↔seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)\right)$
22 fveq2 ${⊢}{x}={N}\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({N}\right)$
23 oveq2 ${⊢}{x}={N}\to 2{x}=2\cdot {N}$
24 23 oveq1d ${⊢}{x}={N}\to 2{x}+1=2\cdot {N}+1$
25 24 oveq2d ${⊢}{x}={N}\to \frac{1}{2{x}+1}=\frac{1}{2\cdot {N}+1}$
26 fveq2 ${⊢}{x}={N}\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({N}\right)$
27 25 26 oveq12d ${⊢}{x}={N}\to \left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)=\left(\frac{1}{2\cdot {N}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({N}\right)$
28 22 27 eqeq12d ${⊢}{x}={N}\to \left(seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({x}\right)=\left(\frac{1}{2{x}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({x}\right)↔seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({N}\right)=\left(\frac{1}{2\cdot {N}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({N}\right)\right)$
29 1z ${⊢}1\in ℤ$
30 seq1 ${⊢}1\in ℤ\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left(1\right)=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left(1\right)$
31 29 30 ax-mp ${⊢}seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left(1\right)=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left(1\right)$
32 1nn ${⊢}1\in ℕ$
33 oveq2 ${⊢}{k}=1\to 2{k}=2\cdot 1$
34 33 oveq1d ${⊢}{k}=1\to 2{k}-1=2\cdot 1-1$
35 33 34 oveq12d ${⊢}{k}=1\to \frac{2{k}}{2{k}-1}=\frac{2\cdot 1}{2\cdot 1-1}$
36 33 oveq1d ${⊢}{k}=1\to 2{k}+1=2\cdot 1+1$
37 33 36 oveq12d ${⊢}{k}=1\to \frac{2{k}}{2{k}+1}=\frac{2\cdot 1}{2\cdot 1+1}$
38 35 37 oveq12d ${⊢}{k}=1\to \left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)=\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)$
39 eqid ${⊢}\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)$
40 ovex ${⊢}\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)\in \mathrm{V}$
41 38 39 40 fvmpt ${⊢}1\in ℕ\to \left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left(1\right)=\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)$
42 32 41 ax-mp ${⊢}\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left(1\right)=\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)$
43 2t1e2 ${⊢}2\cdot 1=2$
44 43 oveq1i ${⊢}2\cdot 1-1=2-1$
45 2m1e1 ${⊢}2-1=1$
46 44 45 eqtri ${⊢}2\cdot 1-1=1$
47 43 46 oveq12i ${⊢}\frac{2\cdot 1}{2\cdot 1-1}=\frac{2}{1}$
48 43 oveq1i ${⊢}2\cdot 1+1=2+1$
49 2p1e3 ${⊢}2+1=3$
50 48 49 eqtri ${⊢}2\cdot 1+1=3$
51 43 50 oveq12i ${⊢}\frac{2\cdot 1}{2\cdot 1+1}=\frac{2}{3}$
52 47 51 oveq12i ${⊢}\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)=\left(\frac{2}{1}\right)\left(\frac{2}{3}\right)$
53 2cn ${⊢}2\in ℂ$
54 ax-1cn ${⊢}1\in ℂ$
55 3cn ${⊢}3\in ℂ$
56 ax-1ne0 ${⊢}1\ne 0$
57 3ne0 ${⊢}3\ne 0$
58 53 54 53 55 56 57 divmuldivi ${⊢}\left(\frac{2}{1}\right)\left(\frac{2}{3}\right)=\frac{2\cdot 2}{1\cdot 3}$
59 2t2e4 ${⊢}2\cdot 2=4$
60 55 mulid2i ${⊢}1\cdot 3=3$
61 59 60 oveq12i ${⊢}\frac{2\cdot 2}{1\cdot 3}=\frac{4}{3}$
62 52 58 61 3eqtri ${⊢}\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)=\frac{4}{3}$
63 4cn ${⊢}4\in ℂ$
64 divrec2 ${⊢}\left(4\in ℂ\wedge 3\in ℂ\wedge 3\ne 0\right)\to \frac{4}{3}=\left(\frac{1}{3}\right)\cdot 4$
65 63 55 57 64 mp3an ${⊢}\frac{4}{3}=\left(\frac{1}{3}\right)\cdot 4$
66 50 eqcomi ${⊢}3=2\cdot 1+1$
67 66 oveq2i ${⊢}\frac{1}{3}=\frac{1}{2\cdot 1+1}$
68 seq1 ${⊢}1\in ℤ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)=\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left(1\right)$
69 29 68 ax-mp ${⊢}seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)=\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left(1\right)$
70 33 oveq1d ${⊢}{k}=1\to {2{k}}^{4}={2\cdot 1}^{4}$
71 33 34 oveq12d ${⊢}{k}=1\to 2{k}\left(2{k}-1\right)=2\cdot 1\left(2\cdot 1-1\right)$
72 71 oveq1d ${⊢}{k}=1\to {2{k}\left(2{k}-1\right)}^{2}={2\cdot 1\left(2\cdot 1-1\right)}^{2}$
73 70 72 oveq12d ${⊢}{k}=1\to \frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}=\frac{{2\cdot 1}^{4}}{{2\cdot 1\left(2\cdot 1-1\right)}^{2}}$
74 eqid ${⊢}\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)=\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)$
75 ovex ${⊢}\frac{{2\cdot 1}^{4}}{{2\cdot 1\left(2\cdot 1-1\right)}^{2}}\in \mathrm{V}$
76 73 74 75 fvmpt ${⊢}1\in ℕ\to \left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left(1\right)=\frac{{2\cdot 1}^{4}}{{2\cdot 1\left(2\cdot 1-1\right)}^{2}}$
77 32 76 ax-mp ${⊢}\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left(1\right)=\frac{{2\cdot 1}^{4}}{{2\cdot 1\left(2\cdot 1-1\right)}^{2}}$
78 43 oveq1i ${⊢}{2\cdot 1}^{4}={2}^{4}$
79 43 46 oveq12i ${⊢}2\cdot 1\left(2\cdot 1-1\right)=2\cdot 1$
80 79 43 eqtri ${⊢}2\cdot 1\left(2\cdot 1-1\right)=2$
81 80 oveq1i ${⊢}{2\cdot 1\left(2\cdot 1-1\right)}^{2}={2}^{2}$
82 78 81 oveq12i ${⊢}\frac{{2\cdot 1}^{4}}{{2\cdot 1\left(2\cdot 1-1\right)}^{2}}=\frac{{2}^{4}}{{2}^{2}}$
83 2exp4 ${⊢}{2}^{4}=16$
84 sq2 ${⊢}{2}^{2}=4$
85 83 84 oveq12i ${⊢}\frac{{2}^{4}}{{2}^{2}}=\frac{16}{4}$
86 4t4e16 ${⊢}4\cdot 4=16$
87 86 eqcomi ${⊢}16=4\cdot 4$
88 87 oveq1i ${⊢}\frac{16}{4}=\frac{4\cdot 4}{4}$
89 4ne0 ${⊢}4\ne 0$
90 63 63 89 divcan3i ${⊢}\frac{4\cdot 4}{4}=4$
91 85 88 90 3eqtri ${⊢}\frac{{2}^{4}}{{2}^{2}}=4$
92 82 91 eqtri ${⊢}\frac{{2\cdot 1}^{4}}{{2\cdot 1\left(2\cdot 1-1\right)}^{2}}=4$
93 69 77 92 3eqtri ${⊢}seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)=4$
94 93 eqcomi ${⊢}4=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)$
95 67 94 oveq12i ${⊢}\left(\frac{1}{3}\right)\cdot 4=\left(\frac{1}{2\cdot 1+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)$
96 62 65 95 3eqtri ${⊢}\left(\frac{2\cdot 1}{2\cdot 1-1}\right)\left(\frac{2\cdot 1}{2\cdot 1+1}\right)=\left(\frac{1}{2\cdot 1+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)$
97 31 42 96 3eqtri ${⊢}seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left(1\right)=\left(\frac{1}{2\cdot 1+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left(1\right)$
98 elnnuz ${⊢}{y}\in ℕ↔{y}\in {ℤ}_{\ge 1}$
99 98 biimpi ${⊢}{y}\in ℕ\to {y}\in {ℤ}_{\ge 1}$
100 99 adantr ${⊢}\left({y}\in ℕ\wedge seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)\to {y}\in {ℤ}_{\ge 1}$
101 seqp1 ${⊢}{y}\in {ℤ}_{\ge 1}\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}+1\right)=seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)$
102 100 101 syl ${⊢}\left({y}\in ℕ\wedge seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}+1\right)=seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)$
103 simpr ${⊢}\left({y}\in ℕ\wedge seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)$
104 103 oveq1d ${⊢}\left({y}\in ℕ\wedge seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)$
105 eqidd ${⊢}{y}\in ℕ\to \left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)=\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)$
106 oveq2 ${⊢}{k}={y}+1\to 2{k}=2\left({y}+1\right)$
107 106 oveq1d ${⊢}{k}={y}+1\to 2{k}-1=2\left({y}+1\right)-1$
108 106 107 oveq12d ${⊢}{k}={y}+1\to \frac{2{k}}{2{k}-1}=\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}$
109 106 oveq1d ${⊢}{k}={y}+1\to 2{k}+1=2\left({y}+1\right)+1$
110 106 109 oveq12d ${⊢}{k}={y}+1\to \frac{2{k}}{2{k}+1}=\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}$
111 108 110 oveq12d ${⊢}{k}={y}+1\to \left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)=\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)$
112 111 adantl ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to \left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)=\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)$
113 peano2nn ${⊢}{y}\in ℕ\to {y}+1\in ℕ$
114 2rp ${⊢}2\in {ℝ}^{+}$
115 114 a1i ${⊢}{y}\in ℕ\to 2\in {ℝ}^{+}$
116 nnre ${⊢}{y}\in ℕ\to {y}\in ℝ$
117 nnnn0 ${⊢}{y}\in ℕ\to {y}\in {ℕ}_{0}$
118 117 nn0ge0d ${⊢}{y}\in ℕ\to 0\le {y}$
119 116 118 ge0p1rpd ${⊢}{y}\in ℕ\to {y}+1\in {ℝ}^{+}$
120 115 119 rpmulcld ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\in {ℝ}^{+}$
121 2re ${⊢}2\in ℝ$
122 121 a1i ${⊢}{y}\in ℕ\to 2\in ℝ$
123 1red ${⊢}{y}\in ℕ\to 1\in ℝ$
124 116 123 readdcld ${⊢}{y}\in ℕ\to {y}+1\in ℝ$
125 122 124 remulcld ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\in ℝ$
126 125 123 resubcld ${⊢}{y}\in ℕ\to 2\left({y}+1\right)-1\in ℝ$
127 1lt2 ${⊢}1<2$
128 127 a1i ${⊢}{y}\in ℕ\to 1<2$
129 nnrp ${⊢}{y}\in ℕ\to {y}\in {ℝ}^{+}$
130 123 129 ltaddrp2d ${⊢}{y}\in ℕ\to 1<{y}+1$
131 122 124 128 130 mulgt1d ${⊢}{y}\in ℕ\to 1<2\left({y}+1\right)$
132 123 125 posdifd ${⊢}{y}\in ℕ\to \left(1<2\left({y}+1\right)↔0<2\left({y}+1\right)-1\right)$
133 131 132 mpbid ${⊢}{y}\in ℕ\to 0<2\left({y}+1\right)-1$
134 126 133 elrpd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)-1\in {ℝ}^{+}$
135 120 134 rpdivcld ${⊢}{y}\in ℕ\to \frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\in {ℝ}^{+}$
136 115 rpge0d ${⊢}{y}\in ℕ\to 0\le 2$
137 0le1 ${⊢}0\le 1$
138 137 a1i ${⊢}{y}\in ℕ\to 0\le 1$
139 116 123 118 138 addge0d ${⊢}{y}\in ℕ\to 0\le {y}+1$
140 122 124 136 139 mulge0d ${⊢}{y}\in ℕ\to 0\le 2\left({y}+1\right)$
141 125 140 ge0p1rpd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)+1\in {ℝ}^{+}$
142 120 141 rpdivcld ${⊢}{y}\in ℕ\to \frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\in {ℝ}^{+}$
143 135 142 rpmulcld ${⊢}{y}\in ℕ\to \left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)\in {ℝ}^{+}$
144 105 112 113 143 fvmptd ${⊢}{y}\in ℕ\to \left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)=\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)$
145 144 oveq2d ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)$
146 125 recnd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\in ℂ$
147 126 recnd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)-1\in ℂ$
148 141 rpcnd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)+1\in ℂ$
149 133 gt0ne0d ${⊢}{y}\in ℕ\to 2\left({y}+1\right)-1\ne 0$
150 141 rpne0d ${⊢}{y}\in ℕ\to 2\left({y}+1\right)+1\ne 0$
151 146 147 146 148 149 150 divmuldivd ${⊢}{y}\in ℕ\to \left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)=\frac{2\left({y}+1\right)2\left({y}+1\right)}{\left(2\left({y}+1\right)-1\right)\left(2\left({y}+1\right)+1\right)}$
152 146 146 mulcld ${⊢}{y}\in ℕ\to 2\left({y}+1\right)2\left({y}+1\right)\in ℂ$
153 152 147 148 149 150 divdiv1d ${⊢}{y}\in ℕ\to \frac{\frac{2\left({y}+1\right)2\left({y}+1\right)}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}=\frac{2\left({y}+1\right)2\left({y}+1\right)}{\left(2\left({y}+1\right)-1\right)\left(2\left({y}+1\right)+1\right)}$
154 146 sqvald ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{2}=2\left({y}+1\right)2\left({y}+1\right)$
155 154 eqcomd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)2\left({y}+1\right)={2\left({y}+1\right)}^{2}$
156 155 oveq1d ${⊢}{y}\in ℕ\to \frac{2\left({y}+1\right)2\left({y}+1\right)}{2\left({y}+1\right)-1}=\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}$
157 156 oveq1d ${⊢}{y}\in ℕ\to \frac{\frac{2\left({y}+1\right)2\left({y}+1\right)}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}=\frac{\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}$
158 151 153 157 3eqtr2d ${⊢}{y}\in ℕ\to \left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)=\frac{\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}$
159 158 oveq2d ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)-1}\right)\left(\frac{2\left({y}+1\right)}{2\left({y}+1\right)+1}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}\right)$
160 146 sqcld ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{2}\in ℂ$
161 160 147 149 divcld ${⊢}{y}\in ℕ\to \frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\in ℂ$
162 161 148 150 divrec2d ${⊢}{y}\in ℕ\to \frac{\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}=\left(\frac{1}{2\left({y}+1\right)+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)$
163 162 oveq2d ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2\left({y}+1\right)+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)$
164 2cnd ${⊢}{y}\in ℕ\to 2\in ℂ$
165 nncn ${⊢}{y}\in ℕ\to {y}\in ℂ$
166 164 165 mulcld ${⊢}{y}\in ℕ\to 2{y}\in ℂ$
167 1cnd ${⊢}{y}\in ℕ\to 1\in ℂ$
168 166 167 addcld ${⊢}{y}\in ℕ\to 2{y}+1\in ℂ$
169 2nn ${⊢}2\in ℕ$
170 169 a1i ${⊢}{y}\in ℕ\to 2\in ℕ$
171 id ${⊢}{y}\in ℕ\to {y}\in ℕ$
172 170 171 nnmulcld ${⊢}{y}\in ℕ\to 2{y}\in ℕ$
173 172 peano2nnd ${⊢}{y}\in ℕ\to 2{y}+1\in ℕ$
174 173 nnne0d ${⊢}{y}\in ℕ\to 2{y}+1\ne 0$
175 168 174 reccld ${⊢}{y}\in ℕ\to \frac{1}{2{y}+1}\in ℂ$
176 eqidd ${⊢}\left({y}\in ℕ\wedge {x}\in \left(1\dots {y}\right)\right)\to \left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)=\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)$
177 oveq2 ${⊢}{k}={x}\to 2{k}=2{x}$
178 177 oveq1d ${⊢}{k}={x}\to {2{k}}^{4}={2{x}}^{4}$
179 177 oveq1d ${⊢}{k}={x}\to 2{k}-1=2{x}-1$
180 177 179 oveq12d ${⊢}{k}={x}\to 2{k}\left(2{k}-1\right)=2{x}\left(2{x}-1\right)$
181 180 oveq1d ${⊢}{k}={x}\to {2{k}\left(2{k}-1\right)}^{2}={2{x}\left(2{x}-1\right)}^{2}$
182 178 181 oveq12d ${⊢}{k}={x}\to \frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}=\frac{{2{x}}^{4}}{{2{x}\left(2{x}-1\right)}^{2}}$
183 182 adantl ${⊢}\left(\left({y}\in ℕ\wedge {x}\in \left(1\dots {y}\right)\right)\wedge {k}={x}\right)\to \frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}=\frac{{2{x}}^{4}}{{2{x}\left(2{x}-1\right)}^{2}}$
184 elfznn ${⊢}{x}\in \left(1\dots {y}\right)\to {x}\in ℕ$
185 184 adantl ${⊢}\left({y}\in ℕ\wedge {x}\in \left(1\dots {y}\right)\right)\to {x}\in ℕ$
186 169 a1i ${⊢}{x}\in ℕ\to 2\in ℕ$
187 id ${⊢}{x}\in ℕ\to {x}\in ℕ$
188 186 187 nnmulcld ${⊢}{x}\in ℕ\to 2{x}\in ℕ$
189 4nn0 ${⊢}4\in {ℕ}_{0}$
190 189 a1i ${⊢}{x}\in ℕ\to 4\in {ℕ}_{0}$
191 188 190 nnexpcld ${⊢}{x}\in ℕ\to {2{x}}^{4}\in ℕ$
192 191 nncnd ${⊢}{x}\in ℕ\to {2{x}}^{4}\in ℂ$
193 2cnd ${⊢}{x}\in ℕ\to 2\in ℂ$
194 nncn ${⊢}{x}\in ℕ\to {x}\in ℂ$
195 193 194 mulcld ${⊢}{x}\in ℕ\to 2{x}\in ℂ$
196 1cnd ${⊢}{x}\in ℕ\to 1\in ℂ$
197 195 196 subcld ${⊢}{x}\in ℕ\to 2{x}-1\in ℂ$
198 195 197 mulcld ${⊢}{x}\in ℕ\to 2{x}\left(2{x}-1\right)\in ℂ$
199 198 sqcld ${⊢}{x}\in ℕ\to {2{x}\left(2{x}-1\right)}^{2}\in ℂ$
200 186 nnne0d ${⊢}{x}\in ℕ\to 2\ne 0$
201 nnne0 ${⊢}{x}\in ℕ\to {x}\ne 0$
202 193 194 200 201 mulne0d ${⊢}{x}\in ℕ\to 2{x}\ne 0$
203 1red ${⊢}{x}\in ℕ\to 1\in ℝ$
204 121 a1i ${⊢}{x}\in ℕ\to 2\in ℝ$
205 204 203 remulcld ${⊢}{x}\in ℕ\to 2\cdot 1\in ℝ$
206 nnre ${⊢}{x}\in ℕ\to {x}\in ℝ$
207 204 206 remulcld ${⊢}{x}\in ℕ\to 2{x}\in ℝ$
208 43 a1i ${⊢}{x}\in ℕ\to 2\cdot 1=2$
209 127 208 breqtrrid ${⊢}{x}\in ℕ\to 1<2\cdot 1$
210 0le2 ${⊢}0\le 2$
211 210 a1i ${⊢}{x}\in ℕ\to 0\le 2$
212 nnge1 ${⊢}{x}\in ℕ\to 1\le {x}$
213 203 206 204 211 212 lemul2ad ${⊢}{x}\in ℕ\to 2\cdot 1\le 2{x}$
214 203 205 207 209 213 ltletrd ${⊢}{x}\in ℕ\to 1<2{x}$
215 203 214 gtned ${⊢}{x}\in ℕ\to 2{x}\ne 1$
216 195 196 215 subne0d ${⊢}{x}\in ℕ\to 2{x}-1\ne 0$
217 195 197 202 216 mulne0d ${⊢}{x}\in ℕ\to 2{x}\left(2{x}-1\right)\ne 0$
218 2z ${⊢}2\in ℤ$
219 218 a1i ${⊢}{x}\in ℕ\to 2\in ℤ$
220 198 217 219 expne0d ${⊢}{x}\in ℕ\to {2{x}\left(2{x}-1\right)}^{2}\ne 0$
221 192 199 220 divcld ${⊢}{x}\in ℕ\to \frac{{2{x}}^{4}}{{2{x}\left(2{x}-1\right)}^{2}}\in ℂ$
222 184 221 syl ${⊢}{x}\in \left(1\dots {y}\right)\to \frac{{2{x}}^{4}}{{2{x}\left(2{x}-1\right)}^{2}}\in ℂ$
223 222 adantl ${⊢}\left({y}\in ℕ\wedge {x}\in \left(1\dots {y}\right)\right)\to \frac{{2{x}}^{4}}{{2{x}\left(2{x}-1\right)}^{2}}\in ℂ$
224 176 183 185 223 fvmptd ${⊢}\left({y}\in ℕ\wedge {x}\in \left(1\dots {y}\right)\right)\to \left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({x}\right)=\frac{{2{x}}^{4}}{{2{x}\left(2{x}-1\right)}^{2}}$
225 224 223 eqeltrd ${⊢}\left({y}\in ℕ\wedge {x}\in \left(1\dots {y}\right)\right)\to \left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({x}\right)\in ℂ$
226 mulcl ${⊢}\left({x}\in ℂ\wedge {w}\in ℂ\right)\to {x}{w}\in ℂ$
227 226 adantl ${⊢}\left({y}\in ℕ\wedge \left({x}\in ℂ\wedge {w}\in ℂ\right)\right)\to {x}{w}\in ℂ$
228 99 225 227 seqcl ${⊢}{y}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\in ℂ$
229 175 228 mulcld ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\in ℂ$
230 148 150 reccld ${⊢}{y}\in ℕ\to \frac{1}{2\left({y}+1\right)+1}\in ℂ$
231 229 230 161 mul12d ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2\left({y}+1\right)+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)$
232 175 228 mulcomd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2{y}+1}\right)$
233 232 oveq1d ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2{y}+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)$
234 228 175 161 mulassd ${⊢}{y}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2{y}+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2{y}+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)$
235 167 168 160 147 174 149 divmuldivd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=\frac{1{2\left({y}+1\right)}^{2}}{\left(2{y}+1\right)\left(2\left({y}+1\right)-1\right)}$
236 160 mulid2d ${⊢}{y}\in ℕ\to 1{2\left({y}+1\right)}^{2}={2\left({y}+1\right)}^{2}$
237 164 165 167 adddid ${⊢}{y}\in ℕ\to 2\left({y}+1\right)=2{y}+2\cdot 1$
238 43 a1i ${⊢}{y}\in ℕ\to 2\cdot 1=2$
239 238 oveq2d ${⊢}{y}\in ℕ\to 2{y}+2\cdot 1=2{y}+2$
240 237 239 eqtrd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)=2{y}+2$
241 240 oveq1d ${⊢}{y}\in ℕ\to 2\left({y}+1\right)-1=2{y}+2-1$
242 166 164 167 addsubassd ${⊢}{y}\in ℕ\to 2{y}+2-1=2{y}+2-1$
243 45 a1i ${⊢}{y}\in ℕ\to 2-1=1$
244 243 oveq2d ${⊢}{y}\in ℕ\to 2{y}+2-1=2{y}+1$
245 241 242 244 3eqtrd ${⊢}{y}\in ℕ\to 2\left({y}+1\right)-1=2{y}+1$
246 245 oveq2d ${⊢}{y}\in ℕ\to \left(2{y}+1\right)\left(2\left({y}+1\right)-1\right)=\left(2{y}+1\right)\left(2{y}+1\right)$
247 168 sqvald ${⊢}{y}\in ℕ\to {\left(2{y}+1\right)}^{2}=\left(2{y}+1\right)\left(2{y}+1\right)$
248 246 247 eqtr4d ${⊢}{y}\in ℕ\to \left(2{y}+1\right)\left(2\left({y}+1\right)-1\right)={\left(2{y}+1\right)}^{2}$
249 236 248 oveq12d ${⊢}{y}\in ℕ\to \frac{1{2\left({y}+1\right)}^{2}}{\left(2{y}+1\right)\left(2\left({y}+1\right)-1\right)}=\frac{{2\left({y}+1\right)}^{2}}{{\left(2{y}+1\right)}^{2}}$
250 2p2e4 ${⊢}2+2=4$
251 53 53 250 mvlladdi ${⊢}2=4-2$
252 251 a1i ${⊢}{y}\in ℕ\to 2=4-2$
253 252 oveq2d ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{2}={2\left({y}+1\right)}^{4-2}$
254 120 rpne0d ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\ne 0$
255 218 a1i ${⊢}{y}\in ℕ\to 2\in ℤ$
256 4z ${⊢}4\in ℤ$
257 256 a1i ${⊢}{y}\in ℕ\to 4\in ℤ$
258 146 254 255 257 expsubd ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{4-2}=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)}^{2}}$
259 253 258 eqtrd ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{2}=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)}^{2}}$
260 245 eqcomd ${⊢}{y}\in ℕ\to 2{y}+1=2\left({y}+1\right)-1$
261 260 oveq1d ${⊢}{y}\in ℕ\to {\left(2{y}+1\right)}^{2}={\left(2\left({y}+1\right)-1\right)}^{2}$
262 259 261 oveq12d ${⊢}{y}\in ℕ\to \frac{{2\left({y}+1\right)}^{2}}{{\left(2{y}+1\right)}^{2}}=\frac{\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)}^{2}}}{{\left(2\left({y}+1\right)-1\right)}^{2}}$
263 146 254 257 expclzd ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{4}\in ℂ$
264 147 sqcld ${⊢}{y}\in ℕ\to {\left(2\left({y}+1\right)-1\right)}^{2}\in ℂ$
265 165 167 addcld ${⊢}{y}\in ℕ\to {y}+1\in ℂ$
266 170 nnne0d ${⊢}{y}\in ℕ\to 2\ne 0$
267 113 nnne0d ${⊢}{y}\in ℕ\to {y}+1\ne 0$
268 164 265 266 267 mulne0d ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\ne 0$
269 146 268 255 expne0d ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{2}\ne 0$
270 147 149 255 expne0d ${⊢}{y}\in ℕ\to {\left(2\left({y}+1\right)-1\right)}^{2}\ne 0$
271 263 160 264 269 270 divdiv1d ${⊢}{y}\in ℕ\to \frac{\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)}^{2}}}{{\left(2\left({y}+1\right)-1\right)}^{2}}=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)}^{2}{\left(2\left({y}+1\right)-1\right)}^{2}}$
272 146 147 sqmuld ${⊢}{y}\in ℕ\to {2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}={2\left({y}+1\right)}^{2}{\left(2\left({y}+1\right)-1\right)}^{2}$
273 272 eqcomd ${⊢}{y}\in ℕ\to {2\left({y}+1\right)}^{2}{\left(2\left({y}+1\right)-1\right)}^{2}={2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}$
274 273 oveq2d ${⊢}{y}\in ℕ\to \frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)}^{2}{\left(2\left({y}+1\right)-1\right)}^{2}}=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}$
275 262 271 274 3eqtrd ${⊢}{y}\in ℕ\to \frac{{2\left({y}+1\right)}^{2}}{{\left(2{y}+1\right)}^{2}}=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}$
276 235 249 275 3eqtrd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}$
277 276 oveq2d ${⊢}{y}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{1}{2{y}+1}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)$
278 233 234 277 3eqtrd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)$
279 278 oveq2d ${⊢}{y}\in ℕ\to \left(\frac{1}{2\left({y}+1\right)+1}\right)\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)$
280 163 231 279 3eqtrd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{\frac{{2\left({y}+1\right)}^{2}}{2\left({y}+1\right)-1}}{2\left({y}+1\right)+1}\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)$
281 145 159 280 3eqtrd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)$
282 eqidd ${⊢}{y}\in ℕ\to \left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)=\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)$
283 simpr ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to {k}={y}+1$
284 283 oveq2d ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to 2{k}=2\left({y}+1\right)$
285 284 oveq1d ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to {2{k}}^{4}={2\left({y}+1\right)}^{4}$
286 284 oveq1d ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to 2{k}-1=2\left({y}+1\right)-1$
287 284 286 oveq12d ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to 2{k}\left(2{k}-1\right)=2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)$
288 287 oveq1d ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to {2{k}\left(2{k}-1\right)}^{2}={2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}$
289 285 288 oveq12d ${⊢}\left({y}\in ℕ\wedge {k}={y}+1\right)\to \frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}$
290 146 147 mulcld ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)\in ℂ$
291 290 sqcld ${⊢}{y}\in ℕ\to {2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}\in ℂ$
292 146 147 254 149 mulne0d ${⊢}{y}\in ℕ\to 2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)\ne 0$
293 290 292 255 expne0d ${⊢}{y}\in ℕ\to {2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}\ne 0$
294 263 291 293 divcld ${⊢}{y}\in ℕ\to \frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\in ℂ$
295 282 289 113 294 fvmptd ${⊢}{y}\in ℕ\to \left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)=\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}$
296 295 eqcomd ${⊢}{y}\in ℕ\to \frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}=\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)$
297 296 oveq2d ${⊢}{y}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)$
298 297 oveq2d ${⊢}{y}\in ℕ\to \left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left(\frac{{2\left({y}+1\right)}^{4}}{{2\left({y}+1\right)\left(2\left({y}+1\right)-1\right)}^{2}}\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)$
299 seqp1 ${⊢}{y}\in {ℤ}_{\ge 1}\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)$
300 99 299 syl ${⊢}{y}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)$
301 300 eqcomd ${⊢}{y}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)=seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
302 301 oveq2d ${⊢}{y}\in ℕ\to \left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
303 281 298 302 3eqtrd ${⊢}{y}\in ℕ\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
304 303 adantr ${⊢}\left({y}\in ℕ\wedge seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)\to \left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
305 102 104 304 3eqtrd ${⊢}\left({y}\in ℕ\wedge seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\right)\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)$
306 305 ex ${⊢}{y}\in ℕ\to \left(seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}\right)=\left(\frac{1}{2{y}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}\right)\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({y}+1\right)=\left(\frac{1}{2\left({y}+1\right)+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({y}+1\right)\right)$
307 7 14 21 28 97 306 nnind ${⊢}{N}\in ℕ\to seq1\left(×,\left({k}\in ℕ⟼\left(\frac{2{k}}{2{k}-1}\right)\left(\frac{2{k}}{2{k}+1}\right)\right)\right)\left({N}\right)=\left(\frac{1}{2\cdot {N}+1}\right)seq1\left(×,\left({k}\in ℕ⟼\frac{{2{k}}^{4}}{{2{k}\left(2{k}-1\right)}^{2}}\right)\right)\left({N}\right)$