Proof of Theorem fourierdlem78
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem78.g | . . . . 5
⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠)))) | 
| 3 | 2 | reseq1d 5995 | . . 3
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ↾ (𝐴(,)𝐵))) | 
| 4 |  | pire 26501 | . . . . . . . . 9
⊢ π
∈ ℝ | 
| 5 | 4 | renegcli 11571 | . . . . . . . 8
⊢ -π
∈ ℝ | 
| 6 | 5 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π ∈
ℝ) | 
| 7 | 4 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → π ∈
ℝ) | 
| 8 |  | elioore 13418 | . . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) | 
| 9 | 8 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 10 | 5 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → -π ∈
ℝ) | 
| 11 | 4 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → π ∈
ℝ) | 
| 12 | 10, 11 | iccssred 13475 | . . . . . . . . . . 11
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) | 
| 13 |  | fourierdlem78.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (-π[,]π)) | 
| 14 | 12, 13 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 15 | 14 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 16 | 5, 4 | elicc2i 13454 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (-π[,]π) ↔
(𝐴 ∈ ℝ ∧
-π ≤ 𝐴 ∧ 𝐴 ≤ π)) | 
| 17 | 16 | simp2bi 1146 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (-π[,]π) →
-π ≤ 𝐴) | 
| 18 | 13, 17 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → -π ≤ 𝐴) | 
| 19 | 18 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝐴) | 
| 20 | 15 | rexrd 11312 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) | 
| 21 |  | fourierdlem78.b | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ (-π[,]π)) | 
| 22 | 12, 21 | sseldd 3983 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 23 | 22 | rexrd 11312 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 24 | 23 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) | 
| 25 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) | 
| 26 |  | ioogtlb 45513 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 27 | 20, 24, 25, 26 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 28 | 6, 15, 9, 19, 27 | lelttrd 11420 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π < 𝑠) | 
| 29 | 6, 9, 28 | ltled 11410 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝑠) | 
| 30 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) | 
| 31 |  | iooltub 45528 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 32 | 20, 24, 25, 31 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 33 | 5, 4 | elicc2i 13454 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ (-π[,]π) ↔
(𝐵 ∈ ℝ ∧
-π ≤ 𝐵 ∧ 𝐵 ≤ π)) | 
| 34 | 33 | simp3bi 1147 | . . . . . . . . . . 11
⊢ (𝐵 ∈ (-π[,]π) →
𝐵 ≤
π) | 
| 35 | 21, 34 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≤ π) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ π) | 
| 37 | 9, 30, 7, 32, 36 | ltletrd 11422 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < π) | 
| 38 | 9, 7, 37 | ltled 11410 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≤ π) | 
| 39 | 6, 7, 9, 29, 38 | eliccd 45522 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π)) | 
| 40 | 39 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ (-π[,]π))) | 
| 41 | 40 | ssrdv 3988 | . . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) | 
| 42 | 41 | resmptd 6057 | . . 3
⊢ (𝜑 → ((𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠)))) | 
| 43 | 3, 42 | eqtrd 2776 | . 2
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠)))) | 
| 44 |  | 0red 11265 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 45 |  | fourierdlem78.f | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) | 
| 47 |  | fourierdlem78.x | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) | 
| 49 | 48, 9 | readdcld 11291 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) | 
| 50 | 46, 49 | ffvelcdmd 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) | 
| 51 |  | fourierdlem78.y | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 52 |  | fourierdlem78.w | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ ℝ) | 
| 53 | 51, 52 | ifcld 4571 | . . . . . . . . . . . . . 14
⊢ (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ) | 
| 54 | 53 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ) | 
| 55 | 50, 54 | resubcld 11692 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ) | 
| 56 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = 0 → (𝑠 ∈ (𝐴(,)𝐵) ↔ 0 ∈ (𝐴(,)𝐵))) | 
| 57 | 56 | biimpac 478 | . . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 58 | 57 | adantll 714 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 59 |  | fourierdlem78.nxelab | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 60 | 59 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 61 | 58, 60 | pm2.65da 816 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0) | 
| 62 | 61 | neqned 2946 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) | 
| 63 | 55, 9, 62 | redivcld 12096 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℝ) | 
| 64 | 44, 63 | ifcld 4571 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ) | 
| 65 |  | fourierdlem78.h | . . . . . . . . . . 11
⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) | 
| 66 | 65 | fvmpt2 7026 | . . . . . . . . . 10
⊢ ((𝑠 ∈ (-π[,]π) ∧
if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) | 
| 67 | 39, 64, 66 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐻‘𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) | 
| 68 | 67, 64 | eqeltrd 2840 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐻‘𝑠) ∈ ℝ) | 
| 69 |  | 1red 11263 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ) | 
| 70 |  | 2re 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ | 
| 71 | 70 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ) | 
| 72 | 9 | rehalfcld 12515 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ) | 
| 73 | 72 | resincld 16180 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ) | 
| 74 | 71, 73 | remulcld 11292 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈
ℝ) | 
| 75 | 71 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) | 
| 76 | 73 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ) | 
| 77 |  | 2ne0 12371 | . . . . . . . . . . . . . 14
⊢ 2 ≠
0 | 
| 78 | 77 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) | 
| 79 |  | fourierdlem44 46171 | . . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ (-π[,]π) ∧
𝑠 ≠ 0) →
(sin‘(𝑠 / 2)) ≠
0) | 
| 80 | 39, 62, 79 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0) | 
| 81 | 75, 76, 78, 80 | mulne0d 11916 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0) | 
| 82 | 9, 74, 81 | redivcld 12096 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ) | 
| 83 | 69, 82 | ifcld 4571 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ) | 
| 84 |  | fourierdlem78.k | . . . . . . . . . . 11
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) | 
| 85 | 84 | fvmpt2 7026 | . . . . . . . . . 10
⊢ ((𝑠 ∈ (-π[,]π) ∧
if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ) →
(𝐾‘𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) | 
| 86 | 39, 83, 85 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐾‘𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) | 
| 87 | 86, 83 | eqeltrd 2840 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐾‘𝑠) ∈ ℝ) | 
| 88 | 68, 87 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐻‘𝑠) · (𝐾‘𝑠)) ∈ ℝ) | 
| 89 |  | fourierdlem78.u | . . . . . . . 8
⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) | 
| 90 | 89 | fvmpt2 7026 | . . . . . . 7
⊢ ((𝑠 ∈ (-π[,]π) ∧
((𝐻‘𝑠) · (𝐾‘𝑠)) ∈ ℝ) → (𝑈‘𝑠) = ((𝐻‘𝑠) · (𝐾‘𝑠))) | 
| 91 | 39, 88, 90 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑈‘𝑠) = ((𝐻‘𝑠) · (𝐾‘𝑠))) | 
| 92 | 91, 88 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑈‘𝑠) ∈ ℝ) | 
| 93 |  | fourierdlem78.n | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 94 | 93 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑁 ∈ ℝ) | 
| 95 | 71, 78 | rereccld 12095 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈
ℝ) | 
| 96 | 94, 95 | readdcld 11291 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℝ) | 
| 97 | 96, 9 | remulcld 11292 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑠) ∈ ℝ) | 
| 98 | 97 | resincld 16180 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ) | 
| 99 |  | fourierdlem78.s | . . . . . . . 8
⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦
(sin‘((𝑁 + (1 / 2))
· 𝑠))) | 
| 100 | 99 | fvmpt2 7026 | . . . . . . 7
⊢ ((𝑠 ∈ (-π[,]π) ∧
(sin‘((𝑁 + (1 / 2))
· 𝑠)) ∈
ℝ) → (𝑆‘𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠))) | 
| 101 | 39, 98, 100 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑆‘𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠))) | 
| 102 | 101, 98 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑆‘𝑠) ∈ ℝ) | 
| 103 | 92, 102 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝑈‘𝑠) · (𝑆‘𝑠)) ∈ ℝ) | 
| 104 |  | eqid 2736 | . . . 4
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) | 
| 105 | 103, 104 | fmptd 7133 | . . 3
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))):(𝐴(,)𝐵)⟶ℝ) | 
| 106 |  | ax-resscn 11213 | . . . . 5
⊢ ℝ
⊆ ℂ | 
| 107 | 106 | a1i 11 | . . . 4
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 108 | 91 | mpteq2dva 5241 | . . . . . 6
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈‘𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))) | 
| 109 | 61 | iffalsed 4535 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) | 
| 110 | 55 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ) | 
| 111 | 9 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ) | 
| 112 | 110, 111,
62 | divrecd 12047 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) | 
| 113 | 67, 109, 112 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐻‘𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) | 
| 114 | 113 | mpteq2dva 5241 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻‘𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))) | 
| 115 | 50 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) | 
| 116 | 54 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ) | 
| 117 | 115, 116 | negsubd 11627 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) | 
| 118 | 117 | eqcomd 2742 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) | 
| 119 | 118 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)))) | 
| 120 | 14, 47 | readdcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ) | 
| 121 | 120 | rexrd 11312 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 + 𝑋) ∈
ℝ*) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) ∈
ℝ*) | 
| 123 | 22, 47 | readdcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ) | 
| 124 | 123 | rexrd 11312 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 + 𝑋) ∈
ℝ*) | 
| 125 | 124 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐵 + 𝑋) ∈
ℝ*) | 
| 126 | 14 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 127 | 47 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 128 | 126, 127 | addcomd 11464 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 + 𝑋) = (𝑋 + 𝐴)) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) = (𝑋 + 𝐴)) | 
| 130 | 15, 9, 48, 27 | ltadd2dd 11421 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) | 
| 131 | 129, 130 | eqbrtrd 5164 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) < (𝑋 + 𝑠)) | 
| 132 | 9, 30, 48, 32 | ltadd2dd 11421 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) | 
| 133 | 22 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 134 | 127, 133 | addcomd 11464 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 + 𝐵) = (𝐵 + 𝑋)) | 
| 135 | 134 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) = (𝐵 + 𝑋)) | 
| 136 | 132, 135 | breqtrd 5168 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝐵 + 𝑋)) | 
| 137 | 122, 125,
49, 131, 136 | eliood 45516 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) | 
| 138 |  | fvres 6924 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠))) | 
| 139 | 137, 138 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠))) | 
| 140 | 139 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) | 
| 141 | 140 | mpteq2dva 5241 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)))) | 
| 142 |  | ioosscn 13450 | . . . . . . . . . . . . . 14
⊢ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ | 
| 143 | 142 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ) | 
| 144 |  | fourierdlem78.fcn | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ)) | 
| 145 |  | ioosscn 13450 | . . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ℂ | 
| 146 | 145 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) | 
| 147 | 143, 144,
146, 127, 137 | fourierdlem23 46150 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 148 | 141, 147 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 149 |  | 0red 11265 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 150 | 14 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 151 | 8 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 152 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝐴) | 
| 153 | 27 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 154 | 149, 150,
151, 152, 153 | lelttrd 11420 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 < 𝑠) | 
| 155 | 154 | iftrued 4532 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌) | 
| 156 | 155 | negeqd 11503 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑌) | 
| 157 | 156 | mpteq2dva 5241 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌)) | 
| 158 | 51 | renegcld 11691 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → -𝑌 ∈ ℝ) | 
| 159 | 158 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → -𝑌 ∈ ℂ) | 
| 160 |  | ssid 4005 | . . . . . . . . . . . . . . . 16
⊢ ℂ
⊆ ℂ | 
| 161 | 160 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 162 | 146, 159,
161 | constcncfg 45892 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 163 | 162 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 164 | 157, 163 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 165 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝜑) | 
| 166 | 14 | rexrd 11312 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 167 | 166 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 ∈
ℝ*) | 
| 168 | 23 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈
ℝ*) | 
| 169 |  | 0red 11265 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈
ℝ) | 
| 170 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → ¬ 0 ≤ 𝐴) | 
| 171 | 14 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 ∈ ℝ) | 
| 172 |  | 0red 11265 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 0 ∈
ℝ) | 
| 173 | 171, 172 | ltnled 11409 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝐴 < 0 ↔ ¬ 0 ≤ 𝐴)) | 
| 174 | 170, 173 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 < 0) | 
| 175 | 174 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 < 0) | 
| 176 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → ¬ 𝐵 ≤ 0) | 
| 177 |  | 0red 11265 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 ∈
ℝ) | 
| 178 | 22 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ) | 
| 179 | 177, 178 | ltnled 11409 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0)) | 
| 180 | 176, 179 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵) | 
| 181 | 180 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵) | 
| 182 | 167, 168,
169, 175, 181 | eliood 45516 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ (𝐴(,)𝐵)) | 
| 183 | 59 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → ¬ 0 ∈ (𝐴(,)𝐵)) | 
| 184 | 182, 183 | condan 817 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐵 ≤ 0) | 
| 185 | 8 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 186 |  | 0red 11265 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) | 
| 187 | 22 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) | 
| 188 | 32 | adantlr 715 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 189 |  | simplr 768 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ 0) | 
| 190 | 185, 187,
186, 188, 189 | ltletrd 11422 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 0) | 
| 191 | 185, 186,
190 | ltnsymd 11411 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 0 < 𝑠) | 
| 192 | 191 | iffalsed 4535 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊) | 
| 193 | 192 | negeqd 11503 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑊) | 
| 194 | 193 | mpteq2dva 5241 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊)) | 
| 195 | 52 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑊 ∈ ℂ) | 
| 196 | 195 | negcld 11608 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → -𝑊 ∈ ℂ) | 
| 197 | 146, 196,
161 | constcncfg 45892 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 198 | 197 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 199 | 194, 198 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 200 | 165, 184,
199 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 201 | 164, 200 | pm2.61dan 812 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 202 | 148, 201 | addcncf 25479 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 203 | 119, 202 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 204 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑠 ∈ (ℂ ∖ {0})
↦ (1 / 𝑠)) = (𝑠 ∈ (ℂ ∖ {0})
↦ (1 / 𝑠)) | 
| 205 |  | 1cnd 11257 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) | 
| 206 | 204 | cdivcncf 24948 | . . . . . . . . . . 11
⊢ (1 ∈
ℂ → (𝑠 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ)) | 
| 207 | 205, 206 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑠)) ∈ ((ℂ
∖ {0})–cn→ℂ)) | 
| 208 |  | velsn 4641 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0) | 
| 209 | 61, 208 | sylnibr 329 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 ∈ {0}) | 
| 210 | 111, 209 | eldifd 3961 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖
{0})) | 
| 211 | 210 | ralrimiva 3145 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖
{0})) | 
| 212 |  | dfss3 3971 | . . . . . . . . . . 11
⊢ ((𝐴(,)𝐵) ⊆ (ℂ ∖ {0}) ↔
∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖
{0})) | 
| 213 | 211, 212 | sylibr 234 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (ℂ ∖
{0})) | 
| 214 | 9, 62 | rereccld 12095 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℝ) | 
| 215 | 214 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℂ) | 
| 216 | 204, 207,
213, 161, 215 | cncfmptssg 45891 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 217 | 203, 216 | mulcncf 25481 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 218 | 114, 217 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻‘𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 219 | 61 | iffalsed 4535 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2))))) | 
| 220 | 74 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) | 
| 221 | 111, 220,
81 | divrecd 12047 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) | 
| 222 | 86, 219, 221 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐾‘𝑠) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) | 
| 223 | 222 | mpteq2dva 5241 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))) | 
| 224 | 219, 221 | eqtr2d 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) | 
| 225 | 224 | mpteq2dva 5241 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))) | 
| 226 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,]π) ↦
if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) | 
| 227 |  | cncfss 24926 | . . . . . . . . . . . 12
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) →
((-π[,]π)–cn→ℝ)
⊆ ((-π[,]π)–cn→ℂ)) | 
| 228 | 106, 160,
227 | mp2an 692 | . . . . . . . . . . 11
⊢
((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ) | 
| 229 | 226 | fourierdlem62 46188 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,]π) ↦
if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈
((-π[,]π)–cn→ℝ) | 
| 230 | 229 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ)) | 
| 231 | 228, 230 | sselid 3980 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℂ)) | 
| 232 | 83 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ) | 
| 233 | 226, 231,
41, 161, 232 | cncfmptssg 45891 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 234 | 225, 233 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 235 | 223, 234 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 236 | 218, 235 | mulcncf 25481 | . . . . . 6
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 237 | 108, 236 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈‘𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 238 | 101 | mpteq2dva 5241 | . . . . . 6
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆‘𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))) | 
| 239 |  | sincn 26489 | . . . . . . . 8
⊢ sin
∈ (ℂ–cn→ℂ) | 
| 240 | 239 | a1i 11 | . . . . . . 7
⊢ (𝜑 → sin ∈
(ℂ–cn→ℂ)) | 
| 241 |  | halfre 12481 | . . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ | 
| 242 | 241 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (1 / 2) ∈
ℝ) | 
| 243 | 93, 242 | readdcld 11291 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ) | 
| 244 | 243 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ) | 
| 245 | 146, 244,
161 | constcncfg 45892 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 246 | 146, 161 | idcncfg 45893 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 247 | 245, 246 | mulcncf 25481 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 248 | 240, 247 | cncfmpt1f 24941 | . . . . . 6
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 249 | 238, 248 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆‘𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 250 | 237, 249 | mulcncf 25481 | . . . 4
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 251 |  | cncfcdm 24925 | . . . 4
⊢ ((ℝ
⊆ ℂ ∧ (𝑠
∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))):(𝐴(,)𝐵)⟶ℝ)) | 
| 252 | 107, 250,
251 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))):(𝐴(,)𝐵)⟶ℝ)) | 
| 253 | 105, 252 | mpbird 257 | . 2
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ)) | 
| 254 | 43, 253 | eqeltrd 2840 | 1
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |