Step | Hyp | Ref
| Expression |
1 | | itgcoscmulx.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
2 | | itgcoscmulx.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
3 | 1, 2 | iccssred 38574 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
4 | 3 | resmptd 5371 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶)) = (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) |
5 | 4 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) = ((𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶))) |
6 | 5 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶)))) |
7 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
9 | 8 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
10 | | itgcoscmulx.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ ℂ) |
11 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ∈ ℂ) |
12 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
13 | 11, 12 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
14 | 13 | sincld 14699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) |
15 | | itgcoscmulx.an0 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≠ 0) |
16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ≠ 0) |
17 | 14, 11, 16 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((sin‘(𝐴 · 𝑦)) / 𝐴) ∈ ℂ) |
18 | 9, 17 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((sin‘(𝐴 · 𝑦)) / 𝐴) ∈ ℂ) |
19 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴)) = (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) |
20 | 18, 19 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)):ℝ⟶ℂ) |
21 | | ssid 3587 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℝ) |
23 | | eqid 2610 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
24 | 23 | tgioo2 22414 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
25 | 23, 24 | dvres 23481 |
. . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)):ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝐵[,]𝐶) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶)))) |
26 | 8, 20, 22, 3, 25 | syl22anc 1319 |
. . . . . . 7
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶)))) |
27 | | reelprrecn 9907 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
29 | 9, 14 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) |
30 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
31 | 30, 9 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐴 · 𝑦) ∈ ℂ) |
32 | 31 | coscld 14700 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
33 | 30, 32 | mulcld 9939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐴 · (cos‘(𝐴 · 𝑦))) ∈ ℂ) |
34 | 8 | resmptd 5371 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘(𝐴 · 𝑦)))) |
35 | 34 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘(𝐴 · 𝑦))) = ((𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) ↾ ℝ)) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(sin‘(𝐴 ·
𝑦)))) = (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) ↾
ℝ))) |
37 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) |
38 | 14, 37 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))):ℂ⟶ℂ) |
39 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ⊆
ℂ) |
41 | | dvsinax 38801 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
42 | 10, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
43 | 42 | dmeqd 5248 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
44 | 13 | coscld 14700 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
45 | 11, 44 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · (cos‘(𝐴 · 𝑦))) ∈ ℂ) |
46 | 45 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑦 ∈ ℂ (𝐴 · (cos‘(𝐴 · 𝑦))) ∈ ℂ) |
47 | | dmmptg 5549 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
ℂ (𝐴 ·
(cos‘(𝐴 ·
𝑦))) ∈ ℂ →
dom (𝑦 ∈ ℂ
↦ (𝐴 ·
(cos‘(𝐴 ·
𝑦)))) =
ℂ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = ℂ) |
49 | 43, 48 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℂ = dom (ℂ D
(𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))))) |
50 | 7, 49 | syl5sseq 3616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑦 ∈
ℂ ↦ (sin‘(𝐴 · 𝑦))))) |
51 | | dvres3 23483 |
. . . . . . . . . . . . 13
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) ↾
ℝ)) |
52 | 28, 38, 40, 50, 51 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) ↾ ℝ)) =
((ℂ D (𝑦 ∈
ℂ ↦ (sin‘(𝐴 · 𝑦)))) ↾ ℝ)) |
53 | 42 | reseq1d 5316 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) ↾ ℝ) =
((𝑦 ∈ ℂ ↦
(𝐴 ·
(cos‘(𝐴 ·
𝑦)))) ↾
ℝ)) |
54 | 8 | resmptd 5371 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
55 | 52, 53, 54 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) ↾ ℝ)) =
(𝑦 ∈ ℝ ↦
(𝐴 ·
(cos‘(𝐴 ·
𝑦))))) |
56 | 36, 55 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℝ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
57 | 28, 29, 33, 56, 10, 15 | dvmptdivc 23534 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴))) = (𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴))) |
58 | | iccntr 22432 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐵[,]𝐶)) = (𝐵(,)𝐶)) |
59 | 1, 2, 58 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐵[,]𝐶)) = (𝐵(,)𝐶)) |
60 | 57, 59 | reseq12d 5318 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶))) = ((𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) ↾ (𝐵(,)𝐶))) |
61 | | ioossre 12106 |
. . . . . . . . 9
⊢ (𝐵(,)𝐶) ⊆ ℝ |
62 | | resmpt 5369 |
. . . . . . . . 9
⊢ ((𝐵(,)𝐶) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) ↾ (𝐵(,)𝐶)) = (𝑦 ∈ (𝐵(,)𝐶) ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴))) |
63 | 61, 62 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) ↾ (𝐵(,)𝐶)) = (𝑦 ∈ (𝐵(,)𝐶) ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴))) |
64 | | elioore 12076 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐵(,)𝐶) → 𝑦 ∈ ℝ) |
65 | 64 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐵(,)𝐶) → 𝑦 ∈ ℂ) |
66 | 65, 44 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
67 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → 𝐴 ∈ ℂ) |
68 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → 𝐴 ≠ 0) |
69 | 66, 67, 68 | divcan3d 10685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴) = (cos‘(𝐴 · 𝑦))) |
70 | 69 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
71 | 60, 63, 70 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
72 | 6, 26, 71 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
73 | 72 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
74 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐴 · 𝑦) = (𝐴 · 𝑥)) |
75 | 74 | fveq2d 6107 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑥))) |
76 | 75 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) ∧ 𝑦 = 𝑥) → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑥))) |
77 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐵(,)𝐶)) |
78 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝐴 ∈ ℂ) |
79 | 61, 8 | syl5ss 3579 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ ℂ) |
80 | 79 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ℂ) |
81 | 78, 80 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (𝐴 · 𝑥) ∈ ℂ) |
82 | 81 | coscld 14700 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (cos‘(𝐴 · 𝑥)) ∈ ℂ) |
83 | 73, 76, 77, 82 | fvmptd 6197 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) = (cos‘(𝐴 · 𝑥))) |
84 | 83 | eqcomd 2616 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (cos‘(𝐴 · 𝑥)) = ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥)) |
85 | 84 | itgeq2dv 23354 |
. 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)(cos‘(𝐴 · 𝑥)) d𝑥 = ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥) |
86 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) = (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) |
87 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (𝐴 · 𝑦) = (𝐴 · 𝐶)) |
88 | 87 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝐶))) |
89 | 88 | oveq1d 6564 |
. . . . . 6
⊢ (𝑦 = 𝐶 → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐶)) / 𝐴)) |
90 | 89 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐶) → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐶)) / 𝐴)) |
91 | 1 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
92 | 2 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
93 | | itgcoscmulx.blec |
. . . . . 6
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
94 | | ubicc2 12160 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐶 ∈ (𝐵[,]𝐶)) |
95 | 91, 92, 93, 94 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (𝐵[,]𝐶)) |
96 | 2 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
97 | 10, 96 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
98 | 97 | sincld 14699 |
. . . . . 6
⊢ (𝜑 → (sin‘(𝐴 · 𝐶)) ∈ ℂ) |
99 | 98, 10, 15 | divcld 10680 |
. . . . 5
⊢ (𝜑 → ((sin‘(𝐴 · 𝐶)) / 𝐴) ∈ ℂ) |
100 | 86, 90, 95, 99 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) = ((sin‘(𝐴 · 𝐶)) / 𝐴)) |
101 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵)) |
102 | 101 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝐵))) |
103 | 102 | oveq1d 6564 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐵)) / 𝐴)) |
104 | 103 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐵)) / 𝐴)) |
105 | | lbicc2 12159 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) |
106 | 91, 92, 93, 105 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐵[,]𝐶)) |
107 | 1 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
108 | 10, 107 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
109 | 108 | sincld 14699 |
. . . . . 6
⊢ (𝜑 → (sin‘(𝐴 · 𝐵)) ∈ ℂ) |
110 | 109, 10, 15 | divcld 10680 |
. . . . 5
⊢ (𝜑 → ((sin‘(𝐴 · 𝐵)) / 𝐴) ∈ ℂ) |
111 | 86, 104, 106, 110 | fvmptd 6197 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐵) = ((sin‘(𝐴 · 𝐵)) / 𝐴)) |
112 | 100, 111 | oveq12d 6567 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = (((sin‘(𝐴 · 𝐶)) / 𝐴) − ((sin‘(𝐴 · 𝐵)) / 𝐴))) |
113 | | coscn 24003 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
114 | 113 | a1i 11 |
. . . . . 6
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
115 | 79, 10, 40 | constcncfg 38756 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝐴) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
116 | 79, 40 | idcncfg 38757 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝑦) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
117 | 115, 116 | mulcncf 23023 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
118 | 114, 117 | cncfmpt1f 22524 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
119 | 72, 118 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
120 | | ioossicc 12130 |
. . . . . . 7
⊢ (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶) |
121 | 120 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶)) |
122 | | ioombl 23140 |
. . . . . . 7
⊢ (𝐵(,)𝐶) ∈ dom vol |
123 | 122 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐵(,)𝐶) ∈ dom vol) |
124 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝐴 ∈ ℂ) |
125 | 3, 7 | syl6ss 3580 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℂ) |
126 | 125 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝑦 ∈ ℂ) |
127 | 124, 126 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (𝐴 · 𝑦) ∈ ℂ) |
128 | 127 | coscld 14700 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
129 | 125, 10, 40 | constcncfg 38756 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
130 | 125, 40 | idcncfg 38757 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝑦) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
131 | 129, 130 | mulcncf 23023 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
132 | 114, 131 | cncfmpt1f 22524 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
133 | | cniccibl 23413 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈
𝐿1) |
134 | 1, 2, 132, 133 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈
𝐿1) |
135 | 121, 123,
128, 134 | iblss 23377 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈
𝐿1) |
136 | 72, 135 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ∈
𝐿1) |
137 | | sincn 24002 |
. . . . . . 7
⊢ sin
∈ (ℂ–cn→ℂ) |
138 | 137 | a1i 11 |
. . . . . 6
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
139 | 138, 131 | cncfmpt1f 22524 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
140 | | neneq 2788 |
. . . . . . . 8
⊢ (𝐴 ≠ 0 → ¬ 𝐴 = 0) |
141 | | elsni 4142 |
. . . . . . . . 9
⊢ (𝐴 ∈ {0} → 𝐴 = 0) |
142 | 141 | con3i 149 |
. . . . . . . 8
⊢ (¬
𝐴 = 0 → ¬ 𝐴 ∈ {0}) |
143 | 15, 140, 142 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐴 ∈ {0}) |
144 | 10, 143 | eldifd 3551 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
{0})) |
145 | | difssd 3700 |
. . . . . 6
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
146 | 125, 144,
145 | constcncfg 38756 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→(ℂ ∖ {0}))) |
147 | 139, 146 | divcncf 38769 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
148 | 1, 2, 93, 119, 136, 147 | ftc2 23611 |
. . 3
⊢ (𝜑 → ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥 = (((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐵))) |
149 | 98, 109, 10, 15 | divsubdird 10719 |
. . 3
⊢ (𝜑 → (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴) = (((sin‘(𝐴 · 𝐶)) / 𝐴) − ((sin‘(𝐴 · 𝐵)) / 𝐴))) |
150 | 112, 148,
149 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥 = (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴)) |
151 | 85, 150 | eqtrd 2644 |
1
⊢ (𝜑 → ∫(𝐵(,)𝐶)(cos‘(𝐴 · 𝑥)) d𝑥 = (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴)) |