Step | Hyp | Ref
| Expression |
1 | | itgcoscmulx.b |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
2 | | itgcoscmulx.c |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
3 | 1, 2 | iccssred 13358 |
. . . . . . . . . 10
β’ (π β (π΅[,]πΆ) β β) |
4 | 3 | resmptd 5999 |
. . . . . . . . 9
β’ (π β ((π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄)) βΎ (π΅[,]πΆ)) = (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) |
5 | 4 | eqcomd 2743 |
. . . . . . . 8
β’ (π β (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)) = ((π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄)) βΎ (π΅[,]πΆ))) |
6 | 5 | oveq2d 7378 |
. . . . . . 7
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) = (β D ((π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄)) βΎ (π΅[,]πΆ)))) |
7 | | ax-resscn 11115 |
. . . . . . . . 9
β’ β
β β |
8 | 7 | a1i 11 |
. . . . . . . 8
β’ (π β β β
β) |
9 | 8 | sselda 3949 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β π¦ β β) |
10 | | itgcoscmulx.a |
. . . . . . . . . . . . . 14
β’ (π β π΄ β β) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β) β π΄ β β) |
12 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β β) β π¦ β β) |
13 | 11, 12 | mulcld 11182 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β (π΄ Β· π¦) β β) |
14 | 13 | sincld 16019 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (sinβ(π΄ Β· π¦)) β β) |
15 | | itgcoscmulx.an0 |
. . . . . . . . . . . 12
β’ (π β π΄ β 0) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β π΄ β 0) |
17 | 14, 11, 16 | divcld 11938 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β ((sinβ(π΄ Β· π¦)) / π΄) β β) |
18 | 9, 17 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β ((sinβ(π΄ Β· π¦)) / π΄) β β) |
19 | 18 | fmpttd 7068 |
. . . . . . . 8
β’ (π β (π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄)):ββΆβ) |
20 | | ssidd 3972 |
. . . . . . . 8
β’ (π β β β
β) |
21 | | eqid 2737 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
22 | | tgioo4 43885 |
. . . . . . . . 9
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
23 | 21, 22 | dvres 25291 |
. . . . . . . 8
β’
(((β β β β§ (π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄)):ββΆβ) β§ (β
β β β§ (π΅[,]πΆ) β β)) β (β D
((π¦ β β β¦
((sinβ(π΄ Β·
π¦)) / π΄)) βΎ (π΅[,]πΆ))) = ((β D (π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄))) βΎ ((intβ(topGenβran
(,)))β(π΅[,]πΆ)))) |
24 | 8, 19, 20, 3, 23 | syl22anc 838 |
. . . . . . 7
β’ (π β (β D ((π¦ β β β¦
((sinβ(π΄ Β·
π¦)) / π΄)) βΎ (π΅[,]πΆ))) = ((β D (π¦ β β β¦ ((sinβ(π΄ Β· π¦)) / π΄))) βΎ ((intβ(topGenβran
(,)))β(π΅[,]πΆ)))) |
25 | | reelprrecn 11150 |
. . . . . . . . . . 11
β’ β
β {β, β} |
26 | 25 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β {β,
β}) |
27 | 9, 14 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (sinβ(π΄ Β· π¦)) β β) |
28 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β π΄ β β) |
29 | 28, 9 | mulcld 11182 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β β) β (π΄ Β· π¦) β β) |
30 | 29 | coscld 16020 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β β) β (cosβ(π΄ Β· π¦)) β β) |
31 | 28, 30 | mulcld 11182 |
. . . . . . . . . 10
β’ ((π β§ π¦ β β) β (π΄ Β· (cosβ(π΄ Β· π¦))) β β) |
32 | 8 | resmptd 5999 |
. . . . . . . . . . . . 13
β’ (π β ((π¦ β β β¦ (sinβ(π΄ Β· π¦))) βΎ β) = (π¦ β β β¦ (sinβ(π΄ Β· π¦)))) |
33 | 32 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (π β (π¦ β β β¦ (sinβ(π΄ Β· π¦))) = ((π¦ β β β¦ (sinβ(π΄ Β· π¦))) βΎ β)) |
34 | 33 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π β (β D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = (β D ((π¦ β β β¦
(sinβ(π΄ Β·
π¦))) βΎ
β))) |
35 | 14 | fmpttd 7068 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β β β¦ (sinβ(π΄ Β· π¦))):ββΆβ) |
36 | | ssidd 3972 |
. . . . . . . . . . . . 13
β’ (π β β β
β) |
37 | | dvsinax 44228 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β (β
D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
38 | 10, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (β D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
39 | 38 | dmeqd 5866 |
. . . . . . . . . . . . . . 15
β’ (π β dom (β D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = dom (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
40 | 13 | coscld 16020 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β β) β (cosβ(π΄ Β· π¦)) β β) |
41 | 11, 40 | mulcld 11182 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β β) β (π΄ Β· (cosβ(π΄ Β· π¦))) β β) |
42 | 41 | ralrimiva 3144 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ¦ β β (π΄ Β· (cosβ(π΄ Β· π¦))) β β) |
43 | | dmmptg 6199 |
. . . . . . . . . . . . . . . 16
β’
(βπ¦ β
β (π΄ Β·
(cosβ(π΄ Β·
π¦))) β β β
dom (π¦ β β
β¦ (π΄ Β·
(cosβ(π΄ Β·
π¦)))) =
β) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β dom (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦)))) = β) |
45 | 39, 44 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
β’ (π β β = dom (β D
(π¦ β β β¦
(sinβ(π΄ Β·
π¦))))) |
46 | 7, 45 | sseqtrid 4001 |
. . . . . . . . . . . . 13
β’ (π β β β dom
(β D (π¦ β
β β¦ (sinβ(π΄ Β· π¦))))) |
47 | | dvres3 25293 |
. . . . . . . . . . . . 13
β’
(((β β {β, β} β§ (π¦ β β β¦ (sinβ(π΄ Β· π¦))):ββΆβ) β§ (β
β β β§ β β dom (β D (π¦ β β β¦ (sinβ(π΄ Β· π¦)))))) β (β D ((π¦ β β β¦ (sinβ(π΄ Β· π¦))) βΎ β)) = ((β D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) βΎ
β)) |
48 | 26, 35, 36, 46, 47 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (π β (β D ((π¦ β β β¦
(sinβ(π΄ Β·
π¦))) βΎ β)) =
((β D (π¦ β
β β¦ (sinβ(π΄ Β· π¦)))) βΎ β)) |
49 | 38 | reseq1d 5941 |
. . . . . . . . . . . 12
β’ (π β ((β D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) βΎ β) =
((π¦ β β β¦
(π΄ Β·
(cosβ(π΄ Β·
π¦)))) βΎ
β)) |
50 | 8 | resmptd 5999 |
. . . . . . . . . . . 12
β’ (π β ((π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦)))) βΎ β) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
51 | 48, 49, 50 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ (π β (β D ((π¦ β β β¦
(sinβ(π΄ Β·
π¦))) βΎ β)) =
(π¦ β β β¦
(π΄ Β·
(cosβ(π΄ Β·
π¦))))) |
52 | 34, 51 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π β (β D (π¦ β β β¦
(sinβ(π΄ Β·
π¦)))) = (π¦ β β β¦ (π΄ Β· (cosβ(π΄ Β· π¦))))) |
53 | 26, 27, 31, 52, 10, 15 | dvmptdivc 25345 |
. . . . . . . . 9
β’ (π β (β D (π¦ β β β¦
((sinβ(π΄ Β·
π¦)) / π΄))) = (π¦ β β β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄))) |
54 | | iccntr 24200 |
. . . . . . . . . 10
β’ ((π΅ β β β§ πΆ β β) β
((intβ(topGenβran (,)))β(π΅[,]πΆ)) = (π΅(,)πΆ)) |
55 | 1, 2, 54 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
((intβ(topGenβran (,)))β(π΅[,]πΆ)) = (π΅(,)πΆ)) |
56 | 53, 55 | reseq12d 5943 |
. . . . . . . 8
β’ (π β ((β D (π¦ β β β¦
((sinβ(π΄ Β·
π¦)) / π΄))) βΎ ((intβ(topGenβran
(,)))β(π΅[,]πΆ))) = ((π¦ β β β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄)) βΎ (π΅(,)πΆ))) |
57 | | ioossre 13332 |
. . . . . . . . 9
β’ (π΅(,)πΆ) β β |
58 | | resmpt 5996 |
. . . . . . . . 9
β’ ((π΅(,)πΆ) β β β ((π¦ β β β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄)) βΎ (π΅(,)πΆ)) = (π¦ β (π΅(,)πΆ) β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄))) |
59 | 57, 58 | mp1i 13 |
. . . . . . . 8
β’ (π β ((π¦ β β β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄)) βΎ (π΅(,)πΆ)) = (π¦ β (π΅(,)πΆ) β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄))) |
60 | | elioore 13301 |
. . . . . . . . . . . 12
β’ (π¦ β (π΅(,)πΆ) β π¦ β β) |
61 | 60 | recnd 11190 |
. . . . . . . . . . 11
β’ (π¦ β (π΅(,)πΆ) β π¦ β β) |
62 | 61, 40 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΅(,)πΆ)) β (cosβ(π΄ Β· π¦)) β β) |
63 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΅(,)πΆ)) β π΄ β β) |
64 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΅(,)πΆ)) β π΄ β 0) |
65 | 62, 63, 64 | divcan3d 11943 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΅(,)πΆ)) β ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄) = (cosβ(π΄ Β· π¦))) |
66 | 65 | mpteq2dva 5210 |
. . . . . . . 8
β’ (π β (π¦ β (π΅(,)πΆ) β¦ ((π΄ Β· (cosβ(π΄ Β· π¦))) / π΄)) = (π¦ β (π΅(,)πΆ) β¦ (cosβ(π΄ Β· π¦)))) |
67 | 56, 59, 66 | 3eqtrd 2781 |
. . . . . . 7
β’ (π β ((β D (π¦ β β β¦
((sinβ(π΄ Β·
π¦)) / π΄))) βΎ ((intβ(topGenβran
(,)))β(π΅[,]πΆ))) = (π¦ β (π΅(,)πΆ) β¦ (cosβ(π΄ Β· π¦)))) |
68 | 6, 24, 67 | 3eqtrd 2781 |
. . . . . 6
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) = (π¦ β (π΅(,)πΆ) β¦ (cosβ(π΄ Β· π¦)))) |
69 | 68 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) = (π¦ β (π΅(,)πΆ) β¦ (cosβ(π΄ Β· π¦)))) |
70 | | oveq2 7370 |
. . . . . . 7
β’ (π¦ = π₯ β (π΄ Β· π¦) = (π΄ Β· π₯)) |
71 | 70 | fveq2d 6851 |
. . . . . 6
β’ (π¦ = π₯ β (cosβ(π΄ Β· π¦)) = (cosβ(π΄ Β· π₯))) |
72 | 71 | adantl 483 |
. . . . 5
β’ (((π β§ π₯ β (π΅(,)πΆ)) β§ π¦ = π₯) β (cosβ(π΄ Β· π¦)) = (cosβ(π΄ Β· π₯))) |
73 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π₯ β (π΅(,)πΆ)) |
74 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π΄ β β) |
75 | 57, 8 | sstrid 3960 |
. . . . . . . 8
β’ (π β (π΅(,)πΆ) β β) |
76 | 75 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅(,)πΆ)) β π₯ β β) |
77 | 74, 76 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (π΄ Β· π₯) β β) |
78 | 77 | coscld 16020 |
. . . . 5
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (cosβ(π΄ Β· π₯)) β β) |
79 | 69, 72, 73, 78 | fvmptd 6960 |
. . . 4
β’ ((π β§ π₯ β (π΅(,)πΆ)) β ((β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)))βπ₯) = (cosβ(π΄ Β· π₯))) |
80 | 79 | eqcomd 2743 |
. . 3
β’ ((π β§ π₯ β (π΅(,)πΆ)) β (cosβ(π΄ Β· π₯)) = ((β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)))βπ₯)) |
81 | 80 | itgeq2dv 25162 |
. 2
β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = β«(π΅(,)πΆ)((β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)))βπ₯) dπ₯) |
82 | | eqidd 2738 |
. . . . 5
β’ (π β (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)) = (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) |
83 | | oveq2 7370 |
. . . . . . . 8
β’ (π¦ = πΆ β (π΄ Β· π¦) = (π΄ Β· πΆ)) |
84 | 83 | fveq2d 6851 |
. . . . . . 7
β’ (π¦ = πΆ β (sinβ(π΄ Β· π¦)) = (sinβ(π΄ Β· πΆ))) |
85 | 84 | oveq1d 7377 |
. . . . . 6
β’ (π¦ = πΆ β ((sinβ(π΄ Β· π¦)) / π΄) = ((sinβ(π΄ Β· πΆ)) / π΄)) |
86 | 85 | adantl 483 |
. . . . 5
β’ ((π β§ π¦ = πΆ) β ((sinβ(π΄ Β· π¦)) / π΄) = ((sinβ(π΄ Β· πΆ)) / π΄)) |
87 | 1 | rexrd 11212 |
. . . . . 6
β’ (π β π΅ β
β*) |
88 | 2 | rexrd 11212 |
. . . . . 6
β’ (π β πΆ β
β*) |
89 | | itgcoscmulx.blec |
. . . . . 6
β’ (π β π΅ β€ πΆ) |
90 | | ubicc2 13389 |
. . . . . 6
β’ ((π΅ β β*
β§ πΆ β
β* β§ π΅
β€ πΆ) β πΆ β (π΅[,]πΆ)) |
91 | 87, 88, 89, 90 | syl3anc 1372 |
. . . . 5
β’ (π β πΆ β (π΅[,]πΆ)) |
92 | 2 | recnd 11190 |
. . . . . . . 8
β’ (π β πΆ β β) |
93 | 10, 92 | mulcld 11182 |
. . . . . . 7
β’ (π β (π΄ Β· πΆ) β β) |
94 | 93 | sincld 16019 |
. . . . . 6
β’ (π β (sinβ(π΄ Β· πΆ)) β β) |
95 | 94, 10, 15 | divcld 11938 |
. . . . 5
β’ (π β ((sinβ(π΄ Β· πΆ)) / π΄) β β) |
96 | 82, 86, 91, 95 | fvmptd 6960 |
. . . 4
β’ (π β ((π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))βπΆ) = ((sinβ(π΄ Β· πΆ)) / π΄)) |
97 | | oveq2 7370 |
. . . . . . . 8
β’ (π¦ = π΅ β (π΄ Β· π¦) = (π΄ Β· π΅)) |
98 | 97 | fveq2d 6851 |
. . . . . . 7
β’ (π¦ = π΅ β (sinβ(π΄ Β· π¦)) = (sinβ(π΄ Β· π΅))) |
99 | 98 | oveq1d 7377 |
. . . . . 6
β’ (π¦ = π΅ β ((sinβ(π΄ Β· π¦)) / π΄) = ((sinβ(π΄ Β· π΅)) / π΄)) |
100 | 99 | adantl 483 |
. . . . 5
β’ ((π β§ π¦ = π΅) β ((sinβ(π΄ Β· π¦)) / π΄) = ((sinβ(π΄ Β· π΅)) / π΄)) |
101 | | lbicc2 13388 |
. . . . . 6
β’ ((π΅ β β*
β§ πΆ β
β* β§ π΅
β€ πΆ) β π΅ β (π΅[,]πΆ)) |
102 | 87, 88, 89, 101 | syl3anc 1372 |
. . . . 5
β’ (π β π΅ β (π΅[,]πΆ)) |
103 | 1 | recnd 11190 |
. . . . . . . 8
β’ (π β π΅ β β) |
104 | 10, 103 | mulcld 11182 |
. . . . . . 7
β’ (π β (π΄ Β· π΅) β β) |
105 | 104 | sincld 16019 |
. . . . . 6
β’ (π β (sinβ(π΄ Β· π΅)) β β) |
106 | 105, 10, 15 | divcld 11938 |
. . . . 5
β’ (π β ((sinβ(π΄ Β· π΅)) / π΄) β β) |
107 | 82, 100, 102, 106 | fvmptd 6960 |
. . . 4
β’ (π β ((π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))βπ΅) = ((sinβ(π΄ Β· π΅)) / π΄)) |
108 | 96, 107 | oveq12d 7380 |
. . 3
β’ (π β (((π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))βπΆ) β ((π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))βπ΅)) = (((sinβ(π΄ Β· πΆ)) / π΄) β ((sinβ(π΄ Β· π΅)) / π΄))) |
109 | | coscn 25820 |
. . . . . . 7
β’ cos
β (ββcnββ) |
110 | 109 | a1i 11 |
. . . . . 6
β’ (π β cos β
(ββcnββ)) |
111 | 75, 10, 36 | constcncfg 44187 |
. . . . . . 7
β’ (π β (π¦ β (π΅(,)πΆ) β¦ π΄) β ((π΅(,)πΆ)βcnββ)) |
112 | 75, 36 | idcncfg 44188 |
. . . . . . 7
β’ (π β (π¦ β (π΅(,)πΆ) β¦ π¦) β ((π΅(,)πΆ)βcnββ)) |
113 | 111, 112 | mulcncf 24826 |
. . . . . 6
β’ (π β (π¦ β (π΅(,)πΆ) β¦ (π΄ Β· π¦)) β ((π΅(,)πΆ)βcnββ)) |
114 | 110, 113 | cncfmpt1f 24293 |
. . . . 5
β’ (π β (π¦ β (π΅(,)πΆ) β¦ (cosβ(π΄ Β· π¦))) β ((π΅(,)πΆ)βcnββ)) |
115 | 68, 114 | eqeltrd 2838 |
. . . 4
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) β ((π΅(,)πΆ)βcnββ)) |
116 | | ioossicc 13357 |
. . . . . . 7
β’ (π΅(,)πΆ) β (π΅[,]πΆ) |
117 | 116 | a1i 11 |
. . . . . 6
β’ (π β (π΅(,)πΆ) β (π΅[,]πΆ)) |
118 | | ioombl 24945 |
. . . . . . 7
β’ (π΅(,)πΆ) β dom vol |
119 | 118 | a1i 11 |
. . . . . 6
β’ (π β (π΅(,)πΆ) β dom vol) |
120 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΅[,]πΆ)) β π΄ β β) |
121 | 3, 7 | sstrdi 3961 |
. . . . . . . . 9
β’ (π β (π΅[,]πΆ) β β) |
122 | 121 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΅[,]πΆ)) β π¦ β β) |
123 | 120, 122 | mulcld 11182 |
. . . . . . 7
β’ ((π β§ π¦ β (π΅[,]πΆ)) β (π΄ Β· π¦) β β) |
124 | 123 | coscld 16020 |
. . . . . 6
β’ ((π β§ π¦ β (π΅[,]πΆ)) β (cosβ(π΄ Β· π¦)) β β) |
125 | 121, 10, 36 | constcncfg 44187 |
. . . . . . . . 9
β’ (π β (π¦ β (π΅[,]πΆ) β¦ π΄) β ((π΅[,]πΆ)βcnββ)) |
126 | 121, 36 | idcncfg 44188 |
. . . . . . . . 9
β’ (π β (π¦ β (π΅[,]πΆ) β¦ π¦) β ((π΅[,]πΆ)βcnββ)) |
127 | 125, 126 | mulcncf 24826 |
. . . . . . . 8
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (π΄ Β· π¦)) β ((π΅[,]πΆ)βcnββ)) |
128 | 110, 127 | cncfmpt1f 24293 |
. . . . . . 7
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (cosβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) |
129 | | cniccibl 25221 |
. . . . . . 7
β’ ((π΅ β β β§ πΆ β β β§ (π¦ β (π΅[,]πΆ) β¦ (cosβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) β (π¦ β (π΅[,]πΆ) β¦ (cosβ(π΄ Β· π¦))) β
πΏ1) |
130 | 1, 2, 128, 129 | syl3anc 1372 |
. . . . . 6
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (cosβ(π΄ Β· π¦))) β
πΏ1) |
131 | 117, 119,
124, 130 | iblss 25185 |
. . . . 5
β’ (π β (π¦ β (π΅(,)πΆ) β¦ (cosβ(π΄ Β· π¦))) β
πΏ1) |
132 | 68, 131 | eqeltrd 2838 |
. . . 4
β’ (π β (β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))) β
πΏ1) |
133 | | sincn 25819 |
. . . . . . 7
β’ sin
β (ββcnββ) |
134 | 133 | a1i 11 |
. . . . . 6
β’ (π β sin β
(ββcnββ)) |
135 | 134, 127 | cncfmpt1f 24293 |
. . . . 5
β’ (π β (π¦ β (π΅[,]πΆ) β¦ (sinβ(π΄ Β· π¦))) β ((π΅[,]πΆ)βcnββ)) |
136 | | neneq 2950 |
. . . . . . . 8
β’ (π΄ β 0 β Β¬ π΄ = 0) |
137 | | elsni 4608 |
. . . . . . . . 9
β’ (π΄ β {0} β π΄ = 0) |
138 | 137 | con3i 154 |
. . . . . . . 8
β’ (Β¬
π΄ = 0 β Β¬ π΄ β {0}) |
139 | 15, 136, 138 | 3syl 18 |
. . . . . . 7
β’ (π β Β¬ π΄ β {0}) |
140 | 10, 139 | eldifd 3926 |
. . . . . 6
β’ (π β π΄ β (β β
{0})) |
141 | | difssd 4097 |
. . . . . 6
β’ (π β (β β {0})
β β) |
142 | 121, 140,
141 | constcncfg 44187 |
. . . . 5
β’ (π β (π¦ β (π΅[,]πΆ) β¦ π΄) β ((π΅[,]πΆ)βcnβ(β β {0}))) |
143 | 135, 142 | divcncf 24827 |
. . . 4
β’ (π β (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)) β ((π΅[,]πΆ)βcnββ)) |
144 | 1, 2, 89, 115, 132, 143 | ftc2 25424 |
. . 3
β’ (π β β«(π΅(,)πΆ)((β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)))βπ₯) dπ₯ = (((π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))βπΆ) β ((π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄))βπ΅))) |
145 | 94, 105, 10, 15 | divsubdird 11977 |
. . 3
β’ (π β (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄) = (((sinβ(π΄ Β· πΆ)) / π΄) β ((sinβ(π΄ Β· π΅)) / π΄))) |
146 | 108, 144,
145 | 3eqtr4d 2787 |
. 2
β’ (π β β«(π΅(,)πΆ)((β D (π¦ β (π΅[,]πΆ) β¦ ((sinβ(π΄ Β· π¦)) / π΄)))βπ₯) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) |
147 | 81, 146 | eqtrd 2777 |
1
β’ (π β β«(π΅(,)πΆ)(cosβ(π΄ Β· π₯)) dπ₯ = (((sinβ(π΄ Β· πΆ)) β (sinβ(π΄ Β· π΅))) / π΄)) |