Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β β β¦
(-(cosβ(π΄ Β·
π¦)) / π΄)) = (π¦ β β β¦ (-(cosβ(π΄ Β· π¦)) / π΄)) |
2 | | itgsincmulx.a |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
3 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β π΄ β β) |
4 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β π¦ β β) |
5 | 3, 4 | mulcld 11231 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (π΄ Β· π¦) β β) |
6 | 5 | coscld 16071 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (cosβ(π΄ Β· π¦)) β β) |
7 | 6 | negcld 11555 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β -(cosβ(π΄ Β· π¦)) β β) |
8 | | itgsincmulx.an0 |
. . . . . . . . 9
β’ (π β π΄ β 0) |
9 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π΄ β 0) |
10 | 7, 3, 9 | divcld 11987 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (-(cosβ(π΄ Β· π¦)) / π΄) β β) |
11 | | cnelprrecn 11200 |
. . . . . . . . . 10
β’ β
β {β, β} |
12 | 11 | a1i 11 |
. . . . . . . . 9
β’ (π β β β {β,
β}) |
13 | 5 | sincld 16070 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β (sinβ(π΄ Β· π¦)) β β) |
14 | 13 | negcld 11555 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β -(sinβ(π΄ Β· π¦)) β β) |
15 | 3, 14 | mulcld 11231 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (π΄ Β· -(sinβ(π΄ Β· π¦))) β β) |
16 | 15 | negcld 11555 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β -(π΄ Β· -(sinβ(π΄ Β· π¦))) β β) |
17 | | dvcosax 44629 |
. . . . . . . . . . 11
β’ (π΄ β β β (β
D (π¦ β β β¦
(cosβ(π΄ Β·
π¦)))) = (π¦ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π¦))))) |
18 | 2, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β (β D (π¦ β β β¦
(cosβ(π΄ Β·
π¦)))) = (π¦ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π¦))))) |
19 | 12, 6, 15, 18 | dvmptneg 25475 |
. . . . . . . . 9
β’ (π β (β D (π¦ β β β¦
-(cosβ(π΄ Β·
π¦)))) = (π¦ β β β¦ -(π΄ Β· -(sinβ(π΄ Β· π¦))))) |
20 | 12, 7, 16, 19, 2, 8 | dvmptdivc 25474 |
. . . . . . . 8
β’ (π β (β D (π¦ β β β¦
(-(cosβ(π΄ Β·
π¦)) / π΄))) = (π¦ β β β¦ (-(π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄))) |
21 | 15, 3, 9 | divnegd 12000 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β -((π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄) = (-(π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄)) |
22 | 21 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (-(π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄) = -((π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄)) |
23 | 14, 3, 9 | divcan3d 11992 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β ((π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄) = -(sinβ(π΄ Β· π¦))) |
24 | 23 | negeqd 11451 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β -((π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄) = --(sinβ(π΄ Β· π¦))) |
25 | 13 | negnegd 11559 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β --(sinβ(π΄ Β· π¦)) = (sinβ(π΄ Β· π¦))) |
26 | 22, 24, 25 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (-(π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄) = (sinβ(π΄ Β· π¦))) |
27 | 26 | mpteq2dva 5248 |
. . . . . . . 8
β’ (π β (π¦ β β β¦ (-(π΄ Β· -(sinβ(π΄ Β· π¦))) / π΄)) = (π¦ β β β¦ (sinβ(π΄ Β· π¦)))) |
28 | 20, 27 | eqtrd 2773 |
. . . . . . 7
β’ (π β (β D (π¦ β β β¦
(-(cosβ(π΄ Β·
π¦)) / π΄))) = (π¦ β β β¦ (sinβ(π΄ Β· π¦)))) |
29 | | itgsincmulx.b |
. . . . . . 7
β’ (π β π΅ β β) |
30 | | itgsincmulx.c |
. . . . . . 7
β’ (π β πΆ β β) |
31 | 1, 10, 28, 13, 29, 30 | dvmptresicc 25425 |
. . . . . 6
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))) = (π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦)))) |
32 | 31 | fveq1d 6891 |
. . . . 5
β’ (π β ((β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)))βπ₯) = ((π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦)))βπ₯)) |
33 | 32 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β (π΅(,)πΆ)) β ((β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)))βπ₯) = ((π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦)))βπ₯)) |
34 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦))) = (π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦)))) |
35 | | oveq2 7414 |
. . . . . . 7
β’ (π¦ = π₯ β (π΄ Β· π¦) = (π΄ Β· π₯)) |
36 | 35 | fveq2d 6893 |
. . . . . 6
β’ (π¦ = π₯ β (sinβ(π΄ Β· π¦)) = (sinβ(π΄ Β· π₯))) |
37 | 36 | adantl 483 |
. . . . 5
β’ (((π β§ π₯ β (π΅(,)πΆ)) β§ π¦ = π₯) β (sinβ(π΄ Β· π¦)) = (sinβ(π΄ Β· π₯))) |
38 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π₯ β (π΅(,)πΆ)) |
39 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π΄ β β) |
40 | | ioosscn 13383 |
. . . . . . . 8
β’ (π΅(,)πΆ) β β |
41 | 40, 38 | sselid 3980 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π₯ β β) |
42 | 39, 41 | mulcld 11231 |
. . . . . 6
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (π΄ Β· π₯) β β) |
43 | 42 | sincld 16070 |
. . . . 5
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (sinβ(π΄ Β· π₯)) β β) |
44 | 34, 37, 38, 43 | fvmptd 7003 |
. . . 4
β’ ((π β§ π₯ β (π΅(,)πΆ)) β ((π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦)))βπ₯) = (sinβ(π΄ Β· π₯))) |
45 | 33, 44 | eqtr2d 2774 |
. . 3
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (sinβ(π΄ Β· π₯)) = ((β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)))βπ₯)) |
46 | 45 | itgeq2dv 25291 |
. 2
β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = β«(π΅(,)πΆ)((β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)))βπ₯) dπ₯) |
47 | | itgsincmulx.blec |
. . 3
β’ (π β π΅ β€ πΆ) |
48 | | sincn 25948 |
. . . . . 6
β’ sin
β (ββcnββ) |
49 | 48 | a1i 11 |
. . . . 5
β’ (π β sin β
(ββcnββ)) |
50 | 40 | a1i 11 |
. . . . . . 7
β’ (π β (π΅(,)πΆ) β β) |
51 | | ssid 4004 |
. . . . . . . 8
β’ β
β β |
52 | 51 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
53 | 50, 2, 52 | constcncfg 44575 |
. . . . . 6
β’ (π β (π¦ β (π΅(,)πΆ) β¦ π΄) β ((π΅(,)πΆ)βcnββ)) |
54 | 50, 52 | idcncfg 44576 |
. . . . . 6
β’ (π β (π¦ β (π΅(,)πΆ) β¦ π¦) β ((π΅(,)πΆ)βcnββ)) |
55 | 53, 54 | mulcncf 24955 |
. . . . 5
β’ (π β (π¦ β (π΅(,)πΆ) β¦ (π΄ Β· π¦)) β ((π΅(,)πΆ)βcnββ)) |
56 | 49, 55 | cncfmpt1f 24422 |
. . . 4
β’ (π β (π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦))) β ((π΅(,)πΆ)βcnββ)) |
57 | 31, 56 | eqeltrd 2834 |
. . 3
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))) β ((π΅(,)πΆ)βcnββ)) |
58 | | ioossicc 13407 |
. . . . . 6
β’ (π΅(,)πΆ) β (π΅[,]πΆ) |
59 | 58 | a1i 11 |
. . . . 5
β’ (π β (π΅(,)πΆ) β (π΅[,]πΆ)) |
60 | | ioombl 25074 |
. . . . . 6
β’ (π΅(,)πΆ) β dom vol |
61 | 60 | a1i 11 |
. . . . 5
β’ (π β (π΅(,)πΆ) β dom vol) |
62 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β (π΅[,]πΆ)) β π΄ β β) |
63 | 29, 30 | iccssred 13408 |
. . . . . . . . 9
β’ (π β (π΅[,]πΆ) β β) |
64 | | ax-resscn 11164 |
. . . . . . . . 9
β’ β
β β |
65 | 63, 64 | sstrdi 3994 |
. . . . . . . 8
β’ (π β (π΅[,]πΆ) β β) |
66 | 65 | sselda 3982 |
. . . . . . 7
β’ ((π β§ π¦ β (π΅[,]πΆ)) β π¦ β β) |
67 | 62, 66 | mulcld 11231 |
. . . . . 6
β’ ((π β§ π¦ β (π΅[,]πΆ)) β (π΄ Β· π¦) β β) |
68 | 67 | sincld 16070 |
. . . . 5
β’ ((π β§ π¦ β (π΅[,]πΆ)) β (sinβ(π΄ Β· π¦)) β β) |
69 | 65, 2, 52 | constcncfg 44575 |
. . . . . . . 8
β’ (π β (π¦ β (π΅[,]πΆ) β¦ π΄) β ((π΅[,]πΆ)βcnββ)) |
70 | 65, 52 | idcncfg 44576 |
. . . . . . . 8
β’ (π β (π¦ β (π΅[,]πΆ) β¦ π¦) β ((π΅[,]πΆ)βcnββ)) |
71 | 69, 70 | mulcncf 24955 |
. . . . . . 7
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (π΄ Β· π¦)) β ((π΅[,]πΆ)βcnββ)) |
72 | 49, 71 | cncfmpt1f 24422 |
. . . . . 6
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (sinβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) |
73 | | cniccibl 25350 |
. . . . . 6
β’ ((π΅ β β β§ πΆ β β β§ (π¦ β (π΅[,]πΆ) β¦ (sinβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) β (π¦ β (π΅[,]πΆ) β¦ (sinβ(π΄ Β· π¦))) β
πΏ1) |
74 | 29, 30, 72, 73 | syl3anc 1372 |
. . . . 5
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (sinβ(π΄ Β· π¦))) β
πΏ1) |
75 | 59, 61, 68, 74 | iblss 25314 |
. . . 4
β’ (π β (π¦ β (π΅(,)πΆ) β¦ (sinβ(π΄ Β· π¦))) β
πΏ1) |
76 | 31, 75 | eqeltrd 2834 |
. . 3
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))) β
πΏ1) |
77 | | coscn 25949 |
. . . . . . 7
β’ cos
β (ββcnββ) |
78 | 77 | a1i 11 |
. . . . . 6
β’ (π β cos β
(ββcnββ)) |
79 | 78, 71 | cncfmpt1f 24422 |
. . . . 5
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (cosβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) |
80 | 79 | negcncfg 44584 |
. . . 4
β’ (π β (π¦ β (π΅[,]πΆ) β¦ -(cosβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) |
81 | 8 | neneqd 2946 |
. . . . . . 7
β’ (π β Β¬ π΄ = 0) |
82 | | elsng 4642 |
. . . . . . . 8
β’ (π΄ β β β (π΄ β {0} β π΄ = 0)) |
83 | 2, 82 | syl 17 |
. . . . . . 7
β’ (π β (π΄ β {0} β π΄ = 0)) |
84 | 81, 83 | mtbird 325 |
. . . . . 6
β’ (π β Β¬ π΄ β {0}) |
85 | 2, 84 | eldifd 3959 |
. . . . 5
β’ (π β π΄ β (β β
{0})) |
86 | | difssd 4132 |
. . . . 5
β’ (π β (β β {0})
β β) |
87 | 65, 85, 86 | constcncfg 44575 |
. . . 4
β’ (π β (π¦ β (π΅[,]πΆ) β¦ π΄) β ((π΅[,]πΆ)βcnβ(β β {0}))) |
88 | 80, 87 | divcncf 24956 |
. . 3
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)) β ((π΅[,]πΆ)βcnββ)) |
89 | 29, 30, 47, 57, 76, 88 | ftc2 25553 |
. 2
β’ (π β β«(π΅(,)πΆ)((β D (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)))βπ₯) dπ₯ = (((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπΆ) β ((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπ΅))) |
90 | | eqidd 2734 |
. . . . . 6
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄)) = (π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))) |
91 | | oveq2 7414 |
. . . . . . . . . 10
β’ (π¦ = πΆ β (π΄ Β· π¦) = (π΄ Β· πΆ)) |
92 | 91 | fveq2d 6893 |
. . . . . . . . 9
β’ (π¦ = πΆ β (cosβ(π΄ Β· π¦)) = (cosβ(π΄ Β· πΆ))) |
93 | 92 | negeqd 11451 |
. . . . . . . 8
β’ (π¦ = πΆ β -(cosβ(π΄ Β· π¦)) = -(cosβ(π΄ Β· πΆ))) |
94 | 93 | oveq1d 7421 |
. . . . . . 7
β’ (π¦ = πΆ β (-(cosβ(π΄ Β· π¦)) / π΄) = (-(cosβ(π΄ Β· πΆ)) / π΄)) |
95 | 94 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ = πΆ) β (-(cosβ(π΄ Β· π¦)) / π΄) = (-(cosβ(π΄ Β· πΆ)) / π΄)) |
96 | 29 | rexrd 11261 |
. . . . . . 7
β’ (π β π΅ β
β*) |
97 | 30 | rexrd 11261 |
. . . . . . 7
β’ (π β πΆ β
β*) |
98 | | ubicc2 13439 |
. . . . . . 7
β’ ((π΅ β β*
β§ πΆ β
β* β§ π΅
β€ πΆ) β πΆ β (π΅[,]πΆ)) |
99 | 96, 97, 47, 98 | syl3anc 1372 |
. . . . . 6
β’ (π β πΆ β (π΅[,]πΆ)) |
100 | | ovexd 7441 |
. . . . . 6
β’ (π β (-(cosβ(π΄ Β· πΆ)) / π΄) β V) |
101 | 90, 95, 99, 100 | fvmptd 7003 |
. . . . 5
β’ (π β ((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπΆ) = (-(cosβ(π΄ Β· πΆ)) / π΄)) |
102 | | oveq2 7414 |
. . . . . . . . . 10
β’ (π¦ = π΅ β (π΄ Β· π¦) = (π΄ Β· π΅)) |
103 | 102 | fveq2d 6893 |
. . . . . . . . 9
β’ (π¦ = π΅ β (cosβ(π΄ Β· π¦)) = (cosβ(π΄ Β· π΅))) |
104 | 103 | negeqd 11451 |
. . . . . . . 8
β’ (π¦ = π΅ β -(cosβ(π΄ Β· π¦)) = -(cosβ(π΄ Β· π΅))) |
105 | 104 | oveq1d 7421 |
. . . . . . 7
β’ (π¦ = π΅ β (-(cosβ(π΄ Β· π¦)) / π΄) = (-(cosβ(π΄ Β· π΅)) / π΄)) |
106 | 105 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ = π΅) β (-(cosβ(π΄ Β· π¦)) / π΄) = (-(cosβ(π΄ Β· π΅)) / π΄)) |
107 | | lbicc2 13438 |
. . . . . . 7
β’ ((π΅ β β*
β§ πΆ β
β* β§ π΅
β€ πΆ) β π΅ β (π΅[,]πΆ)) |
108 | 96, 97, 47, 107 | syl3anc 1372 |
. . . . . 6
β’ (π β π΅ β (π΅[,]πΆ)) |
109 | | ovexd 7441 |
. . . . . 6
β’ (π β (-(cosβ(π΄ Β· π΅)) / π΄) β V) |
110 | 90, 106, 108, 109 | fvmptd 7003 |
. . . . 5
β’ (π β ((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπ΅) = (-(cosβ(π΄ Β· π΅)) / π΄)) |
111 | 101, 110 | oveq12d 7424 |
. . . 4
β’ (π β (((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπΆ) β ((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπ΅)) = ((-(cosβ(π΄ Β· πΆ)) / π΄) β (-(cosβ(π΄ Β· π΅)) / π΄))) |
112 | 29 | recnd 11239 |
. . . . . . . . 9
β’ (π β π΅ β β) |
113 | 2, 112 | mulcld 11231 |
. . . . . . . 8
β’ (π β (π΄ Β· π΅) β β) |
114 | 113 | coscld 16071 |
. . . . . . 7
β’ (π β (cosβ(π΄ Β· π΅)) β β) |
115 | 114, 2, 8 | divnegd 12000 |
. . . . . 6
β’ (π β -((cosβ(π΄ Β· π΅)) / π΄) = (-(cosβ(π΄ Β· π΅)) / π΄)) |
116 | 115 | eqcomd 2739 |
. . . . 5
β’ (π β (-(cosβ(π΄ Β· π΅)) / π΄) = -((cosβ(π΄ Β· π΅)) / π΄)) |
117 | 116 | oveq2d 7422 |
. . . 4
β’ (π β ((-(cosβ(π΄ Β· πΆ)) / π΄) β (-(cosβ(π΄ Β· π΅)) / π΄)) = ((-(cosβ(π΄ Β· πΆ)) / π΄) β -((cosβ(π΄ Β· π΅)) / π΄))) |
118 | 30 | recnd 11239 |
. . . . . . . . 9
β’ (π β πΆ β β) |
119 | 2, 118 | mulcld 11231 |
. . . . . . . 8
β’ (π β (π΄ Β· πΆ) β β) |
120 | 119 | coscld 16071 |
. . . . . . 7
β’ (π β (cosβ(π΄ Β· πΆ)) β β) |
121 | 120 | negcld 11555 |
. . . . . 6
β’ (π β -(cosβ(π΄ Β· πΆ)) β β) |
122 | 121, 2, 8 | divcld 11987 |
. . . . 5
β’ (π β (-(cosβ(π΄ Β· πΆ)) / π΄) β β) |
123 | 114, 2, 8 | divcld 11987 |
. . . . 5
β’ (π β ((cosβ(π΄ Β· π΅)) / π΄) β β) |
124 | 122, 123 | subnegd 11575 |
. . . 4
β’ (π β ((-(cosβ(π΄ Β· πΆ)) / π΄) β -((cosβ(π΄ Β· π΅)) / π΄)) = ((-(cosβ(π΄ Β· πΆ)) / π΄) + ((cosβ(π΄ Β· π΅)) / π΄))) |
125 | 111, 117,
124 | 3eqtrd 2777 |
. . 3
β’ (π β (((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπΆ) β ((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπ΅)) = ((-(cosβ(π΄ Β· πΆ)) / π΄) + ((cosβ(π΄ Β· π΅)) / π΄))) |
126 | 122, 123 | addcomd 11413 |
. . 3
β’ (π β ((-(cosβ(π΄ Β· πΆ)) / π΄) + ((cosβ(π΄ Β· π΅)) / π΄)) = (((cosβ(π΄ Β· π΅)) / π΄) + (-(cosβ(π΄ Β· πΆ)) / π΄))) |
127 | 120, 2, 8 | divnegd 12000 |
. . . . . 6
β’ (π β -((cosβ(π΄ Β· πΆ)) / π΄) = (-(cosβ(π΄ Β· πΆ)) / π΄)) |
128 | 127 | eqcomd 2739 |
. . . . 5
β’ (π β (-(cosβ(π΄ Β· πΆ)) / π΄) = -((cosβ(π΄ Β· πΆ)) / π΄)) |
129 | 128 | oveq2d 7422 |
. . . 4
β’ (π β (((cosβ(π΄ Β· π΅)) / π΄) + (-(cosβ(π΄ Β· πΆ)) / π΄)) = (((cosβ(π΄ Β· π΅)) / π΄) + -((cosβ(π΄ Β· πΆ)) / π΄))) |
130 | 120, 2, 8 | divcld 11987 |
. . . . 5
β’ (π β ((cosβ(π΄ Β· πΆ)) / π΄) β β) |
131 | 123, 130 | negsubd 11574 |
. . . 4
β’ (π β (((cosβ(π΄ Β· π΅)) / π΄) + -((cosβ(π΄ Β· πΆ)) / π΄)) = (((cosβ(π΄ Β· π΅)) / π΄) β ((cosβ(π΄ Β· πΆ)) / π΄))) |
132 | 114, 120,
2, 8 | divsubdird 12026 |
. . . . 5
β’ (π β (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄) = (((cosβ(π΄ Β· π΅)) / π΄) β ((cosβ(π΄ Β· πΆ)) / π΄))) |
133 | 132 | eqcomd 2739 |
. . . 4
β’ (π β (((cosβ(π΄ Β· π΅)) / π΄) β ((cosβ(π΄ Β· πΆ)) / π΄)) = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) |
134 | 129, 131,
133 | 3eqtrd 2777 |
. . 3
β’ (π β (((cosβ(π΄ Β· π΅)) / π΄) + (-(cosβ(π΄ Β· πΆ)) / π΄)) = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) |
135 | 125, 126,
134 | 3eqtrd 2777 |
. 2
β’ (π β (((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπΆ) β ((π¦ β (π΅[,]πΆ) β¦ (-(cosβ(π΄ Β· π¦)) / π΄))βπ΅)) = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) |
136 | 46, 89, 135 | 3eqtrd 2777 |
1
β’ (π β β«(π΅(,)πΆ)(sinβ(π΄ Β· π₯)) dπ₯ = (((cosβ(π΄ Β· π΅)) β (cosβ(π΄ Β· πΆ))) / π΄)) |