| 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 13473 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 7 | | fourierdlem68.ab |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) |
| 8 | 6, 7 | sstrid 3995 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) |
| 9 | | fourierdlem68.n0 |
. . . . . . 7
⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) |
| 10 | 6 | sseli 3979 |
. . . . . . 7
⊢ (0 ∈
(𝐴(,)𝐵) → 0 ∈ (𝐴[,]𝐵)) |
| 11 | 9, 10 | nsyl 140 |
. . . . . 6
⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) |
| 12 | | fourierdlem68.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 13 | | fourierdlem68.o |
. . . . . 6
⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) |
| 14 | 1, 2, 3, 4, 5, 8, 11, 12, 13 | fourierdlem57 46178 |
. . . . 5
⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧
(ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) |
| 15 | 14 | simpli 483 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 /
2)))↑2))))) |
| 16 | 15 | simpld 494 |
. . 3
⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ) |
| 17 | 16 | fdmd 6746 |
. 2
⊢ (𝜑 → dom (ℝ D 𝑂) = (𝐴(,)𝐵)) |
| 18 | | eqid 2737 |
. . . . . 6
⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) |
| 19 | | fourierdlem68.altb |
. . . . . . 7
⊢ (𝜑 → 𝐴 < 𝐵) |
| 20 | 3, 4, 19 | ltled 11409 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 21 | | 2re 12340 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
| 22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℝ) |
| 23 | 3, 4 | iccssred 13474 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 24 | 23 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ) |
| 25 | 24 | rehalfcld 12513 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 / 2) ∈ ℝ) |
| 26 | 25 | resincld 16179 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℝ) |
| 27 | 22, 26 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈
ℝ) |
| 28 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ) |
| 29 | 26 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℂ) |
| 30 | | 2ne0 12370 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
| 31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ≠ 0) |
| 32 | 7 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (-π[,]π)) |
| 33 | | eqcom 2744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 0 ↔ 0 = 𝑡) |
| 34 | 33 | biimpi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 0 → 0 = 𝑡) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 = 𝑡) |
| 36 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 𝑡 ∈ (𝐴[,]𝐵)) |
| 37 | 35, 36 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵)) |
| 38 | 37 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵)) |
| 39 | 9 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → ¬ 0 ∈ (𝐴[,]𝐵)) |
| 40 | 38, 39 | pm2.65da 817 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → ¬ 𝑡 = 0) |
| 41 | 40 | neqned 2947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≠ 0) |
| 42 | | fourierdlem44 46166 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ (-π[,]π) ∧
𝑡 ≠ 0) →
(sin‘(𝑡 / 2)) ≠
0) |
| 43 | 32, 41, 42 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ≠ 0) |
| 44 | 28, 29, 31, 43 | mulne0d 11915 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ≠ 0) |
| 45 | | eldifsn 4786 |
. . . . . . . . 9
⊢ ((2
· (sin‘(𝑡 /
2))) ∈ (ℝ ∖ {0}) ↔ ((2 · (sin‘(𝑡 / 2))) ∈ ℝ ∧ (2
· (sin‘(𝑡 /
2))) ≠ 0)) |
| 46 | 27, 44, 45 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖
{0})) |
| 47 | 46, 18 | fmptd 7134 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖
{0})) |
| 48 | | difss 4136 |
. . . . . . . . . 10
⊢ (ℝ
∖ {0}) ⊆ ℝ |
| 49 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 50 | 48, 49 | sstri 3993 |
. . . . . . . . 9
⊢ (ℝ
∖ {0}) ⊆ ℂ |
| 51 | 50 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℝ ∖ {0})
⊆ ℂ) |
| 52 | 23, 49 | sstrdi 3996 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
| 53 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
| 54 | | ssid 4006 |
. . . . . . . . . . 11
⊢ ℂ
⊆ ℂ |
| 55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℂ ⊆
ℂ) |
| 56 | 52, 53, 55 | constcncfg 45887 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 57 | | sincn 26488 |
. . . . . . . . . . 11
⊢ sin
∈ (ℂ–cn→ℂ) |
| 58 | 57 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) |
| 59 | 52, 55 | idcncfg 45888 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 60 | | eldifsn 4786 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
(ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠
0)) |
| 61 | 28, 31, 60 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ (ℂ ∖
{0})) |
| 62 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) = (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) |
| 63 | 61, 62 | fmptd 7134 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖
{0})) |
| 64 | | difssd 4137 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
| 65 | | cncfcdm 24924 |
. . . . . . . . . . . . 13
⊢
(((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖
{0}))) |
| 66 | 64, 56, 65 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖
{0}))) |
| 67 | 63, 66 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0}))) |
| 68 | 59, 67 | divcncf 25482 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 / 2)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 69 | 58, 68 | cncfmpt1f 24940 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (sin‘(𝑡 / 2))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 70 | 56, 69 | mulcncf 25480 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
| 71 | | cncfcdm 24924 |
. . . . . . . 8
⊢
(((ℝ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖
{0}))) |
| 72 | 51, 70, 71 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖
{0}))) |
| 73 | 47, 72 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0}))) |
| 74 | 18, 3, 4, 20, 73 | cncficcgt0 45903 |
. . . . 5
⊢ (𝜑 → ∃𝑐 ∈ ℝ+ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 /
2))))) |
| 75 | | reelprrecn 11247 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
| 76 | 75 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ℝ ∈ {ℝ, ℂ}) |
| 77 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) |
| 78 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) |
| 79 | | elioore 13417 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) |
| 81 | 78, 80 | readdcld 11290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) |
| 82 | 77, 81 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) |
| 83 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ) |
| 84 | 82, 83 | resubcld 11691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ) |
| 85 | 84 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) |
| 86 | 85 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) |
| 87 | 75 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 88 | 82 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
| 89 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) |
| 90 | 2, 3 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ) |
| 91 | 90 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐴) ∈
ℝ*) |
| 92 | 91 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈
ℝ*) |
| 93 | 2, 4 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ) |
| 94 | 93 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐵) ∈
ℝ*) |
| 95 | 94 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈
ℝ*) |
| 96 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
| 97 | 96 | rexrd 11311 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
| 98 | 4 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
| 100 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) |
| 101 | | ioogtlb 45508 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) |
| 102 | 97, 99, 100, 101 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) |
| 103 | 96, 80, 78, 102 | ltadd2dd 11420 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) |
| 104 | 4 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) |
| 105 | | iooltub 45523 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) |
| 106 | 97, 99, 100, 105 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) |
| 107 | 80, 104, 78, 106 | ltadd2dd 11420 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) |
| 108 | 92, 95, 81, 103, 107 | eliood 45511 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) |
| 109 | 89, 108 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ) |
| 110 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
| 111 | 1, 2, 3, 4, 110, 5 | fourierdlem28 46150 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
| 112 | 83 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ) |
| 113 | | 0red 11264 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) |
| 114 | | iooretop 24786 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
| 115 | | tgioo4 24826 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 116 | 114, 115 | eleqtri 2839 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) |
| 117 | 116 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
| 118 | 12 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 119 | 87, 117, 118 | dvmptconst 45930 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0)) |
| 120 | 87, 88, 109, 111, 112, 113, 119 | dvmptsub 26005 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0))) |
| 121 | 109 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ) |
| 122 | 121 | subid1d 11609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) |
| 123 | 122 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
| 124 | 120, 123 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
| 125 | 124 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (ℝ D (𝑠 ∈
(𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
| 126 | 121 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ) |
| 127 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ) |
| 128 | 79 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ) |
| 129 | 128 | halfcld 12511 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ) |
| 130 | 129 | sincld 16166 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ) |
| 131 | 127, 130 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) |
| 132 | 131 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) |
| 133 | | fourierdlem68.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 134 | 133 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ 𝐸 ∈
ℝ) |
| 135 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 136 | 21, 135 | remulcli 11277 |
. . . . . . . 8
⊢ (2
· 1) ∈ ℝ |
| 137 | 136 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (2 · 1) ∈ ℝ) |
| 138 | | 1red 11262 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ 1 ∈ ℝ) |
| 139 | | fourierdlem68.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 140 | 118 | abscld 15475 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
| 141 | 139, 140 | readdcld 11290 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 + (abs‘𝐶)) ∈ ℝ) |
| 142 | 141 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (𝐷 +
(abs‘𝐶)) ∈
ℝ) |
| 143 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝜑) |
| 144 | 143, 108 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
| 145 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑋 + 𝑠) → (𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ↔ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
| 146 | 145 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑋 + 𝑠) → ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) ↔ (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))) |
| 147 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑋 + 𝑠) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) |
| 148 | 147 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
| 149 | 148 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸 ↔ (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)) |
| 150 | 146, 149 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))) |
| 151 | | fourierdlem68.fdvbd |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) |
| 152 | 150, 151 | vtoclg 3554 |
. . . . . . . . 9
⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)) |
| 153 | 81, 144, 152 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸) |
| 154 | 153 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸) |
| 155 | 127, 130 | absmuld 15493 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 ·
(sin‘(𝑠 / 2)))) =
((abs‘2) · (abs‘(sin‘(𝑠 / 2))))) |
| 156 | | 0le2 12368 |
. . . . . . . . . . . 12
⊢ 0 ≤
2 |
| 157 | | absid 15335 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2) |
| 158 | 21, 156, 157 | mp2an 692 |
. . . . . . . . . . 11
⊢
(abs‘2) = 2 |
| 159 | 158 | oveq1i 7441 |
. . . . . . . . . 10
⊢
((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) = (2 ·
(abs‘(sin‘(𝑠 /
2)))) |
| 160 | 130 | abscld 15475 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ∈
ℝ) |
| 161 | | 1red 11262 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 1 ∈ ℝ) |
| 162 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℝ) |
| 163 | 156 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 0 ≤ 2) |
| 164 | 79 | rehalfcld 12513 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℝ) |
| 165 | | abssinbd 45307 |
. . . . . . . . . . . 12
⊢ ((𝑠 / 2) ∈ ℝ →
(abs‘(sin‘(𝑠 /
2))) ≤ 1) |
| 166 | 164, 165 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ≤ 1) |
| 167 | 160, 161,
162, 163, 166 | lemul2ad 12208 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 ·
(abs‘(sin‘(𝑠 /
2)))) ≤ (2 · 1)) |
| 168 | 159, 167 | eqbrtrid 5178 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((abs‘2) ·
(abs‘(sin‘(𝑠 /
2)))) ≤ (2 · 1)) |
| 169 | 155, 168 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 ·
(sin‘(𝑠 / 2)))) ≤
(2 · 1)) |
| 170 | 169 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(2 ·
(sin‘(𝑠 / 2)))) ≤
(2 · 1)) |
| 171 | | abscosbd 45290 |
. . . . . . . . 9
⊢ ((𝑠 / 2) ∈ ℝ →
(abs‘(cos‘(𝑠 /
2))) ≤ 1) |
| 172 | 100, 164,
171 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1) |
| 173 | 172 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1) |
| 174 | 85 | abscld 15475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ) |
| 175 | 88 | abscld 15475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ∈ ℝ) |
| 176 | 112 | abscld 15475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘𝐶) ∈ ℝ) |
| 177 | 175, 176 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ∈ ℝ) |
| 178 | 139 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℝ) |
| 179 | 178, 176 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐷 + (abs‘𝐶)) ∈ ℝ) |
| 180 | 88, 112 | abs2dif2d 15497 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶))) |
| 181 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝑋 + 𝑠) → (𝐹‘𝑡) = (𝐹‘(𝑋 + 𝑠))) |
| 182 | 181 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘(𝐹‘𝑡)) = (abs‘(𝐹‘(𝑋 + 𝑠)))) |
| 183 | 182 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘(𝐹‘𝑡)) ≤ 𝐷 ↔ (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)) |
| 184 | 146, 183 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))) |
| 185 | | fourierdlem68.fbd |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) |
| 186 | 184, 185 | vtoclg 3554 |
. . . . . . . . . . 11
⊢ ((𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)) |
| 187 | 108, 144,
186 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷) |
| 188 | 175, 178,
176, 187 | leadd1dd 11877 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ≤ (𝐷 + (abs‘𝐶))) |
| 189 | 174, 177,
179, 180, 188 | letrd 11418 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶))) |
| 190 | 189 | 3ad2antl1 1186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶))) |
| 191 | 14 | simpri 485 |
. . . . . . . 8
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))) |
| 192 | 191 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ (ℝ D (𝑠 ∈
(𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) |
| 193 | 129 | coscld 16167 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ) |
| 194 | 193 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ) |
| 195 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ 𝑐 ∈
ℝ+) |
| 196 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑠 → (𝑡 / 2) = (𝑠 / 2)) |
| 197 | 196 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑠 → (sin‘(𝑡 / 2)) = (sin‘(𝑠 / 2))) |
| 198 | 197 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑠 → (2 · (sin‘(𝑡 / 2))) = (2 ·
(sin‘(𝑠 /
2)))) |
| 199 | 198 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑠 → (abs‘(2 ·
(sin‘(𝑡 / 2)))) =
(abs‘(2 · (sin‘(𝑠 / 2))))) |
| 200 | 199 | breq2d 5155 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2))))
↔ 𝑐 ≤ (abs‘(2
· (sin‘(𝑠 /
2)))))) |
| 201 | 200 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
(𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2))))
↔ ∀𝑠 ∈
(𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 202 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠𝜑 |
| 203 | | nfra1 3284 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2)))) |
| 204 | 202, 203 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑠(𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 205 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 206 | 6, 100 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵)) |
| 207 | 206 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵)) |
| 208 | | rspa 3248 |
. . . . . . . . . . . 12
⊢
((∀𝑠 ∈
(𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))) ∧
𝑠 ∈ (𝐴[,]𝐵)) → 𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 209 | 205, 207,
208 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 210 | 209 | ex 412 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
→ (𝑠 ∈ (𝐴(,)𝐵) → 𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2)))))) |
| 211 | 204, 210 | ralrimi 3257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 / 2)))))
→ ∀𝑠 ∈
(𝐴(,)𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 212 | 201, 211 | sylan2b 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ∀𝑠 ∈
(𝐴(,)𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 213 | 212 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ∀𝑠 ∈
(𝐴(,)𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑠 /
2))))) |
| 214 | | eqid 2737 |
. . . . . . 7
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) |
| 215 | 76, 86, 125, 126, 132, 134, 137, 138, 142, 154, 170, 173, 190, 192, 194, 195, 213, 214 | dvdivbd 45938 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ ℝ+ ∧
∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2)))))
→ ∃𝑏 ∈
ℝ ∀𝑠 ∈
(𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏) |
| 216 | 215 | rexlimdv3a 3159 |
. . . . 5
⊢ (𝜑 → (∃𝑐 ∈ ℝ+ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 ·
(sin‘(𝑡 / 2))))
→ ∃𝑏 ∈
ℝ ∀𝑠 ∈
(𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
| 217 | 74, 216 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏) |
| 218 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑠ℝ |
| 219 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑠
D |
| 220 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑠(𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) |
| 221 | 13, 220 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑠𝑂 |
| 222 | 218, 219,
221 | nfov 7461 |
. . . . . . . 8
⊢
Ⅎ𝑠(ℝ D 𝑂) |
| 223 | 222 | nfdm 5962 |
. . . . . . 7
⊢
Ⅎ𝑠dom
(ℝ D 𝑂) |
| 224 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑠(𝐴(,)𝐵) |
| 225 | 223, 224 | raleqf 3353 |
. . . . . 6
⊢ (dom
(ℝ D 𝑂) = (𝐴(,)𝐵) → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
| 226 | 17, 225 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
| 227 | 226 | rexbidv 3179 |
. . . 4
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
| 228 | 217, 227 | mpbird 257 |
. . 3
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏) |
| 229 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) |
| 230 | 229 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))) |
| 231 | 230 | fveq1d 6908 |
. . . . . 6
⊢ (𝜑 → ((ℝ D 𝑂)‘𝑠) = ((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) |
| 232 | 231 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (abs‘((ℝ D
𝑂)‘𝑠)) = (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠))) |
| 233 | 232 | breq1d 5153 |
. . . 4
⊢ (𝜑 → ((abs‘((ℝ D
𝑂)‘𝑠)) ≤ 𝑏 ↔ (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
| 234 | 233 | rexralbidv 3223 |
. . 3
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)) |
| 235 | 228, 234 | mpbird 257 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏) |
| 236 | 17, 235 | jca 511 |
1
⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)) |