Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ∈
Fin) |
2 | | pire 24014 |
. . . . . . . 8
⊢ π
∈ ℝ |
3 | | basellem8.n |
. . . . . . . . 9
⊢ 𝑁 = ((2 · 𝑀) + 1) |
4 | | 2nn 11062 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
5 | | nnmulcl 10920 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
6 | 4, 5 | mpan 702 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) |
7 | 6 | peano2nnd 10914 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) |
8 | 3, 7 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) |
9 | | nndivre 10933 |
. . . . . . . 8
⊢ ((π
∈ ℝ ∧ 𝑁
∈ ℕ) → (π / 𝑁) ∈ ℝ) |
10 | 2, 8, 9 | sylancr 694 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (π /
𝑁) ∈
ℝ) |
11 | 10 | resqcld 12897 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((π /
𝑁)↑2) ∈
ℝ) |
12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ) |
13 | 3 | basellem1 24607 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2))) |
14 | | tanrpcl 24060 |
. . . . . . . 8
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(tan‘((𝑘 ·
π) / 𝑁)) ∈
ℝ+) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈
ℝ+) |
16 | 15 | rpred 11748 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ) |
17 | 15 | rpne0d 11753 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0) |
18 | | 2z 11286 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
19 | | znegcl 11289 |
. . . . . . . 8
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ -2 ∈
ℤ |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈
ℤ) |
22 | 16, 17, 21 | reexpclzd 12896 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ) |
23 | 12, 22 | remulcld 9949 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ∈
ℝ) |
24 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ) |
25 | 24 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ) |
26 | 25 | nnred 10912 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ) |
27 | 25 | nnne0d 10942 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0) |
28 | 26, 27, 21 | reexpclzd 12896 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ) |
29 | 16 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
30 | | 2nn0 11186 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
31 | | expneg 12730 |
. . . . . . . 8
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℂ ∧ 2 ∈ ℕ0) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 /
((tan‘((𝑘 ·
π) / 𝑁))↑2))) |
32 | 29, 30, 31 | sylancl 693 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))) |
33 | 32 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 /
((tan‘((𝑘 ·
π) / 𝑁))↑2)))) |
34 | 10 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (π /
𝑁) ∈
ℂ) |
35 | 34 | sqcld 12868 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((π /
𝑁)↑2) ∈
ℂ) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ) |
37 | | rpexpcl 12741 |
. . . . . . . . . 10
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
38 | 15, 18, 37 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
39 | 38 | rpred 11748 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ) |
40 | 39 | recnd 9947 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ) |
41 | 38 | rpne0d 11753 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0) |
42 | 36, 40, 41 | divrecd 10683 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))) |
43 | 33, 42 | eqtr4d 2647 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2))) |
44 | 25 | nnrpd 11746 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ+) |
45 | | rpexpcl 12741 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ+
∧ -2 ∈ ℤ) → (𝑘↑-2) ∈
ℝ+) |
46 | 44, 20, 45 | sylancl 693 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈
ℝ+) |
47 | | 2cn 10968 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
48 | 47 | negnegi 10230 |
. . . . . . . . . . 11
⊢ --2 =
2 |
49 | 48 | oveq2i 6560 |
. . . . . . . . . 10
⊢ (𝑘↑--2) = (𝑘↑2) |
50 | 25 | nncnd 10913 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ) |
51 | 50, 27, 21 | expnegd 12877 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑--2) = (1 / (𝑘↑-2))) |
52 | 49, 51 | syl5reqr 2659 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑-2)) = (𝑘↑2)) |
53 | 52 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2))) |
54 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
55 | | nnne0 10930 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
56 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → -2 ∈
ℤ) |
57 | 54, 55, 56 | expclzd 12875 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘↑-2) ∈
ℂ) |
58 | 25, 57 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℂ) |
59 | 50, 27, 21 | expne0d 12876 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≠ 0) |
60 | 36, 58, 59 | divrec2d 10684 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2))) |
61 | 2 | recni 9931 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈
ℂ) |
63 | 8 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℂ) |
64 | 8 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0) |
65 | 63, 64 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
67 | | divass 10582 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ π
∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → ((𝑘 ·
π) / 𝑁) = (𝑘 · (π / 𝑁))) |
68 | 50, 62, 66, 67 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁))) |
69 | 68 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2)) |
70 | 34 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ) |
71 | 50, 70 | sqmuld 12882 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2))) |
72 | 69, 71 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2))) |
73 | 53, 60, 72 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = (((𝑘 · π) / 𝑁)↑2)) |
74 | | elioore 12076 |
. . . . . . . . . 10
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
((𝑘 · π) / 𝑁) ∈
ℝ) |
75 | 13, 74 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ) |
76 | 75 | resqcld 12897 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ) |
77 | | tangtx 24061 |
. . . . . . . . . 10
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁))) |
78 | 13, 77 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁))) |
79 | | eliooord 12104 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(0 < ((𝑘 · π)
/ 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π /
2))) |
80 | 13, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2))) |
81 | 80 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁)) |
82 | 75, 81 | elrpd 11745 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈
ℝ+) |
83 | 82 | rpge0d 11752 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁)) |
84 | 15 | rpge0d 11752 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁))) |
85 | 75, 16, 83, 84 | lt2sqd 12905 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))) |
86 | 78, 85 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)) |
87 | 76, 39, 86 | ltled 10064 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2)) |
88 | 73, 87 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2)) |
89 | 12, 46, 38, 88 | lediv23d 11814 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑-2)) |
90 | 43, 89 | eqbrtrd 4605 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ (𝑘↑-2)) |
91 | 1, 23, 28, 90 | fsumle 14372 |
. . 3
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑-2)) |
92 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀)) |
93 | 92 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1)) |
94 | 93, 3 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁) |
95 | 94 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁)) |
96 | 95 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁))) |
97 | 96 | oveq2d 6565 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1
− (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1
− (1 / 𝑁)))) |
98 | 95 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (-2 · (1 / ((2 · 𝑛) + 1))) = (-2 · (1 /
𝑁))) |
99 | 98 | oveq2d 6565 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (1 + (-2 · (1 / ((2 ·
𝑛) + 1)))) = (1 + (-2
· (1 / 𝑁)))) |
100 | 97, 99 | oveq12d 6567 |
. . . . 5
⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1
− (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) + 1))))) =
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁))))) |
101 | | basel.j |
. . . . . 6
⊢ 𝐽 = (𝐻 ∘𝑓 ·
((ℕ × {1}) ∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) |
102 | | nnex 10903 |
. . . . . . . . 9
⊢ ℕ
∈ V |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ℕ ∈ V) |
104 | | ovex 6577 |
. . . . . . . . 9
⊢
(((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) ∈
V |
105 | 104 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2
· 𝑛) + 1)))) ∈
V) |
106 | | ovex 6577 |
. . . . . . . . 9
⊢ (1 + (-2
· (1 / ((2 · 𝑛) + 1)))) ∈ V |
107 | 106 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) ∈ V) |
108 | | basel.h |
. . . . . . . . 9
⊢ 𝐻 = ((ℕ ×
{((π↑2) / 6)}) ∘𝑓 · ((ℕ ×
{1}) ∘𝑓 − 𝐺)) |
109 | 2 | resqcli 12811 |
. . . . . . . . . . . 12
⊢
(π↑2) ∈ ℝ |
110 | | 6re 10978 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
111 | | 6nn 11066 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℕ |
112 | 111 | nnne0i 10932 |
. . . . . . . . . . . 12
⊢ 6 ≠
0 |
113 | 109, 110,
112 | redivcli 10671 |
. . . . . . . . . . 11
⊢
((π↑2) / 6) ∈ ℝ |
114 | 113 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → ((π↑2) / 6) ∈ ℝ) |
115 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (1
− (1 / ((2 · 𝑛) + 1))) ∈ V |
116 | 115 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V) |
117 | | fconstmpt 5085 |
. . . . . . . . . . 11
⊢ (ℕ
× {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) /
6)) |
118 | 117 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) /
6))) |
119 | | 1zzd 11285 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → 1 ∈ ℤ) |
120 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (1 / ((2
· 𝑛) + 1)) ∈
V |
121 | 120 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V) |
122 | | fconstmpt 5085 |
. . . . . . . . . . . 12
⊢ (ℕ
× {1}) = (𝑛 ∈
ℕ ↦ 1) |
123 | 122 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1)) |
124 | | basel.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 ·
𝑛) + 1))) |
125 | 124 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2
· 𝑛) +
1)))) |
126 | 103, 119,
121, 123, 125 | offval2 6812 |
. . . . . . . . . 10
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2
· 𝑛) +
1))))) |
127 | 103, 114,
116, 118, 126 | offval2 6812 |
. . . . . . . . 9
⊢ (⊤
→ ((ℕ × {((π↑2) / 6)}) ∘𝑓
· ((ℕ × {1}) ∘𝑓 − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))))) |
128 | 108, 127 | syl5eq 2656 |
. . . . . . . 8
⊢ (⊤
→ 𝐻 = (𝑛 ∈ ℕ ↦
(((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))))) |
129 | | ovex 6577 |
. . . . . . . . . 10
⊢ (-2
· (1 / ((2 · 𝑛) + 1))) ∈ V |
130 | 129 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (-2 · (1 / ((2 · 𝑛) + 1))) ∈ V) |
131 | 47 | negcli 10228 |
. . . . . . . . . . 11
⊢ -2 ∈
ℂ |
132 | 131 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → -2 ∈ ℂ) |
133 | | fconstmpt 5085 |
. . . . . . . . . . 11
⊢ (ℕ
× {-2}) = (𝑛 ∈
ℕ ↦ -2) |
134 | 133 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2)) |
135 | 103, 132,
121, 134, 125 | offval2 6812 |
. . . . . . . . 9
⊢ (⊤
→ ((ℕ × {-2}) ∘𝑓 · 𝐺) = (𝑛 ∈ ℕ ↦ (-2 · (1 / ((2
· 𝑛) +
1))))) |
136 | 103, 119,
130, 123, 135 | offval2 6812 |
. . . . . . . 8
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + (-2 · (1
/ ((2 · 𝑛) +
1)))))) |
137 | 103, 105,
107, 128, 136 | offval2 6812 |
. . . . . . 7
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + ((ℕ × {-2})
∘𝑓 · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) +
1))))))) |
138 | 137 | trud 1484 |
. . . . . 6
⊢ (𝐻 ∘𝑓
· ((ℕ × {1}) ∘𝑓 + ((ℕ ×
{-2}) ∘𝑓 · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) +
1)))))) |
139 | 101, 138 | eqtri 2632 |
. . . . 5
⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) +
1)))))) |
140 | | ovex 6577 |
. . . . 5
⊢
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) ∈ V |
141 | 100, 139,
140 | fvmpt 6191 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1
− (1 / 𝑁))) ·
(1 + (-2 · (1 / 𝑁))))) |
142 | 113 | recni 9931 |
. . . . . . . 8
⊢
((π↑2) / 6) ∈ ℂ |
143 | 142 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
((π↑2) / 6) ∈ ℂ) |
144 | 6 | nncnd 10913 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℂ) |
145 | 144, 63, 64 | divcld 10680 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) / 𝑁) ∈
ℂ) |
146 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
147 | | subcl 10159 |
. . . . . . . . 9
⊢ (((2
· 𝑀) ∈ ℂ
∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈
ℂ) |
148 | 144, 146,
147 | sylancl 693 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℂ) |
149 | 148, 63, 64 | divcld 10680 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) /
𝑁) ∈
ℂ) |
150 | 143, 145,
149 | mulassd 9942 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2
· 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)))) |
151 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 1 ∈
ℂ) |
152 | 63, 151, 63, 64 | divsubdird 10719 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁))) |
153 | 3 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ (𝑁 − 1) = (((2 ·
𝑀) + 1) −
1) |
154 | | pncan 10166 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑀) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀)) |
155 | 144, 146,
154 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) − 1)
= (2 · 𝑀)) |
156 | 153, 155 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀)) |
157 | 156 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁)) |
158 | 63, 64 | dividd 10678 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1) |
159 | 158 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁))) |
160 | 152, 157,
159 | 3eqtr3rd 2653 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (1
− (1 / 𝑁)) = ((2
· 𝑀) / 𝑁)) |
161 | 160 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2
· 𝑀) / 𝑁))) |
162 | 131 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → -2 ∈
ℂ) |
163 | 63, 162, 63, 64 | divdird 10718 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + (-2 / 𝑁))) |
164 | | negsub 10208 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑁 + -2) =
(𝑁 −
2)) |
165 | 63, 47, 164 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2)) |
166 | | df-2 10956 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
167 | 3, 166 | oveq12i 6561 |
. . . . . . . . . . 11
⊢ (𝑁 − 2) = (((2 ·
𝑀) + 1) − (1 +
1)) |
168 | 144, 151,
151 | pnpcan2d 10309 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) − (1
+ 1)) = ((2 · 𝑀)
− 1)) |
169 | 167, 168 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1)) |
170 | 165, 169 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1)) |
171 | 170 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁)) |
172 | 162, 63, 64 | divrecd 10683 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (-2 /
𝑁) = (-2 · (1 /
𝑁))) |
173 | 158, 172 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (-2 / 𝑁)) = (1 + (-2 · (1 / 𝑁)))) |
174 | 163, 171,
173 | 3eqtr3rd 2653 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (1 + (-2
· (1 / 𝑁))) = (((2
· 𝑀) − 1) /
𝑁)) |
175 | 161, 174 | oveq12d 6567 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = ((((π↑2) / 6)
· ((2 · 𝑀) /
𝑁)) · (((2 ·
𝑀) − 1) / 𝑁))) |
176 | 8 | nnsqcld 12891 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈
ℕ) |
177 | 176 | nncnd 10913 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈
ℂ) |
178 | | 6cn 10979 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
179 | | mulcom 9901 |
. . . . . . . . . 10
⊢ (((𝑁↑2) ∈ ℂ ∧ 6
∈ ℂ) → ((𝑁↑2) · 6) = (6 · (𝑁↑2))) |
180 | 177, 178,
179 | sylancl 693 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6
· (𝑁↑2))) |
181 | 180 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2)
· ((2 · 𝑀)
· ((2 · 𝑀)
− 1))) / (6 · (𝑁↑2)))) |
182 | 109 | recni 9931 |
. . . . . . . . . 10
⊢
(π↑2) ∈ ℂ |
183 | 182 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(π↑2) ∈ ℂ) |
184 | 144, 148 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ) |
185 | 176 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠
0) |
186 | 177, 185 | jca 553 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧
(𝑁↑2) ≠
0)) |
187 | 178, 112 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (6 ∈
ℂ ∧ 6 ≠ 0) |
188 | 187 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (6 ∈
ℂ ∧ 6 ≠ 0)) |
189 | | divmuldiv 10604 |
. . . . . . . . 9
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧
(𝑁↑2) ≠ 0) ∧ (6
∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) =
(((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6))) |
190 | 183, 184,
186, 188, 189 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) =
(((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6))) |
191 | | divmuldiv 10604 |
. . . . . . . . 9
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ ((6
∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) →
(((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · ((2
· 𝑀) − 1))) /
(6 · (𝑁↑2)))) |
192 | 183, 184,
188, 186, 191 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · ((2
· 𝑀) − 1))) /
(6 · (𝑁↑2)))) |
193 | 181, 190,
192 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) =
(((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))) |
194 | 61 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → π
∈ ℂ) |
195 | 194, 63, 64 | sqdivd 12883 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((π /
𝑁)↑2) = ((π↑2)
/ (𝑁↑2))) |
196 | 195 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) · (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6))) |
197 | 144, 63, 148, 63, 64, 64 | divmuldivd 10721 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁))) |
198 | 63 | sqvald 12867 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁)) |
199 | 198 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
(𝑁↑2)) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) / (𝑁 · 𝑁))) |
200 | 197, 199 | eqtr4d 2647 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) |
201 | 200 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
(𝑁↑2)))) |
202 | 193, 196,
201 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) · (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)))) |
203 | 150, 175,
202 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6))) |
204 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ ↦
Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) |
205 | | eqid 2610 |
. . . . . . 7
⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) |
206 | 3, 204, 205 | basellem5 24611 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6)) |
207 | 206 | oveq2d 6565 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6))) |
208 | 203, 207 | eqtr4d 2647 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2))) |
209 | 22 | recnd 9947 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) |
210 | 1, 35, 209 | fsummulc2 14358 |
. . . 4
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2))) |
211 | 141, 208,
210 | 3eqtrd 2648 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2))) |
212 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2)) |
213 | | eqid 2610 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2)) |
214 | | ovex 6577 |
. . . . . . 7
⊢ (𝑘↑-2) ∈
V |
215 | 212, 213,
214 | fvmpt 6191 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2)) |
216 | 25, 215 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2)) |
217 | | id 22 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ) |
218 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
219 | 217, 218 | syl6eleq 2698 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘1)) |
220 | 216, 219,
58 | fsumser 14308 |
. . . 4
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀)) |
221 | | basel.f |
. . . . 5
⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2))) |
222 | 221 | fveq1i 6104 |
. . . 4
⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀) |
223 | 220, 222 | syl6reqr 2663 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑-2)) |
224 | 91, 211, 223 | 3brtr4d 4615 |
. 2
⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀)) |
225 | 75 | resincld 14712 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) |
226 | | sincosq1sgn 24054 |
. . . . . . . . 9
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(0 < (sin‘((𝑘
· π) / 𝑁)) ∧
0 < (cos‘((𝑘
· π) / 𝑁)))) |
227 | 13, 226 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 <
(cos‘((𝑘 ·
π) / 𝑁)))) |
228 | 227 | simpld 474 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁))) |
229 | 228 | gt0ne0d 10471 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0) |
230 | 225, 229,
21 | reexpclzd 12896 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ) |
231 | 12, 230 | remulcld 9949 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) ∈
ℝ) |
232 | | sinltx 14758 |
. . . . . . . . . 10
⊢ (((𝑘 · π) / 𝑁) ∈ ℝ+
→ (sin‘((𝑘
· π) / 𝑁)) <
((𝑘 · π) / 𝑁)) |
233 | 82, 232 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁)) |
234 | 225, 75, 233 | ltled 10064 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁)) |
235 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
236 | | ltle 10005 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 <
(sin‘((𝑘 ·
π) / 𝑁)) → 0 ≤
(sin‘((𝑘 ·
π) / 𝑁)))) |
237 | 235, 225,
236 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤
(sin‘((𝑘 ·
π) / 𝑁)))) |
238 | 228, 237 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))) |
239 | 225, 75, 238, 83 | le2sqd 12906 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))) |
240 | 234, 239 | mpbid 221 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)) |
241 | 240, 73 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2))) |
242 | 225 | resqcld 12897 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ) |
243 | 242, 12, 46 | lemuldiv2d 11798 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔
((sin‘((𝑘 ·
π) / 𝑁))↑2) ≤
(((π / 𝑁)↑2) /
(𝑘↑-2)))) |
244 | 225, 228 | elrpd 11745 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈
ℝ+) |
245 | | rpexpcl 12741 |
. . . . . . . . 9
⊢
(((sin‘((𝑘
· π) / 𝑁)) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
246 | 244, 18, 245 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
247 | 28, 12, 246 | lemuldivd 11797 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))) |
248 | 243, 247 | bitr3d 269 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))) |
249 | 241, 248 | mpbid 221 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) |
250 | 225 | recnd 9947 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
251 | | expneg 12730 |
. . . . . . . 8
⊢
(((sin‘((𝑘
· π) / 𝑁)) ∈
ℂ ∧ 2 ∈ ℕ0) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) |
252 | 250, 30, 251 | sylancl 693 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))) |
253 | 252 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 /
((sin‘((𝑘 ·
π) / 𝑁))↑2)))) |
254 | 242 | recnd 9947 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ) |
255 | 246 | rpne0d 11753 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0) |
256 | 36, 254, 255 | divrecd 10683 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))) |
257 | 253, 256 | eqtr4d 2647 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) |
258 | 249, 257 | breqtrrd 4611 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
259 | 1, 28, 231, 258 | fsumle 14372 |
. . 3
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
260 | 95 | oveq2d 6565 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁))) |
261 | 97, 260 | oveq12d 6567 |
. . . . 5
⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1
− (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) + 1)))) =
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁)))) |
262 | | basel.k |
. . . . . 6
⊢ 𝐾 = (𝐻 ∘𝑓 ·
((ℕ × {1}) ∘𝑓 + 𝐺)) |
263 | | ovex 6577 |
. . . . . . . . 9
⊢ (1 + (1 /
((2 · 𝑛) + 1)))
∈ V |
264 | 263 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V) |
265 | 103, 119,
121, 123, 125 | offval2 6812 |
. . . . . . . 8
⊢ (⊤
→ ((ℕ × {1}) ∘𝑓 + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2
· 𝑛) +
1))))) |
266 | 103, 105,
264, 128, 265 | offval2 6812 |
. . . . . . 7
⊢ (⊤
→ (𝐻
∘𝑓 · ((ℕ × {1})
∘𝑓 + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) +
1)))))) |
267 | 266 | trud 1484 |
. . . . . 6
⊢ (𝐻 ∘𝑓
· ((ℕ × {1}) ∘𝑓 + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) +
1))))) |
268 | 262, 267 | eqtri 2632 |
. . . . 5
⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) +
1))))) |
269 | | ovex 6577 |
. . . . 5
⊢
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V |
270 | 261, 268,
269 | fvmpt 6191 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1
− (1 / 𝑁))) ·
(1 + (1 / 𝑁)))) |
271 | | peano2cn 10087 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
272 | 63, 271 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
273 | 272, 63, 64 | divcld 10680 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ) |
274 | 143, 145,
273 | mulassd 9942 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2
· 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)))) |
275 | 63, 151, 63, 64 | divdird 10718 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁))) |
276 | 158 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁))) |
277 | 275, 276 | eqtr2d 2645 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (1 + (1 /
𝑁)) = ((𝑁 + 1) / 𝑁)) |
278 | 161, 277 | oveq12d 6567 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2
· 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁))) |
279 | 180 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2)
· ((2 · 𝑀)
· (𝑁 + 1))) / (6
· (𝑁↑2)))) |
280 | 144, 272 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (𝑁 + 1)) ∈
ℂ) |
281 | | divmuldiv 10604 |
. . . . . . . 8
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧
(𝑁↑2) ≠ 0) ∧ (6
∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6))) |
282 | 183, 280,
186, 188, 281 | syl22anc 1319 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6))) |
283 | | divmuldiv 10604 |
. . . . . . . 8
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ ((6 ∈
ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) →
(((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2)))) |
284 | 183, 280,
188, 186, 283 | syl22anc 1319 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2)))) |
285 | 279, 282,
284 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) ·
(((2 · 𝑀) ·
(𝑁 + 1)) / (𝑁↑2)))) |
286 | 75 | recoscld 14713 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ) |
287 | 286 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
288 | 287 | sqcld 12868 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ) |
289 | 254, 288,
254, 255 | divdird 10718 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)) =
((((sin‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)) +
(((cos‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)))) |
290 | 75 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ) |
291 | | sincossq 14745 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · π) / 𝑁) ∈ ℂ →
(((sin‘((𝑘 ·
π) / 𝑁))↑2) +
((cos‘((𝑘 ·
π) / 𝑁))↑2)) =
1) |
292 | 290, 291 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) =
1) |
293 | 292 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)) = (1 /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) |
294 | 254, 255 | dividd 10678 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) =
1) |
295 | 227 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁))) |
296 | 295 | gt0ne0d 10471 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0) |
297 | | tanval 14697 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧
(cos‘((𝑘 ·
π) / 𝑁)) ≠ 0) →
(tan‘((𝑘 ·
π) / 𝑁)) =
((sin‘((𝑘 ·
π) / 𝑁)) /
(cos‘((𝑘 ·
π) / 𝑁)))) |
298 | 290, 296,
297 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))) |
299 | 298 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2)) |
300 | 250, 287,
296 | sqdivd 12883 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) |
301 | 299, 300 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) |
302 | 301 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 /
(((sin‘((𝑘 ·
π) / 𝑁))↑2) /
((cos‘((𝑘 ·
π) / 𝑁))↑2)))) |
303 | | sqne0 12792 |
. . . . . . . . . . . . . . . . 17
⊢
((cos‘((𝑘
· π) / 𝑁)) ∈
ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0)) |
304 | 287, 303 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0)) |
305 | 296, 304 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0) |
306 | 254, 288,
255, 305 | recdivd 10697 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) =
(((cos‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) |
307 | 32, 302, 306 | 3eqtrrd 2649 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) =
((tan‘((𝑘 ·
π) / 𝑁))↑-2)) |
308 | 294, 307 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) +
(((cos‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) = (1
+ ((tan‘((𝑘 ·
π) / 𝑁))↑-2))) |
309 | 289, 293,
308 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 +
((tan‘((𝑘 ·
π) / 𝑁))↑-2))) |
310 | | addcom 10101 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) → (1 +
((tan‘((𝑘 ·
π) / 𝑁))↑-2)) =
(((tan‘((𝑘 ·
π) / 𝑁))↑-2) +
1)) |
311 | 146, 209,
310 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) =
(((tan‘((𝑘 ·
π) / 𝑁))↑-2) +
1)) |
312 | 252, 309,
311 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (((tan‘((𝑘 · π) / 𝑁))↑-2) +
1)) |
313 | 312 | sumeq2dv 14281 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1)) |
314 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ) |
315 | 1, 209, 314 | fsumadd 14317 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1)) |
316 | | fsumconst 14364 |
. . . . . . . . . . . 12
⊢
(((1...𝑀) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((#‘(1...𝑀)) · 1)) |
317 | 1, 146, 316 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)1 = ((#‘(1...𝑀)) · 1)) |
318 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
319 | | hashfz1 12996 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
320 | 318, 319 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ →
(#‘(1...𝑀)) = 𝑀) |
321 | 320 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
((#‘(1...𝑀)) ·
1) = (𝑀 ·
1)) |
322 | | nncn 10905 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
323 | 322 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀) |
324 | 317, 321,
323 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)1 = 𝑀) |
325 | 206, 324 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀)) |
326 | 313, 315,
325 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = ((((2 ·
𝑀) · ((2 ·
𝑀) − 1)) / 6) + 𝑀)) |
327 | | 3cn 10972 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
328 | 327 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 3 ∈
ℂ) |
329 | 144, 148,
328 | adddid 9943 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (((2
· 𝑀) − 1) +
3)) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) + ((2 · 𝑀) · 3))) |
330 | | df-3 10957 |
. . . . . . . . . . . . . . . . 17
⊢ 3 = (2 +
1) |
331 | 330 | oveq1i 6559 |
. . . . . . . . . . . . . . . 16
⊢ (3
− 1) = ((2 + 1) − 1) |
332 | 47, 146 | pncan3oi 10176 |
. . . . . . . . . . . . . . . 16
⊢ ((2 + 1)
− 1) = 2 |
333 | 331, 332,
166 | 3eqtri 2636 |
. . . . . . . . . . . . . . 15
⊢ (3
− 1) = (1 + 1) |
334 | 333 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑀) + (3 −
1)) = ((2 · 𝑀) + (1
+ 1)) |
335 | 144, 151,
328 | subadd23d 10293 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) + 3)
= ((2 · 𝑀) + (3
− 1))) |
336 | 144, 151,
151 | addassd 9941 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) + 1) = ((2
· 𝑀) + (1 +
1))) |
337 | 334, 335,
336 | 3eqtr4a 2670 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) + 3)
= (((2 · 𝑀) + 1) +
1)) |
338 | 3 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1) |
339 | 337, 338 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) + 3)
= (𝑁 + 1)) |
340 | 339 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (((2
· 𝑀) − 1) +
3)) = ((2 · 𝑀)
· (𝑁 +
1))) |
341 | | 2cnd 10970 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 2 ∈
ℂ) |
342 | 341, 322,
328 | mul32d 10125 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · 3) =
((2 · 3) · 𝑀)) |
343 | | 3t2e6 11056 |
. . . . . . . . . . . . . . 15
⊢ (3
· 2) = 6 |
344 | 327, 47 | mulcomi 9925 |
. . . . . . . . . . . . . . 15
⊢ (3
· 2) = (2 · 3) |
345 | 343, 344 | eqtr3i 2634 |
. . . . . . . . . . . . . 14
⊢ 6 = (2
· 3) |
346 | 345 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ (6
· 𝑀) = ((2 ·
3) · 𝑀) |
347 | 342, 346 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · 3) =
(6 · 𝑀)) |
348 | 347 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · ((2
· 𝑀) − 1)) +
((2 · 𝑀) ·
3)) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) + (6 · 𝑀))) |
349 | 329, 340,
348 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 ·
𝑀))) |
350 | 349 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · (𝑁 + 1)) / 6) = ((((2 ·
𝑀) · ((2 ·
𝑀) − 1)) + (6
· 𝑀)) /
6)) |
351 | | mulcl 9899 |
. . . . . . . . . . 11
⊢ ((6
∈ ℂ ∧ 𝑀
∈ ℂ) → (6 · 𝑀) ∈ ℂ) |
352 | 178, 322,
351 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (6
· 𝑀) ∈
ℂ) |
353 | 178 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 6 ∈
ℂ) |
354 | 112 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 6 ≠
0) |
355 | 184, 352,
353, 354 | divdird 10718 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((((2
· 𝑀) · ((2
· 𝑀) − 1)) +
(6 · 𝑀)) / 6) =
((((2 · 𝑀) ·
((2 · 𝑀) − 1))
/ 6) + ((6 · 𝑀) /
6))) |
356 | 322, 353,
354 | divcan3d 10685 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((6
· 𝑀) / 6) = 𝑀) |
357 | 356 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((((2
· 𝑀) · ((2
· 𝑀) − 1)) /
6) + ((6 · 𝑀) / 6))
= ((((2 · 𝑀)
· ((2 · 𝑀)
− 1)) / 6) + 𝑀)) |
358 | 350, 355,
357 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · (𝑁 + 1)) / 6) = ((((2 ·
𝑀) · ((2 ·
𝑀) − 1)) / 6) + 𝑀)) |
359 | 326, 358 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · (𝑁 + 1)) / 6)) |
360 | 195, 359 | oveq12d 6567 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) /
(𝑁↑2)) · (((2
· 𝑀) · (𝑁 + 1)) / 6))) |
361 | 144, 63, 272, 63, 64, 64 | divmuldivd 10721 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁))) |
362 | 198 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁))) |
363 | 361, 362 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) |
364 | 363 | oveq2d 6565 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2
· 𝑀) · (𝑁 + 1)) / (𝑁↑2)))) |
365 | 285, 360,
364 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) /
6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)))) |
366 | 274, 278,
365 | 3eqtr4d 2654 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2))) |
367 | 230 | recnd 9947 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) |
368 | 1, 35, 367 | fsummulc2 14358 |
. . . 4
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
369 | 270, 366,
368 | 3eqtrd 2648 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
370 | 259, 223,
369 | 3brtr4d 4615 |
. 2
⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀)) |
371 | 224, 370 | jca 553 |
1
⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀))) |