Step | Hyp | Ref
| Expression |
1 | | fzfid 13425 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ∈
Fin) |
2 | | pire 25195 |
. . . . . . . 8
⊢ π
∈ ℝ |
3 | | basellem8.n |
. . . . . . . . 9
⊢ 𝑁 = ((2 · 𝑀) + 1) |
4 | | 2nn 11782 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
5 | | nnmulcl 11733 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
6 | 4, 5 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) |
7 | 6 | peano2nnd 11726 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) |
8 | 3, 7 | eqeltrid 2837 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) |
9 | | nndivre 11750 |
. . . . . . . 8
⊢ ((π
∈ ℝ ∧ 𝑁
∈ ℕ) → (π / 𝑁) ∈ ℝ) |
10 | 2, 8, 9 | sylancr 590 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (π /
𝑁) ∈
ℝ) |
11 | 10 | resqcld 13696 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((π /
𝑁)↑2) ∈
ℝ) |
12 | 11 | adantr 484 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ) |
13 | 3 | basellem1 25810 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2))) |
14 | | tanrpcl 25241 |
. . . . . . . 8
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(tan‘((𝑘 ·
π) / 𝑁)) ∈
ℝ+) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈
ℝ+) |
16 | 15 | rpred 12507 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ) |
17 | 15 | rpne0d 12512 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0) |
18 | | 2z 12088 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
19 | | znegcl 12091 |
. . . . . . . 8
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ -2 ∈
ℤ |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈
ℤ) |
22 | 16, 17, 21 | reexpclzd 13695 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ) |
23 | 12, 22 | remulcld 10742 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ∈
ℝ) |
24 | | elfznn 13020 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ) |
25 | 24 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ) |
26 | 25 | nnred 11724 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ) |
27 | 25 | nnne0d 11759 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0) |
28 | 26, 27, 21 | reexpclzd 13695 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ) |
29 | 16 | recnd 10740 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
30 | | 2nn0 11986 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
31 | | expneg 13522 |
. . . . . . . 8
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℂ ∧ 2 ∈ ℕ0) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 /
((tan‘((𝑘 ·
π) / 𝑁))↑2))) |
32 | 29, 30, 31 | sylancl 589 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))) |
33 | 32 | oveq2d 7180 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 /
((tan‘((𝑘 ·
π) / 𝑁))↑2)))) |
34 | 10 | recnd 10740 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (π /
𝑁) ∈
ℂ) |
35 | 34 | sqcld 13593 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((π /
𝑁)↑2) ∈
ℂ) |
36 | 35 | adantr 484 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ) |
37 | | rpexpcl 13533 |
. . . . . . . . . 10
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
38 | 15, 18, 37 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
39 | 38 | rpred 12507 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ) |
40 | 39 | recnd 10740 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ) |
41 | 38 | rpne0d 12512 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0) |
42 | 36, 40, 41 | divrecd 11490 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))) |
43 | 33, 42 | eqtr4d 2776 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2))) |
44 | 25 | nnrpd 12505 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ+) |
45 | | rpexpcl 13533 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ+
∧ -2 ∈ ℤ) → (𝑘↑-2) ∈
ℝ+) |
46 | 44, 20, 45 | sylancl 589 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈
ℝ+) |
47 | | 2cn 11784 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
48 | 47 | negnegi 11027 |
. . . . . . . . . . 11
⊢ --2 =
2 |
49 | 48 | oveq2i 7175 |
. . . . . . . . . 10
⊢ (𝑘↑--2) = (𝑘↑2) |
50 | 25 | nncnd 11725 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ) |
51 | 50, 27, 21 | expnegd 13602 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑--2) = (1 / (𝑘↑-2))) |
52 | 49, 51 | syl5reqr 2788 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑-2)) = (𝑘↑2)) |
53 | 52 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2))) |
54 | | nncn 11717 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
55 | | nnne0 11743 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
56 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → -2 ∈
ℤ) |
57 | 54, 55, 56 | expclzd 13600 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘↑-2) ∈
ℂ) |
58 | 25, 57 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℂ) |
59 | 50, 27, 21 | expne0d 13601 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≠ 0) |
60 | 36, 58, 59 | divrec2d 11491 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2))) |
61 | 2 | recni 10726 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈
ℂ) |
63 | 8 | nncnd 11725 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℂ) |
64 | 8 | nnne0d 11759 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0) |
65 | 63, 64 | jca 515 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
66 | 65 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) |
67 | | divass 11387 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ π
∈ ℂ ∧ (𝑁
∈ ℂ ∧ 𝑁 ≠
0)) → ((𝑘 ·
π) / 𝑁) = (𝑘 · (π / 𝑁))) |
68 | 50, 62, 66, 67 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁))) |
69 | 68 | oveq1d 7179 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2)) |
70 | 34 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ) |
71 | 50, 70 | sqmuld 13607 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2))) |
72 | 69, 71 | eqtrd 2773 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2))) |
73 | 53, 60, 72 | 3eqtr4d 2783 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = (((𝑘 · π) / 𝑁)↑2)) |
74 | | elioore 12844 |
. . . . . . . . . 10
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
((𝑘 · π) / 𝑁) ∈
ℝ) |
75 | 13, 74 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ) |
76 | 75 | resqcld 13696 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ) |
77 | | tangtx 25242 |
. . . . . . . . . 10
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁))) |
78 | 13, 77 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁))) |
79 | | eliooord 12873 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(0 < ((𝑘 · π)
/ 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π /
2))) |
80 | 13, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2))) |
81 | 80 | simpld 498 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁)) |
82 | 75, 81 | elrpd 12504 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈
ℝ+) |
83 | 82 | rpge0d 12511 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁)) |
84 | 15 | rpge0d 12511 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁))) |
85 | 75, 16, 83, 84 | lt2sqd 13704 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))) |
86 | 78, 85 | mpbid 235 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)) |
87 | 76, 39, 86 | ltled 10859 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2)) |
88 | 73, 87 | eqbrtrd 5049 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2)) |
89 | 12, 46, 38, 88 | lediv23d 12575 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑-2)) |
90 | 43, 89 | eqbrtrd 5049 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ (𝑘↑-2)) |
91 | 1, 23, 28, 90 | fsumle 15240 |
. . 3
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑-2)) |
92 | | oveq2 7172 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀)) |
93 | 92 | oveq1d 7179 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1)) |
94 | 93, 3 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁) |
95 | 94 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁)) |
96 | 95 | oveq2d 7180 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁))) |
97 | 96 | oveq2d 7180 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1
− (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1
− (1 / 𝑁)))) |
98 | 95 | oveq2d 7180 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (-2 · (1 / ((2 · 𝑛) + 1))) = (-2 · (1 /
𝑁))) |
99 | 98 | oveq2d 7180 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (1 + (-2 · (1 / ((2 ·
𝑛) + 1)))) = (1 + (-2
· (1 / 𝑁)))) |
100 | 97, 99 | oveq12d 7182 |
. . . . 5
⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1
− (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) + 1))))) =
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁))))) |
101 | | basel.j |
. . . . . 6
⊢ 𝐽 = (𝐻 ∘f · ((ℕ
× {1}) ∘f + ((ℕ × {-2}) ∘f
· 𝐺))) |
102 | | nnex 11715 |
. . . . . . . . 9
⊢ ℕ
∈ V |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ℕ ∈ V) |
104 | | ovexd 7199 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2
· 𝑛) + 1)))) ∈
V) |
105 | | ovexd 7199 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) ∈ V) |
106 | | basel.h |
. . . . . . . . 9
⊢ 𝐻 = ((ℕ ×
{((π↑2) / 6)}) ∘f · ((ℕ × {1})
∘f − 𝐺)) |
107 | 2 | resqcli 13634 |
. . . . . . . . . . . 12
⊢
(π↑2) ∈ ℝ |
108 | | 6re 11799 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
109 | | 6nn 11798 |
. . . . . . . . . . . . 13
⊢ 6 ∈
ℕ |
110 | 109 | nnne0i 11749 |
. . . . . . . . . . . 12
⊢ 6 ≠
0 |
111 | 107, 108,
110 | redivcli 11478 |
. . . . . . . . . . 11
⊢
((π↑2) / 6) ∈ ℝ |
112 | 111 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → ((π↑2) / 6) ∈ ℝ) |
113 | | ovexd 7199 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V) |
114 | | fconstmpt 5579 |
. . . . . . . . . . 11
⊢ (ℕ
× {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) /
6)) |
115 | 114 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) /
6))) |
116 | | 1zzd 12087 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → 1 ∈ ℤ) |
117 | | ovexd 7199 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V) |
118 | | fconstmpt 5579 |
. . . . . . . . . . . 12
⊢ (ℕ
× {1}) = (𝑛 ∈
ℕ ↦ 1) |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1)) |
120 | | basel.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 ·
𝑛) + 1))) |
121 | 120 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2
· 𝑛) +
1)))) |
122 | 103, 116,
117, 119, 121 | offval2 7438 |
. . . . . . . . . 10
⊢ (⊤
→ ((ℕ × {1}) ∘f − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2
· 𝑛) +
1))))) |
123 | 103, 112,
113, 115, 122 | offval2 7438 |
. . . . . . . . 9
⊢ (⊤
→ ((ℕ × {((π↑2) / 6)}) ∘f ·
((ℕ × {1}) ∘f − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))))) |
124 | 106, 123 | syl5eq 2785 |
. . . . . . . 8
⊢ (⊤
→ 𝐻 = (𝑛 ∈ ℕ ↦
(((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))))) |
125 | | ovexd 7199 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (-2 · (1 / ((2 · 𝑛) + 1))) ∈ V) |
126 | 47 | negcli 11025 |
. . . . . . . . . . 11
⊢ -2 ∈
ℂ |
127 | 126 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ ℕ) → -2 ∈ ℂ) |
128 | | fconstmpt 5579 |
. . . . . . . . . . 11
⊢ (ℕ
× {-2}) = (𝑛 ∈
ℕ ↦ -2) |
129 | 128 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2)) |
130 | 103, 127,
117, 129, 121 | offval2 7438 |
. . . . . . . . 9
⊢ (⊤
→ ((ℕ × {-2}) ∘f · 𝐺) = (𝑛 ∈ ℕ ↦ (-2 · (1 / ((2
· 𝑛) +
1))))) |
131 | 103, 116,
125, 119, 130 | offval2 7438 |
. . . . . . . 8
⊢ (⊤
→ ((ℕ × {1}) ∘f + ((ℕ × {-2})
∘f · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + (-2 · (1
/ ((2 · 𝑛) +
1)))))) |
132 | 103, 104,
105, 124, 131 | offval2 7438 |
. . . . . . 7
⊢ (⊤
→ (𝐻
∘f · ((ℕ × {1}) ∘f +
((ℕ × {-2}) ∘f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) +
1))))))) |
133 | 132 | mptru 1549 |
. . . . . 6
⊢ (𝐻 ∘f ·
((ℕ × {1}) ∘f + ((ℕ × {-2})
∘f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) +
1)))))) |
134 | 101, 133 | eqtri 2761 |
. . . . 5
⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2
· 𝑛) +
1)))))) |
135 | | ovex 7197 |
. . . . 5
⊢
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) ∈ V |
136 | 100, 134,
135 | fvmpt 6769 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1
− (1 / 𝑁))) ·
(1 + (-2 · (1 / 𝑁))))) |
137 | 111 | recni 10726 |
. . . . . . . 8
⊢
((π↑2) / 6) ∈ ℂ |
138 | 137 | a1i 11 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
((π↑2) / 6) ∈ ℂ) |
139 | 6 | nncnd 11725 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℂ) |
140 | 139, 63, 64 | divcld 11487 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) / 𝑁) ∈
ℂ) |
141 | | ax-1cn 10666 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
142 | | subcl 10956 |
. . . . . . . . 9
⊢ (((2
· 𝑀) ∈ ℂ
∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈
ℂ) |
143 | 139, 141,
142 | sylancl 589 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℂ) |
144 | 143, 63, 64 | divcld 11487 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) /
𝑁) ∈
ℂ) |
145 | 138, 140,
144 | mulassd 10735 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2
· 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)))) |
146 | | 1cnd 10707 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 1 ∈
ℂ) |
147 | 63, 146, 63, 64 | divsubdird 11526 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁))) |
148 | 3 | oveq1i 7174 |
. . . . . . . . . . 11
⊢ (𝑁 − 1) = (((2 ·
𝑀) + 1) −
1) |
149 | | pncan 10963 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑀) ∈ ℂ
∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀)) |
150 | 139, 141,
149 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) − 1)
= (2 · 𝑀)) |
151 | 148, 150 | syl5eq 2785 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀)) |
152 | 151 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁)) |
153 | 63, 64 | dividd 11485 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1) |
154 | 153 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁))) |
155 | 147, 152,
154 | 3eqtr3rd 2782 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (1
− (1 / 𝑁)) = ((2
· 𝑀) / 𝑁)) |
156 | 155 | oveq2d 7180 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2
· 𝑀) / 𝑁))) |
157 | 126 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → -2 ∈
ℂ) |
158 | 63, 157, 63, 64 | divdird 11525 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + (-2 / 𝑁))) |
159 | | negsub 11005 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑁 + -2) =
(𝑁 −
2)) |
160 | 63, 47, 159 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2)) |
161 | | df-2 11772 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
162 | 3, 161 | oveq12i 7176 |
. . . . . . . . . . 11
⊢ (𝑁 − 2) = (((2 ·
𝑀) + 1) − (1 +
1)) |
163 | 139, 146,
146 | pnpcan2d 11106 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) − (1
+ 1)) = ((2 · 𝑀)
− 1)) |
164 | 162, 163 | syl5eq 2785 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1)) |
165 | 160, 164 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1)) |
166 | 165 | oveq1d 7179 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁)) |
167 | 157, 63, 64 | divrecd 11490 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (-2 /
𝑁) = (-2 · (1 /
𝑁))) |
168 | 153, 167 | oveq12d 7182 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (-2 / 𝑁)) = (1 + (-2 · (1 / 𝑁)))) |
169 | 158, 166,
168 | 3eqtr3rd 2782 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (1 + (-2
· (1 / 𝑁))) = (((2
· 𝑀) − 1) /
𝑁)) |
170 | 156, 169 | oveq12d 7182 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = ((((π↑2) / 6)
· ((2 · 𝑀) /
𝑁)) · (((2 ·
𝑀) − 1) / 𝑁))) |
171 | 8 | nnsqcld 13690 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈
ℕ) |
172 | 171 | nncnd 11725 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈
ℂ) |
173 | | 6cn 11800 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
174 | | mulcom 10694 |
. . . . . . . . . 10
⊢ (((𝑁↑2) ∈ ℂ ∧ 6
∈ ℂ) → ((𝑁↑2) · 6) = (6 · (𝑁↑2))) |
175 | 172, 173,
174 | sylancl 589 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6
· (𝑁↑2))) |
176 | 175 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2)
· ((2 · 𝑀)
· ((2 · 𝑀)
− 1))) / (6 · (𝑁↑2)))) |
177 | 107 | recni 10726 |
. . . . . . . . . 10
⊢
(π↑2) ∈ ℂ |
178 | 177 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(π↑2) ∈ ℂ) |
179 | 139, 143 | mulcld 10732 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ) |
180 | 171 | nnne0d 11759 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠
0) |
181 | 172, 180 | jca 515 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧
(𝑁↑2) ≠
0)) |
182 | 173, 110 | pm3.2i 474 |
. . . . . . . . . 10
⊢ (6 ∈
ℂ ∧ 6 ≠ 0) |
183 | 182 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (6 ∈
ℂ ∧ 6 ≠ 0)) |
184 | | divmuldiv 11411 |
. . . . . . . . 9
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧
(𝑁↑2) ≠ 0) ∧ (6
∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) =
(((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6))) |
185 | 178, 179,
181, 183, 184 | syl22anc 838 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) =
(((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6))) |
186 | | divmuldiv 11411 |
. . . . . . . . 9
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ ((6
∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) →
(((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · ((2
· 𝑀) − 1))) /
(6 · (𝑁↑2)))) |
187 | 178, 179,
183, 181, 186 | syl22anc 838 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · ((2
· 𝑀) − 1))) /
(6 · (𝑁↑2)))) |
188 | 176, 185,
187 | 3eqtr4d 2783 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) =
(((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))) |
189 | 61 | a1i 11 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → π
∈ ℂ) |
190 | 189, 63, 64 | sqdivd 13608 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((π /
𝑁)↑2) = ((π↑2)
/ (𝑁↑2))) |
191 | 190 | oveq1d 7179 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) · (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6))) |
192 | 139, 63, 143, 63, 64, 64 | divmuldivd 11528 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁))) |
193 | 63 | sqvald 13592 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁)) |
194 | 193 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
(𝑁↑2)) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) / (𝑁 · 𝑁))) |
195 | 192, 194 | eqtr4d 2776 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) |
196 | 195 | oveq2d 7180 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
(𝑁↑2)))) |
197 | 188, 191,
196 | 3eqtr4d 2783 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) · (((2
· 𝑀) · ((2
· 𝑀) − 1)) /
6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)))) |
198 | 145, 170,
197 | 3eqtr4d 2783 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6))) |
199 | | eqid 2738 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ ↦
Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) |
200 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) |
201 | 3, 199, 200 | basellem5 25814 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6)) |
202 | 201 | oveq2d 7180 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6))) |
203 | 198, 202 | eqtr4d 2776 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2))) |
204 | 22 | recnd 10740 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) |
205 | 1, 35, 204 | fsummulc2 15225 |
. . . 4
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2))) |
206 | 136, 203,
205 | 3eqtrd 2777 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2))) |
207 | | basel.f |
. . . . 5
⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2))) |
208 | 207 | fveq1i 6669 |
. . . 4
⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀) |
209 | | oveq1 7171 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2)) |
210 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2)) |
211 | | ovex 7197 |
. . . . . . 7
⊢ (𝑘↑-2) ∈
V |
212 | 209, 210,
211 | fvmpt 6769 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2)) |
213 | 25, 212 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2)) |
214 | | id 22 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ) |
215 | | nnuz 12356 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
216 | 214, 215 | eleqtrdi 2843 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘1)) |
217 | 213, 216,
58 | fsumser 15173 |
. . . 4
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀)) |
218 | 208, 217 | eqtr4id 2792 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑-2)) |
219 | 91, 206, 218 | 3brtr4d 5059 |
. 2
⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀)) |
220 | 75 | resincld 15581 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) |
221 | | sincosq1sgn 25235 |
. . . . . . . . 9
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(0 < (sin‘((𝑘
· π) / 𝑁)) ∧
0 < (cos‘((𝑘
· π) / 𝑁)))) |
222 | 13, 221 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 <
(cos‘((𝑘 ·
π) / 𝑁)))) |
223 | 222 | simpld 498 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁))) |
224 | 223 | gt0ne0d 11275 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0) |
225 | 220, 224,
21 | reexpclzd 13695 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ) |
226 | 12, 225 | remulcld 10742 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) ∈
ℝ) |
227 | | sinltx 15627 |
. . . . . . . . . 10
⊢ (((𝑘 · π) / 𝑁) ∈ ℝ+
→ (sin‘((𝑘
· π) / 𝑁)) <
((𝑘 · π) / 𝑁)) |
228 | 82, 227 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁)) |
229 | 220, 75, 228 | ltled 10859 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁)) |
230 | | 0re 10714 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
231 | | ltle 10800 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 <
(sin‘((𝑘 ·
π) / 𝑁)) → 0 ≤
(sin‘((𝑘 ·
π) / 𝑁)))) |
232 | 230, 220,
231 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤
(sin‘((𝑘 ·
π) / 𝑁)))) |
233 | 223, 232 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))) |
234 | 220, 75, 233, 83 | le2sqd 13705 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))) |
235 | 229, 234 | mpbid 235 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)) |
236 | 235, 73 | breqtrrd 5055 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2))) |
237 | 220 | resqcld 13696 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ) |
238 | 237, 12, 46 | lemuldiv2d 12557 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔
((sin‘((𝑘 ·
π) / 𝑁))↑2) ≤
(((π / 𝑁)↑2) /
(𝑘↑-2)))) |
239 | 220, 223 | elrpd 12504 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈
ℝ+) |
240 | | rpexpcl 13533 |
. . . . . . . . 9
⊢
(((sin‘((𝑘
· π) / 𝑁)) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
241 | 239, 18, 240 | sylancl 589 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
242 | 28, 12, 241 | lemuldivd 12556 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))) |
243 | 238, 242 | bitr3d 284 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))) |
244 | 236, 243 | mpbid 235 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) |
245 | 220 | recnd 10740 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
246 | | expneg 13522 |
. . . . . . . 8
⊢
(((sin‘((𝑘
· π) / 𝑁)) ∈
ℂ ∧ 2 ∈ ℕ0) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) |
247 | 245, 30, 246 | sylancl 589 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))) |
248 | 247 | oveq2d 7180 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 /
((sin‘((𝑘 ·
π) / 𝑁))↑2)))) |
249 | 237 | recnd 10740 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ) |
250 | 241 | rpne0d 12512 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0) |
251 | 36, 249, 250 | divrecd 11490 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))) |
252 | 248, 251 | eqtr4d 2776 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) |
253 | 244, 252 | breqtrrd 5055 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
254 | 1, 28, 226, 253 | fsumle 15240 |
. . 3
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
255 | 95 | oveq2d 7180 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁))) |
256 | 97, 255 | oveq12d 7182 |
. . . . 5
⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1
− (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) + 1)))) =
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁)))) |
257 | | basel.k |
. . . . . 6
⊢ 𝐾 = (𝐻 ∘f · ((ℕ
× {1}) ∘f + 𝐺)) |
258 | | ovexd 7199 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V) |
259 | 103, 116,
117, 119, 121 | offval2 7438 |
. . . . . . . 8
⊢ (⊤
→ ((ℕ × {1}) ∘f + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2
· 𝑛) +
1))))) |
260 | 103, 104,
258, 124, 259 | offval2 7438 |
. . . . . . 7
⊢ (⊤
→ (𝐻
∘f · ((ℕ × {1}) ∘f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) +
1)))))) |
261 | 260 | mptru 1549 |
. . . . . 6
⊢ (𝐻 ∘f ·
((ℕ × {1}) ∘f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) +
1))))) |
262 | 257, 261 | eqtri 2761 |
. . . . 5
⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6)
· (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 ·
𝑛) +
1))))) |
263 | | ovex 7197 |
. . . . 5
⊢
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V |
264 | 256, 262,
263 | fvmpt 6769 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1
− (1 / 𝑁))) ·
(1 + (1 / 𝑁)))) |
265 | | peano2cn 10883 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈
ℂ) |
266 | 63, 265 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈
ℂ) |
267 | 266, 63, 64 | divcld 11487 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ) |
268 | 138, 140,
267 | mulassd 10735 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2
· 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)))) |
269 | 63, 146, 63, 64 | divdird 11525 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁))) |
270 | 153 | oveq1d 7179 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁))) |
271 | 269, 270 | eqtr2d 2774 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (1 + (1 /
𝑁)) = ((𝑁 + 1) / 𝑁)) |
272 | 156, 271 | oveq12d 7182 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2
· 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁))) |
273 | 175 | oveq2d 7180 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2)
· ((2 · 𝑀)
· (𝑁 + 1))) / (6
· (𝑁↑2)))) |
274 | 139, 266 | mulcld 10732 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (𝑁 + 1)) ∈
ℂ) |
275 | | divmuldiv 11411 |
. . . . . . . 8
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧
(𝑁↑2) ≠ 0) ∧ (6
∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6))) |
276 | 178, 274,
181, 183, 275 | syl22anc 838 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6))) |
277 | | divmuldiv 11411 |
. . . . . . . 8
⊢
((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ ((6 ∈
ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) →
(((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2)))) |
278 | 178, 274,
183, 181, 277 | syl22anc 838 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2
· 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2)))) |
279 | 273, 276,
278 | 3eqtr4d 2783 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) ·
(((2 · 𝑀) ·
(𝑁 + 1)) / (𝑁↑2)))) |
280 | 75 | recoscld 15582 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ) |
281 | 280 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
282 | 281 | sqcld 13593 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ) |
283 | 249, 282,
249, 250 | divdird 11525 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)) =
((((sin‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)) +
(((cos‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)))) |
284 | 75 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ) |
285 | | sincossq 15614 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · π) / 𝑁) ∈ ℂ →
(((sin‘((𝑘 ·
π) / 𝑁))↑2) +
((cos‘((𝑘 ·
π) / 𝑁))↑2)) =
1) |
286 | 284, 285 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) =
1) |
287 | 286 | oveq1d 7179 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) /
((sin‘((𝑘 ·
π) / 𝑁))↑2)) = (1 /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) |
288 | 249, 250 | dividd 11485 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) =
1) |
289 | 222 | simprd 499 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁))) |
290 | 289 | gt0ne0d 11275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0) |
291 | | tanval 15566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧
(cos‘((𝑘 ·
π) / 𝑁)) ≠ 0) →
(tan‘((𝑘 ·
π) / 𝑁)) =
((sin‘((𝑘 ·
π) / 𝑁)) /
(cos‘((𝑘 ·
π) / 𝑁)))) |
292 | 284, 290,
291 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))) |
293 | 292 | oveq1d 7179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2)) |
294 | 245, 281,
290 | sqdivd 13608 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) |
295 | 293, 294 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) |
296 | 295 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 /
(((sin‘((𝑘 ·
π) / 𝑁))↑2) /
((cos‘((𝑘 ·
π) / 𝑁))↑2)))) |
297 | | sqne0 13574 |
. . . . . . . . . . . . . . . . 17
⊢
((cos‘((𝑘
· π) / 𝑁)) ∈
ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0)) |
298 | 281, 297 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0)) |
299 | 290, 298 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0) |
300 | 249, 282,
250, 299 | recdivd 11504 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) =
(((cos‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) |
301 | 32, 296, 300 | 3eqtrrd 2778 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) =
((tan‘((𝑘 ·
π) / 𝑁))↑-2)) |
302 | 288, 301 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) +
(((cos‘((𝑘 ·
π) / 𝑁))↑2) /
((sin‘((𝑘 ·
π) / 𝑁))↑2))) = (1
+ ((tan‘((𝑘 ·
π) / 𝑁))↑-2))) |
303 | 283, 287,
302 | 3eqtr3d 2781 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 +
((tan‘((𝑘 ·
π) / 𝑁))↑-2))) |
304 | | addcom 10897 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) → (1 +
((tan‘((𝑘 ·
π) / 𝑁))↑-2)) =
(((tan‘((𝑘 ·
π) / 𝑁))↑-2) +
1)) |
305 | 141, 204,
304 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) =
(((tan‘((𝑘 ·
π) / 𝑁))↑-2) +
1)) |
306 | 247, 303,
305 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (((tan‘((𝑘 · π) / 𝑁))↑-2) +
1)) |
307 | 306 | sumeq2dv 15146 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1)) |
308 | | 1cnd 10707 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ) |
309 | 1, 204, 308 | fsumadd 15182 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1)) |
310 | | fsumconst 15231 |
. . . . . . . . . . . 12
⊢
(((1...𝑀) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1)) |
311 | 1, 141, 310 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1)) |
312 | | nnnn0 11976 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
313 | | hashfz1 13791 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
314 | 312, 313 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ →
(♯‘(1...𝑀)) =
𝑀) |
315 | 314 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ →
((♯‘(1...𝑀))
· 1) = (𝑀 ·
1)) |
316 | | nncn 11717 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
317 | 316 | mulid1d 10729 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀) |
318 | 311, 315,
317 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)1 = 𝑀) |
319 | 201, 318 | oveq12d 7182 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀)) |
320 | 307, 309,
319 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = ((((2 ·
𝑀) · ((2 ·
𝑀) − 1)) / 6) + 𝑀)) |
321 | | 3cn 11790 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
322 | 321 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 3 ∈
ℂ) |
323 | 139, 143,
322 | adddid 10736 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (((2
· 𝑀) − 1) +
3)) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) + ((2 · 𝑀) · 3))) |
324 | | df-3 11773 |
. . . . . . . . . . . . . . . . 17
⊢ 3 = (2 +
1) |
325 | 324 | oveq1i 7174 |
. . . . . . . . . . . . . . . 16
⊢ (3
− 1) = ((2 + 1) − 1) |
326 | 47, 141 | pncan3oi 10973 |
. . . . . . . . . . . . . . . 16
⊢ ((2 + 1)
− 1) = 2 |
327 | 325, 326,
161 | 3eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ (3
− 1) = (1 + 1) |
328 | 327 | oveq2i 7175 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑀) + (3 −
1)) = ((2 · 𝑀) + (1
+ 1)) |
329 | 139, 146,
322 | subadd23d 11090 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) + 3)
= ((2 · 𝑀) + (3
− 1))) |
330 | 139, 146,
146 | addassd 10734 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) + 1) = ((2
· 𝑀) + (1 +
1))) |
331 | 328, 329,
330 | 3eqtr4a 2799 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) + 3)
= (((2 · 𝑀) + 1) +
1)) |
332 | 3 | oveq1i 7174 |
. . . . . . . . . . . . 13
⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1) |
333 | 331, 332 | eqtr4di 2791 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) + 3)
= (𝑁 + 1)) |
334 | 333 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (((2
· 𝑀) − 1) +
3)) = ((2 · 𝑀)
· (𝑁 +
1))) |
335 | | 2cnd 11787 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 2 ∈
ℂ) |
336 | 335, 316,
322 | mul32d 10921 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · 3) =
((2 · 3) · 𝑀)) |
337 | | 3t2e6 11875 |
. . . . . . . . . . . . . . 15
⊢ (3
· 2) = 6 |
338 | 321, 47 | mulcomi 10720 |
. . . . . . . . . . . . . . 15
⊢ (3
· 2) = (2 · 3) |
339 | 337, 338 | eqtr3i 2763 |
. . . . . . . . . . . . . 14
⊢ 6 = (2
· 3) |
340 | 339 | oveq1i 7174 |
. . . . . . . . . . . . 13
⊢ (6
· 𝑀) = ((2 ·
3) · 𝑀) |
341 | 336, 340 | eqtr4di 2791 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · 3) =
(6 · 𝑀)) |
342 | 341 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · ((2
· 𝑀) − 1)) +
((2 · 𝑀) ·
3)) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) + (6 · 𝑀))) |
343 | 323, 334,
342 | 3eqtr3d 2781 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 ·
𝑀))) |
344 | 343 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · (𝑁 + 1)) / 6) = ((((2 ·
𝑀) · ((2 ·
𝑀) − 1)) + (6
· 𝑀)) /
6)) |
345 | | mulcl 10692 |
. . . . . . . . . . 11
⊢ ((6
∈ ℂ ∧ 𝑀
∈ ℂ) → (6 · 𝑀) ∈ ℂ) |
346 | 173, 316,
345 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (6
· 𝑀) ∈
ℂ) |
347 | 173 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 6 ∈
ℂ) |
348 | 110 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 6 ≠
0) |
349 | 179, 346,
347, 348 | divdird 11525 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((((2
· 𝑀) · ((2
· 𝑀) − 1)) +
(6 · 𝑀)) / 6) =
((((2 · 𝑀) ·
((2 · 𝑀) − 1))
/ 6) + ((6 · 𝑀) /
6))) |
350 | 316, 347,
348 | divcan3d 11492 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((6
· 𝑀) / 6) = 𝑀) |
351 | 350 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((((2
· 𝑀) · ((2
· 𝑀) − 1)) /
6) + ((6 · 𝑀) / 6))
= ((((2 · 𝑀)
· ((2 · 𝑀)
− 1)) / 6) + 𝑀)) |
352 | 344, 349,
351 | 3eqtrd 2777 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · (𝑁 + 1)) / 6) = ((((2 ·
𝑀) · ((2 ·
𝑀) − 1)) / 6) + 𝑀)) |
353 | 320, 352 | eqtr4d 2776 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · (𝑁 + 1)) / 6)) |
354 | 190, 353 | oveq12d 7182 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) /
(𝑁↑2)) · (((2
· 𝑀) · (𝑁 + 1)) / 6))) |
355 | 139, 63, 266, 63, 64, 64 | divmuldivd 11528 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁))) |
356 | 193 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁))) |
357 | 355, 356 | eqtr4d 2776 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) |
358 | 357 | oveq2d 7180 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2
· 𝑀) · (𝑁 + 1)) / (𝑁↑2)))) |
359 | 279, 354,
358 | 3eqtr4d 2783 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) /
6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)))) |
360 | 268, 272,
359 | 3eqtr4d 2783 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2))) |
361 | 225 | recnd 10740 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) |
362 | 1, 35, 361 | fsummulc2 15225 |
. . . 4
⊢ (𝑀 ∈ ℕ → (((π /
𝑁)↑2) ·
Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
363 | 264, 360,
362 | 3eqtrd 2777 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2))) |
364 | 254, 218,
363 | 3brtr4d 5059 |
. 2
⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀)) |
365 | 219, 364 | jca 515 |
1
⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀))) |