Step | Hyp | Ref
| Expression |
1 | | dirkertrigeq.f |
. . 3
β’ πΉ = (π·βπ) |
2 | 1 | a1i 11 |
. 2
β’ (π β πΉ = (π·βπ)) |
3 | | dirkertrigeq.n |
. . 3
β’ (π β π β β) |
4 | | dirkertrigeq.d |
. . . 4
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
5 | 4 | dirkerval 44418 |
. . 3
β’ (π β β β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
6 | 3, 5 | syl 17 |
. 2
β’ (π β (π·βπ) = (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
7 | | dirkertrigeq.h |
. . 3
β’ π» = (π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
8 | | 2cnd 12236 |
. . . . . . . . . . 11
β’ (π β 2 β
β) |
9 | 3 | nncnd 12174 |
. . . . . . . . . . 11
β’ (π β π β β) |
10 | 8, 9 | mulcld 11180 |
. . . . . . . . . 10
β’ (π β (2 Β· π) β
β) |
11 | | peano2cn 11332 |
. . . . . . . . . 10
β’ ((2
Β· π) β β
β ((2 Β· π) + 1)
β β) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ (π β ((2 Β· π) + 1) β
β) |
13 | | picn 25832 |
. . . . . . . . . 10
β’ Ο
β β |
14 | 13 | a1i 11 |
. . . . . . . . 9
β’ (π β Ο β
β) |
15 | | 2ne0 12262 |
. . . . . . . . . 10
β’ 2 β
0 |
16 | 15 | a1i 11 |
. . . . . . . . 9
β’ (π β 2 β 0) |
17 | | pire 25831 |
. . . . . . . . . . 11
β’ Ο
β β |
18 | | pipos 25833 |
. . . . . . . . . . 11
β’ 0 <
Ο |
19 | 17, 18 | gt0ne0ii 11696 |
. . . . . . . . . 10
β’ Ο β
0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ (π β Ο β
0) |
21 | 12, 8, 14, 16, 20 | divdiv1d 11967 |
. . . . . . . 8
β’ (π β ((((2 Β· π) + 1) / 2) / Ο) = (((2
Β· π) + 1) / (2
Β· Ο))) |
22 | 21 | eqcomd 2739 |
. . . . . . 7
β’ (π β (((2 Β· π) + 1) / (2 Β· Ο)) =
((((2 Β· π) + 1) / 2)
/ Ο)) |
23 | 22 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β (((2
Β· π) + 1) / (2
Β· Ο)) = ((((2 Β· π) + 1) / 2) / Ο)) |
24 | | iftrue 4493 |
. . . . . . 7
β’ ((π mod (2 Β· Ο)) = 0
β if((π mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) = (((2 Β· π) + 1) / (2 Β·
Ο))) |
25 | 24 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2))))) =
(((2 Β· π) + 1) / (2
Β· Ο))) |
26 | | elfzelz 13447 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β π β β€) |
27 | 26 | zcnd 12613 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β π β β) |
28 | 27 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β π β β) |
29 | | recn 11146 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β π β β) |
31 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
32 | 31, 13 | mulcli 11167 |
. . . . . . . . . . . . . . . . 17
β’ (2
Β· Ο) β β |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β (2 Β· Ο)
β β) |
34 | 31, 13, 15, 19 | mulne0i 11803 |
. . . . . . . . . . . . . . . . 17
β’ (2
Β· Ο) β 0 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β (2 Β· Ο) β
0) |
36 | 28, 30, 33, 35 | divassd 11971 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β ((π Β· π ) / (2 Β· Ο)) = (π Β· (π / (2 Β· Ο)))) |
37 | 26 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β π β β€) |
38 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (π mod (2 Β· Ο)) = 0)
β (π mod (2 Β·
Ο)) = 0) |
39 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π mod (2 Β· Ο)) = 0)
β π β
β) |
40 | | 2rp 12925 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β+ |
41 | | pirp 25834 |
. . . . . . . . . . . . . . . . . . . 20
β’ Ο
β β+ |
42 | | rpmulcl 12943 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((2
β β+ β§ Ο β β+) β (2
Β· Ο) β β+) |
43 | 40, 41, 42 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’ (2
Β· Ο) β β+ |
44 | | mod0 13787 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (2
Β· Ο) β β+) β ((π mod (2 Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
45 | 39, 43, 44 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (π mod (2 Β· Ο)) = 0)
β ((π mod (2 Β·
Ο)) = 0 β (π / (2
Β· Ο)) β β€)) |
46 | 38, 45 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π mod (2 Β· Ο)) = 0)
β (π / (2 Β·
Ο)) β β€) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β (π / (2 Β· Ο)) β
β€) |
48 | 37, 47 | zmulcld 12618 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β (π Β· (π / (2 Β· Ο))) β
β€) |
49 | 36, 48 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β ((π Β· π ) / (2 Β· Ο)) β
β€) |
50 | 27 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (1...π)) β π β β) |
51 | 29 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β (1...π)) β π β β) |
52 | 50, 51 | mulcld 11180 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β (1...π)) β (π Β· π ) β β) |
53 | | coseq1 25897 |
. . . . . . . . . . . . . . . 16
β’ ((π Β· π ) β β β ((cosβ(π Β· π )) = 1 β ((π Β· π ) / (2 Β· Ο)) β
β€)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β (1...π)) β ((cosβ(π Β· π )) = 1 β ((π Β· π ) / (2 Β· Ο)) β
β€)) |
55 | 54 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β ((cosβ(π Β· π )) = 1 β ((π Β· π ) / (2 Β· Ο)) β
β€)) |
56 | 49, 55 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π mod (2 Β· Ο)) = 0)
β§ π β (1...π)) β (cosβ(π Β· π )) = 1) |
57 | 56 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π mod (2 Β· Ο)) = 0)
β βπ β
(1...π)(cosβ(π Β· π )) = 1) |
58 | 57 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β
βπ β (1...π)(cosβ(π Β· π )) = 1) |
59 | 58 | sumeq2d 15592 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β
Ξ£π β (1...π)(cosβ(π Β· π )) = Ξ£π β (1...π)1) |
60 | | fzfid 13884 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β
(1...π) β
Fin) |
61 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β 1 β
β) |
62 | | fsumconst 15680 |
. . . . . . . . . . 11
β’
(((1...π) β Fin
β§ 1 β β) β Ξ£π β (1...π)1 = ((β―β(1...π)) Β· 1)) |
63 | 60, 61, 62 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β
Ξ£π β (1...π)1 = ((β―β(1...π)) Β· 1)) |
64 | 3 | nnnn0d 12478 |
. . . . . . . . . . . . . 14
β’ (π β π β
β0) |
65 | | hashfz1 14252 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (β―β(1...π)) = π) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β―β(1...π)) = π) |
67 | 66 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ (π β ((β―β(1...π)) Β· 1) = (π Β· 1)) |
68 | 9 | mulid1d 11177 |
. . . . . . . . . . . 12
β’ (π β (π Β· 1) = π) |
69 | 67, 68 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β ((β―β(1...π)) Β· 1) = π) |
70 | 69 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β
((β―β(1...π))
Β· 1) = π) |
71 | 59, 63, 70 | 3eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β
Ξ£π β (1...π)(cosβ(π Β· π )) = π) |
72 | 71 | oveq2d 7374 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β ((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) = ((1 / 2) + π)) |
73 | 9 | div1d 11928 |
. . . . . . . . . . . 12
β’ (π β (π / 1) = π) |
74 | 73 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π β π = (π / 1)) |
75 | 74 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β ((1 / 2) + π) = ((1 / 2) + (π / 1))) |
76 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
77 | | ax-1ne0 11125 |
. . . . . . . . . . . 12
β’ 1 β
0 |
78 | 77 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 1 β 0) |
79 | 76, 8, 9, 76, 16, 78 | divadddivd 11980 |
. . . . . . . . . 10
β’ (π β ((1 / 2) + (π / 1)) = (((1 Β· 1) +
(π Β· 2)) / (2
Β· 1))) |
80 | 76, 76 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (π β (1 Β· 1) β
β) |
81 | 9, 8 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ (π β (π Β· 2) β
β) |
82 | 80, 81 | addcomd 11362 |
. . . . . . . . . . . 12
β’ (π β ((1 Β· 1) + (π Β· 2)) = ((π Β· 2) + (1 Β·
1))) |
83 | 9, 8 | mulcomd 11181 |
. . . . . . . . . . . . 13
β’ (π β (π Β· 2) = (2 Β· π)) |
84 | 76 | mulid1d 11177 |
. . . . . . . . . . . . 13
β’ (π β (1 Β· 1) =
1) |
85 | 83, 84 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π β ((π Β· 2) + (1 Β· 1)) = ((2
Β· π) +
1)) |
86 | 82, 85 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β ((1 Β· 1) + (π Β· 2)) = ((2 Β·
π) + 1)) |
87 | 8 | mulid1d 11177 |
. . . . . . . . . . 11
β’ (π β (2 Β· 1) =
2) |
88 | 86, 87 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π β (((1 Β· 1) + (π Β· 2)) / (2 Β· 1))
= (((2 Β· π) + 1) /
2)) |
89 | 75, 79, 88 | 3eqtrd 2777 |
. . . . . . . . 9
β’ (π β ((1 / 2) + π) = (((2 Β· π) + 1) / 2)) |
90 | 89 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β ((1 / 2)
+ π) = (((2 Β· π) + 1) / 2)) |
91 | 72, 90 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β ((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) = (((2 Β· π) + 1) / 2)) |
92 | 91 | oveq1d 7373 |
. . . . . 6
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β (((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο) = ((((2 Β· π) + 1) / 2) /
Ο)) |
93 | 23, 25, 92 | 3eqtr4rd 2784 |
. . . . 5
β’ (((π β§ π β β) β§ (π mod (2 Β· Ο)) = 0) β (((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο) = if((π mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))))) |
94 | | iffalse 4496 |
. . . . . . 7
β’ (Β¬
(π mod (2 Β· Ο)) =
0 β if((π mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) = ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))) |
95 | 94 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β if((π mod (2
Β· Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) = ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))) |
96 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β Ο
β β) |
97 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β Ο β
0) |
98 | 29, 96, 97 | divcan1d 11937 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((π / Ο) Β· Ο) = π ) |
99 | 98 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π = ((π / Ο) Β· Ο)) |
100 | 99 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β π = ((π / Ο) Β·
Ο)) |
101 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π mod Ο) = 0) β (π mod Ο) = 0) |
102 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (π mod Ο) = 0) β π β
β) |
103 | | mod0 13787 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ Ο
β β+) β ((π mod Ο) = 0 β (π / Ο) β β€)) |
104 | 102, 41, 103 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ (π mod Ο) = 0) β ((π mod Ο) = 0 β (π / Ο) β
β€)) |
105 | 101, 104 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (π mod Ο) = 0) β (π / Ο) β
β€) |
106 | 105 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β (π / Ο) β
β€) |
107 | | rpreccl 12946 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Ο
β β+ β (1 / Ο) β
β+) |
108 | 41, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 /
Ο) β β+ |
109 | | moddi 13850 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((1 /
Ο) β β+ β§ π β β β§ (2 Β· Ο)
β β+) β ((1 / Ο) Β· (π mod (2 Β· Ο))) = (((1 / Ο)
Β· π ) mod ((1 / Ο)
Β· (2 Β· Ο)))) |
110 | 108, 43, 109 | mp3an13 1453 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β ((1 /
Ο) Β· (π mod (2
Β· Ο))) = (((1 / Ο) Β· π ) mod ((1 / Ο) Β· (2 Β·
Ο)))) |
111 | 29, 96, 97 | divrec2d 11940 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (π / Ο) = ((1 / Ο) Β·
π )) |
112 | 111 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β ((1 /
Ο) Β· π ) = (π / Ο)) |
113 | 96, 97 | reccld 11929 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (1 /
Ο) β β) |
114 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (2
Β· Ο) β β) |
115 | 113, 114 | mulcomd 11181 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β ((1 /
Ο) Β· (2 Β· Ο)) = ((2 Β· Ο) Β· (1 /
Ο))) |
116 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 2 β
β) |
117 | 116, 96, 113 | mulassd 11183 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β ((2
Β· Ο) Β· (1 / Ο)) = (2 Β· (Ο Β· (1 /
Ο)))) |
118 | 13, 19 | recidi 11891 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Ο
Β· (1 / Ο)) = 1 |
119 | 118 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (2
Β· (Ο Β· (1 / Ο))) = (2 Β· 1) |
120 | 116 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (2
Β· 1) = 2) |
121 | 119, 120 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (2
Β· (Ο Β· (1 / Ο))) = 2) |
122 | 115, 117,
121 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β ((1 /
Ο) Β· (2 Β· Ο)) = 2) |
123 | 112, 122 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (((1 /
Ο) Β· π ) mod ((1 /
Ο) Β· (2 Β· Ο))) = ((π / Ο) mod 2)) |
124 | 110, 123 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β ((π / Ο) mod 2) = ((1 / Ο)
Β· (π mod (2 Β·
Ο)))) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((π / Ο) mod
2) = ((1 / Ο) Β· (π mod (2 Β· Ο)))) |
126 | 113 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (1 / Ο) β β) |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β π β
β) |
128 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (2
Β· Ο) β β+) |
129 | 127, 128 | modcld 13786 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β (π mod (2 Β· Ο)) β
β) |
130 | 129 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (π mod (2 Β· Ο)) β
β) |
131 | 130 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (π mod (2
Β· Ο)) β β) |
132 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β |
133 | 132, 13, 77, 19 | divne0i 11908 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 /
Ο) β 0 |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (1 / Ο) β 0) |
135 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
(π mod (2 Β· Ο)) =
0 β (π mod (2 Β·
Ο)) β 0) |
136 | 135 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β (π mod (2
Β· Ο)) β 0) |
137 | 126, 131,
134, 136 | mulne0d 11812 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((1 / Ο) Β· (π mod (2 Β· Ο))) β
0) |
138 | 125, 137 | eqnetrd 3008 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β ((π / Ο) mod
2) β 0) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β ((π / Ο) mod 2)
β 0) |
140 | | oddfl 43598 |
. . . . . . . . . . . . . . . . 17
β’ (((π / Ο) β β€ β§
((π / Ο) mod 2) β 0)
β (π / Ο) = ((2
Β· (ββ((π
/ Ο) / 2))) + 1)) |
141 | 106, 139,
140 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β (π / Ο) = ((2
Β· (ββ((π
/ Ο) / 2))) + 1)) |
142 | 141 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β ((π / Ο) Β·
Ο) = (((2 Β· (ββ((π / Ο) / 2))) + 1) Β·
Ο)) |
143 | 100, 142 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β π = (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο)) |
144 | 143 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β (π Β· π ) = (π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο))) |
145 | 144 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β (cosβ(π
Β· π )) =
(cosβ(π Β· (((2
Β· (ββ((π
/ Ο) / 2))) + 1) Β· Ο)))) |
146 | 145 | sumeq2sdv 15594 |
. . . . . . . . . . 11
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β Ξ£π β
(1...π)(cosβ(π Β· π )) = Ξ£π β (1...π)(cosβ(π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο)))) |
147 | 146 | oveq2d 7374 |
. . . . . . . . . 10
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β ((1 / 2) + Ξ£π
β (1...π)(cosβ(π Β· π ))) = ((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο))))) |
148 | 147 | oveq1d 7373 |
. . . . . . . . 9
β’ (((π β β β§ Β¬
(π mod (2 Β· Ο)) =
0) β§ (π mod Ο) = 0)
β (((1 / 2) + Ξ£π
β (1...π)(cosβ(π Β· π ))) / Ο) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο)))) / Ο)) |
149 | 148 | adantlll 717 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β (((1 / 2) + Ξ£π
β (1...π)(cosβ(π Β· π ))) / Ο) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο)))) / Ο)) |
150 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π mod Ο) = 0) β π β β) |
151 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β Ο
β β) |
152 | 127, 151,
97 | redivcld 11988 |
. . . . . . . . . . . . 13
β’ (π β β β (π / Ο) β
β) |
153 | 152 | rehalfcld 12405 |
. . . . . . . . . . . 12
β’ (π β β β ((π / Ο) / 2) β
β) |
154 | 153 | flcld 13709 |
. . . . . . . . . . 11
β’ (π β β β
(ββ((π / Ο)
/ 2)) β β€) |
155 | 154 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π mod Ο) = 0) β (ββ((π / Ο) / 2)) β
β€) |
156 | | eqid 2733 |
. . . . . . . . . 10
β’ (((2
Β· (ββ((π
/ Ο) / 2))) + 1) Β· Ο) = (((2 Β· (ββ((π / Ο) / 2))) + 1) Β·
Ο) |
157 | 150, 155,
156 | dirkertrigeqlem3 44427 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π mod Ο) = 0) β (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο)))) / Ο) = ((sinβ((π + (1 / 2)) Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο))) / ((2 Β· Ο) Β· (sinβ((((2
Β· (ββ((π
/ Ο) / 2))) + 1) Β· Ο) / 2))))) |
158 | 157 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β (((1 / 2) + Ξ£π
β (1...π)(cosβ(π Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο)))) / Ο) = ((sinβ((π + (1 / 2)) Β· (((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο))) / ((2 Β· Ο) Β· (sinβ((((2
Β· (ββ((π
/ Ο) / 2))) + 1) Β· Ο) / 2))))) |
159 | 141 | adantlll 717 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β (π / Ο) = ((2
Β· (ββ((π
/ Ο) / 2))) + 1)) |
160 | 159 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((2 Β· (ββ((π / Ο) / 2))) + 1) = (π / Ο)) |
161 | 160 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β (((2 Β· (ββ((π / Ο) / 2))) + 1) Β· Ο) = ((π / Ο) Β·
Ο)) |
162 | 161 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((π + (1 / 2))
Β· (((2 Β· (ββ((π / Ο) / 2))) + 1) Β· Ο)) =
((π + (1 / 2)) Β·
((π / Ο) Β·
Ο))) |
163 | 162 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β (sinβ((π + (1
/ 2)) Β· (((2 Β· (ββ((π / Ο) / 2))) + 1) Β· Ο))) =
(sinβ((π + (1 / 2))
Β· ((π / Ο)
Β· Ο)))) |
164 | 161 | fvoveq1d 7380 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β (sinβ((((2 Β· (ββ((π / Ο) / 2))) + 1) Β· Ο) / 2)) =
(sinβ(((π / Ο)
Β· Ο) / 2))) |
165 | 164 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((2 Β· Ο) Β· (sinβ((((2 Β·
(ββ((π / Ο)
/ 2))) + 1) Β· Ο) / 2))) = ((2 Β· Ο) Β·
(sinβ(((π / Ο)
Β· Ο) / 2)))) |
166 | 163, 165 | oveq12d 7376 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((sinβ((π + (1
/ 2)) Β· (((2 Β· (ββ((π / Ο) / 2))) + 1) Β· Ο))) / ((2
Β· Ο) Β· (sinβ((((2 Β· (ββ((π / Ο) / 2))) + 1) Β·
Ο) / 2)))) = ((sinβ((π + (1 / 2)) Β· ((π / Ο) Β· Ο))) / ((2 Β·
Ο) Β· (sinβ(((π / Ο) Β· Ο) /
2))))) |
167 | 98 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π β β β ((π + (1 / 2)) Β· ((π / Ο) Β· Ο)) =
((π + (1 / 2)) Β·
π )) |
168 | 167 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π β β β
(sinβ((π + (1 / 2))
Β· ((π / Ο)
Β· Ο))) = (sinβ((π + (1 / 2)) Β· π ))) |
169 | 98 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
β’ (π β β β
(sinβ(((π / Ο)
Β· Ο) / 2)) = (sinβ(π / 2))) |
170 | 169 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π β β β ((2
Β· Ο) Β· (sinβ(((π / Ο) Β· Ο) / 2))) = ((2 Β·
Ο) Β· (sinβ(π / 2)))) |
171 | 168, 170 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (π β β β
((sinβ((π + (1 / 2))
Β· ((π / Ο)
Β· Ο))) / ((2 Β· Ο) Β· (sinβ(((π / Ο) Β· Ο) / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
172 | 171 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((sinβ((π + (1 / 2)) Β· ((π / Ο) Β· Ο))) / ((2
Β· Ο) Β· (sinβ(((π / Ο) Β· Ο) / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
173 | 172 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((sinβ((π + (1
/ 2)) Β· ((π / Ο)
Β· Ο))) / ((2 Β· Ο) Β· (sinβ(((π / Ο) Β· Ο) / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
174 | 166, 173 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((sinβ((π + (1
/ 2)) Β· (((2 Β· (ββ((π / Ο) / 2))) + 1) Β· Ο))) / ((2
Β· Ο) Β· (sinβ((((2 Β· (ββ((π / Ο) / 2))) + 1) Β·
Ο) / 2)))) = ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))) |
175 | 149, 158,
174 | 3eqtrrd 2778 |
. . . . . . 7
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ (π mod Ο) = 0)
β ((sinβ((π + (1
/ 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
176 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β π β
β) |
177 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β Β¬
(π mod Ο) =
0) |
178 | 176, 41, 103 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β ((π mod Ο) = 0 β (π / Ο) β
β€)) |
179 | 177, 178 | mtbid 324 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β Β¬
(π / Ο) β
β€) |
180 | 176 | recnd 11188 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β π β
β) |
181 | | sineq0 25896 |
. . . . . . . . . . . . 13
β’ (π β β β
((sinβπ ) = 0 β
(π / Ο) β
β€)) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β
((sinβπ ) = 0 β
(π / Ο) β
β€)) |
183 | 179, 182 | mtbird 325 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β Β¬
(sinβπ ) =
0) |
184 | 183 | neqned 2947 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β
(sinβπ ) β
0) |
185 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β π β
β) |
186 | 176, 184,
185 | dirkertrigeqlem2 44426 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β (((1 / 2)
+ Ξ£π β
(1...π)(cosβ(π Β· π ))) / Ο) = ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))) |
187 | 186 | eqcomd 2739 |
. . . . . . . 8
β’ (((π β§ π β β) β§ Β¬ (π mod Ο) = 0) β
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2)))) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
188 | 187 | adantlr 714 |
. . . . . . 7
β’ ((((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β§ Β¬ (π mod Ο) =
0) β ((sinβ((π +
(1 / 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
189 | 175, 188 | pm2.61dan 812 |
. . . . . 6
β’ (((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β ((sinβ((π + (1
/ 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))) = (((1 / 2) + Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) |
190 | 95, 189 | eqtr2d 2774 |
. . . . 5
β’ (((π β§ π β β) β§ Β¬ (π mod (2 Β· Ο)) = 0)
β (((1 / 2) + Ξ£π
β (1...π)(cosβ(π Β· π ))) / Ο) = if((π mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))))) |
191 | 93, 190 | pm2.61dan 812 |
. . . 4
β’ ((π β§ π β β) β (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο) = if((π mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))))) |
192 | 191 | mpteq2dva 5206 |
. . 3
β’ (π β (π β β β¦ (((1 / 2) +
Ξ£π β (1...π)(cosβ(π Β· π ))) / Ο)) = (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
193 | 7, 192 | eqtr2id 2786 |
. 2
β’ (π β (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2)))))) =
π») |
194 | 2, 6, 193 | 3eqtrd 2777 |
1
β’ (π β πΉ = π») |