| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . . 7
⊢ (𝑦 ∈ ℂ ↦
(-(cos‘(𝐴 ·
𝑦)) / 𝐴)) = (𝑦 ∈ ℂ ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)) | 
| 2 |  | itgsincmulx.a | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 3 | 2 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ∈ ℂ) | 
| 4 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) | 
| 5 | 3, 4 | mulcld 11282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) | 
| 6 | 5 | coscld 16168 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) | 
| 7 | 6 | negcld 11608 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -(cos‘(𝐴 · 𝑦)) ∈ ℂ) | 
| 8 |  | itgsincmulx.an0 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 0) | 
| 9 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ≠ 0) | 
| 10 | 7, 3, 9 | divcld 12044 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (-(cos‘(𝐴 · 𝑦)) / 𝐴) ∈ ℂ) | 
| 11 |  | cnelprrecn 11249 | . . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} | 
| 12 | 11 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) | 
| 13 | 5 | sincld 16167 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) | 
| 14 | 13 | negcld 11608 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -(sin‘(𝐴 · 𝑦)) ∈ ℂ) | 
| 15 | 3, 14 | mulcld 11282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · -(sin‘(𝐴 · 𝑦))) ∈ ℂ) | 
| 16 | 15 | negcld 11608 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -(𝐴 · -(sin‘(𝐴 · 𝑦))) ∈ ℂ) | 
| 17 |  | dvcosax 45946 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) | 
| 18 | 2, 17 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(cos‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · -(sin‘(𝐴 · 𝑦))))) | 
| 19 | 12, 6, 15, 18 | dvmptneg 26005 | . . . . . . . . 9
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
-(cos‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ -(𝐴 · -(sin‘(𝐴 · 𝑦))))) | 
| 20 | 12, 7, 16, 19, 2, 8 | dvmptdivc 26004 | . . . . . . . 8
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(-(cos‘(𝐴 ·
𝑦)) / 𝐴))) = (𝑦 ∈ ℂ ↦ (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴))) | 
| 21 | 15, 3, 9 | divnegd 12057 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴)) | 
| 22 | 21 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = -((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴)) | 
| 23 | 14, 3, 9 | divcan3d 12049 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = -(sin‘(𝐴 · 𝑦))) | 
| 24 | 23 | negeqd 11503 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → -((𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = --(sin‘(𝐴 · 𝑦))) | 
| 25 | 13 | negnegd 11612 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → --(sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑦))) | 
| 26 | 22, 24, 25 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴) = (sin‘(𝐴 · 𝑦))) | 
| 27 | 26 | mpteq2dva 5241 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (-(𝐴 · -(sin‘(𝐴 · 𝑦))) / 𝐴)) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) | 
| 28 | 20, 27 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(-(cos‘(𝐴 ·
𝑦)) / 𝐴))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))) | 
| 29 |  | itgsincmulx.b | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 30 |  | itgsincmulx.c | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 31 | 1, 10, 28, 13, 29, 30 | dvmptresicc 25952 | . . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))) | 
| 32 | 31 | fveq1d 6907 | . . . . 5
⊢ (𝜑 → ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) = ((𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))‘𝑥)) | 
| 33 | 32 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) = ((𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))‘𝑥)) | 
| 34 |  | eqidd 2737 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))) | 
| 35 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐴 · 𝑦) = (𝐴 · 𝑥)) | 
| 36 | 35 | fveq2d 6909 | . . . . . 6
⊢ (𝑦 = 𝑥 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑥))) | 
| 37 | 36 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) ∧ 𝑦 = 𝑥) → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝑥))) | 
| 38 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐵(,)𝐶)) | 
| 39 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝐴 ∈ ℂ) | 
| 40 |  | ioosscn 13450 | . . . . . . . 8
⊢ (𝐵(,)𝐶) ⊆ ℂ | 
| 41 | 40, 38 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ℂ) | 
| 42 | 39, 41 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (𝐴 · 𝑥) ∈ ℂ) | 
| 43 | 42 | sincld 16167 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (sin‘(𝐴 · 𝑥)) ∈ ℂ) | 
| 44 | 34, 37, 38, 43 | fvmptd 7022 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → ((𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦)))‘𝑥) = (sin‘(𝐴 · 𝑥))) | 
| 45 | 33, 44 | eqtr2d 2777 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (sin‘(𝐴 · 𝑥)) = ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥)) | 
| 46 | 45 | itgeq2dv 25818 | . 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)(sin‘(𝐴 · 𝑥)) d𝑥 = ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥) | 
| 47 |  | itgsincmulx.blec | . . 3
⊢ (𝜑 → 𝐵 ≤ 𝐶) | 
| 48 |  | sincn 26489 | . . . . . 6
⊢ sin
∈ (ℂ–cn→ℂ) | 
| 49 | 48 | a1i 11 | . . . . 5
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) | 
| 50 | 40 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ ℂ) | 
| 51 |  | ssid 4005 | . . . . . . . 8
⊢ ℂ
⊆ ℂ | 
| 52 | 51 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 53 | 50, 2, 52 | constcncfg 45892 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝐴) ∈ ((𝐵(,)𝐶)–cn→ℂ)) | 
| 54 | 50, 52 | idcncfg 45893 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝑦) ∈ ((𝐵(,)𝐶)–cn→ℂ)) | 
| 55 | 53, 54 | mulcncf 25481 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵(,)𝐶)–cn→ℂ)) | 
| 56 | 49, 55 | cncfmpt1f 24941 | . . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) | 
| 57 | 31, 56 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) | 
| 58 |  | ioossicc 13474 | . . . . . 6
⊢ (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶) | 
| 59 | 58 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶)) | 
| 60 |  | ioombl 25601 | . . . . . 6
⊢ (𝐵(,)𝐶) ∈ dom vol | 
| 61 | 60 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ∈ dom vol) | 
| 62 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝐴 ∈ ℂ) | 
| 63 | 29, 30 | iccssred 13475 | . . . . . . . . 9
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) | 
| 64 |  | ax-resscn 11213 | . . . . . . . . 9
⊢ ℝ
⊆ ℂ | 
| 65 | 63, 64 | sstrdi 3995 | . . . . . . . 8
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℂ) | 
| 66 | 65 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝑦 ∈ ℂ) | 
| 67 | 62, 66 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (𝐴 · 𝑦) ∈ ℂ) | 
| 68 | 67 | sincld 16167 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) | 
| 69 | 65, 2, 52 | constcncfg 45892 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 70 | 65, 52 | idcncfg 45893 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝑦) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 71 | 69, 70 | mulcncf 25481 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 72 | 49, 71 | cncfmpt1f 24941 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 73 |  | cniccibl 25877 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈
𝐿1) | 
| 74 | 29, 30, 72, 73 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈
𝐿1) | 
| 75 | 59, 61, 68, 74 | iblss 25841 | . . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈
𝐿1) | 
| 76 | 31, 75 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) ∈
𝐿1) | 
| 77 |  | coscn 26490 | . . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) | 
| 78 | 77 | a1i 11 | . . . . . 6
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) | 
| 79 | 78, 71 | cncfmpt1f 24941 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 80 | 79 | negcncfg 45901 | . . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ -(cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 81 | 8 | neneqd 2944 | . . . . . . 7
⊢ (𝜑 → ¬ 𝐴 = 0) | 
| 82 |  | elsng 4639 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ {0} ↔ 𝐴 = 0)) | 
| 83 | 2, 82 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐴 ∈ {0} ↔ 𝐴 = 0)) | 
| 84 | 81, 83 | mtbird 325 | . . . . . 6
⊢ (𝜑 → ¬ 𝐴 ∈ {0}) | 
| 85 | 2, 84 | eldifd 3961 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
{0})) | 
| 86 |  | difssd 4136 | . . . . 5
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) | 
| 87 | 65, 85, 86 | constcncfg 45892 | . . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→(ℂ ∖ {0}))) | 
| 88 | 80, 87 | divcncf 25483 | . . 3
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) | 
| 89 | 29, 30, 47, 57, 76, 88 | ftc2 26086 | . 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥 = (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵))) | 
| 90 |  | eqidd 2737 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴)) = (𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))) | 
| 91 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑦 = 𝐶 → (𝐴 · 𝑦) = (𝐴 · 𝐶)) | 
| 92 | 91 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑦 = 𝐶 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝐶))) | 
| 93 | 92 | negeqd 11503 | . . . . . . . 8
⊢ (𝑦 = 𝐶 → -(cos‘(𝐴 · 𝑦)) = -(cos‘(𝐴 · 𝐶))) | 
| 94 | 93 | oveq1d 7447 | . . . . . . 7
⊢ (𝑦 = 𝐶 → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) | 
| 95 | 94 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐶) → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) | 
| 96 | 29 | rexrd 11312 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 97 | 30 | rexrd 11312 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ*) | 
| 98 |  | ubicc2 13506 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐶 ∈ (𝐵[,]𝐶)) | 
| 99 | 96, 97, 47, 98 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐵[,]𝐶)) | 
| 100 |  | ovexd 7467 | . . . . . 6
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐶)) / 𝐴) ∈ V) | 
| 101 | 90, 95, 99, 100 | fvmptd 7022 | . . . . 5
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) | 
| 102 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵)) | 
| 103 | 102 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑦 = 𝐵 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝐵))) | 
| 104 | 103 | negeqd 11503 | . . . . . . . 8
⊢ (𝑦 = 𝐵 → -(cos‘(𝐴 · 𝑦)) = -(cos‘(𝐴 · 𝐵))) | 
| 105 | 104 | oveq1d 7447 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) | 
| 106 | 105 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (-(cos‘(𝐴 · 𝑦)) / 𝐴) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) | 
| 107 |  | lbicc2 13505 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) | 
| 108 | 96, 97, 47, 107 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝐵[,]𝐶)) | 
| 109 |  | ovexd 7467 | . . . . . 6
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐵)) / 𝐴) ∈ V) | 
| 110 | 90, 106, 108, 109 | fvmptd 7022 | . . . . 5
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) | 
| 111 | 101, 110 | oveq12d 7450 | . . . 4
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − (-(cos‘(𝐴 · 𝐵)) / 𝐴))) | 
| 112 | 29 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 113 | 2, 112 | mulcld 11282 | . . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | 
| 114 | 113 | coscld 16168 | . . . . . . 7
⊢ (𝜑 → (cos‘(𝐴 · 𝐵)) ∈ ℂ) | 
| 115 | 114, 2, 8 | divnegd 12057 | . . . . . 6
⊢ (𝜑 → -((cos‘(𝐴 · 𝐵)) / 𝐴) = (-(cos‘(𝐴 · 𝐵)) / 𝐴)) | 
| 116 | 115 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐵)) / 𝐴) = -((cos‘(𝐴 · 𝐵)) / 𝐴)) | 
| 117 | 116 | oveq2d 7448 | . . . 4
⊢ (𝜑 → ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − (-(cos‘(𝐴 · 𝐵)) / 𝐴)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − -((cos‘(𝐴 · 𝐵)) / 𝐴))) | 
| 118 | 30 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 119 | 2, 118 | mulcld 11282 | . . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) | 
| 120 | 119 | coscld 16168 | . . . . . . 7
⊢ (𝜑 → (cos‘(𝐴 · 𝐶)) ∈ ℂ) | 
| 121 | 120 | negcld 11608 | . . . . . 6
⊢ (𝜑 → -(cos‘(𝐴 · 𝐶)) ∈ ℂ) | 
| 122 | 121, 2, 8 | divcld 12044 | . . . . 5
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐶)) / 𝐴) ∈ ℂ) | 
| 123 | 114, 2, 8 | divcld 12044 | . . . . 5
⊢ (𝜑 → ((cos‘(𝐴 · 𝐵)) / 𝐴) ∈ ℂ) | 
| 124 | 122, 123 | subnegd 11628 | . . . 4
⊢ (𝜑 → ((-(cos‘(𝐴 · 𝐶)) / 𝐴) − -((cos‘(𝐴 · 𝐵)) / 𝐴)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) + ((cos‘(𝐴 · 𝐵)) / 𝐴))) | 
| 125 | 111, 117,
124 | 3eqtrd 2780 | . . 3
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = ((-(cos‘(𝐴 · 𝐶)) / 𝐴) + ((cos‘(𝐴 · 𝐵)) / 𝐴))) | 
| 126 | 122, 123 | addcomd 11464 | . . 3
⊢ (𝜑 → ((-(cos‘(𝐴 · 𝐶)) / 𝐴) + ((cos‘(𝐴 · 𝐵)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) / 𝐴) + (-(cos‘(𝐴 · 𝐶)) / 𝐴))) | 
| 127 | 120, 2, 8 | divnegd 12057 | . . . . . 6
⊢ (𝜑 → -((cos‘(𝐴 · 𝐶)) / 𝐴) = (-(cos‘(𝐴 · 𝐶)) / 𝐴)) | 
| 128 | 127 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (-(cos‘(𝐴 · 𝐶)) / 𝐴) = -((cos‘(𝐴 · 𝐶)) / 𝐴)) | 
| 129 | 128 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) + (-(cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) / 𝐴) + -((cos‘(𝐴 · 𝐶)) / 𝐴))) | 
| 130 | 120, 2, 8 | divcld 12044 | . . . . 5
⊢ (𝜑 → ((cos‘(𝐴 · 𝐶)) / 𝐴) ∈ ℂ) | 
| 131 | 123, 130 | negsubd 11627 | . . . 4
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) + -((cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) / 𝐴) − ((cos‘(𝐴 · 𝐶)) / 𝐴))) | 
| 132 | 114, 120,
2, 8 | divsubdird 12083 | . . . . 5
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴) = (((cos‘(𝐴 · 𝐵)) / 𝐴) − ((cos‘(𝐴 · 𝐶)) / 𝐴))) | 
| 133 | 132 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) − ((cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) | 
| 134 | 129, 131,
133 | 3eqtrd 2780 | . . 3
⊢ (𝜑 → (((cos‘(𝐴 · 𝐵)) / 𝐴) + (-(cos‘(𝐴 · 𝐶)) / 𝐴)) = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) | 
| 135 | 125, 126,
134 | 3eqtrd 2780 | . 2
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ (-(cos‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) | 
| 136 | 46, 89, 135 | 3eqtrd 2780 | 1
⊢ (𝜑 → ∫(𝐵(,)𝐶)(sin‘(𝐴 · 𝑥)) d𝑥 = (((cos‘(𝐴 · 𝐵)) − (cos‘(𝐴 · 𝐶))) / 𝐴)) |