Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ ℂ ↦
(-(cos‘(𝐴 ·
𝑦)) / 𝐴)) = (𝑦 ∈ ℂ ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)) |
2 | | itgsincmulx.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ∈ ℂ) |
4 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
5 | 3, 4 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
6 | 5 | coscld 14700 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
7 | 6 | negcld 10258 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -(cos‘(𝐴 · 𝑦)) ∈ ℂ) |
8 | | itgsincmulx.an0 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 0) |
9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ≠ 0) |
10 | 7, 3, 9 | divcld 10680 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (-(cos‘(𝐴 · 𝑦)) / 𝐴) ∈ ℂ) |
11 | | cnelprrecn 9908 |
. . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
13 | 5 | sincld 14699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) |
14 | 13 | negcld 10258 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -(sin‘(𝐴 · 𝑦)) ∈ ℂ) |
15 | 3, 14 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · -(sin‘(𝐴 · 𝑦))) ∈ ℂ) |
16 | 15 | negcld 10258 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -(𝐴 · -(sin‘(𝐴 · 𝑦))) ∈ ℂ) |
17 | | dvcosax 38816 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
18 | 2, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) |
19 | 12, 6, 15, 18 | dvmptneg 23535 |
. . . . . . . . 9
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
-(cos‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ -(𝐴 · -(sin‘(𝐴 · 𝑦))))) |
20 | 12, 7, 16, 19, 2, 8 | dvmptdivc 23534 |
. . . . . . . 8
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(-(cos‘(𝐴 ·
𝑦)) / 𝐴))) = (𝑦 ∈ ℂ ↦ (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴))) |
21 | 15, 3, 9 | divnegd 10693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴)) |
22 | 21 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = -((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴)) |
23 | 14, 3, 9 | divcan3d 10685 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = -(sin‘(𝐴 · 𝑦))) |
24 | 23 | negeqd 10154 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = --(sin‘(𝐴 · 𝑦))) |
25 | 13 | negnegd 10262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → --(sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑦))) |
26 | 22, 24, 25 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = (sin‘(𝐴 · 𝑦))) |
27 | 26 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴)) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) |
28 | 20, 27 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(-(cos‘(𝐴 ·
𝑦)) / 𝐴))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) |
29 | | itgsincmulx.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
30 | | itgsincmulx.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
31 | 1, 10, 28, 13, 29, 30 | dvmptresicc 38809 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))) |
32 | 31 | fveq1d 6105 |
. . . . 5
⊢ (𝜑 → ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) = ((𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))‘𝑥)) |
33 | 32 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) = ((𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))‘𝑥)) |
34 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))) |
35 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐴 · 𝑦) = (𝐴 · 𝑥)) |
36 | 35 | fveq2d 6107 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑥))) |
37 | 36 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) ∧ 𝑦 = 𝑥) → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑥))) |
38 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐵(,)𝐶)) |
39 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝐴 ∈ ℂ) |
40 | | ioosscn 38563 |
. . . . . . . 8
⊢ (𝐵(,)𝐶) ⊆ ℂ |
41 | 40, 38 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ℂ) |
42 | 39, 41 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (𝐴 · 𝑥) ∈ ℂ) |
43 | 42 | sincld 14699 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (sin‘(𝐴 · 𝑥)) ∈ ℂ) |
44 | 34, 37, 38, 43 | fvmptd 6197 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → ((𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))‘𝑥) = (sin‘(𝐴 · 𝑥))) |
45 | 33, 44 | eqtr2d 2645 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (sin‘(𝐴 · 𝑥)) = ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥)) |
46 | 45 | itgeq2dv 23354 |
. 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)(sin‘(𝐴 · 𝑥)) d𝑥 = ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥) |
47 | | itgsincmulx.blec |
. . 3
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
48 | | sincn 24002 |
. . . . . 6
⊢ sin
∈ (ℂ–cn→ℂ) |
49 | 48 | a1i 11 |
. . . . 5
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
50 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ ℂ) |
51 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
52 | 51 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
53 | 50, 2, 52 | constcncfg 38756 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝐴) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
54 | 50, 52 | idcncfg 38757 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝑦) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
55 | 53, 54 | mulcncf 23023 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
56 | 49, 55 | cncfmpt1f 22524 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
57 | 31, 56 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
58 | | ioossicc 12130 |
. . . . . 6
⊢ (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶) |
59 | 58 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶)) |
60 | | ioombl 23140 |
. . . . . 6
⊢ (𝐵(,)𝐶) ∈ dom vol |
61 | 60 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ∈ dom vol) |
62 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝐴 ∈ ℂ) |
63 | 29, 30 | iccssred 38574 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
64 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
65 | 63, 64 | syl6ss 3580 |
. . . . . . . 8
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℂ) |
66 | 65 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝑦 ∈ ℂ) |
67 | 62, 66 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (𝐴 · 𝑦) ∈ ℂ) |
68 | 67 | sincld 14699 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) |
69 | 65, 2, 52 | constcncfg 38756 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
70 | 65, 52 | idcncfg 38757 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝑦) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
71 | 69, 70 | mulcncf 23023 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
72 | 49, 71 | cncfmpt1f 22524 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
73 | | cniccibl 23413 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈
𝐿1) |
74 | 29, 30, 72, 73 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈
𝐿1) |
75 | 59, 61, 68, 74 | iblss 23377 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈
𝐿1) |
76 | 31, 75 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) ∈
𝐿1) |
77 | | coscn 24003 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
78 | 77 | a1i 11 |
. . . . . 6
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
79 | 78, 71 | cncfmpt1f 22524 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
80 | 79 | negcncfg 38766 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ -(cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
81 | 8 | neneqd 2787 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐴 = 0) |
82 | | elsng 4139 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ {0} ↔ 𝐴 = 0)) |
83 | 2, 82 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ {0} ↔ 𝐴 = 0)) |
84 | 81, 83 | mtbird 314 |
. . . . . 6
⊢ (𝜑 → ¬ 𝐴 ∈ {0}) |
85 | 2, 84 | eldifd 3551 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
{0})) |
86 | | difssd 3700 |
. . . . 5
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
87 | 65, 85, 86 | constcncfg 38756 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→(ℂ ∖ {0}))) |
88 | 80, 87 | divcncf 38769 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
89 | 29, 30, 47, 57, 76, 88 | ftc2 23611 |
. 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥 = (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵))) |
90 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)) = (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) |
91 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐶 → (𝐴 · 𝑦) = (𝐴 · 𝐶)) |
92 | 91 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑦 = 𝐶 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝐶))) |
93 | 92 | negeqd 10154 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → -(cos‘(𝐴 · 𝑦)) = -(cos‘(𝐴 · 𝐶))) |
94 | 93 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) |
95 | 94 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐶) → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) |
96 | 29 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
97 | 30 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
98 | | ubicc2 12160 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐶 ∈ (𝐵[,]𝐶)) |
99 | 96, 97, 47, 98 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐵[,]𝐶)) |
100 | | ovex 6577 |
. . . . . . 7
⊢
(-(cos‘(𝐴
· 𝐶)) / 𝐴) ∈ V |
101 | 100 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐶)) / 𝐴) ∈ V) |
102 | 90, 95, 99, 101 | fvmptd 6197 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) |
103 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵)) |
104 | 103 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝐵))) |
105 | 104 | negeqd 10154 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → -(cos‘(𝐴 · 𝑦)) = -(cos‘(𝐴 · 𝐵))) |
106 | 105 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) |
107 | 106 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) |
108 | | lbicc2 12159 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) |
109 | 96, 97, 47, 108 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝐵[,]𝐶)) |
110 | | ovex 6577 |
. . . . . . 7
⊢
(-(cos‘(𝐴
· 𝐵)) / 𝐴) ∈ V |
111 | 110 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐵)) / 𝐴) ∈ V) |
112 | 90, 107, 109, 111 | fvmptd 6197 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) |
113 | 102, 112 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − (-(cos‘(𝐴 · 𝐵)) / 𝐴))) |
114 | 29 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
115 | 2, 114 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
116 | 115 | coscld 14700 |
. . . . . . 7
⊢ (𝜑 → (cos‘(𝐴 · 𝐵)) ∈ ℂ) |
117 | 116, 2, 8 | divnegd 10693 |
. . . . . 6
⊢ (𝜑 → -((cos‘(𝐴 · 𝐵)) / 𝐴) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) |
118 | 117 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐵)) / 𝐴) = -((cos‘(𝐴 · 𝐵)) / 𝐴)) |
119 | 118 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − (-(cos‘(𝐴 · 𝐵)) / 𝐴)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − -((cos‘(𝐴 · 𝐵)) / 𝐴))) |
120 | 30 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
121 | 2, 120 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
122 | 121 | coscld 14700 |
. . . . . . 7
⊢ (𝜑 → (cos‘(𝐴 · 𝐶)) ∈ ℂ) |
123 | 122 | negcld 10258 |
. . . . . 6
⊢ (𝜑 → -(cos‘(𝐴 · 𝐶)) ∈ ℂ) |
124 | 123, 2, 8 | divcld 10680 |
. . . . 5
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐶)) / 𝐴) ∈ ℂ) |
125 | 116, 2, 8 | divcld 10680 |
. . . . 5
⊢ (𝜑 → ((cos‘(𝐴 · 𝐵)) / 𝐴) ∈ ℂ) |
126 | 124, 125 | subnegd 10278 |
. . . 4
⊢ (𝜑 → ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − -((cos‘(𝐴 · 𝐵)) / 𝐴)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) + ((cos‘(𝐴 · 𝐵)) / 𝐴))) |
127 | 113, 119,
126 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) + ((cos‘(𝐴 · 𝐵)) / 𝐴))) |
128 | 124, 125 | addcomd 10117 |
. . 3
⊢ (𝜑 → ((-(cos‘(𝐴 · 𝐶)) / 𝐴) + ((cos‘(𝐴 · 𝐵)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) / 𝐴) + (-(cos‘(𝐴 · 𝐶)) / 𝐴))) |
129 | 122, 2, 8 | divnegd 10693 |
. . . . . 6
⊢ (𝜑 → -((cos‘(𝐴 · 𝐶)) / 𝐴) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) |
130 | 129 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐶)) / 𝐴) = -((cos‘(𝐴 · 𝐶)) / 𝐴)) |
131 | 130 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) + (-(cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) / 𝐴) + -((cos‘(𝐴 · 𝐶)) / 𝐴))) |
132 | 122, 2, 8 | divcld 10680 |
. . . . 5
⊢ (𝜑 → ((cos‘(𝐴 · 𝐶)) / 𝐴) ∈ ℂ) |
133 | 125, 132 | negsubd 10277 |
. . . 4
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) + -((cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) / 𝐴) − ((cos‘(𝐴 · 𝐶)) / 𝐴))) |
134 | 116, 122,
2, 8 | divsubdird 10719 |
. . . . 5
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴) = (((cos‘(𝐴 · 𝐵)) / 𝐴) − ((cos‘(𝐴 · 𝐶)) / 𝐴))) |
135 | 134 | eqcomd 2616 |
. . . 4
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) − ((cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) |
136 | 131, 133,
135 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) + (-(cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) |
137 | 127, 128,
136 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) |
138 | 46, 89, 137 | 3eqtrd 2648 |
1
⊢ (𝜑 → ∫(𝐵(,)𝐶)(sin‘(𝐴 · 𝑥)) d𝑥 = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) |