Step | Hyp | Ref
| Expression |
1 | | mulcl 11143 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β β) β (π΄ Β· π₯) β β) |
2 | | eqidd 2734 |
. . . . . 6
β’ (π΄ β β β (π₯ β β β¦ (π΄ Β· π₯)) = (π₯ β β β¦ (π΄ Β· π₯))) |
3 | | cosf 16015 |
. . . . . . . 8
β’
cos:ββΆβ |
4 | 3 | a1i 11 |
. . . . . . 7
β’ (π΄ β β β
cos:ββΆβ) |
5 | 4 | feqmptd 6914 |
. . . . . 6
β’ (π΄ β β β cos =
(π¦ β β β¦
(cosβπ¦))) |
6 | | fveq2 6846 |
. . . . . 6
β’ (π¦ = (π΄ Β· π₯) β (cosβπ¦) = (cosβ(π΄ Β· π₯))) |
7 | 1, 2, 5, 6 | fmptco 7079 |
. . . . 5
β’ (π΄ β β β (cos
β (π₯ β β
β¦ (π΄ Β· π₯))) = (π₯ β β β¦ (cosβ(π΄ Β· π₯)))) |
8 | 7 | eqcomd 2739 |
. . . 4
β’ (π΄ β β β (π₯ β β β¦
(cosβ(π΄ Β·
π₯))) = (cos β (π₯ β β β¦ (π΄ Β· π₯)))) |
9 | 8 | oveq2d 7377 |
. . 3
β’ (π΄ β β β (β
D (π₯ β β β¦
(cosβ(π΄ Β·
π₯)))) = (β D (cos
β (π₯ β β
β¦ (π΄ Β· π₯))))) |
10 | | cnelprrecn 11152 |
. . . . 5
β’ β
β {β, β} |
11 | 10 | a1i 11 |
. . . 4
β’ (π΄ β β β β
β {β, β}) |
12 | 1 | fmpttd 7067 |
. . . 4
β’ (π΄ β β β (π₯ β β β¦ (π΄ Β· π₯)):ββΆβ) |
13 | | dvcos 25370 |
. . . . . . 7
β’ (β
D cos) = (π₯ β β
β¦ -(sinβπ₯)) |
14 | 13 | dmeqi 5864 |
. . . . . 6
β’ dom
(β D cos) = dom (π₯
β β β¦ -(sinβπ₯)) |
15 | | dmmptg 6198 |
. . . . . . 7
β’
(βπ₯ β
β -(sinβπ₯)
β β β dom (π₯ β β β¦ -(sinβπ₯)) = β) |
16 | | sincl 16016 |
. . . . . . . 8
β’ (π₯ β β β
(sinβπ₯) β
β) |
17 | 16 | negcld 11507 |
. . . . . . 7
β’ (π₯ β β β
-(sinβπ₯) β
β) |
18 | 15, 17 | mprg 3067 |
. . . . . 6
β’ dom
(π₯ β β β¦
-(sinβπ₯)) =
β |
19 | 14, 18 | eqtri 2761 |
. . . . 5
β’ dom
(β D cos) = β |
20 | 19 | a1i 11 |
. . . 4
β’ (π΄ β β β dom
(β D cos) = β) |
21 | | simpl 484 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β) β π΄ β
β) |
22 | | 0red 11166 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β) β 0 β
β) |
23 | | id 22 |
. . . . . . . 8
β’ (π΄ β β β π΄ β
β) |
24 | 11, 23 | dvmptc 25345 |
. . . . . . 7
β’ (π΄ β β β (β
D (π₯ β β β¦
π΄)) = (π₯ β β β¦ 0)) |
25 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β) β π₯ β
β) |
26 | | 1red 11164 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β) β 1 β
β) |
27 | 11 | dvmptid 25344 |
. . . . . . 7
β’ (π΄ β β β (β
D (π₯ β β β¦
π₯)) = (π₯ β β β¦ 1)) |
28 | 11, 21, 22, 24, 25, 26, 27 | dvmptmul 25348 |
. . . . . 6
β’ (π΄ β β β (β
D (π₯ β β β¦
(π΄ Β· π₯))) = (π₯ β β β¦ ((0 Β· π₯) + (1 Β· π΄)))) |
29 | 28 | dmeqd 5865 |
. . . . 5
β’ (π΄ β β β dom
(β D (π₯ β
β β¦ (π΄ Β·
π₯))) = dom (π₯ β β β¦ ((0
Β· π₯) + (1 Β·
π΄)))) |
30 | | dmmptg 6198 |
. . . . . 6
β’
(βπ₯ β
β ((0 Β· π₯) +
(1 Β· π΄)) β V
β dom (π₯ β
β β¦ ((0 Β· π₯) + (1 Β· π΄))) = β) |
31 | | ovex 7394 |
. . . . . . 7
β’ ((0
Β· π₯) + (1 Β·
π΄)) β
V |
32 | 31 | a1i 11 |
. . . . . 6
β’ (π₯ β β β ((0
Β· π₯) + (1 Β·
π΄)) β
V) |
33 | 30, 32 | mprg 3067 |
. . . . 5
β’ dom
(π₯ β β β¦
((0 Β· π₯) + (1
Β· π΄))) =
β |
34 | 29, 33 | eqtrdi 2789 |
. . . 4
β’ (π΄ β β β dom
(β D (π₯ β
β β¦ (π΄ Β·
π₯))) =
β) |
35 | 11, 11, 4, 12, 20, 34 | dvcof 25335 |
. . 3
β’ (π΄ β β β (β
D (cos β (π₯ β
β β¦ (π΄ Β·
π₯)))) = (((β D cos)
β (π₯ β β
β¦ (π΄ Β· π₯))) βf Β·
(β D (π₯ β
β β¦ (π΄ Β·
π₯))))) |
36 | | dvcos 25370 |
. . . . . . 7
β’ (β
D cos) = (π¦ β β
β¦ -(sinβπ¦)) |
37 | 36 | a1i 11 |
. . . . . 6
β’ (π΄ β β β (β
D cos) = (π¦ β β
β¦ -(sinβπ¦))) |
38 | | fveq2 6846 |
. . . . . . 7
β’ (π¦ = (π΄ Β· π₯) β (sinβπ¦) = (sinβ(π΄ Β· π₯))) |
39 | 38 | negeqd 11403 |
. . . . . 6
β’ (π¦ = (π΄ Β· π₯) β -(sinβπ¦) = -(sinβ(π΄ Β· π₯))) |
40 | 1, 2, 37, 39 | fmptco 7079 |
. . . . 5
β’ (π΄ β β β ((β
D cos) β (π₯ β
β β¦ (π΄ Β·
π₯))) = (π₯ β β β¦ -(sinβ(π΄ Β· π₯)))) |
41 | 40 | oveq1d 7376 |
. . . 4
β’ (π΄ β β β
(((β D cos) β (π₯ β β β¦ (π΄ Β· π₯))) βf Β· (β D
(π₯ β β β¦
(π΄ Β· π₯)))) = ((π₯ β β β¦ -(sinβ(π΄ Β· π₯))) βf Β· (β D
(π₯ β β β¦
(π΄ Β· π₯))))) |
42 | | cnex 11140 |
. . . . . . 7
β’ β
β V |
43 | 42 | mptex 7177 |
. . . . . 6
β’ (π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) β
V |
44 | | ovex 7394 |
. . . . . 6
β’ (β
D (π₯ β β β¦
(π΄ Β· π₯))) β V |
45 | | offval3 7919 |
. . . . . 6
β’ (((π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) β V β§
(β D (π₯ β
β β¦ (π΄ Β·
π₯))) β V) β
((π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) βf
Β· (β D (π₯
β β β¦ (π΄
Β· π₯)))) = (π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯)))) β¦ (((π₯ β β β¦ -(sinβ(π΄ Β· π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦)))) |
46 | 43, 44, 45 | mp2an 691 |
. . . . 5
β’ ((π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) βf
Β· (β D (π₯
β β β¦ (π΄
Β· π₯)))) = (π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯)))) β¦ (((π₯ β β β¦ -(sinβ(π΄ Β· π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦))) |
47 | 46 | a1i 11 |
. . . 4
β’ (π΄ β β β ((π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) βf
Β· (β D (π₯
β β β¦ (π΄
Β· π₯)))) = (π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯)))) β¦ (((π₯ β β β¦ -(sinβ(π΄ Β· π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦)))) |
48 | 1 | sincld 16020 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π₯ β β) β
(sinβ(π΄ Β·
π₯)) β
β) |
49 | 48 | negcld 11507 |
. . . . . . . . 9
β’ ((π΄ β β β§ π₯ β β) β
-(sinβ(π΄ Β·
π₯)) β
β) |
50 | 49 | ralrimiva 3140 |
. . . . . . . 8
β’ (π΄ β β β
βπ₯ β β
-(sinβ(π΄ Β·
π₯)) β
β) |
51 | | dmmptg 6198 |
. . . . . . . 8
β’
(βπ₯ β
β -(sinβ(π΄
Β· π₯)) β β
β dom (π₯ β
β β¦ -(sinβ(π΄ Β· π₯))) = β) |
52 | 50, 51 | syl 17 |
. . . . . . 7
β’ (π΄ β β β dom
(π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) =
β) |
53 | 52, 34 | ineq12d 4177 |
. . . . . 6
β’ (π΄ β β β (dom
(π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) β© dom (β D
(π₯ β β β¦
(π΄ Β· π₯)))) = (β β©
β)) |
54 | | inidm 4182 |
. . . . . 6
β’ (β
β© β) = β |
55 | 53, 54 | eqtrdi 2789 |
. . . . 5
β’ (π΄ β β β (dom
(π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) β© dom (β D
(π₯ β β β¦
(π΄ Β· π₯)))) = β) |
56 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯))))) β π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯))))) |
57 | 55 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯))))) β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯)))) = β) |
58 | 56, 57 | eleqtrd 2836 |
. . . . . 6
β’ ((π΄ β β β§ π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯))))) β π¦ β β) |
59 | | eqidd 2734 |
. . . . . . . . . 10
β’ (π¦ β β β (π₯ β β β¦
-(sinβ(π΄ Β·
π₯))) = (π₯ β β β¦ -(sinβ(π΄ Β· π₯)))) |
60 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (π΄ Β· π₯) = (π΄ Β· π¦)) |
61 | 60 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (sinβ(π΄ Β· π₯)) = (sinβ(π΄ Β· π¦))) |
62 | 61 | negeqd 11403 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β -(sinβ(π΄ Β· π₯)) = -(sinβ(π΄ Β· π¦))) |
63 | 62 | adantl 483 |
. . . . . . . . . 10
β’ ((π¦ β β β§ π₯ = π¦) β -(sinβ(π΄ Β· π₯)) = -(sinβ(π΄ Β· π¦))) |
64 | | id 22 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β
β) |
65 | | negex 11407 |
. . . . . . . . . . 11
β’
-(sinβ(π΄
Β· π¦)) β
V |
66 | 65 | a1i 11 |
. . . . . . . . . 10
β’ (π¦ β β β
-(sinβ(π΄ Β·
π¦)) β
V) |
67 | 59, 63, 64, 66 | fvmptd 6959 |
. . . . . . . . 9
β’ (π¦ β β β ((π₯ β β β¦
-(sinβ(π΄ Β·
π₯)))βπ¦) = -(sinβ(π΄ Β· π¦))) |
68 | 67 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β β β§ π¦ β β) β ((π₯ β β β¦
-(sinβ(π΄ Β·
π₯)))βπ¦) = -(sinβ(π΄ Β· π¦))) |
69 | 28 | adantr 482 |
. . . . . . . . 9
β’ ((π΄ β β β§ π¦ β β) β (β
D (π₯ β β β¦
(π΄ Β· π₯))) = (π₯ β β β¦ ((0 Β· π₯) + (1 Β· π΄)))) |
70 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (0 Β· π₯) = (0 Β· π¦)) |
71 | 70 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((0 Β· π₯) + (1 Β· π΄)) = ((0 Β· π¦) + (1 Β· π΄))) |
72 | | mul02 11341 |
. . . . . . . . . . . 12
β’ (π¦ β β β (0
Β· π¦) =
0) |
73 | | mulid2 11162 |
. . . . . . . . . . . 12
β’ (π΄ β β β (1
Β· π΄) = π΄) |
74 | 72, 73 | oveqan12rd 7381 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β β) β ((0
Β· π¦) + (1 Β·
π΄)) = (0 + π΄)) |
75 | | addid2 11346 |
. . . . . . . . . . . 12
β’ (π΄ β β β (0 +
π΄) = π΄) |
76 | 75 | adantr 482 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π¦ β β) β (0 +
π΄) = π΄) |
77 | 74, 76 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β ((0
Β· π¦) + (1 Β·
π΄)) = π΄) |
78 | 71, 77 | sylan9eqr 2795 |
. . . . . . . . 9
β’ (((π΄ β β β§ π¦ β β) β§ π₯ = π¦) β ((0 Β· π₯) + (1 Β· π΄)) = π΄) |
79 | | simpr 486 |
. . . . . . . . 9
β’ ((π΄ β β β§ π¦ β β) β π¦ β
β) |
80 | | simpl 484 |
. . . . . . . . 9
β’ ((π΄ β β β§ π¦ β β) β π΄ β
β) |
81 | 69, 78, 79, 80 | fvmptd 6959 |
. . . . . . . 8
β’ ((π΄ β β β§ π¦ β β) β
((β D (π₯ β
β β¦ (π΄ Β·
π₯)))βπ¦) = π΄) |
82 | 68, 81 | oveq12d 7379 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β β) β (((π₯ β β β¦
-(sinβ(π΄ Β·
π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦)) = (-(sinβ(π΄ Β· π¦)) Β· π΄)) |
83 | | mulcl 11143 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π¦ β β) β (π΄ Β· π¦) β β) |
84 | 83 | sincld 16020 |
. . . . . . . . 9
β’ ((π΄ β β β§ π¦ β β) β
(sinβ(π΄ Β·
π¦)) β
β) |
85 | 84 | negcld 11507 |
. . . . . . . 8
β’ ((π΄ β β β§ π¦ β β) β
-(sinβ(π΄ Β·
π¦)) β
β) |
86 | 85, 80 | mulcomd 11184 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β β) β
(-(sinβ(π΄ Β·
π¦)) Β· π΄) = (π΄ Β· -(sinβ(π΄ Β· π¦)))) |
87 | 82, 86 | eqtrd 2773 |
. . . . . 6
β’ ((π΄ β β β§ π¦ β β) β (((π₯ β β β¦
-(sinβ(π΄ Β·
π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦)) = (π΄ Β· -(sinβ(π΄ Β· π¦)))) |
88 | 58, 87 | syldan 592 |
. . . . 5
β’ ((π΄ β β β§ π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯))))) β (((π₯ β β β¦ -(sinβ(π΄ Β· π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦)) = (π΄ Β· -(sinβ(π΄ Β· π¦)))) |
89 | 55, 88 | mpteq12dva 5198 |
. . . 4
β’ (π΄ β β β (π¦ β (dom (π₯ β β β¦ -(sinβ(π΄ Β· π₯))) β© dom (β D (π₯ β β β¦ (π΄ Β· π₯)))) β¦ (((π₯ β β β¦ -(sinβ(π΄ Β· π₯)))βπ¦) Β· ((β D (π₯ β β β¦ (π΄ Β· π₯)))βπ¦))) = (π¦ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π¦))))) |
90 | 41, 47, 89 | 3eqtrd 2777 |
. . 3
β’ (π΄ β β β
(((β D cos) β (π₯ β β β¦ (π΄ Β· π₯))) βf Β· (β D
(π₯ β β β¦
(π΄ Β· π₯)))) = (π¦ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π¦))))) |
91 | 9, 35, 90 | 3eqtrd 2777 |
. 2
β’ (π΄ β β β (β
D (π₯ β β β¦
(cosβ(π΄ Β·
π₯)))) = (π¦ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π¦))))) |
92 | | oveq2 7369 |
. . . . . 6
β’ (π¦ = π₯ β (π΄ Β· π¦) = (π΄ Β· π₯)) |
93 | 92 | fveq2d 6850 |
. . . . 5
β’ (π¦ = π₯ β (sinβ(π΄ Β· π¦)) = (sinβ(π΄ Β· π₯))) |
94 | 93 | negeqd 11403 |
. . . 4
β’ (π¦ = π₯ β -(sinβ(π΄ Β· π¦)) = -(sinβ(π΄ Β· π₯))) |
95 | 94 | oveq2d 7377 |
. . 3
β’ (π¦ = π₯ β (π΄ Β· -(sinβ(π΄ Β· π¦))) = (π΄ Β· -(sinβ(π΄ Β· π₯)))) |
96 | 95 | cbvmptv 5222 |
. 2
β’ (π¦ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π¦)))) = (π₯ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π₯)))) |
97 | 91, 96 | eqtrdi 2789 |
1
β’ (π΄ β β β (β
D (π₯ β β β¦
(cosβ(π΄ Β·
π₯)))) = (π₯ β β β¦ (π΄ Β· -(sinβ(π΄ Β· π₯))))) |