Step | Hyp | Ref
| Expression |
1 | | fourierdlem68.f |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | | fourierdlem68.xre |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℝ) |
3 | | fourierdlem68.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | | fourierdlem68.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | | fourierdlem68.fdv |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) |
6 | | ioossicc 12130 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
7 | | fourierdlem68.ab |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) |
8 | 6, 7 | syl5ss 3579 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) |
9 | | fourierdlem68.n0 |
. . . . . . 7
⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) |
10 | 6 | sseli 3564 |
. . . . . . 7
⊢ (0 ∈
(𝐴(,)𝐵) → 0 ∈ (𝐴[,]𝐵)) |
11 | 9, 10 | nsyl 134 |
. . . . . 6
⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) |
12 | | fourierdlem68.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
13 | | fourierdlem68.o |
. . . . . 6
⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) |
14 | 1, 2, 3, 4, 5, 8, 11, 12, 13 | fourierdlem57 39056 |
. . . . 5
⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧
(ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) |
15 | 14 | simpli 473 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 /
2)))↑2))))) |
16 | 15 | simpld 474 |
. . 3
⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ) |
17 | | fdm 5964 |
. . 3
⊢ ((ℝ
D 𝑂):(𝐴(,)𝐵)⟶ℝ → dom (ℝ D 𝑂) = (𝐴(,)𝐵)) |
18 | 16, 17 | syl 17 |
. 2
⊢ (𝜑 → dom (ℝ D 𝑂) = (𝐴(,)𝐵)) |
19 | | eqid 2610 |
. . . . . 6
⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) |
20 | | fourierdlem68.altb |
. . . . . . 7
⊢ (𝜑 → 𝐴 < 𝐵) |
21 | 3, 4, 20 | ltled 10064 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
22 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℝ) |
24 | 3, 4 | iccssred 38574 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
25 | 24 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ) |
26 | 25 | rehalfcld 11156 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 / 2) ∈ ℝ) |
27 | 26 | resincld 14712 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℝ) |
28 | 23, 27 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈
ℝ) |
29 | | 2cnd 10970 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ) |
30 | 27 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℂ) |
31 | | 2ne0 10990 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ≠ 0) |
33 | 7 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (-π[,]π)) |
34 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 0 ↔ 0 = 𝑡) |
35 | 34 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 0 → 0 = 𝑡) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 = 𝑡) |
37 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 𝑡 ∈ (𝐴[,]𝐵)) |
38 | 36, 37 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵)) |
39 | 38 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵)) |
40 | 9 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → ¬ 0 ∈ (𝐴[,]𝐵)) |
41 | 39, 40 | pm2.65da 598 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → ¬ 𝑡 = 0) |
42 | 41 | neqned 2789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≠ 0) |
43 | | fourierdlem44 39044 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (-π[,]π) ∧
𝑡 ≠ 0) →
(sin‘(𝑡 / 2)) ≠
0) |
44 | 33, 42, 43 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ≠ 0) |
45 | 29, 30, 32, 44 | mulne0d 10558 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ≠ 0) |
46 | | eldifsn 4260 |
. . . . . . . . 9
⊢ ((2
· (sin‘(𝑡 /
2))) ∈ (ℝ ∖ {0}) ↔ ((2 · (sin‘(𝑡 / 2))) ∈ ℝ ∧ (2
· (sin‘(𝑡 /
2))) ≠ 0)) |
47 | 28, 45, 46 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖
{0})) |
48 | 47, 19 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
49 | | difss 3699 |
. . . . . . . . . 10
⊢ (ℝ
∖ {0}) ⊆ ℝ |
50 | | ax-resscn 9872 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
51 | 49, 50 | sstri 3577 |
. . . . . . . . 9
⊢ (ℝ
∖ {0}) ⊆ ℂ |
52 | 51 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℝ ∖ {0})
⊆ ℂ) |
53 | 24, 50 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
54 | | 2cnd 10970 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
55 | | ssid 3587 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
57 | 53, 54, 56 | constcncfg 38756 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
58 | | sincn 24002 |
. . . . . . . . . . 11
⊢ sin
∈ (ℂ–cn→ℂ) |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
60 | 53, 56 | idcncfg 38757 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
61 | | eldifsn 4260 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
(ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠
0)) |
62 | 29, 32, 61 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ (ℂ ∖
{0})) |
63 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) = (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) |
64 | 62, 63 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖
{0})) |
65 | | difssd 3700 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
66 | | cncffvrn 22509 |
. . . . . . . . . . . . 13
⊢
(((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖
{0}))) |
67 | 65, 57, 66 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖
{0}))) |
68 | 64, 67 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0}))) |
69 | 60, 68 | divcncf 38769 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 / 2)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
70 | 59, 69 | cncfmpt1f 22524 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (sin‘(𝑡 / 2))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
71 | 57, 70 | mulcncf 23023 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
72 | | cncffvrn 22509 |
. . . . . . . 8
⊢
(((ℝ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖
{0}))) |
73 | 52, 71, 72 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖
{0}))) |
74 | 48, 73 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0}))) |
75 | 19, 3, 4, 21, 74 | cncficcgt0 38774 |
. . . . 5
⊢ (𝜑 → ∃𝑐 ∈ ℝ+ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 /
2))))) |
76 | | reelprrecn 9907 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
77 | 76 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ℝ ∈ {ℝ, ℂ}) |
78 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) |
79 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) |
80 | | elioore 12076 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) |
81 | 80 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) |
82 | 79, 81 | readdcld 9948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) |
83 | 78, 82 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) |
84 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ) |
85 | 83, 84 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ) |
86 | 85 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) |
87 | 86 | 3ad2antl1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) |
88 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
89 | 83 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
90 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) |
91 | 2, 3 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ) |
92 | 91 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐴) ∈
ℝ*) |
93 | 92 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈
ℝ*) |
94 | 2, 4 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ) |
95 | 94 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐵) ∈
ℝ*) |
96 | 95 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈
ℝ*) |
97 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
98 | 97 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
99 | 4 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
101 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) |
102 | | ioogtlb 38564 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) |
103 | 98, 100, 101, 102 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) |
104 | 97, 81, 79, 103 | ltadd2dd 10075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) |
105 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) |
106 | | iooltub 38582 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) |
107 | 98, 100, 101, 106 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) |
108 | 81, 105, 79, 107 | ltadd2dd 10075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) |
109 | 93, 96, 82, 104, 108 | eliood 38567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) |
110 | 90, 109 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ) |
111 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
112 | 1, 2, 3, 4, 111, 5 | fourierdlem28 39028 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
113 | 84 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ) |
114 | | 0red 9920 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) |
115 | | iooretop 22379 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
116 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
117 | 116 | tgioo2 22414 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
118 | 115, 117 | eleqtri 2686 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
120 | 12 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
121 | 88, 119, 120 | dvmptconst 38803 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0)) |
122 | 88, 89, 110, 112, 113, 114, 121 | dvmptsub 23536 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0))) |
123 | 110 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ) |
124 | 123 | subid1d 10260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) |
125 | 124 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
126 | 122, 125 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
127 | 126 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (ℝ D (𝑠 ∈
(𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
128 | 123 | 3ad2antl1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ) |
129 | | 2cnd 10970 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ) |
130 | 80 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ) |
131 | 130 | halfcld 11154 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ) |
132 | 131 | sincld 14699 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ) |
133 | 129, 132 | mulcld 9939 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) |
134 | 133 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) |
135 | | fourierdlem68.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℝ) |
136 | 135 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ 𝐸 ∈
ℝ) |
137 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
138 | 22, 137 | remulcli 9933 |
. . . . . . . 8
⊢ (2
· 1) ∈ ℝ |
139 | 138 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (2 · 1) ∈ ℝ) |
140 | | 1red 9934 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ 1 ∈ ℝ) |
141 | | fourierdlem68.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
142 | 120 | abscld 14023 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
143 | 141, 142 | readdcld 9948 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 + (abs‘𝐶)) ∈ ℝ) |
144 | 143 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (𝐷 +
(abs‘𝐶)) ∈
ℝ) |
145 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝜑) |
146 | 145, 109 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
147 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑋 + 𝑠) → (𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ↔ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
148 | 147 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑋 + 𝑠) → ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) ↔ (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))) |
149 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑋 + 𝑠) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) |
150 | 149 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
151 | 150 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸 ↔ (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)) |
152 | 148, 151 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))) |
153 | | fourierdlem68.fdvbd |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) |
154 | 152, 153 | vtoclg 3239 |
. . . . . . . . 9
⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)) |
155 | 82, 146, 154 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸) |
156 | 155 | 3ad2antl1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸) |
157 | 129, 132 | absmuld 14041 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 ·
(sin‘(𝑠 / 2)))) =
((abs‘2) · (abs‘(sin‘(𝑠 / 2))))) |
158 | | 0le2 10988 |
. . . . . . . . . . . 12
⊢ 0 ≤
2 |
159 | | absid 13884 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2) |
160 | 22, 158, 159 | mp2an 704 |
. . . . . . . . . . 11
⊢
(abs‘2) = 2 |
161 | 160 | oveq1i 6559 |
. . . . . . . . . 10
⊢
((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) = (2 ·
(abs‘(sin‘(𝑠 /
2)))) |
162 | 132 | abscld 14023 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ∈
ℝ) |
163 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 1 ∈ ℝ) |
164 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℝ) |
165 | 158 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 0 ≤ 2) |
166 | 80 | rehalfcld 11156 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℝ) |
167 | | abssinbd 38450 |
. . . . . . . . . . . 12
⊢ ((𝑠 / 2) ∈ ℝ →
(abs‘(sin‘(𝑠 /
2))) ≤ 1) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ≤ 1) |
169 | 162, 163,
164, 165, 168 | lemul2ad 10843 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 ·
(abs‘(sin‘(𝑠 /
2)))) ≤ (2 · 1)) |
170 | 161, 169 | syl5eqbr 4618 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((abs‘2) ·
(abs‘(sin‘(𝑠 /
2)))) ≤ (2 · 1)) |
171 | 157, 170 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 ·
(sin‘(𝑠 / 2)))) ≤
(2 · 1)) |
172 | 171 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(2 ·
(sin‘(𝑠 / 2)))) ≤
(2 · 1)) |
173 | | abscosbd 38431 |
. . . . . . . . 9
⊢ ((𝑠 / 2) ∈ ℝ →
(abs‘(cos‘(𝑠 /
2))) ≤ 1) |
174 | 101, 166,
173 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1) |
175 | 174 | 3ad2antl1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1) |
176 | 86 | abscld 14023 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ) |
177 | 89 | abscld 14023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ∈ ℝ) |
178 | 113 | abscld 14023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘𝐶) ∈ ℝ) |
179 | 177, 178 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ∈ ℝ) |
180 | 141 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℝ) |
181 | 180, 178 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐷 + (abs‘𝐶)) ∈ ℝ) |
182 | 89, 113 | abs2dif2d 14045 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶))) |
183 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝑋 + 𝑠) → (𝐹‘𝑡) = (𝐹‘(𝑋 + 𝑠))) |
184 | 183 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘(𝐹‘𝑡)) = (abs‘(𝐹‘(𝑋 + 𝑠)))) |
185 | 184 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘(𝐹‘𝑡)) ≤ 𝐷 ↔ (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)) |
186 | 148, 185 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))) |
187 | | fourierdlem68.fbd |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) |
188 | 186, 187 | vtoclg 3239 |
. . . . . . . . . . 11
⊢ ((𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)) |
189 | 109, 146,
188 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷) |
190 | 177, 180,
178, 189 | leadd1dd 10520 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ≤ (𝐷 + (abs‘𝐶))) |
191 | 176, 179,
181, 182, 190 | letrd 10073 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶))) |
192 | 191 | 3ad2antl1 1216 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶))) |
193 | 14 | simpri 477 |
. . . . . . . 8
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))) |
194 | 193 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (ℝ D (𝑠 ∈
(𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) |
195 | 131 | coscld 14700 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ) |
196 | 195 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ) |
197 | | simp2 1055 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ 𝑐 ∈
ℝ+) |
198 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (𝑡 / 2) = (𝑠 / 2)) |
199 | 198 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → (sin‘(𝑡 / 2)) = (sin‘(𝑠 / 2))) |
200 | 199 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑠 → (2 · (sin‘(𝑡 / 2))) = (2 ·
(sin‘(𝑠 /
2)))) |
201 | 200 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑠 → (abs‘(2 ·
(sin‘(𝑡 / 2)))) =
(abs‘(2 · (sin‘(𝑠 / 2))))) |
202 | 201 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2))))
↔ 𝑐 ≤ (abs‘(2
· (sin‘(𝑠 /
2)))))) |
203 | 202 | cbvralv 3147 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
(𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2))))
↔ ∀𝑠 ∈
(𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
204 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠𝜑 |
205 | | nfra1 2925 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2)))) |
206 | 204, 205 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑠(𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
207 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
208 | 6, 101 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵)) |
209 | 208 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵)) |
210 | | rspa 2914 |
. . . . . . . . . . . 12
⊢
((∀𝑠 ∈
(𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))) ∧
𝑠 ∈ (𝐴[,]𝐵)) → 𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
211 | 207, 209,
210 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
212 | 211 | ex 449 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
→ (𝑠 ∈ (𝐴(,)𝐵) → 𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2)))))) |
213 | 206, 212 | ralrimi 2940 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
→ ∀𝑠 ∈
(𝐴(,)𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
214 | 203, 213 | sylan2b 491 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ∀𝑠 ∈
(𝐴(,)𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
215 | 214 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ∀𝑠 ∈
(𝐴(,)𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
216 | | eqid 2610 |
. . . . . . 7
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) |
217 | 77, 87, 127, 128, 134, 136, 139, 140, 144, 156, 172, 175, 192, 194, 196, 197, 215, 216 | dvdivbd 38813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ∃𝑏 ∈
ℝ ∀𝑠 ∈
(𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏) |
218 | 217 | rexlimdv3a 3015 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ ℝ+ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2))))
→ ∃𝑏 ∈
ℝ ∀𝑠 ∈
(𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
219 | 75, 218 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏) |
220 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑠ℝ |
221 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑠
D |
222 | | nfmpt1 4675 |
. . . . . . . . . 10
⊢
Ⅎ𝑠(𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) |
223 | 13, 222 | nfcxfr 2749 |
. . . . . . . . 9
⊢
Ⅎ𝑠𝑂 |
224 | 220, 221,
223 | nfov 6575 |
. . . . . . . 8
⊢
Ⅎ𝑠(ℝ D 𝑂) |
225 | 224 | nfdm 5288 |
. . . . . . 7
⊢
Ⅎ𝑠dom
(ℝ D 𝑂) |
226 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑠(𝐴(,)𝐵) |
227 | 225, 226 | raleqf 3111 |
. . . . . 6
⊢ (dom
(ℝ D 𝑂) = (𝐴(,)𝐵) → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
228 | 18, 227 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
229 | 228 | rexbidv 3034 |
. . . 4
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
230 | 219, 229 | mpbird 246 |
. . 3
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏) |
231 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) |
232 | 231 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))) |
233 | 232 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((ℝ D 𝑂)‘𝑠) = ((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) |
234 | 233 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (abs‘((ℝ D
𝑂)‘𝑠)) = (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠))) |
235 | 234 | breq1d 4593 |
. . . 4
⊢ (𝜑 → ((abs‘((ℝ D
𝑂)‘𝑠)) ≤ 𝑏 ↔ (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
236 | 235 | rexralbidv 3040 |
. . 3
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
237 | 230, 236 | mpbird 246 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏) |
238 | 18, 237 | jca 553 |
1
⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)) |