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