Step | Hyp | Ref
| Expression |
1 | | fourierdlem39.a |
. 2
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | fourierdlem39.b |
. 2
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | fourierdlem39.aleb |
. 2
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
4 | | fourierdlem39.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
5 | | cncff 24056 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
7 | 6 | feqmptd 6837 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) |
8 | 7 | eqcomd 2744 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) = 𝐹) |
9 | 8, 4 | eqeltrd 2839 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
10 | | coscn 25604 |
. . . . . 6
⊢ cos
∈ (ℂ–cn→ℂ) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
12 | 1, 2 | iccssred 13166 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
13 | | ax-resscn 10928 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
14 | 12, 13 | sstrdi 3933 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
15 | | fourierdlem39.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
16 | 15 | rpred 12772 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℝ) |
17 | 16 | recnd 11003 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℂ) |
18 | | ssid 3943 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ⊆
ℂ) |
20 | 14, 17, 19 | constcncfg 43413 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑅) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
21 | 14, 19 | idcncfg 43414 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
22 | 20, 21 | mulcncf 24610 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑅 · 𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
23 | 11, 22 | cncfmpt1f 24077 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (cos‘(𝑅 · 𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
24 | 15 | rpcnne0d 12781 |
. . . . . 6
⊢ (𝜑 → (𝑅 ∈ ℂ ∧ 𝑅 ≠ 0)) |
25 | | eldifsn 4720 |
. . . . . 6
⊢ (𝑅 ∈ (ℂ ∖ {0})
↔ (𝑅 ∈ ℂ
∧ 𝑅 ≠
0)) |
26 | 24, 25 | sylibr 233 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ (ℂ ∖
{0})) |
27 | | difssd 4067 |
. . . . 5
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
28 | 14, 26, 27 | constcncfg 43413 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑅) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0}))) |
29 | 23, 28 | divcncf 24611 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
30 | 29 | negcncfg 43422 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
31 | | fourierdlem39.gcn |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
32 | | cncff 24056 |
. . . . . 6
⊢ (𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
34 | 33 | feqmptd 6837 |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
35 | 34 | eqcomd 2744 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) = 𝐺) |
36 | 35, 31 | eqeltrd 2839 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
37 | | sincn 25603 |
. . . 4
⊢ sin
∈ (ℂ–cn→ℂ) |
38 | 37 | a1i 11 |
. . 3
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
39 | | ioosscn 13141 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ ℂ |
40 | 39 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
41 | 40, 17, 19 | constcncfg 43413 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑅) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
42 | 40, 19 | idcncfg 43414 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑥) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
43 | 41, 42 | mulcncf 24610 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝑅 · 𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
44 | 38, 43 | cncfmpt1f 24077 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
45 | | ioombl 24729 |
. . . 4
⊢ (𝐴(,)𝐵) ∈ dom vol |
46 | 45 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
47 | | volioo 24733 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
48 | 1, 2, 3, 47 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
49 | 2, 1 | resubcld 11403 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
50 | 48, 49 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
51 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) |
52 | | ioossicc 13165 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
53 | 52 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
54 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
55 | 53 | sselda 3921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
56 | 54, 55 | ffvelrnd 6962 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
57 | 51, 9, 53, 19, 56 | cncfmptssg 43412 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
58 | 57, 44 | mulcncf 24610 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
59 | | cniccbdd 24625 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) |
60 | 1, 2, 4, 59 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) |
61 | | nfra1 3144 |
. . . . . . . 8
⊢
Ⅎ𝑧∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 |
62 | 52 | sseli 3917 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵)) |
63 | | rspa 3132 |
. . . . . . . . . 10
⊢
((∀𝑧 ∈
(𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (abs‘(𝐹‘𝑧)) ≤ 𝑦) |
64 | 62, 63 | sylan2 593 |
. . . . . . . . 9
⊢
((∀𝑧 ∈
(𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑧)) ≤ 𝑦) |
65 | 64 | ex 413 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 → (𝑧 ∈ (𝐴(,)𝐵) → (abs‘(𝐹‘𝑧)) ≤ 𝑦)) |
66 | 61, 65 | ralrimi 3141 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) |
67 | 66 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦)) |
68 | 67 | reximdva 3203 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦)) |
69 | 60, 68 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) |
70 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝜑 ∧ 𝑦 ∈ ℝ) |
71 | | nfra1 3144 |
. . . . . . . 8
⊢
Ⅎ𝑧∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 |
72 | 70, 71 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑧((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) |
73 | | simpll 764 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → (𝜑 ∧ 𝑦 ∈ ℝ)) |
74 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) |
75 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ) |
76 | | elioore 13109 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) |
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ) |
78 | 75, 77 | remulcld 11005 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑥) ∈ ℝ) |
79 | 78 | resincld 15852 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑥)) ∈ ℝ) |
80 | 79 | recnd 11003 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑥)) ∈ ℂ) |
81 | 56, 80 | mulcld 10995 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ) |
82 | 81 | ralrimiva 3103 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ) |
83 | | dmmptg 6145 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) ∈ ℂ → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵)) |
85 | 84 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝐴(,)𝐵)) |
86 | 74, 85 | eleqtrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵)) |
87 | 86 | ad4ant14 749 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵)) |
88 | | simplr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) |
89 | 86 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → 𝑧 ∈ (𝐴(,)𝐵)) |
90 | | rspa 3132 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
(𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑧)) ≤ 𝑦) |
91 | 88, 89, 90 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘(𝐹‘𝑧)) ≤ 𝑦) |
92 | 91 | adantllr 716 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘(𝐹‘𝑧)) ≤ 𝑦) |
93 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) |
94 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
95 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝑅 · 𝑥) = (𝑅 · 𝑧)) |
96 | 95 | fveq2d 6778 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (sin‘(𝑅 · 𝑥)) = (sin‘(𝑅 · 𝑧))) |
97 | 94, 96 | oveq12d 7293 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) = ((𝐹‘𝑧) · (sin‘(𝑅 · 𝑧)))) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑧) → ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) = ((𝐹‘𝑧) · (sin‘(𝑅 · 𝑧)))) |
99 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ (𝐴(,)𝐵)) |
100 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
101 | 52, 99 | sselid 3919 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ (𝐴[,]𝐵)) |
102 | 100, 101 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
103 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ) |
104 | 39, 99 | sselid 3919 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℂ) |
105 | 103, 104 | mulcld 10995 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℂ) |
106 | 105 | sincld 15839 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (sin‘(𝑅 · 𝑧)) ∈ ℂ) |
107 | 102, 106 | mulcld 10995 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝑧) · (sin‘(𝑅 · 𝑧))) ∈ ℂ) |
108 | 93, 98, 99, 107 | fvmptd 6882 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧) = ((𝐹‘𝑧) · (sin‘(𝑅 · 𝑧)))) |
109 | 108 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = (abs‘((𝐹‘𝑧) · (sin‘(𝑅 · 𝑧))))) |
110 | 102, 106 | absmuld 15166 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘𝑧) · (sin‘(𝑅 · 𝑧)))) = ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧))))) |
111 | 109, 110 | eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧))))) |
112 | 111 | adantlr 712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧))))) |
113 | 112 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) = ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧))))) |
114 | | simplll 772 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 𝜑) |
115 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 𝑧 ∈ (𝐴(,)𝐵)) |
116 | 114, 115,
102 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (𝐹‘𝑧) ∈ ℂ) |
117 | 116 | abscld 15148 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
118 | 17 | ad3antrrr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 𝑅 ∈ ℂ) |
119 | 39, 115 | sselid 3919 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 𝑧 ∈ ℂ) |
120 | 118, 119 | mulcld 10995 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (𝑅 · 𝑧) ∈ ℂ) |
121 | 120 | sincld 15839 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (sin‘(𝑅 · 𝑧)) ∈ ℂ) |
122 | 121 | abscld 15148 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (abs‘(sin‘(𝑅 · 𝑧))) ∈ ℝ) |
123 | 117, 122 | remulcld 11005 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ∈ ℝ) |
124 | | 1red 10976 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 1 ∈ ℝ) |
125 | 117, 124 | remulcld 11005 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → ((abs‘(𝐹‘𝑧)) · 1) ∈
ℝ) |
126 | | simpllr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 𝑦 ∈ ℝ) |
127 | 126, 124 | remulcld 11005 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (𝑦 · 1) ∈ ℝ) |
128 | 106 | abscld 15148 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(sin‘(𝑅 · 𝑧))) ∈ ℝ) |
129 | | 1red 10976 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ) |
130 | 102 | abscld 15148 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘𝑧)) ∈ ℝ) |
131 | 102 | absge0d 15156 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘(𝐹‘𝑧))) |
132 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℝ) |
133 | | elioore 13109 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ ℝ) |
134 | 133 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℝ) |
135 | 132, 134 | remulcld 11005 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℝ) |
136 | | abssinbd 42834 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 · 𝑧) ∈ ℝ →
(abs‘(sin‘(𝑅
· 𝑧))) ≤
1) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(sin‘(𝑅 · 𝑧))) ≤ 1) |
138 | 128, 129,
130, 131, 137 | lemul2ad 11915 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹‘𝑧)) · 1)) |
139 | 138 | adantlr 712 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹‘𝑧)) · 1)) |
140 | 139 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ ((abs‘(𝐹‘𝑧)) · 1)) |
141 | | 0le1 11498 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
1 |
142 | 141 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 0 ≤ 1) |
143 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (abs‘(𝐹‘𝑧)) ≤ 𝑦) |
144 | 117, 126,
124, 142, 143 | lemul1ad 11914 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → ((abs‘(𝐹‘𝑧)) · 1) ≤ (𝑦 · 1)) |
145 | 123, 125,
127, 140, 144 | letrd 11132 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → ((abs‘(𝐹‘𝑧)) · (abs‘(sin‘(𝑅 · 𝑧)))) ≤ (𝑦 · 1)) |
146 | 113, 145 | eqbrtrd 5096 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ (𝑦 · 1)) |
147 | 126 | recnd 11003 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → 𝑦 ∈ ℂ) |
148 | 147 | mulid1d 10992 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (𝑦 · 1) = 𝑦) |
149 | 146, 148 | breqtrd 5100 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝐹‘𝑧)) ≤ 𝑦) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦) |
150 | 73, 87, 92, 149 | syl21anc 835 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦) |
151 | 150 | ex 413 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) → (𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)) |
152 | 72, 151 | ralrimi 3141 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦) → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦) |
153 | 152 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)) |
154 | 153 | reximdva 3203 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑧)) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦)) |
155 | 69, 154 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))))‘𝑧)) ≤ 𝑦) |
156 | 46, 50, 58, 155 | cnbdibl 43503 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥)))) ∈
𝐿1) |
157 | 11, 43 | cncfmpt1f 24077 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑅 · 𝑥))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
158 | 40, 26, 27 | constcncfg 43413 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝑅) ∈ ((𝐴(,)𝐵)–cn→(ℂ ∖ {0}))) |
159 | 157, 158 | divcncf 24611 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
160 | 159 | negcncfg 43422 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
161 | 36, 160 | mulcncf 24610 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
162 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
163 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑅 ∈ ℝ) |
164 | 15 | rpne0d 12777 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ≠ 0) |
165 | 164 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑅 ≠ 0) |
166 | 162, 163,
165 | redivcld 11803 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 / 𝑅) ∈ ℝ) |
167 | 166 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) → (𝑦 / 𝑅) ∈ ℝ) |
168 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) |
169 | 33 | ffvelrnda 6961 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) ∈ ℂ) |
170 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ) |
171 | 76 | recnd 11003 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℂ) |
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ) |
173 | 170, 172 | mulcld 10995 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑥) ∈ ℂ) |
174 | 173 | coscld 15840 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑥)) ∈ ℂ) |
175 | 164 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0) |
176 | 174, 170,
175 | divcld 11751 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ) |
177 | 176 | negcld 11319 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ) |
178 | 169, 177 | mulcld 10995 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ) |
179 | 178 | ralrimiva 3103 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ) |
180 | 179 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → ∀𝑥 ∈ (𝐴(,)𝐵)((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ) |
181 | | dmmptg 6145 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) ∈ ℂ → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝐴(,)𝐵)) |
182 | 180, 181 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝐴(,)𝐵)) |
183 | 168, 182 | eleqtrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ (𝐴(,)𝐵)) |
184 | 183 | ad4ant14 749 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → 𝑧 ∈ (𝐴(,)𝐵)) |
185 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) |
186 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
187 | 95 | fveq2d 6778 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝑧))) |
188 | 187 | oveq1d 7290 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝑧)) / 𝑅)) |
189 | 188 | negeqd 11215 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝑧)) / 𝑅)) |
190 | 186, 189 | oveq12d 7293 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) |
191 | 190 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝑧) → ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) |
192 | 33 | ffvelrnda 6961 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ) |
193 | 105 | coscld 15840 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑧)) ∈ ℂ) |
194 | 164 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0) |
195 | 193, 103,
194 | divcld 11751 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ) |
196 | 195 | negcld 11319 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ) |
197 | 192, 196 | mulcld 10995 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)) ∈ ℂ) |
198 | 185, 191,
99, 197 | fvmptd 6882 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧) = ((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) |
199 | 198 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) = (abs‘((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))) |
200 | 199 | ad4ant14 749 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) = (abs‘((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅)))) |
201 | 33 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) → 𝐺:(𝐴(,)𝐵)⟶ℂ) |
202 | 201 | ffvelrnda 6961 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ) |
203 | 202 | abscld 15148 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺‘𝑧)) ∈ ℝ) |
204 | | simpllr 773 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℝ) |
205 | 17 | ad3antrrr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ) |
206 | 104 | ad4ant14 749 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 ∈ ℂ) |
207 | 205, 206 | mulcld 10995 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑅 · 𝑧) ∈ ℂ) |
208 | 207 | coscld 15840 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (cos‘(𝑅 · 𝑧)) ∈ ℂ) |
209 | 164 | ad3antrrr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ≠ 0) |
210 | 208, 205,
209 | divcld 11751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ) |
211 | 210 | negcld 11319 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → -((cos‘(𝑅 · 𝑧)) / 𝑅) ∈ ℂ) |
212 | 211 | abscld 15148 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ∈ ℝ) |
213 | 15 | rprecred 12783 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 𝑅) ∈ ℝ) |
214 | 213 | ad3antrrr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (1 / 𝑅) ∈ ℝ) |
215 | 202 | absge0d 15156 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘(𝐺‘𝑧))) |
216 | 211 | absge0d 15156 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 0 ≤
(abs‘-((cos‘(𝑅
· 𝑧)) / 𝑅))) |
217 | 186 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (abs‘(𝐺‘𝑥)) = (abs‘(𝐺‘𝑧))) |
218 | 217 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ((abs‘(𝐺‘𝑥)) ≤ 𝑦 ↔ (abs‘(𝐺‘𝑧)) ≤ 𝑦)) |
219 | 218 | rspccva 3560 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺‘𝑧)) ≤ 𝑦) |
220 | 219 | adantll 711 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(𝐺‘𝑧)) ≤ 𝑦) |
221 | 195 | absnegd 15161 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) = (abs‘((cos‘(𝑅 · 𝑧)) / 𝑅))) |
222 | 193, 103,
194 | absdivd 15167 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((cos‘(𝑅 · 𝑧)) / 𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅))) |
223 | 15 | rpge0d 12776 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 𝑅) |
224 | 16, 223 | absidd 15134 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘𝑅) = 𝑅) |
225 | 224 | oveq2d 7291 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((abs‘(cos‘(𝑅
· 𝑧))) /
(abs‘𝑅)) =
((abs‘(cos‘(𝑅
· 𝑧))) / 𝑅)) |
226 | 225 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(cos‘(𝑅 · 𝑧))) / (abs‘𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅)) |
227 | 221, 222,
226 | 3eqtrd 2782 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) = ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅)) |
228 | 193 | abscld 15148 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑅 · 𝑧))) ∈ ℝ) |
229 | 15 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑅 ∈
ℝ+) |
230 | | abscosbd 42817 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 · 𝑧) ∈ ℝ →
(abs‘(cos‘(𝑅
· 𝑧))) ≤
1) |
231 | 135, 230 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑅 · 𝑧))) ≤ 1) |
232 | 228, 129,
229, 231 | lediv1dd 12830 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(cos‘(𝑅 · 𝑧))) / 𝑅) ≤ (1 / 𝑅)) |
233 | 227, 232 | eqbrtrd 5096 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ≤ (1 / 𝑅)) |
234 | 233 | ad4ant14 749 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)) ≤ (1 / 𝑅)) |
235 | 203, 204,
212, 214, 215, 216, 220, 234 | lemul12ad 11917 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐺‘𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅))) ≤ (𝑦 · (1 / 𝑅))) |
236 | 192, 196 | absmuld 15166 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) = ((abs‘(𝐺‘𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)))) |
237 | 236 | ad4ant14 749 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) = ((abs‘(𝐺‘𝑧)) · (abs‘-((cos‘(𝑅 · 𝑧)) / 𝑅)))) |
238 | 204 | recnd 11003 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ℂ) |
239 | 238, 205,
209 | divrecd 11754 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝑦 / 𝑅) = (𝑦 · (1 / 𝑅))) |
240 | 235, 237,
239 | 3brtr4d 5106 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝐺‘𝑧) · -((cos‘(𝑅 · 𝑧)) / 𝑅))) ≤ (𝑦 / 𝑅)) |
241 | 200, 240 | eqbrtrd 5096 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)) |
242 | 184, 241 | syldan 591 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) ∧ 𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))) → (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)) |
243 | 242 | ralrimiva 3103 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) → ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)) |
244 | | breq2 5078 |
. . . . . . 7
⊢ (𝑤 = (𝑦 / 𝑅) → ((abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤 ↔ (abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))) |
245 | 244 | ralbidv 3112 |
. . . . . 6
⊢ (𝑤 = (𝑦 / 𝑅) → (∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤 ↔ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅))) |
246 | 245 | rspcev 3561 |
. . . . 5
⊢ (((𝑦 / 𝑅) ∈ ℝ ∧ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ (𝑦 / 𝑅)) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤) |
247 | 167, 243,
246 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤) |
248 | | fourierdlem39.gbd |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) |
249 | 247, 248 | r19.29a 3218 |
. . 3
⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ dom (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))(abs‘((𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)))‘𝑧)) ≤ 𝑤) |
250 | 46, 50, 161, 249 | cnbdibl 43503 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅))) ∈
𝐿1) |
251 | 8 | oveq2d 7291 |
. . 3
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D 𝐹)) |
252 | | fourierdlem39.g |
. . . . 5
⊢ 𝐺 = (ℝ D 𝐹) |
253 | 252 | eqcomi 2747 |
. . . 4
⊢ (ℝ
D 𝐹) = 𝐺 |
254 | 253 | a1i 11 |
. . 3
⊢ (𝜑 → (ℝ D 𝐹) = 𝐺) |
255 | 251, 254,
34 | 3eqtrd 2782 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑥))) |
256 | | reelprrecn 10963 |
. . . . 5
⊢ ℝ
∈ {ℝ, ℂ} |
257 | 256 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
258 | 17 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℂ) |
259 | | recn 10961 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
260 | 259 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
261 | 258, 260 | mulcld 10995 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 · 𝑥) ∈ ℂ) |
262 | 261 | coscld 15840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (cos‘(𝑅 · 𝑥)) ∈ ℂ) |
263 | 164 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ≠ 0) |
264 | 262, 258,
263 | divcld 11751 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ) |
265 | 264 | negcld 11319 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((cos‘(𝑅 · 𝑥)) / 𝑅) ∈ ℂ) |
266 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℝ) |
267 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
268 | 266, 267 | remulcld 11005 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 · 𝑥) ∈ ℝ) |
269 | 268 | resincld 15852 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (sin‘(𝑅 · 𝑥)) ∈ ℝ) |
270 | 269 | renegcld 11402 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(sin‘(𝑅 · 𝑥)) ∈ ℝ) |
271 | 270, 266 | remulcld 11005 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(sin‘(𝑅 · 𝑥)) · 𝑅) ∈ ℝ) |
272 | 271, 266,
263 | redivcld 11803 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℝ) |
273 | 272 | renegcld 11402 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℝ) |
274 | | recoscl 15850 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
(cos‘𝑦) ∈
ℝ) |
275 | 274 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (cos‘𝑦) ∈
ℝ) |
276 | 275 | recnd 11003 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (cos‘𝑦) ∈
ℂ) |
277 | | resincl 15849 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
(sin‘𝑦) ∈
ℝ) |
278 | 277 | renegcld 11402 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ →
-(sin‘𝑦) ∈
ℝ) |
279 | 278 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -(sin‘𝑦) ∈
ℝ) |
280 | | 1red 10976 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℝ) |
281 | 257 | dvmptid 25121 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
282 | 257, 260,
280, 281, 17 | dvmptcmul 25128 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝑅 · 𝑥))) = (𝑥 ∈ ℝ ↦ (𝑅 · 1))) |
283 | 258 | mulid1d 10992 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 · 1) = 𝑅) |
284 | 283 | mpteq2dva 5174 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑅 · 1)) = (𝑥 ∈ ℝ ↦ 𝑅)) |
285 | 282, 284 | eqtrd 2778 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝑅 · 𝑥))) = (𝑥 ∈ ℝ ↦ 𝑅)) |
286 | | dvcosre 43453 |
. . . . . . . 8
⊢ (ℝ
D (𝑦 ∈ ℝ ↦
(cos‘𝑦))) = (𝑦 ∈ ℝ ↦
-(sin‘𝑦)) |
287 | 286 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦
(cos‘𝑦))) = (𝑦 ∈ ℝ ↦
-(sin‘𝑦))) |
288 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑦 = (𝑅 · 𝑥) → (cos‘𝑦) = (cos‘(𝑅 · 𝑥))) |
289 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑦 = (𝑅 · 𝑥) → (sin‘𝑦) = (sin‘(𝑅 · 𝑥))) |
290 | 289 | negeqd 11215 |
. . . . . . 7
⊢ (𝑦 = (𝑅 · 𝑥) → -(sin‘𝑦) = -(sin‘(𝑅 · 𝑥))) |
291 | 257, 257,
268, 266, 276, 279, 285, 287, 288, 290 | dvmptco 25136 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
(cos‘(𝑅 ·
𝑥)))) = (𝑥 ∈ ℝ ↦ (-(sin‘(𝑅 · 𝑥)) · 𝑅))) |
292 | 257, 262,
271, 291, 17, 164 | dvmptdivc 25129 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
((cos‘(𝑅 ·
𝑥)) / 𝑅))) = (𝑥 ∈ ℝ ↦ ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))) |
293 | 257, 264,
272, 292 | dvmptneg 25130 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
-((cos‘(𝑅 ·
𝑥)) / 𝑅))) = (𝑥 ∈ ℝ ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))) |
294 | | eqid 2738 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
295 | 294 | tgioo2 23966 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
296 | | iccntr 23984 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
297 | 1, 2, 296 | syl2anc 584 |
. . . 4
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
298 | 257, 265,
273, 293, 12, 295, 294, 297 | dvmptres2 25126 |
. . 3
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅))) |
299 | 80, 170 | mulneg1d 11428 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (-(sin‘(𝑅 · 𝑥)) · 𝑅) = -((sin‘(𝑅 · 𝑥)) · 𝑅)) |
300 | 299 | oveq1d 7290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (-((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) |
301 | 80, 170 | mulcld 10995 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((sin‘(𝑅 · 𝑥)) · 𝑅) ∈ ℂ) |
302 | 301, 170,
175 | divnegd 11764 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (-((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) |
303 | 300, 302 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = -(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) |
304 | 303 | negeqd 11215 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = --(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) |
305 | 301, 170,
175 | divcld 11751 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) ∈ ℂ) |
306 | 305 | negnegd 11323 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → --(((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) |
307 | 80, 170, 175 | divcan4d 11757 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (sin‘(𝑅 · 𝑥))) |
308 | 304, 306,
307 | 3eqtrd 2782 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅) = (sin‘(𝑅 · 𝑥))) |
309 | 308 | mpteq2dva 5174 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ -((-(sin‘(𝑅 · 𝑥)) · 𝑅) / 𝑅)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥)))) |
310 | 298, 309 | eqtrd 2778 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ -((cos‘(𝑅 · 𝑥)) / 𝑅))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (sin‘(𝑅 · 𝑥)))) |
311 | | fveq2 6774 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
312 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑅 · 𝑥) = (𝑅 · 𝐴)) |
313 | 312 | fveq2d 6778 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝐴))) |
314 | 313 | oveq1d 7290 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝐴)) / 𝑅)) |
315 | 314 | negeqd 11215 |
. . . 4
⊢ (𝑥 = 𝐴 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝐴)) / 𝑅)) |
316 | 311, 315 | oveq12d 7293 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹‘𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) |
317 | 316 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ((𝐹‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹‘𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) |
318 | | fveq2 6774 |
. . . 4
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
319 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑅 · 𝑥) = (𝑅 · 𝐵)) |
320 | 319 | fveq2d 6778 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (cos‘(𝑅 · 𝑥)) = (cos‘(𝑅 · 𝐵))) |
321 | 320 | oveq1d 7290 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((cos‘(𝑅 · 𝑥)) / 𝑅) = ((cos‘(𝑅 · 𝐵)) / 𝑅)) |
322 | 321 | negeqd 11215 |
. . . 4
⊢ (𝑥 = 𝐵 → -((cos‘(𝑅 · 𝑥)) / 𝑅) = -((cos‘(𝑅 · 𝐵)) / 𝑅)) |
323 | 318, 322 | oveq12d 7293 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹‘𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅))) |
324 | 323 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → ((𝐹‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) = ((𝐹‘𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅))) |
325 | 1, 2, 3, 9, 30, 36, 44, 156, 250, 255, 310, 317, 324 | itgparts 25211 |
1
⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹‘𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹‘𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥)) |