Step | Hyp | Ref
| Expression |
1 | | itgcoscmulx.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
2 | | itgcoscmulx.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
3 | 1, 2 | iccssred 39727 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
4 | 3 | resmptd 5452 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶)) = (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) |
5 | 4 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) = ((𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶))) |
6 | 5 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) = (ℝ D ((𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶)))) |
7 | | ax-resscn 9993 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
9 | 8 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
10 | | itgcoscmulx.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ ℂ) |
11 | 10 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ∈ ℂ) |
12 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ) |
13 | 11, 12 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · 𝑦) ∈ ℂ) |
14 | 13 | sincld 14860 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) |
15 | | itgcoscmulx.an0 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≠ 0) |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → 𝐴 ≠ 0) |
17 | 14, 11, 16 | divcld 10801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → ((sin‘(𝐴 · 𝑦)) / 𝐴) ∈ ℂ) |
18 | 9, 17 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((sin‘(𝐴 · 𝑦)) / 𝐴) ∈ ℂ) |
19 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴)) = (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) |
20 | 18, 19 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)):ℝ⟶ℂ) |
21 | | ssid 3624 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℝ) |
23 | | eqid 2622 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
24 | 23 | tgioo2 22606 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
25 | 23, 24 | dvres 23675 |
. . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)):ℝ⟶ℂ) ∧ (ℝ
⊆ ℝ ∧ (𝐵[,]𝐶) ⊆ ℝ)) → (ℝ D
((𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶)))) |
26 | 8, 20, 22, 3, 25 | syl22anc 1327 |
. . . . . . 7
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴)) ↾ (𝐵[,]𝐶))) = ((ℝ D (𝑦 ∈ ℝ ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶)))) |
27 | | reelprrecn 10028 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
29 | 9, 14 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (sin‘(𝐴 · 𝑦)) ∈ ℂ) |
30 | 10 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
31 | 30, 9 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐴 · 𝑦) ∈ ℂ) |
32 | 31 | coscld 14861 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
33 | 30, 32 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐴 · (cos‘(𝐴 · 𝑦))) ∈ ℂ) |
34 | 8 | resmptd 5452 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (sin‘(𝐴 · 𝑦)))) |
35 | 34 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (sin‘(𝐴 · 𝑦))) = ((𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) ↾ ℝ)) |
36 | 35 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(sin‘(𝐴 ·
𝑦)))) = (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) ↾
ℝ))) |
37 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) = (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) |
38 | 14, 37 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))):ℂ⟶ℂ) |
39 | | ssid 3624 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
40 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ⊆
ℂ) |
41 | | dvsinax 40127 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (ℂ
D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
42 | 10, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
43 | 42 | dmeqd 5326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) = dom (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
44 | 13 | coscld 14861 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
45 | 11, 44 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℂ) → (𝐴 · (cos‘(𝐴 · 𝑦))) ∈ ℂ) |
46 | 45 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑦 ∈ ℂ (𝐴 · (cos‘(𝐴 · 𝑦))) ∈ ℂ) |
47 | | dmmptg 5632 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
ℂ (𝐴 ·
(cos‘(𝐴 ·
𝑦))) ∈ ℂ →
dom (𝑦 ∈ ℂ
↦ (𝐴 ·
(cos‘(𝐴 ·
𝑦)))) =
ℂ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) = ℂ) |
49 | 43, 48 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℂ = dom (ℂ D
(𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))))) |
50 | 7, 49 | syl5sseq 3653 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆ dom
(ℂ D (𝑦 ∈
ℂ ↦ (sin‘(𝐴 · 𝑦))))) |
51 | | dvres3 23677 |
. . . . . . . . . . . . 13
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦)))))) → (ℝ D ((𝑦 ∈ ℂ ↦ (sin‘(𝐴 · 𝑦))) ↾ ℝ)) = ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) ↾
ℝ)) |
52 | 28, 38, 40, 50, 51 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) ↾ ℝ)) =
((ℂ D (𝑦 ∈
ℂ ↦ (sin‘(𝐴 · 𝑦)))) ↾ ℝ)) |
53 | 42 | reseq1d 5395 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℂ D (𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦)))) ↾ ℝ) =
((𝑦 ∈ ℂ ↦
(𝐴 ·
(cos‘(𝐴 ·
𝑦)))) ↾
ℝ)) |
54 | 8 | resmptd 5452 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ (𝐴 · (cos‘(𝐴 · 𝑦)))) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
55 | 52, 53, 54 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℂ ↦
(sin‘(𝐴 ·
𝑦))) ↾ ℝ)) =
(𝑦 ∈ ℝ ↦
(𝐴 ·
(cos‘(𝐴 ·
𝑦))))) |
56 | 36, 55 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(sin‘(𝐴 ·
𝑦)))) = (𝑦 ∈ ℝ ↦ (𝐴 · (cos‘(𝐴 · 𝑦))))) |
57 | 28, 29, 33, 56, 10, 15 | dvmptdivc 23728 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴))) = (𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴))) |
58 | | iccntr 22624 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐵[,]𝐶)) = (𝐵(,)𝐶)) |
59 | 1, 2, 58 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐵[,]𝐶)) = (𝐵(,)𝐶)) |
60 | 57, 59 | reseq12d 5397 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶))) = ((𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) ↾ (𝐵(,)𝐶))) |
61 | | ioossre 12235 |
. . . . . . . . 9
⊢ (𝐵(,)𝐶) ⊆ ℝ |
62 | | resmpt 5449 |
. . . . . . . . 9
⊢ ((𝐵(,)𝐶) ⊆ ℝ → ((𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) ↾ (𝐵(,)𝐶)) = (𝑦 ∈ (𝐵(,)𝐶) ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴))) |
63 | 61, 62 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) ↾ (𝐵(,)𝐶)) = (𝑦 ∈ (𝐵(,)𝐶) ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴))) |
64 | | elioore 12205 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐵(,)𝐶) → 𝑦 ∈ ℝ) |
65 | 64 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐵(,)𝐶) → 𝑦 ∈ ℂ) |
66 | 65, 44 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
67 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → 𝐴 ∈ ℂ) |
68 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → 𝐴 ≠ 0) |
69 | 66, 67, 68 | divcan3d 10806 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵(,)𝐶)) → ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴) = (cos‘(𝐴 · 𝑦))) |
70 | 69 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ ((𝐴 · (cos‘(𝐴 · 𝑦))) / 𝐴)) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
71 | 60, 63, 70 | 3eqtrd 2660 |
. . . . . . 7
⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦
((sin‘(𝐴 ·
𝑦)) / 𝐴))) ↾ ((int‘(topGen‘ran
(,)))‘(𝐵[,]𝐶))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
72 | 6, 26, 71 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
73 | 72 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) = (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦)))) |
74 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐴 · 𝑦) = (𝐴 · 𝑥)) |
75 | 74 | fveq2d 6195 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑥))) |
76 | 75 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) ∧ 𝑦 = 𝑥) → (cos‘(𝐴 · 𝑦)) = (cos‘(𝐴 · 𝑥))) |
77 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐵(,)𝐶)) |
78 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝐴 ∈ ℂ) |
79 | 61, 8 | syl5ss 3614 |
. . . . . . . 8
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ ℂ) |
80 | 79 | sselda 3603 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ℂ) |
81 | 78, 80 | mulcld 10060 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (𝐴 · 𝑥) ∈ ℂ) |
82 | 81 | coscld 14861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (cos‘(𝐴 · 𝑥)) ∈ ℂ) |
83 | 73, 76, 77, 82 | fvmptd 6288 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) = (cos‘(𝐴 · 𝑥))) |
84 | 83 | eqcomd 2628 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → (cos‘(𝐴 · 𝑥)) = ((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥)) |
85 | 84 | itgeq2dv 23548 |
. 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)(cos‘(𝐴 · 𝑥)) d𝑥 = ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥) |
86 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) = (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) |
87 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝐶 → (𝐴 · 𝑦) = (𝐴 · 𝐶)) |
88 | 87 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝐶))) |
89 | 88 | oveq1d 6665 |
. . . . . 6
⊢ (𝑦 = 𝐶 → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐶)) / 𝐴)) |
90 | 89 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐶) → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐶)) / 𝐴)) |
91 | 1 | rexrd 10089 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
92 | 2 | rexrd 10089 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
93 | | itgcoscmulx.blec |
. . . . . 6
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
94 | | ubicc2 12289 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐶 ∈ (𝐵[,]𝐶)) |
95 | 91, 92, 93, 94 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (𝐵[,]𝐶)) |
96 | 2 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
97 | 10, 96 | mulcld 10060 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
98 | 97 | sincld 14860 |
. . . . . 6
⊢ (𝜑 → (sin‘(𝐴 · 𝐶)) ∈ ℂ) |
99 | 98, 10, 15 | divcld 10801 |
. . . . 5
⊢ (𝜑 → ((sin‘(𝐴 · 𝐶)) / 𝐴) ∈ ℂ) |
100 | 86, 90, 95, 99 | fvmptd 6288 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) = ((sin‘(𝐴 · 𝐶)) / 𝐴)) |
101 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵)) |
102 | 101 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (sin‘(𝐴 · 𝑦)) = (sin‘(𝐴 · 𝐵))) |
103 | 102 | oveq1d 6665 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐵)) / 𝐴)) |
104 | 103 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → ((sin‘(𝐴 · 𝑦)) / 𝐴) = ((sin‘(𝐴 · 𝐵)) / 𝐴)) |
105 | | lbicc2 12288 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
≤ 𝐶) → 𝐵 ∈ (𝐵[,]𝐶)) |
106 | 91, 92, 93, 105 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐵[,]𝐶)) |
107 | 1 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
108 | 10, 107 | mulcld 10060 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
109 | 108 | sincld 14860 |
. . . . . 6
⊢ (𝜑 → (sin‘(𝐴 · 𝐵)) ∈ ℂ) |
110 | 109, 10, 15 | divcld 10801 |
. . . . 5
⊢ (𝜑 → ((sin‘(𝐴 · 𝐵)) / 𝐴) ∈ ℂ) |
111 | 86, 104, 106, 110 | fvmptd 6288 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐵) = ((sin‘(𝐴 · 𝐵)) / 𝐴)) |
112 | 100, 111 | oveq12d 6668 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐵)) = (((sin‘(𝐴 · 𝐶)) / 𝐴) − ((sin‘(𝐴 · 𝐵)) / 𝐴))) |
113 | | coscn 24199 |
. . . . . . 7
⊢ cos
∈ (ℂ–cn→ℂ) |
114 | 113 | a1i 11 |
. . . . . 6
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
115 | 79, 10, 40 | constcncfg 40084 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝐴) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
116 | 79, 40 | idcncfg 40085 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ 𝑦) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
117 | 115, 116 | mulcncf 23215 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
118 | 114, 117 | cncfmpt1f 22716 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
119 | 72, 118 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ∈ ((𝐵(,)𝐶)–cn→ℂ)) |
120 | | ioossicc 12259 |
. . . . . . 7
⊢ (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶) |
121 | 120 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐵[,]𝐶)) |
122 | | ioombl 23333 |
. . . . . . 7
⊢ (𝐵(,)𝐶) ∈ dom vol |
123 | 122 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐵(,)𝐶) ∈ dom vol) |
124 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝐴 ∈ ℂ) |
125 | 3, 7 | syl6ss 3615 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℂ) |
126 | 125 | sselda 3603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → 𝑦 ∈ ℂ) |
127 | 124, 126 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (𝐴 · 𝑦) ∈ ℂ) |
128 | 127 | coscld 14861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵[,]𝐶)) → (cos‘(𝐴 · 𝑦)) ∈ ℂ) |
129 | 125, 10, 40 | constcncfg 40084 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
130 | 125, 40 | idcncfg 40085 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝑦) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
131 | 129, 130 | mulcncf 23215 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (𝐴 · 𝑦)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
132 | 114, 131 | cncfmpt1f 22716 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
133 | | cniccibl 23607 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈
𝐿1) |
134 | 1, 2, 132, 133 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈
𝐿1) |
135 | 121, 123,
128, 134 | iblss 23571 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵(,)𝐶) ↦ (cos‘(𝐴 · 𝑦))) ∈
𝐿1) |
136 | 72, 135 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))) ∈
𝐿1) |
137 | | sincn 24198 |
. . . . . . 7
⊢ sin
∈ (ℂ–cn→ℂ) |
138 | 137 | a1i 11 |
. . . . . 6
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
139 | 138, 131 | cncfmpt1f 22716 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ (sin‘(𝐴 · 𝑦))) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
140 | | neneq 2800 |
. . . . . . . 8
⊢ (𝐴 ≠ 0 → ¬ 𝐴 = 0) |
141 | | elsni 4194 |
. . . . . . . . 9
⊢ (𝐴 ∈ {0} → 𝐴 = 0) |
142 | 141 | con3i 150 |
. . . . . . . 8
⊢ (¬
𝐴 = 0 → ¬ 𝐴 ∈ {0}) |
143 | 15, 140, 142 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐴 ∈ {0}) |
144 | 10, 143 | eldifd 3585 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
{0})) |
145 | | difssd 3738 |
. . . . . 6
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
146 | 125, 144,
145 | constcncfg 40084 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ 𝐴) ∈ ((𝐵[,]𝐶)–cn→(ℂ ∖ {0}))) |
147 | 139, 146 | divcncf 23216 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)) ∈ ((𝐵[,]𝐶)–cn→ℂ)) |
148 | 1, 2, 93, 119, 136, 147 | ftc2 23807 |
. . 3
⊢ (𝜑 → ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥 = (((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐶) − ((𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴))‘𝐵))) |
149 | 98, 109, 10, 15 | divsubdird 10840 |
. . 3
⊢ (𝜑 → (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴) = (((sin‘(𝐴 · 𝐶)) / 𝐴) − ((sin‘(𝐴 · 𝐵)) / 𝐴))) |
150 | 112, 148,
149 | 3eqtr4d 2666 |
. 2
⊢ (𝜑 → ∫(𝐵(,)𝐶)((ℝ D (𝑦 ∈ (𝐵[,]𝐶) ↦ ((sin‘(𝐴 · 𝑦)) / 𝐴)))‘𝑥) d𝑥 = (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴)) |
151 | 85, 150 | eqtrd 2656 |
1
⊢ (𝜑 → ∫(𝐵(,)𝐶)(cos‘(𝐴 · 𝑥)) d𝑥 = (((sin‘(𝐴 · 𝐶)) − (sin‘(𝐴 · 𝐵))) / 𝐴)) |