Step | Hyp | Ref
| Expression |
1 | | basel.n |
. . . . . . . . 9
⊢ 𝑁 = ((2 · 𝑀) + 1) |
2 | 1 | basellem1 24807 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((𝑛 · π) / 𝑁) ∈ (0(,)(π / 2))) |
3 | | tanrpcl 24256 |
. . . . . . . 8
⊢ (((𝑛 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(tan‘((𝑛 ·
π) / 𝑁)) ∈
ℝ+) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (tan‘((𝑛 · π) / 𝑁)) ∈
ℝ+) |
5 | | 2z 11409 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
6 | | znegcl 11412 |
. . . . . . . 8
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ -2 ∈
ℤ |
8 | | rpexpcl 12879 |
. . . . . . 7
⊢
(((tan‘((𝑛
· π) / 𝑁)) ∈
ℝ+ ∧ -2 ∈ ℤ) → ((tan‘((𝑛 · π) / 𝑁))↑-2) ∈
ℝ+) |
9 | 4, 7, 8 | sylancl 694 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((tan‘((𝑛 · π) / 𝑁))↑-2) ∈
ℝ+) |
10 | 9 | rpcnd 11874 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((tan‘((𝑛 · π) / 𝑁))↑-2) ∈ ℂ) |
11 | | basel.p |
. . . . . . . 8
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) |
12 | 1, 11 | basellem3 24809 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ ((𝑛 · π) / 𝑁) ∈ (0(,)(π / 2)))
→ (𝑃‘((tan‘((𝑛 · π) / 𝑁))↑-2)) = ((sin‘(𝑁 · ((𝑛 · π) / 𝑁))) / ((sin‘((𝑛 · π) / 𝑁))↑𝑁))) |
13 | 2, 12 | syldan 487 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (𝑃‘((tan‘((𝑛 · π) / 𝑁))↑-2)) = ((sin‘(𝑁 · ((𝑛 · π) / 𝑁))) / ((sin‘((𝑛 · π) / 𝑁))↑𝑁))) |
14 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℤ) |
15 | 14 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑛 ∈ ℤ) |
16 | 15 | zred 11482 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑛 ∈ ℝ) |
17 | | pire 24210 |
. . . . . . . . . . . 12
⊢ π
∈ ℝ |
18 | | remulcl 10021 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℝ ∧ π
∈ ℝ) → (𝑛
· π) ∈ ℝ) |
19 | 16, 17, 18 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (𝑛 · π) ∈
ℝ) |
20 | 19 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (𝑛 · π) ∈
ℂ) |
21 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
22 | | nnmulcl 11043 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
23 | 21, 22 | mpan 706 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) |
24 | 23 | peano2nnd 11037 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) |
25 | 1, 24 | syl5eqel 2705 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) |
26 | 25 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑁 ∈ ℕ) |
27 | 26 | nncnd 11036 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑁 ∈ ℂ) |
28 | 26 | nnne0d 11065 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑁 ≠ 0) |
29 | 20, 27, 28 | divcan2d 10803 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (𝑁 · ((𝑛 · π) / 𝑁)) = (𝑛 · π)) |
30 | 29 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (sin‘(𝑁 · ((𝑛 · π) / 𝑁))) = (sin‘(𝑛 · π))) |
31 | | sinkpi 24271 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ →
(sin‘(𝑛 ·
π)) = 0) |
32 | 15, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (sin‘(𝑛 · π)) = 0) |
33 | 30, 32 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (sin‘(𝑁 · ((𝑛 · π) / 𝑁))) = 0) |
34 | 33 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((sin‘(𝑁 · ((𝑛 · π) / 𝑁))) / ((sin‘((𝑛 · π) / 𝑁))↑𝑁)) = (0 / ((sin‘((𝑛 · π) / 𝑁))↑𝑁))) |
35 | 19, 26 | nndivred 11069 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((𝑛 · π) / 𝑁) ∈ ℝ) |
36 | 35 | resincld 14873 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (sin‘((𝑛 · π) / 𝑁)) ∈ ℝ) |
37 | 36 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (sin‘((𝑛 · π) / 𝑁)) ∈ ℂ) |
38 | 26 | nnnn0d 11351 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑁 ∈
ℕ0) |
39 | 37, 38 | expcld 13008 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((sin‘((𝑛 · π) / 𝑁))↑𝑁) ∈ ℂ) |
40 | | sincosq1sgn 24250 |
. . . . . . . . . . 11
⊢ (((𝑛 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(0 < (sin‘((𝑛
· π) / 𝑁)) ∧
0 < (cos‘((𝑛
· π) / 𝑁)))) |
41 | 2, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (0 < (sin‘((𝑛 · π) / 𝑁)) ∧ 0 <
(cos‘((𝑛 ·
π) / 𝑁)))) |
42 | 41 | simpld 475 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 0 < (sin‘((𝑛 · π) / 𝑁))) |
43 | 42 | gt0ne0d 10592 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (sin‘((𝑛 · π) / 𝑁)) ≠ 0) |
44 | 26 | nnzd 11481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑁 ∈ ℤ) |
45 | 37, 43, 44 | expne0d 13014 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((sin‘((𝑛 · π) / 𝑁))↑𝑁) ≠ 0) |
46 | 39, 45 | div0d 10800 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (0 / ((sin‘((𝑛 · π) / 𝑁))↑𝑁)) = 0) |
47 | 13, 34, 46 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (𝑃‘((tan‘((𝑛 · π) / 𝑁))↑-2)) = 0) |
48 | 1, 11 | basellem2 24808 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (Poly‘ℂ)
∧ (deg‘𝑃) = 𝑀 ∧ (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))))) |
49 | 48 | simp1d 1073 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑃 ∈
(Poly‘ℂ)) |
50 | | plyf 23954 |
. . . . . . . 8
⊢ (𝑃 ∈ (Poly‘ℂ)
→ 𝑃:ℂ⟶ℂ) |
51 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑃:ℂ⟶ℂ →
𝑃 Fn
ℂ) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑃 Fn ℂ) |
53 | 52 | adantr 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → 𝑃 Fn ℂ) |
54 | | fniniseg 6338 |
. . . . . 6
⊢ (𝑃 Fn ℂ →
(((tan‘((𝑛 ·
π) / 𝑁))↑-2) ∈
(◡𝑃 “ {0}) ↔ (((tan‘((𝑛 · π) / 𝑁))↑-2) ∈ ℂ ∧
(𝑃‘((tan‘((𝑛 · π) / 𝑁))↑-2)) = 0))) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → (((tan‘((𝑛 · π) / 𝑁))↑-2) ∈ (◡𝑃 “ {0}) ↔ (((tan‘((𝑛 · π) / 𝑁))↑-2) ∈ ℂ ∧
(𝑃‘((tan‘((𝑛 · π) / 𝑁))↑-2)) = 0))) |
56 | 10, 47, 55 | mpbir2and 957 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((tan‘((𝑛 · π) / 𝑁))↑-2) ∈ (◡𝑃 “ {0})) |
57 | | basel.t |
. . . 4
⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) |
58 | 56, 57 | fmptd 6385 |
. . 3
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)⟶(◡𝑃 “ {0})) |
59 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑚 → (𝑇‘𝑘) = (𝑇‘𝑚)) |
60 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑥 → (𝑇‘𝑘) = (𝑇‘𝑥)) |
61 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑦 → (𝑇‘𝑘) = (𝑇‘𝑦)) |
62 | 14 | zred 11482 |
. . . . . . 7
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℝ) |
63 | 62 | ssriv 3607 |
. . . . . 6
⊢
(1...𝑀) ⊆
ℝ |
64 | 9 | rpred 11872 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ (1...𝑀)) → ((tan‘((𝑛 · π) / 𝑁))↑-2) ∈ ℝ) |
65 | 64, 57 | fmptd 6385 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)⟶ℝ) |
66 | 65 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑇‘𝑘) ∈ ℝ) |
67 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 𝑘 < 𝑚) |
68 | 63 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℝ) |
69 | 68 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 𝑘 ∈ ℝ) |
70 | 63 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℝ) |
71 | 70 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 𝑚 ∈ ℝ) |
72 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → π ∈
ℝ) |
73 | | pipos 24212 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
π |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 0 < π) |
75 | | ltmul1 10873 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ (π
∈ ℝ ∧ 0 < π)) → (𝑘 < 𝑚 ↔ (𝑘 · π) < (𝑚 · π))) |
76 | 69, 71, 72, 74, 75 | syl112anc 1330 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑘 < 𝑚 ↔ (𝑘 · π) < (𝑚 · π))) |
77 | 67, 76 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑘 · π) < (𝑚 · π)) |
78 | | remulcl 10021 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℝ ∧ π
∈ ℝ) → (𝑘
· π) ∈ ℝ) |
79 | 69, 17, 78 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑘 · π) ∈
ℝ) |
80 | | remulcl 10021 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℝ ∧ π
∈ ℝ) → (𝑚
· π) ∈ ℝ) |
81 | 71, 17, 80 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑚 · π) ∈
ℝ) |
82 | 25 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 𝑁 ∈ ℕ) |
83 | 82 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 𝑁 ∈ ℝ) |
84 | 82 | nngt0d 11064 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → 0 < 𝑁) |
85 | | ltdiv1 10887 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 · π) ∈ ℝ
∧ (𝑚 · π)
∈ ℝ ∧ (𝑁
∈ ℝ ∧ 0 < 𝑁)) → ((𝑘 · π) < (𝑚 · π) ↔ ((𝑘 · π) / 𝑁) < ((𝑚 · π) / 𝑁))) |
86 | 79, 81, 83, 84, 85 | syl112anc 1330 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((𝑘 · π) < (𝑚 · π) ↔ ((𝑘 · π) / 𝑁) < ((𝑚 · π) / 𝑁))) |
87 | 77, 86 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((𝑘 · π) / 𝑁) < ((𝑚 · π) / 𝑁)) |
88 | | neghalfpirx 24218 |
. . . . . . . . . . . . . . 15
⊢ -(π /
2) ∈ ℝ* |
89 | | pirp 24213 |
. . . . . . . . . . . . . . . . 17
⊢ π
∈ ℝ+ |
90 | | rphalfcl 11858 |
. . . . . . . . . . . . . . . . 17
⊢ (π
∈ ℝ+ → (π / 2) ∈
ℝ+) |
91 | | rpge0 11845 |
. . . . . . . . . . . . . . . . 17
⊢ ((π /
2) ∈ ℝ+ → 0 ≤ (π / 2)) |
92 | 89, 90, 91 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
(π / 2) |
93 | | halfpire 24216 |
. . . . . . . . . . . . . . . . 17
⊢ (π /
2) ∈ ℝ |
94 | | le0neg2 10537 |
. . . . . . . . . . . . . . . . 17
⊢ ((π /
2) ∈ ℝ → (0 ≤ (π / 2) ↔ -(π / 2) ≤
0)) |
95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (0 ≤
(π / 2) ↔ -(π / 2) ≤ 0) |
96 | 92, 95 | mpbi 220 |
. . . . . . . . . . . . . . 15
⊢ -(π /
2) ≤ 0 |
97 | | iooss1 12210 |
. . . . . . . . . . . . . . 15
⊢ ((-(π
/ 2) ∈ ℝ* ∧ -(π / 2) ≤ 0) → (0(,)(π /
2)) ⊆ (-(π / 2)(,)(π / 2))) |
98 | 88, 96, 97 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢
(0(,)(π / 2)) ⊆ (-(π / 2)(,)(π / 2)) |
99 | 1 | basellem1 24807 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2))) |
100 | 99 | ad2ant2r 783 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2))) |
101 | 98, 100 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((𝑘 · π) / 𝑁) ∈ (-(π / 2)(,)(π /
2))) |
102 | 1 | basellem1 24807 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑚 ∈ (1...𝑀)) → ((𝑚 · π) / 𝑁) ∈ (0(,)(π / 2))) |
103 | 102 | ad2ant2rl 785 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((𝑚 · π) / 𝑁) ∈ (0(,)(π / 2))) |
104 | 98, 103 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((𝑚 · π) / 𝑁) ∈ (-(π / 2)(,)(π /
2))) |
105 | | tanord 24284 |
. . . . . . . . . . . . 13
⊢ ((((𝑘 · π) / 𝑁) ∈ (-(π / 2)(,)(π /
2)) ∧ ((𝑚 ·
π) / 𝑁) ∈ (-(π /
2)(,)(π / 2))) → (((𝑘 · π) / 𝑁) < ((𝑚 · π) / 𝑁) ↔ (tan‘((𝑘 · π) / 𝑁)) < (tan‘((𝑚 · π) / 𝑁)))) |
106 | 101, 104,
105 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (((𝑘 · π) / 𝑁) < ((𝑚 · π) / 𝑁) ↔ (tan‘((𝑘 · π) / 𝑁)) < (tan‘((𝑚 · π) / 𝑁)))) |
107 | 87, 106 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (tan‘((𝑘 · π) / 𝑁)) < (tan‘((𝑚 · π) / 𝑁))) |
108 | | tanrpcl 24256 |
. . . . . . . . . . . . 13
⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(tan‘((𝑘 ·
π) / 𝑁)) ∈
ℝ+) |
109 | 100, 108 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (tan‘((𝑘 · π) / 𝑁)) ∈
ℝ+) |
110 | | tanrpcl 24256 |
. . . . . . . . . . . . 13
⊢ (((𝑚 · π) / 𝑁) ∈ (0(,)(π / 2)) →
(tan‘((𝑚 ·
π) / 𝑁)) ∈
ℝ+) |
111 | 103, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (tan‘((𝑚 · π) / 𝑁)) ∈
ℝ+) |
112 | | rprege0 11847 |
. . . . . . . . . . . . 13
⊢
((tan‘((𝑘
· π) / 𝑁)) ∈
ℝ+ → ((tan‘((𝑘 · π) / 𝑁)) ∈ ℝ ∧ 0 ≤
(tan‘((𝑘 ·
π) / 𝑁)))) |
113 | | rprege0 11847 |
. . . . . . . . . . . . 13
⊢
((tan‘((𝑚
· π) / 𝑁)) ∈
ℝ+ → ((tan‘((𝑚 · π) / 𝑁)) ∈ ℝ ∧ 0 ≤
(tan‘((𝑚 ·
π) / 𝑁)))) |
114 | | lt2sq 12937 |
. . . . . . . . . . . . 13
⊢
((((tan‘((𝑘
· π) / 𝑁)) ∈
ℝ ∧ 0 ≤ (tan‘((𝑘 · π) / 𝑁))) ∧ ((tan‘((𝑚 · π) / 𝑁)) ∈ ℝ ∧ 0 ≤
(tan‘((𝑚 ·
π) / 𝑁)))) →
((tan‘((𝑘 ·
π) / 𝑁)) <
(tan‘((𝑚 ·
π) / 𝑁)) ↔
((tan‘((𝑘 ·
π) / 𝑁))↑2) <
((tan‘((𝑚 ·
π) / 𝑁))↑2))) |
115 | 112, 113,
114 | syl2an 494 |
. . . . . . . . . . . 12
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℝ+ ∧ (tan‘((𝑚 · π) / 𝑁)) ∈ ℝ+) →
((tan‘((𝑘 ·
π) / 𝑁)) <
(tan‘((𝑚 ·
π) / 𝑁)) ↔
((tan‘((𝑘 ·
π) / 𝑁))↑2) <
((tan‘((𝑚 ·
π) / 𝑁))↑2))) |
116 | 109, 111,
115 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((tan‘((𝑘 · π) / 𝑁)) < (tan‘((𝑚 · π) / 𝑁)) ↔ ((tan‘((𝑘 · π) / 𝑁))↑2) < ((tan‘((𝑚 · π) / 𝑁))↑2))) |
117 | 107, 116 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((tan‘((𝑘 · π) / 𝑁))↑2) < ((tan‘((𝑚 · π) / 𝑁))↑2)) |
118 | | rpexpcl 12879 |
. . . . . . . . . . . 12
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
119 | 109, 5, 118 | sylancl 694 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈
ℝ+) |
120 | | rpexpcl 12879 |
. . . . . . . . . . . 12
⊢
(((tan‘((𝑚
· π) / 𝑁)) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((tan‘((𝑚 · π) / 𝑁))↑2) ∈
ℝ+) |
121 | 111, 5, 120 | sylancl 694 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((tan‘((𝑚 · π) / 𝑁))↑2) ∈
ℝ+) |
122 | 119, 121 | ltrecd 11890 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (((tan‘((𝑘 · π) / 𝑁))↑2) < ((tan‘((𝑚 · π) / 𝑁))↑2) ↔ (1 /
((tan‘((𝑚 ·
π) / 𝑁))↑2)) <
(1 / ((tan‘((𝑘
· π) / 𝑁))↑2)))) |
123 | 117, 122 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (1 / ((tan‘((𝑚 · π) / 𝑁))↑2)) < (1 /
((tan‘((𝑘 ·
π) / 𝑁))↑2))) |
124 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑛 · π) = (𝑚 · π)) |
125 | 124 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝑛 · π) / 𝑁) = ((𝑚 · π) / 𝑁)) |
126 | 125 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (tan‘((𝑛 · π) / 𝑁)) = (tan‘((𝑚 · π) / 𝑁))) |
127 | 126 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((tan‘((𝑛 · π) / 𝑁))↑-2) = ((tan‘((𝑚 · π) / 𝑁))↑-2)) |
128 | | ovex 6678 |
. . . . . . . . . . . 12
⊢
((tan‘((𝑚
· π) / 𝑁))↑-2) ∈ V |
129 | 127, 57, 128 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...𝑀) → (𝑇‘𝑚) = ((tan‘((𝑚 · π) / 𝑁))↑-2)) |
130 | 129 | ad2antll 765 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑇‘𝑚) = ((tan‘((𝑚 · π) / 𝑁))↑-2)) |
131 | 111 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (tan‘((𝑚 · π) / 𝑁)) ∈ ℂ) |
132 | | 2nn0 11309 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
133 | | expneg 12868 |
. . . . . . . . . . 11
⊢
(((tan‘((𝑚
· π) / 𝑁)) ∈
ℂ ∧ 2 ∈ ℕ0) → ((tan‘((𝑚 · π) / 𝑁))↑-2) = (1 /
((tan‘((𝑚 ·
π) / 𝑁))↑2))) |
134 | 131, 132,
133 | sylancl 694 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((tan‘((𝑚 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑚 · π) / 𝑁))↑2))) |
135 | 130, 134 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑇‘𝑚) = (1 / ((tan‘((𝑚 · π) / 𝑁))↑2))) |
136 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝑛 · π) = (𝑘 · π)) |
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → ((𝑛 · π) / 𝑁) = ((𝑘 · π) / 𝑁)) |
138 | 137 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (tan‘((𝑛 · π) / 𝑁)) = (tan‘((𝑘 · π) / 𝑁))) |
139 | 138 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → ((tan‘((𝑛 · π) / 𝑁))↑-2) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
140 | | ovex 6678 |
. . . . . . . . . . . 12
⊢
((tan‘((𝑘
· π) / 𝑁))↑-2) ∈ V |
141 | 139, 57, 140 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑀) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
142 | 141 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
143 | 109 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ) |
144 | | expneg 12868 |
. . . . . . . . . . 11
⊢
(((tan‘((𝑘
· π) / 𝑁)) ∈
ℂ ∧ 2 ∈ ℕ0) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 /
((tan‘((𝑘 ·
π) / 𝑁))↑2))) |
145 | 143, 132,
144 | sylancl 694 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))) |
146 | 142, 145 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑇‘𝑘) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))) |
147 | 123, 135,
146 | 3brtr4d 4685 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝑘 < 𝑚) ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑇‘𝑚) < (𝑇‘𝑘)) |
148 | 147 | an32s 846 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) ∧ 𝑘 < 𝑚) → (𝑇‘𝑚) < (𝑇‘𝑘)) |
149 | 148 | ex 450 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ (𝑘 ∈ (1...𝑀) ∧ 𝑚 ∈ (1...𝑀))) → (𝑘 < 𝑚 → (𝑇‘𝑚) < (𝑇‘𝑘))) |
150 | 59, 60, 61, 63, 66, 149 | eqord2 10559 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑀))) → (𝑥 = 𝑦 ↔ (𝑇‘𝑥) = (𝑇‘𝑦))) |
151 | 150 | biimprd 238 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ (𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑀))) → ((𝑇‘𝑥) = (𝑇‘𝑦) → 𝑥 = 𝑦)) |
152 | 151 | ralrimivva 2971 |
. . 3
⊢ (𝑀 ∈ ℕ →
∀𝑥 ∈ (1...𝑀)∀𝑦 ∈ (1...𝑀)((𝑇‘𝑥) = (𝑇‘𝑦) → 𝑥 = 𝑦)) |
153 | | dff13 6512 |
. . 3
⊢ (𝑇:(1...𝑀)–1-1→(◡𝑃 “ {0}) ↔ (𝑇:(1...𝑀)⟶(◡𝑃 “ {0}) ∧ ∀𝑥 ∈ (1...𝑀)∀𝑦 ∈ (1...𝑀)((𝑇‘𝑥) = (𝑇‘𝑦) → 𝑥 = 𝑦))) |
154 | 58, 152, 153 | sylanbrc 698 |
. 2
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1→(◡𝑃 “ {0})) |
155 | 48 | simp2d 1074 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) = 𝑀) |
156 | | nnne0 11053 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
157 | 155, 156 | eqnetrd 2861 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) ≠
0) |
158 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑃 = 0𝑝 →
(deg‘𝑃) =
(deg‘0𝑝)) |
159 | | dgr0 24018 |
. . . . . . . . . 10
⊢
(deg‘0𝑝) = 0 |
160 | 158, 159 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑃 = 0𝑝 →
(deg‘𝑃) =
0) |
161 | 160 | necon3i 2826 |
. . . . . . . 8
⊢
((deg‘𝑃) ≠
0 → 𝑃 ≠
0𝑝) |
162 | 157, 161 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑃 ≠
0𝑝) |
163 | | eqid 2622 |
. . . . . . . 8
⊢ (◡𝑃 “ {0}) = (◡𝑃 “ {0}) |
164 | 163 | fta1 24063 |
. . . . . . 7
⊢ ((𝑃 ∈ (Poly‘ℂ)
∧ 𝑃 ≠
0𝑝) → ((◡𝑃 “ {0}) ∈ Fin ∧
(#‘(◡𝑃 “ {0})) ≤ (deg‘𝑃))) |
165 | 49, 162, 164 | syl2anc 693 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((◡𝑃 “ {0}) ∈ Fin ∧
(#‘(◡𝑃 “ {0})) ≤ (deg‘𝑃))) |
166 | 165 | simpld 475 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ∈ Fin) |
167 | | f1domg 7975 |
. . . . 5
⊢ ((◡𝑃 “ {0}) ∈ Fin → (𝑇:(1...𝑀)–1-1→(◡𝑃 “ {0}) → (1...𝑀) ≼ (◡𝑃 “ {0}))) |
168 | 166, 154,
167 | sylc 65 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ≼ (◡𝑃 “ {0})) |
169 | 165 | simprd 479 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(#‘(◡𝑃 “ {0})) ≤ (deg‘𝑃)) |
170 | | nnnn0 11299 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
171 | | hashfz1 13134 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
172 | 170, 171 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(#‘(1...𝑀)) = 𝑀) |
173 | 155, 172 | eqtr4d 2659 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) =
(#‘(1...𝑀))) |
174 | 169, 173 | breqtrd 4679 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
(#‘(◡𝑃 “ {0})) ≤ (#‘(1...𝑀))) |
175 | | fzfid 12772 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ∈
Fin) |
176 | | hashdom 13168 |
. . . . . 6
⊢ (((◡𝑃 “ {0}) ∈ Fin ∧ (1...𝑀) ∈ Fin) →
((#‘(◡𝑃 “ {0})) ≤ (#‘(1...𝑀)) ↔ (◡𝑃 “ {0}) ≼ (1...𝑀))) |
177 | 166, 175,
176 | syl2anc 693 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((#‘(◡𝑃 “ {0})) ≤ (#‘(1...𝑀)) ↔ (◡𝑃 “ {0}) ≼ (1...𝑀))) |
178 | 174, 177 | mpbid 222 |
. . . 4
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ≼ (1...𝑀)) |
179 | | sbth 8080 |
. . . 4
⊢
(((1...𝑀) ≼
(◡𝑃 “ {0}) ∧ (◡𝑃 “ {0}) ≼ (1...𝑀)) → (1...𝑀) ≈ (◡𝑃 “ {0})) |
180 | 168, 178,
179 | syl2anc 693 |
. . 3
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ≈ (◡𝑃 “ {0})) |
181 | | f1finf1o 8187 |
. . 3
⊢
(((1...𝑀) ≈
(◡𝑃 “ {0}) ∧ (◡𝑃 “ {0}) ∈ Fin) → (𝑇:(1...𝑀)–1-1→(◡𝑃 “ {0}) ↔ 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0}))) |
182 | 180, 166,
181 | syl2anc 693 |
. 2
⊢ (𝑀 ∈ ℕ → (𝑇:(1...𝑀)–1-1→(◡𝑃 “ {0}) ↔ 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0}))) |
183 | 154, 182 | mpbid 222 |
1
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) |