This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℕ → ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) − 1 ) ) · ( ( 2 · 𝑘 ) / ( ( 2 · 𝑘 ) + 1 ) ) ) ) ) ‘ 𝑁 ) = ( ( 1 / ( ( 2 · 𝑁 ) + 1 ) ) · ( seq 1 ( · , ( 𝑘 ∈ ℕ ↦ ( ( ( 2 · 𝑘 ) ↑ 4 ) / ( ( ( 2 · 𝑘 ) · ( ( 2 · 𝑘 ) − 1 ) ) ↑ 2 ) ) ) ) ‘ 𝑁 ) ) )

Proof

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