Proof of Theorem fourierdlem57
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem57.fdv | . . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) | 
| 2 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) | 
| 3 |  | fourierdlem57.xre | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 4 |  | fourierdlem57.a | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 5 | 3, 4 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ) | 
| 6 | 5 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 + 𝐴) ∈
ℝ*) | 
| 7 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈
ℝ*) | 
| 8 |  | fourierdlem57.b | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 9 | 3, 8 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ) | 
| 10 | 9 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 + 𝐵) ∈
ℝ*) | 
| 11 | 10 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈
ℝ*) | 
| 12 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) | 
| 13 |  | elioore 13417 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) | 
| 14 | 13 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 15 | 12, 14 | readdcld 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) | 
| 16 | 4 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 17 | 16 | rexrd 11311 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) | 
| 18 | 8 | rexrd 11311 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 19 | 18 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) | 
| 20 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) | 
| 21 |  | ioogtlb 45508 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 22 | 17, 19, 20, 21 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 23 | 16, 14, 12, 22 | ltadd2dd 11420 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) | 
| 24 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) | 
| 25 |  | iooltub 45523 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 26 | 17, 19, 20, 25 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 27 | 14, 24, 12, 26 | ltadd2dd 11420 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) | 
| 28 | 7, 11, 15, 23, 27 | eliood 45511 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) | 
| 29 | 2, 28 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ) | 
| 30 |  | 2re 12340 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 31 | 30 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ) | 
| 32 |  | rehalfcl 12492 | . . . . . . . . . . 11
⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈
ℝ) | 
| 33 | 14, 32 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ) | 
| 34 | 33 | resincld 16179 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ) | 
| 35 | 31, 34 | remulcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈
ℝ) | 
| 36 | 29, 35 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) ∈
ℝ) | 
| 37 | 33 | recoscld 16180 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℝ) | 
| 38 |  | fourierdlem57.f | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 39 | 38 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) | 
| 40 | 39, 15 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) | 
| 41 |  | fourierdlem57.c | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 42 | 41 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ) | 
| 43 | 40, 42 | resubcld 11691 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ) | 
| 44 | 37, 43 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ) | 
| 45 | 36, 44 | resubcld 11691 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) ∈ ℝ) | 
| 46 | 35 | resqcld 14165 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ∈
ℝ) | 
| 47 |  | 2cnd 12344 | . . . . . . . . 9
⊢ (𝑠 ∈ ℝ → 2 ∈
ℂ) | 
| 48 | 32 | recnd 11289 | . . . . . . . . . 10
⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈
ℂ) | 
| 49 | 48 | sincld 16166 | . . . . . . . . 9
⊢ (𝑠 ∈ ℝ →
(sin‘(𝑠 / 2)) ∈
ℂ) | 
| 50 | 47, 49 | mulcld 11281 | . . . . . . . 8
⊢ (𝑠 ∈ ℝ → (2
· (sin‘(𝑠 /
2))) ∈ ℂ) | 
| 51 | 14, 50 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) | 
| 52 |  | 2cnd 12344 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) | 
| 53 | 14, 49 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ) | 
| 54 |  | 2ne0 12370 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 55 | 54 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) | 
| 56 |  | fourierdlem57.ab | . . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) | 
| 57 | 56 | sselda 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π)) | 
| 58 |  | eqcom 2744 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = 0 ↔ 0 = 𝑠) | 
| 59 | 58 | biimpi 216 | . . . . . . . . . . . . . 14
⊢ (𝑠 = 0 → 0 = 𝑠) | 
| 60 | 59 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 = 𝑠) | 
| 61 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴(,)𝐵)) | 
| 62 | 60, 61 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 63 | 62 | adantll 714 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 64 |  | fourierdlem57.n0 | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 65 | 64 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 66 | 63, 65 | pm2.65da 817 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0) | 
| 67 | 66 | neqned 2947 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) | 
| 68 |  | fourierdlem44 46166 | . . . . . . . . 9
⊢ ((𝑠 ∈ (-π[,]π) ∧
𝑠 ≠ 0) →
(sin‘(𝑠 / 2)) ≠
0) | 
| 69 | 57, 67, 68 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0) | 
| 70 | 52, 53, 55, 69 | mulne0d 11915 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0) | 
| 71 |  | 2z 12649 | . . . . . . . 8
⊢ 2 ∈
ℤ | 
| 72 | 71 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ) | 
| 73 | 51, 70, 72 | expne0d 14192 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ≠
0) | 
| 74 | 45, 46, 73 | redivcld 12095 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)) ∈
ℝ) | 
| 75 |  | eqid 2737 | . . . . 5
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 /
2)))↑2))) | 
| 76 | 74, 75 | fmptd 7134 | . . . 4
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ) | 
| 77 |  | fourierdlem57.o | . . . . . . . 8
⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) | 
| 78 | 77 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) | 
| 79 | 78 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))) | 
| 80 |  | reelprrecn 11247 | . . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} | 
| 81 | 80 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 82 | 43 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) | 
| 83 | 40 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) | 
| 84 |  | eqid 2737 | . . . . . . . . . 10
⊢ (ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) | 
| 85 | 38, 3, 4, 8, 84, 1 | fourierdlem28 46150 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) | 
| 86 | 42 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ) | 
| 87 |  | 0red 11264 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 88 |  | iooretop 24786 | . . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) | 
| 89 |  | tgioo4 24826 | . . . . . . . . . . . 12
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 90 | 88, 89 | eleqtri 2839 | . . . . . . . . . . 11
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) | 
| 91 | 90 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) | 
| 92 | 41 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 93 | 81, 91, 92 | dvmptconst 45930 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0)) | 
| 94 | 81, 83, 29, 85, 86, 87, 93 | dvmptsub 26005 | . . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0))) | 
| 95 | 29 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ) | 
| 96 | 95 | subid1d 11609 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) | 
| 97 | 96 | mpteq2dva 5242 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) | 
| 98 | 94, 97 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) | 
| 99 |  | eldifsn 4786 | . . . . . . . 8
⊢ ((2
· (sin‘(𝑠 /
2))) ∈ (ℂ ∖ {0}) ↔ ((2 · (sin‘(𝑠 / 2))) ∈ ℂ ∧ (2
· (sin‘(𝑠 /
2))) ≠ 0)) | 
| 100 | 51, 70, 99 | sylanbrc 583 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖
{0})) | 
| 101 |  | recn 11245 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) | 
| 102 | 54 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 2 ≠
0) | 
| 103 | 101, 47, 102 | divrec2d 12047 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ → (𝑠 / 2) = ((1 / 2) · 𝑠)) | 
| 104 | 103 | eqcomd 2743 | . . . . . . . . . . 11
⊢ (𝑠 ∈ ℝ → ((1 / 2)
· 𝑠) = (𝑠 / 2)) | 
| 105 | 13, 104 | syl 17 | . . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((1 / 2) · 𝑠) = (𝑠 / 2)) | 
| 106 | 105 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2))) | 
| 107 |  | halfcn 12481 | . . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℂ | 
| 108 | 107 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℂ → (1 / 2)
∈ ℂ) | 
| 109 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℂ → 𝑠 ∈
ℂ) | 
| 110 | 108, 109 | mulcld 11281 | . . . . . . . . . . 11
⊢ (𝑠 ∈ ℂ → ((1 / 2)
· 𝑠) ∈
ℂ) | 
| 111 | 110 | coscld 16167 | . . . . . . . . . 10
⊢ (𝑠 ∈ ℂ →
(cos‘((1 / 2) · 𝑠)) ∈ ℂ) | 
| 112 | 13, 101, 111 | 3syl 18 | . . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) ∈
ℂ) | 
| 113 | 106, 112 | eqeltrrd 2842 | . . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ) | 
| 114 | 113 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ) | 
| 115 |  | ioossre 13448 | . . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℝ | 
| 116 |  | resmpt 6055 | . . . . . . . . . . . . 13
⊢ ((𝐴(,)𝐵) ⊆ ℝ → ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) | 
| 117 | 115, 116 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))) | 
| 118 | 117 | eqcomi 2746 | . . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2))))
↾ (𝐴(,)𝐵)) | 
| 119 | 118 | oveq2i 7442 | . . . . . . . . . 10
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ (𝐴(,)𝐵))) | 
| 120 |  | ax-resscn 11212 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℂ | 
| 121 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) = (𝑠 ∈ ℝ
↦ (2 · (sin‘(𝑠 / 2)))) | 
| 122 | 121, 50 | fmpti 7132 | . . . . . . . . . . 11
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))):ℝ⟶ℂ | 
| 123 |  | ssid 4006 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℝ | 
| 124 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 125 | 124, 89 | dvres 25946 | . . . . . . . . . . 11
⊢
(((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ)) → (ℝ D
((𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))) | 
| 126 | 120, 122,
123, 115, 125 | mp4an 693 | . . . . . . . . . 10
⊢ (ℝ
D ((𝑠 ∈ ℝ
↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2)))))
↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) | 
| 127 |  | resmpt 6055 | . . . . . . . . . . . . . . 15
⊢ (ℝ
⊆ ℂ → ((𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) | 
| 128 | 120, 127 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) | 
| 129 | 104 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℝ →
(sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2))) | 
| 130 | 129 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℝ → (2
· (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2)))) | 
| 131 | 130 | mpteq2ia 5245 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))) | 
| 132 | 128, 131 | eqtr2i 2766 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) = ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) | 
| 133 | 132 | oveq2i 7442 | . . . . . . . . . . . 12
⊢ (ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) = (ℝ D ((𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾
ℝ)) | 
| 134 |  | ioontr 45524 | . . . . . . . . . . . 12
⊢
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵) | 
| 135 | 133, 134 | reseq12i 5995 | . . . . . . . . . . 11
⊢ ((ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = ((ℝ D ((𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵)) | 
| 136 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) | 
| 137 |  | 2cnd 12344 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ → 2 ∈
ℂ) | 
| 138 | 110 | sincld 16166 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ →
(sin‘((1 / 2) · 𝑠)) ∈ ℂ) | 
| 139 | 137, 138 | mulcld 11281 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℂ → (2
· (sin‘((1 / 2) · 𝑠))) ∈ ℂ) | 
| 140 | 136, 139 | fmpti 7132 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ | 
| 141 |  | ssid 4006 | . . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ | 
| 142 |  | dmmptg 6262 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑠 ∈
ℂ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ → dom
(𝑠 ∈ ℂ ↦
((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ) | 
| 143 |  | 2cn 12341 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ | 
| 144 | 143, 107 | mulcli 11268 | . . . . . . . . . . . . . . . . . 18
⊢ (2
· (1 / 2)) ∈ ℂ | 
| 145 | 144 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℂ → (2
· (1 / 2)) ∈ ℂ) | 
| 146 | 145, 111 | mulcld 11281 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℂ → ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ) | 
| 147 | 142, 146 | mprg 3067 | . . . . . . . . . . . . . . 15
⊢ dom
(𝑠 ∈ ℂ ↦
((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ | 
| 148 | 120, 147 | sseqtrri 4033 | . . . . . . . . . . . . . 14
⊢ ℝ
⊆ dom (𝑠 ∈
ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) ·
𝑠)))) | 
| 149 |  | dvasinbx 45935 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠))))) | 
| 150 | 143, 107,
149 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) | 
| 151 | 150 | dmeqi 5915 | . . . . . . . . . . . . . 14
⊢ dom
(ℂ D (𝑠 ∈
ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) | 
| 152 | 148, 151 | sseqtrri 4033 | . . . . . . . . . . . . 13
⊢ ℝ
⊆ dom (ℂ D (𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) | 
| 153 |  | dvres3 25948 | . . . . . . . . . . . . 13
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠))))))) → (ℝ D ((𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)) | 
| 154 | 80, 140, 141, 152, 153 | mp4an 693 | . . . . . . . . . . . 12
⊢ (ℝ
D ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) | 
| 155 | 154 | reseq1i 5993 | . . . . . . . . . . 11
⊢ ((ℝ
D ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵)) = (((ℂ D (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) | 
| 156 | 150 | reseq1i 5993 | . . . . . . . . . . . . 13
⊢ ((ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) | 
| 157 | 156 | reseq1i 5993 | . . . . . . . . . . . 12
⊢
(((ℂ D (𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾
(𝐴(,)𝐵)) = (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) | 
| 158 |  | resabs1 6024 | . . . . . . . . . . . . 13
⊢ ((𝐴(,)𝐵) ⊆ ℝ → (((𝑠 ∈ ℂ ↦ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵))) | 
| 159 | 115, 158 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (((𝑠 ∈ ℂ ↦ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) | 
| 160 |  | ioosscn 13449 | . . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℂ | 
| 161 |  | resmpt 6055 | . . . . . . . . . . . . 13
⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑠 ∈ ℂ ↦ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠))))) | 
| 162 | 160, 161 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ ℂ ↦ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠)))) | 
| 163 | 157, 159,
162 | 3eqtri 2769 | . . . . . . . . . . 11
⊢
(((ℂ D (𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾
(𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠)))) | 
| 164 | 135, 155,
163 | 3eqtri 2769 | . . . . . . . . . 10
⊢ ((ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠)))) | 
| 165 | 119, 126,
164 | 3eqtri 2769 | . . . . . . . . 9
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠)))) | 
| 166 | 143, 54 | recidi 11998 | . . . . . . . . . . . . 13
⊢ (2
· (1 / 2)) = 1 | 
| 167 | 166 | oveq1i 7441 | . . . . . . . . . . . 12
⊢ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘((1 / 2)
· 𝑠))) | 
| 168 | 167 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠))) = (1 · (cos‘((1 / 2)
· 𝑠)))) | 
| 169 | 112 | mullidd 11279 | . . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴(,)𝐵) → (1 · (cos‘((1 / 2)
· 𝑠))) =
(cos‘((1 / 2) · 𝑠))) | 
| 170 | 168, 169,
106 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2))) | 
| 171 | 170 | mpteq2ia 5245 | . . . . . . . . 9
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) ·
(cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))) | 
| 172 | 165, 171 | eqtri 2765 | . . . . . . . 8
⊢ (ℝ
D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))) | 
| 173 | 172 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) | 
| 174 | 81, 82, 29, 98, 100, 114, 173 | dvmptdiv 26012 | . . . . . 6
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 /
2)))↑2)))) | 
| 175 | 79, 174 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 /
2)))↑2)))) | 
| 176 | 175 | feq1d 6720 | . . . 4
⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ)) | 
| 177 | 76, 176 | mpbird 257 | . . 3
⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ) | 
| 178 | 177, 175 | jca 511 | . 2
⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 /
2)))↑2))))) | 
| 179 | 178, 172 | pm3.2i 470 | 1
⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) −
((cos‘(𝑠 / 2))
· ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧
(ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) |