Metamath Proof Explorer

Theorem basellem8

Description: Lemma for basel . The function F of partial sums of the inverse squares is bounded below by J and above by K , obtained by summing the inequality cot ^ 2 x <_ 1 / x ^ 2 <_ csc ^ 2 x = cot ^ 2 x + 1 over the M roots of the polynomial P , and applying the identity basellem5 . (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Hypotheses basel.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
basel.f ⊢ 𝐹 = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) )
basel.h ⊢ 𝐻 = ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − 𝐺 ) )
basel.j ⊢ 𝐽 = ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · 𝐺 ) ) )
basel.k ⊢ 𝐾 = ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + 𝐺 ) )
basellem8.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
Assertion basellem8 ( 𝑀 ∈ ℕ → ( ( 𝐽 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ∧ ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐾 ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 basel.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) )
2 basel.f ⊢ 𝐹 = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) )
3 basel.h ⊢ 𝐻 = ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − 𝐺 ) )
4 basel.j ⊢ 𝐽 = ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · 𝐺 ) ) )
5 basel.k ⊢ 𝐾 = ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + 𝐺 ) )
6 basellem8.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
7 fzfid ⊢ ( 𝑀 ∈ ℕ → ( 1 ... 𝑀 ) ∈ Fin )
8 pire ⊢ π ∈ ℝ
9 2nn ⊢ 2 ∈ ℕ
10 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) ∈ ℕ )
11 9 10 mpan ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℕ )
12 11 peano2nnd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) + 1 ) ∈ ℕ )
13 6 12 eqeltrid ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℕ )
14 nndivre ⊢ ( ( π ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( π / 𝑁 ) ∈ ℝ )
15 8 13 14 sylancr ⊢ ( 𝑀 ∈ ℕ → ( π / 𝑁 ) ∈ ℝ )
16 15 resqcld ⊢ ( 𝑀 ∈ ℕ → ( ( π / 𝑁 ) ↑ 2 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( π / 𝑁 ) ↑ 2 ) ∈ ℝ )
18 6 basellem1 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) )
19 tanrpcl ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ )
20 18 19 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ )
21 20 rpred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ )
22 20 rpne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≠ 0 )
23 2z ⊢ 2 ∈ ℤ
24 znegcl ⊢ ( 2 ∈ ℤ → - 2 ∈ ℤ )
25 23 24 ax-mp ⊢ - 2 ∈ ℤ
26 25 a1i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → - 2 ∈ ℤ )
27 21 22 26 reexpclzd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℝ )
28 17 27 remulcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) ∈ ℝ )
29 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ℕ )
30 29 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ℕ )
31 30 nnred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ℝ )
32 30 nnne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ≠ 0 )
33 31 32 26 reexpclzd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - 2 ) ∈ ℝ )
34 20 rpcnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ )
35 2nn0 ⊢ 2 ∈ ℕ0
36 expneg ⊢ ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
37 34 35 36 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
38 37 oveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
39 15 recnd ⊢ ( 𝑀 ∈ ℕ → ( π / 𝑁 ) ∈ ℂ )
40 39 sqcld ⊢ ( 𝑀 ∈ ℕ → ( ( π / 𝑁 ) ↑ 2 ) ∈ ℂ )
41 40 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( π / 𝑁 ) ↑ 2 ) ∈ ℂ )
42 rpexpcl ⊢ ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
43 20 23 42 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
44 43 rpcnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℂ )
45 43 rpne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≠ 0 )
46 41 44 45 divrecd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
47 38 46 eqtr4d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
48 30 nnrpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ℝ+ )
49 rpexpcl ⊢ ( ( 𝑘 ∈ ℝ+ ∧ - 2 ∈ ℤ ) → ( 𝑘 ↑ - 2 ) ∈ ℝ+ )
50 48 25 49 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - 2 ) ∈ ℝ+ )
51 30 nncnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑘 ∈ ℂ )
52 51 32 26 expnegd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - - 2 ) = ( 1 / ( 𝑘 ↑ - 2 ) ) )
53 2cn ⊢ 2 ∈ ℂ
54 53 negnegi ⊢ - - 2 = 2
55 54 oveq2i ⊢ ( 𝑘 ↑ - - 2 ) = ( 𝑘 ↑ 2 )
56 52 55 eqtr3di ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 1 / ( 𝑘 ↑ - 2 ) ) = ( 𝑘 ↑ 2 ) )
57 56 oveq1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 1 / ( 𝑘 ↑ - 2 ) ) · ( ( π / 𝑁 ) ↑ 2 ) ) = ( ( 𝑘 ↑ 2 ) · ( ( π / 𝑁 ) ↑ 2 ) ) )
58 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
59 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
60 25 a1i ⊢ ( 𝑘 ∈ ℕ → - 2 ∈ ℤ )
61 58 59 60 expclzd ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ↑ - 2 ) ∈ ℂ )
62 30 61 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - 2 ) ∈ ℂ )
63 51 32 26 expne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - 2 ) ≠ 0 )
64 41 62 63 divrec2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) / ( 𝑘 ↑ - 2 ) ) = ( ( 1 / ( 𝑘 ↑ - 2 ) ) · ( ( π / 𝑁 ) ↑ 2 ) ) )
65 picn ⊢ π ∈ ℂ
66 65 a1i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → π ∈ ℂ )
67 13 nncnd ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℂ )
68 67 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ∈ ℂ )
69 13 nnne0d ⊢ ( 𝑀 ∈ ℕ → 𝑁 ≠ 0 )
70 69 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ≠ 0 )
71 51 66 68 70 divassd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) = ( 𝑘 · ( π / 𝑁 ) ) )
72 71 oveq1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) = ( ( 𝑘 · ( π / 𝑁 ) ) ↑ 2 ) )
73 39 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( π / 𝑁 ) ∈ ℂ )
74 51 73 sqmuld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · ( π / 𝑁 ) ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( ( π / 𝑁 ) ↑ 2 ) ) )
75 72 74 eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) = ( ( 𝑘 ↑ 2 ) · ( ( π / 𝑁 ) ↑ 2 ) ) )
76 57 64 75 3eqtr4d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) / ( 𝑘 ↑ - 2 ) ) = ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) )
77 elioore ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ℝ )
78 18 77 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ℝ )
79 78 resqcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) ∈ ℝ )
80 43 rpred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ )
81 tangtx ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( ( 𝑘 · π ) / 𝑁 ) < ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
82 18 81 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) < ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
83 eliooord ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( ( 𝑘 · π ) / 𝑁 ) ∧ ( ( 𝑘 · π ) / 𝑁 ) < ( π / 2 ) ) )
84 18 83 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 0 < ( ( 𝑘 · π ) / 𝑁 ) ∧ ( ( 𝑘 · π ) / 𝑁 ) < ( π / 2 ) ) )
85 84 simpld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 < ( ( 𝑘 · π ) / 𝑁 ) )
86 78 85 elrpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ℝ+ )
87 86 rpge0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( ( 𝑘 · π ) / 𝑁 ) )
88 20 rpge0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
89 78 21 87 88 lt2sqd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) < ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↔ ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
90 82 89 mpbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) )
91 79 80 90 ltled ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) ≤ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) )
92 76 91 eqbrtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) / ( 𝑘 ↑ - 2 ) ) ≤ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) )
93 17 50 43 92 lediv23d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ≤ ( 𝑘 ↑ - 2 ) )
94 47 93 eqbrtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) ≤ ( 𝑘 ↑ - 2 ) )
95 7 28 33 94 fsumle ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) ≤ Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 ↑ - 2 ) )
96 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 2 · 𝑛 ) = ( 2 · 𝑀 ) )
97 96 oveq1d ⊢ ( 𝑛 = 𝑀 → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑀 ) + 1 ) )
98 97 6 eqtr4di ⊢ ( 𝑛 = 𝑀 → ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
99 98 oveq2d ⊢ ( 𝑛 = 𝑀 → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) = ( 1 / 𝑁 ) )
100 99 oveq2d ⊢ ( 𝑛 = 𝑀 → ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 1 − ( 1 / 𝑁 ) ) )
101 100 oveq2d ⊢ ( 𝑛 = 𝑀 → ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) )
102 99 oveq2d ⊢ ( 𝑛 = 𝑀 → ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( - 2 · ( 1 / 𝑁 ) ) )
103 102 oveq2d ⊢ ( 𝑛 = 𝑀 → ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) )
104 101 103 oveq12d ⊢ ( 𝑛 = 𝑀 → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) = ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) ) )
105 nnex ⊢ ℕ ∈ V
106 105 a1i ⊢ ( ⊤ → ℕ ∈ V )
107 ovexd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ V )
108 ovexd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ∈ V )
109 8 resqcli ⊢ ( π ↑ 2 ) ∈ ℝ
110 6re ⊢ 6 ∈ ℝ
111 6nn ⊢ 6 ∈ ℕ
112 111 nnne0i ⊢ 6 ≠ 0
113 109 110 112 redivcli ⊢ ( ( π ↑ 2 ) / 6 ) ∈ ℝ
114 113 a1i ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( ( π ↑ 2 ) / 6 ) ∈ ℝ )
115 ovexd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ V )
116 fconstmpt ⊢ ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) = ( 𝑛 ∈ ℕ ↦ ( ( π ↑ 2 ) / 6 ) )
117 116 a1i ⊢ ( ⊤ → ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) = ( 𝑛 ∈ ℕ ↦ ( ( π ↑ 2 ) / 6 ) ) )
118 1zzd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℤ )
119 ovexd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ∈ V )
120 fconstmpt ⊢ ( ℕ × { 1 } ) = ( 𝑛 ∈ ℕ ↦ 1 )
121 120 a1i ⊢ ( ⊤ → ( ℕ × { 1 } ) = ( 𝑛 ∈ ℕ ↦ 1 ) )
122 1 a1i ⊢ ( ⊤ → 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) )
123 106 118 119 121 122 offval2 ⊢ ( ⊤ → ( ( ℕ × { 1 } ) ∘f − 𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
124 106 114 115 117 123 offval2 ⊢ ( ⊤ → ( ( ℕ × { ( ( π ↑ 2 ) / 6 ) } ) ∘f · ( ( ℕ × { 1 } ) ∘f − 𝐺 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
125 3 124 eqtrid ⊢ ( ⊤ → 𝐻 = ( 𝑛 ∈ ℕ ↦ ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
126 ovexd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ V )
127 53 negcli ⊢ - 2 ∈ ℂ
128 127 a1i ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → - 2 ∈ ℂ )
129 fconstmpt ⊢ ( ℕ × { - 2 } ) = ( 𝑛 ∈ ℕ ↦ - 2 )
130 129 a1i ⊢ ( ⊤ → ( ℕ × { - 2 } ) = ( 𝑛 ∈ ℕ ↦ - 2 ) )
131 106 128 119 130 122 offval2 ⊢ ( ⊤ → ( ( ℕ × { - 2 } ) ∘f · 𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
132 106 118 126 121 131 offval2 ⊢ ( ⊤ → ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · 𝐺 ) ) = ( 𝑛 ∈ ℕ ↦ ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
133 106 107 108 125 132 offval2 ⊢ ( ⊤ → ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · 𝐺 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) ) )
134 133 mptru ⊢ ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + ( ( ℕ × { - 2 } ) ∘f · 𝐺 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
135 4 134 eqtri ⊢ 𝐽 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( - 2 · ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
136 ovex ⊢ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) ) ∈ V
137 104 135 136 fvmpt ⊢ ( 𝑀 ∈ ℕ → ( 𝐽 ‘ 𝑀 ) = ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) ) )
138 113 recni ⊢ ( ( π ↑ 2 ) / 6 ) ∈ ℂ
139 138 a1i ⊢ ( 𝑀 ∈ ℕ → ( ( π ↑ 2 ) / 6 ) ∈ ℂ )
140 11 nncnd ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℂ )
141 140 67 69 divcld ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) / 𝑁 ) ∈ ℂ )
142 ax-1cn ⊢ 1 ∈ ℂ
143 subcl ⊢ ( ( ( 2 · 𝑀 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 · 𝑀 ) − 1 ) ∈ ℂ )
144 140 142 143 sylancl ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ℂ )
145 144 67 69 divcld ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ∈ ℂ )
146 139 141 145 mulassd ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( ( 2 · 𝑀 ) / 𝑁 ) ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) ) )
147 1cnd ⊢ ( 𝑀 ∈ ℕ → 1 ∈ ℂ )
148 67 147 67 69 divsubdird ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − 1 ) / 𝑁 ) = ( ( 𝑁 / 𝑁 ) − ( 1 / 𝑁 ) ) )
149 6 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ( 2 · 𝑀 ) + 1 ) − 1 )
150 pncan ⊢ ( ( ( 2 · 𝑀 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑀 ) + 1 ) − 1 ) = ( 2 · 𝑀 ) )
151 140 142 150 sylancl ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) + 1 ) − 1 ) = ( 2 · 𝑀 ) )
152 149 151 eqtrid ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 − 1 ) = ( 2 · 𝑀 ) )
153 152 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − 1 ) / 𝑁 ) = ( ( 2 · 𝑀 ) / 𝑁 ) )
154 67 69 dividd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 / 𝑁 ) = 1 )
155 154 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 / 𝑁 ) − ( 1 / 𝑁 ) ) = ( 1 − ( 1 / 𝑁 ) ) )
156 148 153 155 3eqtr3rd ⊢ ( 𝑀 ∈ ℕ → ( 1 − ( 1 / 𝑁 ) ) = ( ( 2 · 𝑀 ) / 𝑁 ) )
157 156 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( 2 · 𝑀 ) / 𝑁 ) ) )
158 127 a1i ⊢ ( 𝑀 ∈ ℕ → - 2 ∈ ℂ )
159 67 158 67 69 divdird ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 + - 2 ) / 𝑁 ) = ( ( 𝑁 / 𝑁 ) + ( - 2 / 𝑁 ) ) )
160 negsub ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ) → ( 𝑁 + - 2 ) = ( 𝑁 − 2 ) )
161 67 53 160 sylancl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 + - 2 ) = ( 𝑁 − 2 ) )
162 df-2 ⊢ 2 = ( 1 + 1 )
163 6 162 oveq12i ⊢ ( 𝑁 − 2 ) = ( ( ( 2 · 𝑀 ) + 1 ) − ( 1 + 1 ) )
164 140 147 147 pnpcan2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) + 1 ) − ( 1 + 1 ) ) = ( ( 2 · 𝑀 ) − 1 ) )
165 163 164 eqtrid ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 − 2 ) = ( ( 2 · 𝑀 ) − 1 ) )
166 161 165 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 + - 2 ) = ( ( 2 · 𝑀 ) − 1 ) )
167 166 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 + - 2 ) / 𝑁 ) = ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) )
168 158 67 69 divrecd ⊢ ( 𝑀 ∈ ℕ → ( - 2 / 𝑁 ) = ( - 2 · ( 1 / 𝑁 ) ) )
169 154 168 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 / 𝑁 ) + ( - 2 / 𝑁 ) ) = ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) )
170 159 167 169 3eqtr3rd ⊢ ( 𝑀 ∈ ℕ → ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) = ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) )
171 157 170 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) ) = ( ( ( ( π ↑ 2 ) / 6 ) · ( ( 2 · 𝑀 ) / 𝑁 ) ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) )
172 13 nnsqcld ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℕ )
173 172 nncnd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ↑ 2 ) ∈ ℂ )
174 6cn ⊢ 6 ∈ ℂ
175 174 a1i ⊢ ( 𝑀 ∈ ℕ → 6 ∈ ℂ )
176 173 175 mulcomd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 ↑ 2 ) · 6 ) = ( 6 · ( 𝑁 ↑ 2 ) ) )
177 176 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) / ( ( 𝑁 ↑ 2 ) · 6 ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) / ( 6 · ( 𝑁 ↑ 2 ) ) ) )
178 109 recni ⊢ ( π ↑ 2 ) ∈ ℂ
179 178 a1i ⊢ ( 𝑀 ∈ ℕ → ( π ↑ 2 ) ∈ ℂ )
180 140 144 mulcld ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ )
181 172 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ↑ 2 ) ≠ 0 )
182 173 181 jca ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 ↑ 2 ) ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ≠ 0 ) )
183 174 112 pm3.2i ⊢ ( 6 ∈ ℂ ∧ 6 ≠ 0 )
184 183 a1i ⊢ ( 𝑀 ∈ ℕ → ( 6 ∈ ℂ ∧ 6 ≠ 0 ) )
185 divmuldiv ⊢ ( ( ( ( π ↑ 2 ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ ) ∧ ( ( ( 𝑁 ↑ 2 ) ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ≠ 0 ) ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ) ) → ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) / ( ( 𝑁 ↑ 2 ) · 6 ) ) )
186 179 180 182 184 185 syl22anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) / ( ( 𝑁 ↑ 2 ) · 6 ) ) )
187 divmuldiv ⊢ ( ( ( ( π ↑ 2 ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ ) ∧ ( ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( ( 𝑁 ↑ 2 ) ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ≠ 0 ) ) ) → ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 ↑ 2 ) ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) / ( 6 · ( 𝑁 ↑ 2 ) ) ) )
188 179 180 184 182 187 syl22anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 ↑ 2 ) ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) / ( 6 · ( 𝑁 ↑ 2 ) ) ) )
189 177 186 188 3eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
190 65 a1i ⊢ ( 𝑀 ∈ ℕ → π ∈ ℂ )
191 190 67 69 sqdivd ⊢ ( 𝑀 ∈ ℕ → ( ( π / 𝑁 ) ↑ 2 ) = ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) )
192 191 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) )
193 140 67 144 67 69 69 divmuldivd ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 · 𝑁 ) ) )
194 67 sqvald ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
195 194 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 ↑ 2 ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 · 𝑁 ) ) )
196 193 195 eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 ↑ 2 ) ) )
197 196 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
198 189 192 197 3eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( ( 2 · 𝑀 ) − 1 ) / 𝑁 ) ) ) )
199 146 171 198 3eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) )
200 eqid ⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑥 ↑ 𝑗 ) ) ) = ( 𝑥 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑥 ↑ 𝑗 ) ) )
201 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) )
202 6 200 201 basellem5 ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )
203 202 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) ) )
204 199 203 eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( - 2 · ( 1 / 𝑁 ) ) ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
205 27 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℂ )
206 7 40 205 fsummulc2 ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
207 137 204 206 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝐽 ‘ 𝑀 ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
208 2 fveq1i ⊢ ( 𝐹 ‘ 𝑀 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) ) ‘ 𝑀 )
209 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ↑ - 2 ) = ( 𝑘 ↑ - 2 ) )
210 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) )
211 ovex ⊢ ( 𝑘 ↑ - 2 ) ∈ V
212 209 210 211 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) ‘ 𝑘 ) = ( 𝑘 ↑ - 2 ) )
213 30 212 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) ‘ 𝑘 ) = ( 𝑘 ↑ - 2 ) )
214 id ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ )
215 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
216 214 215 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
217 213 216 62 fsumser ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 ↑ - 2 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑛 ↑ - 2 ) ) ) ‘ 𝑀 ) )
218 208 217 eqtr4id ⊢ ( 𝑀 ∈ ℕ → ( 𝐹 ‘ 𝑀 ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 ↑ - 2 ) )
219 95 207 218 3brtr4d ⊢ ( 𝑀 ∈ ℕ → ( 𝐽 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) )
220 78 resincld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ )
221 sincosq1sgn ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∧ 0 < ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
222 18 221 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 0 < ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∧ 0 < ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
223 222 simpld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 < ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
224 223 gt0ne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≠ 0 )
225 220 224 26 reexpclzd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℝ )
226 17 225 remulcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) ∈ ℝ )
227 sinltx ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ℝ+ → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( ( 𝑘 · π ) / 𝑁 ) )
228 86 227 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( ( 𝑘 · π ) / 𝑁 ) )
229 220 78 228 ltled ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≤ ( ( 𝑘 · π ) / 𝑁 ) )
230 0re ⊢ 0 ∈ ℝ
231 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ ) → ( 0 < ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) → 0 ≤ ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
232 230 220 231 sylancr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 0 < ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) → 0 ≤ ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
233 223 232 mpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
234 220 78 233 87 le2sqd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≤ ( ( 𝑘 · π ) / 𝑁 ) ↔ ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≤ ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) ) )
235 229 234 mpbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≤ ( ( ( 𝑘 · π ) / 𝑁 ) ↑ 2 ) )
236 235 76 breqtrrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) / ( 𝑘 ↑ - 2 ) ) )
237 220 resqcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ )
238 237 17 50 lemuldiv2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 ↑ - 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ≤ ( ( π / 𝑁 ) ↑ 2 ) ↔ ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) / ( 𝑘 ↑ - 2 ) ) ) )
239 220 223 elrpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ )
240 rpexpcl ⊢ ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
241 239 23 240 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
242 33 17 241 lemuldivd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑘 ↑ - 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ≤ ( ( π / 𝑁 ) ↑ 2 ) ↔ ( 𝑘 ↑ - 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
243 238 242 bitr3d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) / ( 𝑘 ↑ - 2 ) ) ↔ ( 𝑘 ↑ - 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
244 236 243 mpbid ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
245 220 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ )
246 expneg ⊢ ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
247 245 35 246 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
248 247 oveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · ( 1 / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
249 237 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℂ )
250 241 rpne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≠ 0 )
251 41 249 250 divrecd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · ( 1 / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
252 248 251 eqtr4d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
253 244 252 breqtrrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑘 ↑ - 2 ) ≤ ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
254 7 33 226 253 fsumle ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑘 ↑ - 2 ) ≤ Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
255 99 oveq2d ⊢ ( 𝑛 = 𝑀 → ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 1 + ( 1 / 𝑁 ) ) )
256 101 255 oveq12d ⊢ ( 𝑛 = 𝑀 → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( 1 / 𝑁 ) ) ) )
257 ovexd ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ V )
258 106 118 119 121 122 offval2 ⊢ ( ⊤ → ( ( ℕ × { 1 } ) ∘f + 𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
259 106 107 257 125 258 offval2 ⊢ ( ⊤ → ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + 𝐺 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
260 259 mptru ⊢ ( 𝐻 ∘f · ( ( ℕ × { 1 } ) ∘f + 𝐺 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
261 5 260 eqtri ⊢ 𝐾 = ( 𝑛 ∈ ℕ ↦ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) · ( 1 + ( 1 / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
262 ovex ⊢ ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( 1 / 𝑁 ) ) ) ∈ V
263 256 261 262 fvmpt ⊢ ( 𝑀 ∈ ℕ → ( 𝐾 ‘ 𝑀 ) = ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( 1 / 𝑁 ) ) ) )
264 peano2cn ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
265 67 264 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ )
266 265 67 69 divcld ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) ∈ ℂ )
267 139 141 266 mulassd ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( ( 2 · 𝑀 ) / 𝑁 ) ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
268 67 147 67 69 divdird ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 + 1 ) / 𝑁 ) = ( ( 𝑁 / 𝑁 ) + ( 1 / 𝑁 ) ) )
269 154 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 / 𝑁 ) + ( 1 / 𝑁 ) ) = ( 1 + ( 1 / 𝑁 ) ) )
270 268 269 eqtr2d ⊢ ( 𝑀 ∈ ℕ → ( 1 + ( 1 / 𝑁 ) ) = ( ( 𝑁 + 1 ) / 𝑁 ) )
271 157 270 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( 1 / 𝑁 ) ) ) = ( ( ( ( π ↑ 2 ) / 6 ) · ( ( 2 · 𝑀 ) / 𝑁 ) ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) )
272 176 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ) / ( ( 𝑁 ↑ 2 ) · 6 ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ) / ( 6 · ( 𝑁 ↑ 2 ) ) ) )
273 140 265 mulcld ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ∈ ℂ )
274 divmuldiv ⊢ ( ( ( ( π ↑ 2 ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ∈ ℂ ) ∧ ( ( ( 𝑁 ↑ 2 ) ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ≠ 0 ) ∧ ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ) ) → ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ) / ( ( 𝑁 ↑ 2 ) · 6 ) ) )
275 179 273 182 184 274 syl22anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ) / ( ( 𝑁 ↑ 2 ) · 6 ) ) )
276 divmuldiv ⊢ ( ( ( ( π ↑ 2 ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ∈ ℂ ) ∧ ( ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( ( 𝑁 ↑ 2 ) ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ≠ 0 ) ) ) → ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ) / ( 6 · ( 𝑁 ↑ 2 ) ) ) )
277 179 273 184 182 276 syl22anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) = ( ( ( π ↑ 2 ) · ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) ) / ( 6 · ( 𝑁 ↑ 2 ) ) ) )
278 272 275 277 3eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
279 78 recoscld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ )
280 279 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ )
281 280 sqcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℂ )
282 249 281 249 250 divdird ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) + ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) + ( ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
283 78 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ℂ )
284 sincossq ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ℂ → ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) + ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = 1 )
285 283 284 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) + ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = 1 )
286 285 oveq1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) + ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( 1 / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
287 249 250 dividd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = 1 )
288 222 simprd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 0 < ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
289 288 gt0ne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≠ 0 )
290 tanval ⊢ ( ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ℂ ∧ ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≠ 0 ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) = ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) / ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
291 283 289 290 syl2anc ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) = ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) / ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
292 291 oveq1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) = ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) / ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) ↑ 2 ) )
293 245 280 289 sqdivd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) / ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) ↑ 2 ) = ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
294 292 293 eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) = ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
295 294 oveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( 1 / ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
296 sqne0 ⊢ ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ → ( ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≠ 0 ↔ ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≠ 0 ) )
297 280 296 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≠ 0 ↔ ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ≠ 0 ) )
298 289 297 mpbird ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ≠ 0 )
299 249 281 250 298 recdivd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 1 / ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) = ( ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
300 37 295 299 3eqtrrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
301 287 300 oveq12d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) + ( ( ( cos ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) = ( 1 + ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
302 282 286 301 3eqtr3d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 1 / ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) = ( 1 + ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
303 addcom ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℂ ) → ( 1 + ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + 1 ) )
304 142 205 303 sylancr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 1 + ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + 1 ) )
305 247 302 304 3eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + 1 ) )
306 305 sumeq2dv ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + 1 ) )
307 1cnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 1 ∈ ℂ )
308 7 205 307 fsumadd ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + 1 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑀 ) 1 ) )
309 fsumconst ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑀 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 1 ) )
310 7 142 309 sylancl ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 1 ) )
311 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
312 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
313 311 312 syl ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
314 313 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 1 ) = ( 𝑀 · 1 ) )
315 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
316 315 mulridd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 · 1 ) = 𝑀 )
317 310 314 316 3eqtrd ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) 1 = 𝑀 )
318 202 317 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑀 ) 1 ) = ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) + 𝑀 ) )
319 306 308 318 3eqtrd ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) + 𝑀 ) )
320 3cn ⊢ 3 ∈ ℂ
321 320 a1i ⊢ ( 𝑀 ∈ ℕ → 3 ∈ ℂ )
322 140 144 321 adddid ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( ( ( 2 · 𝑀 ) − 1 ) + 3 ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) + ( ( 2 · 𝑀 ) · 3 ) ) )
323 3m1e2 ⊢ ( 3 − 1 ) = 2
324 323 162 eqtri ⊢ ( 3 − 1 ) = ( 1 + 1 )
325 324 oveq2i ⊢ ( ( 2 · 𝑀 ) + ( 3 − 1 ) ) = ( ( 2 · 𝑀 ) + ( 1 + 1 ) )
326 140 147 321 subadd23d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) + 3 ) = ( ( 2 · 𝑀 ) + ( 3 − 1 ) ) )
327 140 147 147 addassd ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) + 1 ) + 1 ) = ( ( 2 · 𝑀 ) + ( 1 + 1 ) ) )
328 325 326 327 3eqtr4a ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) + 3 ) = ( ( ( 2 · 𝑀 ) + 1 ) + 1 ) )
329 6 oveq1i ⊢ ( 𝑁 + 1 ) = ( ( ( 2 · 𝑀 ) + 1 ) + 1 )
330 328 329 eqtr4di ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) + 3 ) = ( 𝑁 + 1 ) )
331 330 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( ( ( 2 · 𝑀 ) − 1 ) + 3 ) ) = ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) )
332 2cnd ⊢ ( 𝑀 ∈ ℕ → 2 ∈ ℂ )
333 332 315 321 mul32d ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · 3 ) = ( ( 2 · 3 ) · 𝑀 ) )
334 2t3e6 ⊢ ( 2 · 3 ) = 6
335 334 oveq1i ⊢ ( ( 2 · 3 ) · 𝑀 ) = ( 6 · 𝑀 )
336 333 335 eqtrdi ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · 3 ) = ( 6 · 𝑀 ) )
337 336 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) + ( ( 2 · 𝑀 ) · 3 ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) + ( 6 · 𝑀 ) ) )
338 322 331 337 3eqtr3d ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) + ( 6 · 𝑀 ) ) )
339 338 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) = ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) + ( 6 · 𝑀 ) ) / 6 ) )
340 mulcl ⊢ ( ( 6 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 6 · 𝑀 ) ∈ ℂ )
341 174 315 340 sylancr ⊢ ( 𝑀 ∈ ℕ → ( 6 · 𝑀 ) ∈ ℂ )
342 112 a1i ⊢ ( 𝑀 ∈ ℕ → 6 ≠ 0 )
343 180 341 175 342 divdird ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) + ( 6 · 𝑀 ) ) / 6 ) = ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) + ( ( 6 · 𝑀 ) / 6 ) ) )
344 315 175 342 divcan3d ⊢ ( 𝑀 ∈ ℕ → ( ( 6 · 𝑀 ) / 6 ) = 𝑀 )
345 344 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) + ( ( 6 · 𝑀 ) / 6 ) ) = ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) + 𝑀 ) )
346 339 343 345 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) = ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) + 𝑀 ) )
347 319 346 eqtr4d ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) )
348 191 347 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π ↑ 2 ) / ( 𝑁 ↑ 2 ) ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / 6 ) ) )
349 140 67 265 67 69 69 divmuldivd ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 · 𝑁 ) ) )
350 194 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 ↑ 2 ) ) = ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 · 𝑁 ) ) )
351 349 350 eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) = ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 ↑ 2 ) ) )
352 351 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) · ( 𝑁 + 1 ) ) / ( 𝑁 ↑ 2 ) ) ) )
353 278 348 352 3eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( ( π ↑ 2 ) / 6 ) · ( ( ( 2 · 𝑀 ) / 𝑁 ) · ( ( 𝑁 + 1 ) / 𝑁 ) ) ) )
354 267 271 353 3eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( ( π ↑ 2 ) / 6 ) · ( 1 − ( 1 / 𝑁 ) ) ) · ( 1 + ( 1 / 𝑁 ) ) ) = ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
355 225 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℂ )
356 7 40 355 fsummulc2 ⊢ ( 𝑀 ∈ ℕ → ( ( ( π / 𝑁 ) ↑ 2 ) · Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
357 263 354 356 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝐾 ‘ 𝑀 ) = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( ( π / 𝑁 ) ↑ 2 ) · ( ( sin ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ) )
358 254 218 357 3brtr4d ⊢ ( 𝑀 ∈ ℕ → ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐾 ‘ 𝑀 ) )
359 219 358 jca ⊢ ( 𝑀 ∈ ℕ → ( ( 𝐽 ‘ 𝑀 ) ≤ ( 𝐹 ‘ 𝑀 ) ∧ ( 𝐹 ‘ 𝑀 ) ≤ ( 𝐾 ‘ 𝑀 ) ) )