Step | Hyp | Ref
| Expression |
1 | | 1cnd 11155 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
2 | 1 | halfcld 12403 |
. . . . . . . 8
โข (๐ โ (1 / 2) โ
โ) |
3 | | fzfid 13884 |
. . . . . . . . 9
โข (๐ โ (1...๐) โ Fin) |
4 | | elfzelz 13447 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โค) |
5 | 4 | zcnd 12613 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ๐ โ โ) |
6 | 5 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ๐ โ โ) |
7 | | dirkertrigeqlem2.a |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ โ) |
8 | 7 | recnd 11188 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
9 | 8 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ๐ด โ โ) |
10 | 6, 9 | mulcld 11180 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...๐)) โ (๐ ยท ๐ด) โ โ) |
11 | 10 | coscld 16018 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...๐)) โ (cosโ(๐ ยท ๐ด)) โ โ) |
12 | 3, 11 | fsumcl 15623 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด)) โ โ) |
13 | 2, 12 | addcld 11179 |
. . . . . . 7
โข (๐ โ ((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) โ โ) |
14 | 8 | sincld 16017 |
. . . . . . 7
โข (๐ โ (sinโ๐ด) โ
โ) |
15 | | dirkertrigeqlem2.sinne0 |
. . . . . . 7
โข (๐ โ (sinโ๐ด) โ 0) |
16 | 13, 14, 15 | divcan4d 11942 |
. . . . . 6
โข (๐ โ ((((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) ยท (sinโ๐ด)) / (sinโ๐ด)) = ((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด)))) |
17 | 16 | eqcomd 2739 |
. . . . 5
โข (๐ โ ((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) = ((((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) ยท (sinโ๐ด)) / (sinโ๐ด))) |
18 | 3, 14, 11 | fsummulc1 15675 |
. . . . . . . . 9
โข (๐ โ (ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด)) = ฮฃ๐ โ (1...๐)((cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด))) |
19 | 14 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ๐ด) โ โ) |
20 | 11, 19 | mulcomd 11181 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ((cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด)) = ((sinโ๐ด) ยท (cosโ(๐ ยท ๐ด)))) |
21 | | sinmulcos 44192 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง (๐ ยท ๐ด) โ โ) โ ((sinโ๐ด) ยท (cosโ(๐ ยท ๐ด))) = (((sinโ(๐ด + (๐ ยท ๐ด))) + (sinโ(๐ด โ (๐ ยท ๐ด)))) / 2)) |
22 | 9, 10, 21 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ๐ด) ยท (cosโ(๐ ยท ๐ด))) = (((sinโ(๐ด + (๐ ยท ๐ด))) + (sinโ(๐ด โ (๐ ยท ๐ด)))) / 2)) |
23 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (1...๐)) โ 1 โ โ) |
24 | 6, 23, 9 | adddird 11185 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ ((๐ + 1) ยท ๐ด) = ((๐ ยท ๐ด) + (1 ยท ๐ด))) |
25 | 23, 9 | mulcld 11180 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (1...๐)) โ (1 ยท ๐ด) โ โ) |
26 | 10, 25 | addcomd 11362 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ ((๐ ยท ๐ด) + (1 ยท ๐ด)) = ((1 ยท ๐ด) + (๐ ยท ๐ด))) |
27 | 8 | mulid2d 11178 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1 ยท ๐ด) = ๐ด) |
28 | 27 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((1 ยท ๐ด) + (๐ ยท ๐ด)) = (๐ด + (๐ ยท ๐ด))) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ ((1 ยท ๐ด) + (๐ ยท ๐ด)) = (๐ด + (๐ ยท ๐ด))) |
30 | 24, 26, 29 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ (๐ด + (๐ ยท ๐ด)) = ((๐ + 1) ยท ๐ด)) |
31 | 30 | fveq2d 6847 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ(๐ด + (๐ ยท ๐ด))) = (sinโ((๐ + 1) ยท ๐ด))) |
32 | 10, 9 | negsubdi2d 11533 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (1...๐)) โ -((๐ ยท ๐ด) โ ๐ด) = (๐ด โ (๐ ยท ๐ด))) |
33 | 32 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ (๐ด โ (๐ ยท ๐ด)) = -((๐ ยท ๐ด) โ ๐ด)) |
34 | 33 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ(๐ด โ (๐ ยท ๐ด))) = (sinโ-((๐ ยท ๐ด) โ ๐ด))) |
35 | 10, 9 | subcld 11517 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ ((๐ ยท ๐ด) โ ๐ด) โ โ) |
36 | | sinneg 16033 |
. . . . . . . . . . . . . . . 16
โข (((๐ ยท ๐ด) โ ๐ด) โ โ โ (sinโ-((๐ ยท ๐ด) โ ๐ด)) = -(sinโ((๐ ยท ๐ด) โ ๐ด))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ-((๐ ยท ๐ด) โ ๐ด)) = -(sinโ((๐ ยท ๐ด) โ ๐ด))) |
38 | 34, 37 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ(๐ด โ (๐ ยท ๐ด))) = -(sinโ((๐ ยท ๐ด) โ ๐ด))) |
39 | 31, 38 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ(๐ด + (๐ ยท ๐ด))) + (sinโ(๐ด โ (๐ ยท ๐ด)))) = ((sinโ((๐ + 1) ยท ๐ด)) + -(sinโ((๐ ยท ๐ด) โ ๐ด)))) |
40 | 9, 10 | addcld 11179 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...๐)) โ (๐ด + (๐ ยท ๐ด)) โ โ) |
41 | 40 | sincld 16017 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ(๐ด + (๐ ยท ๐ด))) โ โ) |
42 | 31, 41 | eqeltrrd 2835 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ((๐ + 1) ยท ๐ด)) โ โ) |
43 | 35 | sincld 16017 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ((๐ ยท ๐ด) โ ๐ด)) โ โ) |
44 | 42, 43 | negsubd 11523 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ((๐ + 1) ยท ๐ด)) + -(sinโ((๐ ยท ๐ด) โ ๐ด))) = ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ ยท ๐ด) โ ๐ด)))) |
45 | 6, 9 | mulsubfacd 11621 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ ((๐ ยท ๐ด) โ ๐ด) = ((๐ โ 1) ยท ๐ด)) |
46 | 45 | fveq2d 6847 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ((๐ ยท ๐ด) โ ๐ด)) = (sinโ((๐ โ 1) ยท ๐ด))) |
47 | 46 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ ยท ๐ด) โ ๐ด))) = ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) |
48 | 39, 44, 47 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ(๐ด + (๐ ยท ๐ด))) + (sinโ(๐ด โ (๐ ยท ๐ด)))) = ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) |
49 | 48 | oveq1d 7373 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ (((sinโ(๐ด + (๐ ยท ๐ด))) + (sinโ(๐ด โ (๐ ยท ๐ด)))) / 2) = (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2)) |
50 | 20, 22, 49 | 3eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (1...๐)) โ ((cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด)) = (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2)) |
51 | 50 | sumeq2dv 15593 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ (1...๐)((cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด)) = ฮฃ๐ โ (1...๐)(((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2)) |
52 | | 2cnd 12236 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
53 | | peano2cnm 11472 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
54 | 6, 53 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (๐ โ 1) โ โ) |
55 | 54, 9 | mulcld 11180 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐)) โ ((๐ โ 1) ยท ๐ด) โ โ) |
56 | 55 | sincld 16017 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ((๐ โ 1) ยท ๐ด)) โ โ) |
57 | 42, 56 | subcld 11517 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) โ โ) |
58 | | 2ne0 12262 |
. . . . . . . . . . . 12
โข 2 โ
0 |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ 2 โ 0) |
60 | 3, 52, 57, 59 | fsumdivc 15676 |
. . . . . . . . . 10
โข (๐ โ (ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2) = ฮฃ๐ โ (1...๐)(((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2)) |
61 | 3, 57 | fsumcl 15623 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) โ โ) |
62 | 61, 52, 59 | divrec2d 11940 |
. . . . . . . . . 10
โข (๐ โ (ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2) = ((1 / 2) ยท ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) |
63 | 60, 62 | eqtr3d 2775 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ (1...๐)(((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) / 2) = ((1 / 2) ยท ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) |
64 | 18, 51, 63 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด)) = ((1 / 2) ยท ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) |
65 | 64 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ (((1 / 2) ยท
(sinโ๐ด)) +
(ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด))) = (((1 / 2) ยท (sinโ๐ด)) + ((1 / 2) ยท
ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))))) |
66 | 2, 12, 14 | adddird 11185 |
. . . . . . 7
โข (๐ โ (((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) ยท (sinโ๐ด)) = (((1 / 2) ยท (sinโ๐ด)) + (ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด)) ยท (sinโ๐ด)))) |
67 | 2, 14, 61 | adddid 11184 |
. . . . . . 7
โข (๐ โ ((1 / 2) ยท
((sinโ๐ด) +
ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) = (((1 / 2) ยท (sinโ๐ด)) + ((1 / 2) ยท
ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))))) |
68 | 65, 66, 67 | 3eqtr4d 2783 |
. . . . . 6
โข (๐ โ (((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) ยท (sinโ๐ด)) = ((1 / 2) ยท ((sinโ๐ด) + ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))))) |
69 | 68 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) ยท (sinโ๐ด)) / (sinโ๐ด)) = (((1 / 2) ยท ((sinโ๐ด) + ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) / (sinโ๐ด))) |
70 | 10 | sincld 16017 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ(๐ ยท ๐ด)) โ โ) |
71 | 42, 70, 56 | npncand 11541 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...๐)) โ (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) = ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) |
72 | 71 | eqcomd 2739 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) |
73 | 72 | sumeq2dv 15593 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = ฮฃ๐ โ (1...๐)(((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) |
74 | 42, 70 | subcld 11517 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) โ โ) |
75 | 70, 56 | subcld 11517 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) โ โ) |
76 | 3, 74, 75 | fsumadd 15630 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ (1...๐)(((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) = (ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) + ฮฃ๐ โ (1...๐)((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) |
77 | | fvoveq1 7381 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (sinโ(๐ ยท ๐ด)) = (sinโ(๐ ยท ๐ด))) |
78 | | fvoveq1 7381 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ (sinโ(๐ ยท ๐ด)) = (sinโ((๐ + 1) ยท ๐ด))) |
79 | | fvoveq1 7381 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (sinโ(๐ ยท ๐ด)) = (sinโ(1 ยท ๐ด))) |
80 | | fvoveq1 7381 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ (sinโ(๐ ยท ๐ด)) = (sinโ((๐ + 1) ยท ๐ด))) |
81 | | dirkertrigeqlem2.n |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
82 | 81 | nnzd 12531 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
83 | | nnuz 12811 |
. . . . . . . . . . . . . 14
โข โ =
(โคโฅโ1) |
84 | 81, 83 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
(โคโฅโ1)) |
85 | | peano2uz 12831 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ1) โ (๐ + 1) โ
(โคโฅโ1)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โ
(โคโฅโ1)) |
87 | | elfzelz 13447 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โค) |
88 | 87 | zcnd 12613 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1...(๐ + 1)) โ ๐ โ โ) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐ โ โ) |
90 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ๐ด โ โ) |
91 | 89, 90 | mulcld 11180 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (๐ ยท ๐ด) โ โ) |
92 | 91 | sincld 16017 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (sinโ(๐ ยท ๐ด)) โ โ) |
93 | 77, 78, 79, 80, 82, 86, 92 | telfsum2 15695 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) = ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด)))) |
94 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1...๐) โ 1 โ โ) |
95 | 5, 94 | pncand 11518 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ ((๐ + 1) โ 1) = ๐) |
96 | 95 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ ๐ = ((๐ + 1) โ 1)) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐)) โ ๐ = ((๐ + 1) โ 1)) |
98 | 97 | fvoveq1d 7380 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐)) โ (sinโ(๐ ยท ๐ด)) = (sinโ(((๐ + 1) โ 1) ยท ๐ด))) |
99 | 98 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...๐)) โ ((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = ((sinโ(((๐ + 1) โ 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) |
100 | 99 | sumeq2dv 15593 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = ฮฃ๐ โ (1...๐)((sinโ(((๐ + 1) โ 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) |
101 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
102 | 101 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (sinโ((๐ โ 1) ยท ๐ด)) = (sinโ((๐ โ 1) ยท ๐ด))) |
103 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ (๐ โ 1) = ((๐ + 1) โ 1)) |
104 | 103 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (sinโ((๐ โ 1) ยท ๐ด)) = (sinโ(((๐ + 1) โ 1) ยท ๐ด))) |
105 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (๐ โ 1) = (1 โ 1)) |
106 | 105 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ (sinโ((๐ โ 1) ยท ๐ด)) = (sinโ((1 โ 1)
ยท ๐ด))) |
107 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ (๐ โ 1) = ((๐ + 1) โ 1)) |
108 | 107 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (sinโ((๐ โ 1) ยท ๐ด)) = (sinโ(((๐ + 1) โ 1) ยท ๐ด))) |
109 | | 1cnd 11155 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ 1 โ
โ) |
110 | 89, 109 | subcld 11517 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (๐ โ 1) โ โ) |
111 | 110, 90 | mulcld 11180 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ ((๐ โ 1) ยท ๐ด) โ โ) |
112 | 111 | sincld 16017 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(๐ + 1))) โ (sinโ((๐ โ 1) ยท ๐ด)) โ
โ) |
113 | 102, 104,
106, 108, 82, 86, 112 | telfsum2 15695 |
. . . . . . . . . . . 12
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ(((๐ + 1) โ 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = ((sinโ(((๐ + 1) โ 1) ยท ๐ด)) โ (sinโ((1 โ 1)
ยท ๐ด)))) |
114 | 81 | nnred 12173 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
115 | 114 | recnd 11188 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
116 | 115, 1 | pncand 11518 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ + 1) โ 1) = ๐) |
117 | 116 | fvoveq1d 7380 |
. . . . . . . . . . . . 13
โข (๐ โ (sinโ(((๐ + 1) โ 1) ยท ๐ด)) = (sinโ(๐ ยท ๐ด))) |
118 | 1 | subidd 11505 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1 โ 1) =
0) |
119 | 118 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((1 โ 1) ยท
๐ด) = (0 ยท ๐ด)) |
120 | 8 | mul02d 11358 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0 ยท ๐ด) = 0) |
121 | 119, 120 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((1 โ 1) ยท
๐ด) = 0) |
122 | 121 | fveq2d 6847 |
. . . . . . . . . . . . . 14
โข (๐ โ (sinโ((1 โ 1)
ยท ๐ด)) =
(sinโ0)) |
123 | | sin0 16036 |
. . . . . . . . . . . . . . 15
โข
(sinโ0) = 0 |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ (sinโ0) =
0) |
125 | 122, 124 | eqtrd 2773 |
. . . . . . . . . . . . 13
โข (๐ โ (sinโ((1 โ 1)
ยท ๐ด)) =
0) |
126 | 117, 125 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ โ ((sinโ(((๐ + 1) โ 1) ยท ๐ด)) โ (sinโ((1
โ 1) ยท ๐ด))) =
((sinโ(๐ ยท
๐ด)) โ
0)) |
127 | 100, 113,
126 | 3eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = ((sinโ(๐ ยท ๐ด)) โ 0)) |
128 | 93, 127 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ (ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(๐ ยท ๐ด))) + ฮฃ๐ โ (1...๐)((sinโ(๐ ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) = (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0))) |
129 | 73, 76, 128 | 3eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))) = (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0))) |
130 | 129 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ ((sinโ๐ด) + ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) = ((sinโ๐ด) + (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0)))) |
131 | 27 | fveq2d 6847 |
. . . . . . . . . . . 12
โข (๐ โ (sinโ(1 ยท
๐ด)) = (sinโ๐ด)) |
132 | 131 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) = ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด))) |
133 | 132 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0)) = (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด)) + ((sinโ(๐ ยท ๐ด)) โ 0))) |
134 | 133 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ ((sinโ๐ด) + (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0))) = ((sinโ๐ด) + (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด)) + ((sinโ(๐ ยท ๐ด)) โ 0)))) |
135 | 115, 1 | addcld 11179 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ + 1) โ โ) |
136 | 135, 8 | mulcld 11180 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + 1) ยท ๐ด) โ โ) |
137 | 136 | sincld 16017 |
. . . . . . . . . . . 12
โข (๐ โ (sinโ((๐ + 1) ยท ๐ด)) โ โ) |
138 | 137, 14 | subcld 11517 |
. . . . . . . . . . 11
โข (๐ โ ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด)) โ โ) |
139 | 115, 8 | mulcld 11180 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท ๐ด) โ โ) |
140 | 139 | sincld 16017 |
. . . . . . . . . . . 12
โข (๐ โ (sinโ(๐ ยท ๐ด)) โ โ) |
141 | | 0cnd 11153 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ
โ) |
142 | 140, 141 | subcld 11517 |
. . . . . . . . . . 11
โข (๐ โ ((sinโ(๐ ยท ๐ด)) โ 0) โ
โ) |
143 | 14, 138, 142 | addassd 11182 |
. . . . . . . . . 10
โข (๐ โ (((sinโ๐ด) + ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0)) = ((sinโ๐ด) + (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด)) + ((sinโ(๐ ยท ๐ด)) โ 0)))) |
144 | 143 | eqcomd 2739 |
. . . . . . . . 9
โข (๐ โ ((sinโ๐ด) + (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด)) + ((sinโ(๐ ยท ๐ด)) โ 0))) = (((sinโ๐ด) + ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0))) |
145 | 14, 137 | pncan3d 11520 |
. . . . . . . . . . 11
โข (๐ โ ((sinโ๐ด) + ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด))) = (sinโ((๐ + 1) ยท ๐ด))) |
146 | 140 | subid1d 11506 |
. . . . . . . . . . 11
โข (๐ โ ((sinโ(๐ ยท ๐ด)) โ 0) = (sinโ(๐ ยท ๐ด))) |
147 | 145, 146 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ (((sinโ๐ด) + ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0)) = ((sinโ((๐ + 1) ยท ๐ด)) + (sinโ(๐ ยท ๐ด)))) |
148 | 137, 140 | addcomd 11362 |
. . . . . . . . . 10
โข (๐ โ ((sinโ((๐ + 1) ยท ๐ด)) + (sinโ(๐ ยท ๐ด))) = ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) |
149 | 147, 148 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ (((sinโ๐ด) + ((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0)) = ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) |
150 | 134, 144,
149 | 3eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((sinโ๐ด) + (((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ(1 ยท ๐ด))) + ((sinโ(๐ ยท ๐ด)) โ 0))) = ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) |
151 | 130, 150 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ ((sinโ๐ด) + ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด)))) = ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) |
152 | 151 | oveq2d 7374 |
. . . . . 6
โข (๐ โ ((1 / 2) ยท
((sinโ๐ด) +
ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) = ((1 / 2) ยท ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด))))) |
153 | 152 | oveq1d 7373 |
. . . . 5
โข (๐ โ (((1 / 2) ยท
((sinโ๐ด) +
ฮฃ๐ โ (1...๐)((sinโ((๐ + 1) ยท ๐ด)) โ (sinโ((๐ โ 1) ยท ๐ด))))) / (sinโ๐ด)) = (((1 / 2) ยท ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) / (sinโ๐ด))) |
154 | 17, 69, 153 | 3eqtrd 2777 |
. . . 4
โข (๐ โ ((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) = (((1 / 2) ยท ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) / (sinโ๐ด))) |
155 | | halfre 12372 |
. . . . . . . . . . . 12
โข (1 / 2)
โ โ |
156 | 155 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (1 / 2) โ
โ) |
157 | 114, 156 | readdcld 11189 |
. . . . . . . . . 10
โข (๐ โ (๐ + (1 / 2)) โ โ) |
158 | 157, 7 | remulcld 11190 |
. . . . . . . . 9
โข (๐ โ ((๐ + (1 / 2)) ยท ๐ด) โ โ) |
159 | 158 | recnd 11188 |
. . . . . . . 8
โข (๐ โ ((๐ + (1 / 2)) ยท ๐ด) โ โ) |
160 | 2, 8 | mulcld 11180 |
. . . . . . . 8
โข (๐ โ ((1 / 2) ยท ๐ด) โ
โ) |
161 | | sinmulcos 44192 |
. . . . . . . 8
โข ((((๐ + (1 / 2)) ยท ๐ด) โ โ โง ((1 / 2)
ยท ๐ด) โ โ)
โ ((sinโ((๐ + (1
/ 2)) ยท ๐ด)) ยท
(cosโ((1 / 2) ยท ๐ด))) = (((sinโ(((๐ + (1 / 2)) ยท ๐ด) + ((1 / 2) ยท ๐ด))) + (sinโ(((๐ + (1 / 2)) ยท ๐ด) โ ((1 / 2) ยท ๐ด)))) / 2)) |
162 | 159, 160,
161 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2)
ยท ๐ด))) =
(((sinโ(((๐ + (1 /
2)) ยท ๐ด) + ((1 / 2)
ยท ๐ด))) +
(sinโ(((๐ + (1 / 2))
ยท ๐ด) โ ((1 /
2) ยท ๐ด)))) /
2)) |
163 | 115, 2, 8 | adddird 11185 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + (1 / 2)) ยท ๐ด) = ((๐ ยท ๐ด) + ((1 / 2) ยท ๐ด))) |
164 | 163 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + (1 / 2)) ยท ๐ด) + ((1 / 2) ยท ๐ด)) = (((๐ ยท ๐ด) + ((1 / 2) ยท ๐ด)) + ((1 / 2) ยท ๐ด))) |
165 | 139, 160,
160 | addassd 11182 |
. . . . . . . . . . 11
โข (๐ โ (((๐ ยท ๐ด) + ((1 / 2) ยท ๐ด)) + ((1 / 2) ยท ๐ด)) = ((๐ ยท ๐ด) + (((1 / 2) ยท ๐ด) + ((1 / 2) ยท ๐ด)))) |
166 | 2, 2, 8 | adddird 11185 |
. . . . . . . . . . . . . 14
โข (๐ โ (((1 / 2) + (1 / 2))
ยท ๐ด) = (((1 / 2)
ยท ๐ด) + ((1 / 2)
ยท ๐ด))) |
167 | 1 | 2halvesd 12404 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((1 / 2) + (1 / 2)) =
1) |
168 | 167 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ โ (((1 / 2) + (1 / 2))
ยท ๐ด) = (1 ยท
๐ด)) |
169 | 166, 168 | eqtr3d 2775 |
. . . . . . . . . . . . 13
โข (๐ โ (((1 / 2) ยท ๐ด) + ((1 / 2) ยท ๐ด)) = (1 ยท ๐ด)) |
170 | 169 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ ยท ๐ด) + (((1 / 2) ยท ๐ด) + ((1 / 2) ยท ๐ด))) = ((๐ ยท ๐ด) + (1 ยท ๐ด))) |
171 | 115, 1, 8 | adddird 11185 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ + 1) ยท ๐ด) = ((๐ ยท ๐ด) + (1 ยท ๐ด))) |
172 | 170, 171 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (๐ โ ((๐ ยท ๐ด) + (((1 / 2) ยท ๐ด) + ((1 / 2) ยท ๐ด))) = ((๐ + 1) ยท ๐ด)) |
173 | 164, 165,
172 | 3eqtrrd 2778 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1) ยท ๐ด) = (((๐ + (1 / 2)) ยท ๐ด) + ((1 / 2) ยท ๐ด))) |
174 | 173 | fveq2d 6847 |
. . . . . . . . 9
โข (๐ โ (sinโ((๐ + 1) ยท ๐ด)) = (sinโ(((๐ + (1 / 2)) ยท ๐ด) + ((1 / 2) ยท ๐ด)))) |
175 | 163 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ โ (((๐ + (1 / 2)) ยท ๐ด) โ ((1 / 2) ยท ๐ด)) = (((๐ ยท ๐ด) + ((1 / 2) ยท ๐ด)) โ ((1 / 2) ยท ๐ด))) |
176 | 139, 160 | pncand 11518 |
. . . . . . . . . . 11
โข (๐ โ (((๐ ยท ๐ด) + ((1 / 2) ยท ๐ด)) โ ((1 / 2) ยท ๐ด)) = (๐ ยท ๐ด)) |
177 | 175, 176 | eqtr2d 2774 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท ๐ด) = (((๐ + (1 / 2)) ยท ๐ด) โ ((1 / 2) ยท ๐ด))) |
178 | 177 | fveq2d 6847 |
. . . . . . . . 9
โข (๐ โ (sinโ(๐ ยท ๐ด)) = (sinโ(((๐ + (1 / 2)) ยท ๐ด) โ ((1 / 2) ยท ๐ด)))) |
179 | 174, 178 | oveq12d 7376 |
. . . . . . . 8
โข (๐ โ ((sinโ((๐ + 1) ยท ๐ด)) + (sinโ(๐ ยท ๐ด))) = ((sinโ(((๐ + (1 / 2)) ยท ๐ด) + ((1 / 2) ยท ๐ด))) + (sinโ(((๐ + (1 / 2)) ยท ๐ด) โ ((1 / 2) ยท ๐ด))))) |
180 | 179 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ (((sinโ((๐ + 1) ยท ๐ด)) + (sinโ(๐ ยท ๐ด))) / 2) = (((sinโ(((๐ + (1 / 2)) ยท ๐ด) + ((1 / 2) ยท ๐ด))) + (sinโ(((๐ + (1 / 2)) ยท ๐ด) โ ((1 / 2) ยท ๐ด)))) / 2)) |
181 | 162, 180 | eqtr4d 2776 |
. . . . . 6
โข (๐ โ ((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2)
ยท ๐ด))) =
(((sinโ((๐ + 1)
ยท ๐ด)) +
(sinโ(๐ ยท
๐ด))) / 2)) |
182 | 148 | oveq1d 7373 |
. . . . . 6
โข (๐ โ (((sinโ((๐ + 1) ยท ๐ด)) + (sinโ(๐ ยท ๐ด))) / 2) = (((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด))) / 2)) |
183 | 140, 137 | addcld 11179 |
. . . . . . 7
โข (๐ โ ((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด))) โ โ) |
184 | 183, 52, 59 | divrec2d 11940 |
. . . . . 6
โข (๐ โ (((sinโ(๐ ยท ๐ด)) + (sinโ((๐ + 1) ยท ๐ด))) / 2) = ((1 / 2) ยท
((sinโ(๐ ยท
๐ด)) + (sinโ((๐ + 1) ยท ๐ด))))) |
185 | 181, 182,
184 | 3eqtrrd 2778 |
. . . . 5
โข (๐ โ ((1 / 2) ยท
((sinโ(๐ ยท
๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) = ((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2) ยท
๐ด)))) |
186 | 185 | oveq1d 7373 |
. . . 4
โข (๐ โ (((1 / 2) ยท
((sinโ(๐ ยท
๐ด)) + (sinโ((๐ + 1) ยท ๐ด)))) / (sinโ๐ด)) = (((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2) ยท
๐ด))) / (sinโ๐ด))) |
187 | 8, 52, 59 | divcan2d 11938 |
. . . . . . . . 9
โข (๐ โ (2 ยท (๐ด / 2)) = ๐ด) |
188 | 187 | eqcomd 2739 |
. . . . . . . 8
โข (๐ โ ๐ด = (2 ยท (๐ด / 2))) |
189 | 188 | fveq2d 6847 |
. . . . . . 7
โข (๐ โ (sinโ๐ด) = (sinโ(2 ยท
(๐ด / 2)))) |
190 | 8 | halfcld 12403 |
. . . . . . . 8
โข (๐ โ (๐ด / 2) โ โ) |
191 | | sin2t 16064 |
. . . . . . . 8
โข ((๐ด / 2) โ โ โ
(sinโ(2 ยท (๐ด /
2))) = (2 ยท ((sinโ(๐ด / 2)) ยท (cosโ(๐ด / 2))))) |
192 | 190, 191 | syl 17 |
. . . . . . 7
โข (๐ โ (sinโ(2 ยท
(๐ด / 2))) = (2 ยท
((sinโ(๐ด / 2))
ยท (cosโ(๐ด /
2))))) |
193 | 189, 192 | eqtrd 2773 |
. . . . . 6
โข (๐ โ (sinโ๐ด) = (2 ยท
((sinโ(๐ด / 2))
ยท (cosโ(๐ด /
2))))) |
194 | 193 | oveq2d 7374 |
. . . . 5
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2)
ยท ๐ด))) /
(sinโ๐ด)) =
(((sinโ((๐ + (1 / 2))
ยท ๐ด)) ยท
(cosโ((1 / 2) ยท ๐ด))) / (2 ยท ((sinโ(๐ด / 2)) ยท
(cosโ(๐ด /
2)))))) |
195 | 190 | sincld 16017 |
. . . . . . . 8
โข (๐ โ (sinโ(๐ด / 2)) โ
โ) |
196 | 190 | coscld 16018 |
. . . . . . . 8
โข (๐ โ (cosโ(๐ด / 2)) โ
โ) |
197 | 52, 195, 196 | mulassd 11183 |
. . . . . . 7
โข (๐ โ ((2 ยท
(sinโ(๐ด / 2)))
ยท (cosโ(๐ด /
2))) = (2 ยท ((sinโ(๐ด / 2)) ยท (cosโ(๐ด / 2))))) |
198 | 8, 52, 59 | divrec2d 11940 |
. . . . . . . . 9
โข (๐ โ (๐ด / 2) = ((1 / 2) ยท ๐ด)) |
199 | 198 | fveq2d 6847 |
. . . . . . . 8
โข (๐ โ (cosโ(๐ด / 2)) = (cosโ((1 / 2)
ยท ๐ด))) |
200 | 199 | oveq2d 7374 |
. . . . . . 7
โข (๐ โ ((2 ยท
(sinโ(๐ด / 2)))
ยท (cosโ(๐ด /
2))) = ((2 ยท (sinโ(๐ด / 2))) ยท (cosโ((1 / 2)
ยท ๐ด)))) |
201 | 197, 200 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ (2 ยท
((sinโ(๐ด / 2))
ยท (cosโ(๐ด /
2)))) = ((2 ยท (sinโ(๐ด / 2))) ยท (cosโ((1 / 2)
ยท ๐ด)))) |
202 | 201 | oveq2d 7374 |
. . . . 5
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2)
ยท ๐ด))) / (2 ยท
((sinโ(๐ด / 2))
ยท (cosโ(๐ด /
2))))) = (((sinโ((๐ +
(1 / 2)) ยท ๐ด))
ยท (cosโ((1 / 2) ยท ๐ด))) / ((2 ยท (sinโ(๐ด / 2))) ยท (cosโ((1
/ 2) ยท ๐ด))))) |
203 | 159 | sincld 16017 |
. . . . . 6
โข (๐ โ (sinโ((๐ + (1 / 2)) ยท ๐ด)) โ
โ) |
204 | 52, 195 | mulcld 11180 |
. . . . . 6
โข (๐ โ (2 ยท
(sinโ(๐ด / 2))) โ
โ) |
205 | 160 | coscld 16018 |
. . . . . 6
โข (๐ โ (cosโ((1 / 2)
ยท ๐ด)) โ
โ) |
206 | 195, 196 | mulcld 11180 |
. . . . . . . . 9
โข (๐ โ ((sinโ(๐ด / 2)) ยท
(cosโ(๐ด / 2))) โ
โ) |
207 | 193, 15 | eqnetrrd 3009 |
. . . . . . . . 9
โข (๐ โ (2 ยท
((sinโ(๐ด / 2))
ยท (cosโ(๐ด /
2)))) โ 0) |
208 | 52, 206, 207 | mulne0bbd 11816 |
. . . . . . . 8
โข (๐ โ ((sinโ(๐ด / 2)) ยท
(cosโ(๐ด / 2))) โ
0) |
209 | 195, 196,
208 | mulne0bad 11815 |
. . . . . . 7
โข (๐ โ (sinโ(๐ด / 2)) โ 0) |
210 | 52, 195, 59, 209 | mulne0d 11812 |
. . . . . 6
โข (๐ โ (2 ยท
(sinโ(๐ด / 2))) โ
0) |
211 | 195, 196,
208 | mulne0bbd 11816 |
. . . . . . 7
โข (๐ โ (cosโ(๐ด / 2)) โ 0) |
212 | 199, 211 | eqnetrrd 3009 |
. . . . . 6
โข (๐ โ (cosโ((1 / 2)
ยท ๐ด)) โ
0) |
213 | 203, 204,
205, 210, 212 | divcan5rd 11963 |
. . . . 5
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2)
ยท ๐ด))) / ((2
ยท (sinโ(๐ด /
2))) ยท (cosโ((1 / 2) ยท ๐ด)))) = ((sinโ((๐ + (1 / 2)) ยท ๐ด)) / (2 ยท (sinโ(๐ด / 2))))) |
214 | 194, 202,
213 | 3eqtrd 2777 |
. . . 4
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) ยท (cosโ((1 / 2)
ยท ๐ด))) /
(sinโ๐ด)) =
((sinโ((๐ + (1 / 2))
ยท ๐ด)) / (2 ยท
(sinโ(๐ด /
2))))) |
215 | 154, 186,
214 | 3eqtrd 2777 |
. . 3
โข (๐ โ ((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) = ((sinโ((๐ + (1 / 2)) ยท ๐ด)) / (2 ยท (sinโ(๐ด / 2))))) |
216 | 215 | oveq1d 7373 |
. 2
โข (๐ โ (((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) / ฯ) = (((sinโ((๐ + (1 / 2)) ยท ๐ด)) / (2 ยท
(sinโ(๐ด / 2)))) /
ฯ)) |
217 | | picn 25832 |
. . . 4
โข ฯ
โ โ |
218 | 217 | a1i 11 |
. . 3
โข (๐ โ ฯ โ
โ) |
219 | | pire 25831 |
. . . . 5
โข ฯ
โ โ |
220 | | pipos 25833 |
. . . . 5
โข 0 <
ฯ |
221 | 219, 220 | gt0ne0ii 11696 |
. . . 4
โข ฯ โ
0 |
222 | 221 | a1i 11 |
. . 3
โข (๐ โ ฯ โ
0) |
223 | 203, 204,
218, 210, 222 | divdiv32d 11961 |
. 2
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) / (2 ยท
(sinโ(๐ด / 2)))) /
ฯ) = (((sinโ((๐ +
(1 / 2)) ยท ๐ด)) /
ฯ) / (2 ยท (sinโ(๐ด / 2))))) |
224 | 203, 218,
204, 222, 210 | divdiv1d 11967 |
. . 3
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) / ฯ) / (2 ยท
(sinโ(๐ด / 2)))) =
((sinโ((๐ + (1 / 2))
ยท ๐ด)) / (ฯ
ยท (2 ยท (sinโ(๐ด / 2)))))) |
225 | 218, 52, 195 | mulassd 11183 |
. . . . 5
โข (๐ โ ((ฯ ยท 2)
ยท (sinโ(๐ด /
2))) = (ฯ ยท (2 ยท (sinโ(๐ด / 2))))) |
226 | 218, 52 | mulcomd 11181 |
. . . . . 6
โข (๐ โ (ฯ ยท 2) = (2
ยท ฯ)) |
227 | 226 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((ฯ ยท 2)
ยท (sinโ(๐ด /
2))) = ((2 ยท ฯ) ยท (sinโ(๐ด / 2)))) |
228 | 225, 227 | eqtr3d 2775 |
. . . 4
โข (๐ โ (ฯ ยท (2 ยท
(sinโ(๐ด / 2)))) = ((2
ยท ฯ) ยท (sinโ(๐ด / 2)))) |
229 | 228 | oveq2d 7374 |
. . 3
โข (๐ โ ((sinโ((๐ + (1 / 2)) ยท ๐ด)) / (ฯ ยท (2 ยท
(sinโ(๐ด / 2))))) =
((sinโ((๐ + (1 / 2))
ยท ๐ด)) / ((2 ยท
ฯ) ยท (sinโ(๐ด / 2))))) |
230 | 224, 229 | eqtrd 2773 |
. 2
โข (๐ โ (((sinโ((๐ + (1 / 2)) ยท ๐ด)) / ฯ) / (2 ยท
(sinโ(๐ด / 2)))) =
((sinโ((๐ + (1 / 2))
ยท ๐ด)) / ((2 ยท
ฯ) ยท (sinโ(๐ด / 2))))) |
231 | 216, 223,
230 | 3eqtrd 2777 |
1
โข (๐ โ (((1 / 2) + ฮฃ๐ โ (1...๐)(cosโ(๐ ยท ๐ด))) / ฯ) = ((sinโ((๐ + (1 / 2)) ยท ๐ด)) / ((2 ยท ฯ) ยท
(sinโ(๐ด /
2))))) |