Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem78 Structured version   Visualization version   GIF version

Theorem fourierdlem78 45805
Description: 𝐺 is continuous when restricted on an interval not containing 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem78.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem78.a (𝜑𝐴 ∈ (-π[,]π))
fourierdlem78.b (𝜑𝐵 ∈ (-π[,]π))
fourierdlem78.x (𝜑𝑋 ∈ ℝ)
fourierdlem78.nxelab (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
fourierdlem78.fcn (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ))
fourierdlem78.y (𝜑𝑌 ∈ ℝ)
fourierdlem78.w (𝜑𝑊 ∈ ℝ)
fourierdlem78.h 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
fourierdlem78.k 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
fourierdlem78.u 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
fourierdlem78.n (𝜑𝑁 ∈ ℝ)
fourierdlem78.s 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))
fourierdlem78.g 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠)))
Assertion
Ref Expression
fourierdlem78 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ))
Distinct variable groups:   𝐴,𝑠   𝐵,𝑠   𝐹,𝑠   𝑁,𝑠   𝑊,𝑠   𝑋,𝑠   𝑌,𝑠   𝜑,𝑠
Allowed substitution hints:   𝑆(𝑠)   𝑈(𝑠)   𝐺(𝑠)   𝐻(𝑠)   𝐾(𝑠)

Proof of Theorem fourierdlem78
StepHypRef Expression
1 fourierdlem78.g . . . . 5 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠)))
21a1i 11 . . . 4 (𝜑𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))))
32reseq1d 5988 . . 3 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))) ↾ (𝐴(,)𝐵)))
4 pire 26486 . . . . . . . . 9 π ∈ ℝ
54renegcli 11571 . . . . . . . 8 -π ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ∈ ℝ)
74a1i 11 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → π ∈ ℝ)
8 elioore 13408 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
98adantl 480 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
105a1i 11 . . . . . . . . . . . 12 (𝜑 → -π ∈ ℝ)
114a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℝ)
1210, 11iccssred 13465 . . . . . . . . . . 11 (𝜑 → (-π[,]π) ⊆ ℝ)
13 fourierdlem78.a . . . . . . . . . . 11 (𝜑𝐴 ∈ (-π[,]π))
1412, 13sseldd 3980 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
1514adantr 479 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
165, 4elicc2i 13444 . . . . . . . . . . . 12 (𝐴 ∈ (-π[,]π) ↔ (𝐴 ∈ ℝ ∧ -π ≤ 𝐴𝐴 ≤ π))
1716simp2bi 1143 . . . . . . . . . . 11 (𝐴 ∈ (-π[,]π) → -π ≤ 𝐴)
1813, 17syl 17 . . . . . . . . . 10 (𝜑 → -π ≤ 𝐴)
1918adantr 479 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝐴)
2015rexrd 11314 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ*)
21 fourierdlem78.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (-π[,]π))
2212, 21sseldd 3980 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2322rexrd 11314 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ*)
2423adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ*)
25 simpr 483 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
26 ioogtlb 45113 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
2720, 24, 25, 26syl3anc 1368 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
286, 15, 9, 19, 27lelttrd 11422 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π < 𝑠)
296, 9, 28ltled 11412 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝑠)
3022adantr 479 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
31 iooltub 45128 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
3220, 24, 25, 31syl3anc 1368 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
335, 4elicc2i 13444 . . . . . . . . . . . 12 (𝐵 ∈ (-π[,]π) ↔ (𝐵 ∈ ℝ ∧ -π ≤ 𝐵𝐵 ≤ π))
3433simp3bi 1144 . . . . . . . . . . 11 (𝐵 ∈ (-π[,]π) → 𝐵 ≤ π)
3521, 34syl 17 . . . . . . . . . 10 (𝜑𝐵 ≤ π)
3635adantr 479 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ π)
379, 30, 7, 32, 36ltletrd 11424 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < π)
389, 7, 37ltled 11412 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≤ π)
396, 7, 9, 29, 38eliccd 45122 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π))
4039ex 411 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ (-π[,]π)))
4140ssrdv 3985 . . . 4 (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
4241resmptd 6049 . . 3 (𝜑 → ((𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))))
433, 42eqtrd 2766 . 2 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))))
44 0red 11267 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
45 fourierdlem78.f . . . . . . . . . . . . . . 15 (𝜑𝐹:ℝ⟶ℝ)
4645adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
47 fourierdlem78.x . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ)
4847adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
4948, 9readdcld 11293 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
5046, 49ffvelcdmd 7099 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
51 fourierdlem78.y . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ)
52 fourierdlem78.w . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ ℝ)
5351, 52ifcld 4579 . . . . . . . . . . . . . 14 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5453adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5550, 54resubcld 11692 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ)
56 eleq1 2814 . . . . . . . . . . . . . . . 16 (𝑠 = 0 → (𝑠 ∈ (𝐴(,)𝐵) ↔ 0 ∈ (𝐴(,)𝐵)))
5756biimpac 477 . . . . . . . . . . . . . . 15 ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
5857adantll 712 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
59 fourierdlem78.nxelab . . . . . . . . . . . . . . 15 (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
6059ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵))
6158, 60pm2.65da 815 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0)
6261neqned 2937 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)
6355, 9, 62redivcld 12093 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℝ)
6444, 63ifcld 4579 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ)
65 fourierdlem78.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6665fvmpt2 7020 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6739, 64, 66syl2anc 582 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6867, 64eqeltrd 2826 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) ∈ ℝ)
69 1red 11265 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ)
70 2re 12338 . . . . . . . . . . . . . 14 2 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
729rehalfcld 12511 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ)
7372resincld 16145 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ)
7471, 73remulcld 11294 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
7571recnd 11292 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
7673recnd 11292 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
77 2ne0 12368 . . . . . . . . . . . . . 14 2 ≠ 0
7877a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
79 fourierdlem44 45772 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
8039, 62, 79syl2anc 582 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
8175, 76, 78, 80mulne0d 11916 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
829, 74, 81redivcld 12093 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
8369, 82ifcld 4579 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ)
84 fourierdlem78.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8584fvmpt2 7020 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8639, 83, 85syl2anc 582 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8786, 83eqeltrd 2826 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) ∈ ℝ)
8868, 87remulcld 11294 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ)
89 fourierdlem78.u . . . . . . . 8 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
9089fvmpt2 7020 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
9139, 88, 90syl2anc 582 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
9291, 88eqeltrd 2826 . . . . 5 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑈𝑠) ∈ ℝ)
93 fourierdlem78.n . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
9493adantr 479 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑁 ∈ ℝ)
9571, 78rereccld 12092 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈ ℝ)
9694, 95readdcld 11293 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℝ)
9796, 9remulcld 11294 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑠) ∈ ℝ)
9897resincld 16145 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ)
99 fourierdlem78.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))
10099fvmpt2 7020 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ) → (𝑆𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠)))
10139, 98, 100syl2anc 582 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑆𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠)))
102101, 98eqeltrd 2826 . . . . 5 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑆𝑠) ∈ ℝ)
10392, 102remulcld 11294 . . . 4 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ)
104 eqid 2726 . . . 4 (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠)))
105103, 104fmptd 7128 . . 3 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ)
106 ax-resscn 11215 . . . . 5 ℝ ⊆ ℂ
107106a1i 11 . . . 4 (𝜑 → ℝ ⊆ ℂ)
10891mpteq2dva 5253 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻𝑠) · (𝐾𝑠))))
10961iffalsed 4544 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
11055recnd 11292 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
1119recnd 11292 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ)
112110, 111, 62divrecd 12044 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))
11367, 109, 1123eqtrd 2770 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))
114113mpteq2dva 5253 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))))
11550recnd 11292 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
11654recnd 11292 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
117115, 116negsubd 11627 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
118117eqcomd 2732 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)))
119118mpteq2dva 5253 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))))
12014, 47readdcld 11293 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + 𝑋) ∈ ℝ)
121120rexrd 11314 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 + 𝑋) ∈ ℝ*)
122121adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) ∈ ℝ*)
12322, 47readdcld 11293 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵 + 𝑋) ∈ ℝ)
124123rexrd 11314 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + 𝑋) ∈ ℝ*)
125124adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐵 + 𝑋) ∈ ℝ*)
12614recnd 11292 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℂ)
12747recnd 11292 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℂ)
128126, 127addcomd 11466 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + 𝑋) = (𝑋 + 𝐴))
129128adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) = (𝑋 + 𝐴))
13015, 9, 48, 27ltadd2dd 11423 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
131129, 130eqbrtrd 5175 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) < (𝑋 + 𝑠))
1329, 30, 48, 32ltadd2dd 11423 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
13322recnd 11292 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℂ)
134127, 133addcomd 11466 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 + 𝐵) = (𝐵 + 𝑋))
135134adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) = (𝐵 + 𝑋))
136132, 135breqtrd 5179 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝐵 + 𝑋))
137122, 125, 49, 131, 136eliood 45116 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))
138 fvres 6920 . . . . . . . . . . . . . . 15 ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
139137, 138syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
140139eqcomd 2732 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)))
141140mpteq2dva 5253 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))))
142 ioosscn 13440 . . . . . . . . . . . . . 14 ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ)
144 fourierdlem78.fcn . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ))
145 ioosscn 13440 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ℂ
146145a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
147143, 144, 146, 127, 137fourierdlem23 45751 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
148141, 147eqeltrd 2826 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
149 0red 11267 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
15014ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
1518adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
152 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝐴)
15327adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
154149, 150, 151, 152, 153lelttrd 11422 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 < 𝑠)
155154iftrued 4541 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
156155negeqd 11504 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑌)
157156mpteq2dva 5253 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌))
15851renegcld 11691 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑌 ∈ ℝ)
159158recnd 11292 . . . . . . . . . . . . . . 15 (𝜑 → -𝑌 ∈ ℂ)
160 ssid 4002 . . . . . . . . . . . . . . . 16 ℂ ⊆ ℂ
161160a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ⊆ ℂ)
162146, 159, 161constcncfg 45493 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ))
163162adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ))
164157, 163eqeltrd 2826 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
165 simpl 481 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝜑)
16614rexrd 11314 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
167166ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 ∈ ℝ*)
16823ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ*)
169 0red 11267 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ ℝ)
170 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → ¬ 0 ≤ 𝐴)
17114adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 ∈ ℝ)
172 0red 11267 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 0 ∈ ℝ)
173171, 172ltnled 11411 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝐴 < 0 ↔ ¬ 0 ≤ 𝐴))
174170, 173mpbird 256 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 < 0)
175174adantr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 < 0)
176 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → ¬ 𝐵 ≤ 0)
177 0red 11267 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 ∈ ℝ)
17822adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ)
179177, 178ltnled 11411 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0))
180176, 179mpbird 256 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵)
181180adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵)
182167, 168, 169, 175, 181eliood 45116 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ (𝐴(,)𝐵))
18359ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → ¬ 0 ∈ (𝐴(,)𝐵))
184182, 183condan 816 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐵 ≤ 0)
1858adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
186 0red 11267 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
18722ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
18832adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
189 simplr 767 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ 0)
190185, 187, 186, 188, 189ltletrd 11424 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 0)
191185, 186, 190ltnsymd 11413 . . . . . . . . . . . . . . . . 17 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 0 < 𝑠)
192191iffalsed 4544 . . . . . . . . . . . . . . . 16 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
193192negeqd 11504 . . . . . . . . . . . . . . 15 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑊)
194193mpteq2dva 5253 . . . . . . . . . . . . . 14 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊))
19552recnd 11292 . . . . . . . . . . . . . . . . 17 (𝜑𝑊 ∈ ℂ)
196195negcld 11608 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑊 ∈ ℂ)
197146, 196, 161constcncfg 45493 . . . . . . . . . . . . . . 15 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ))
198197adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ))
199194, 198eqeltrd 2826 . . . . . . . . . . . . 13 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
200165, 184, 199syl2anc 582 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
201164, 200pm2.61dan 811 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
202148, 201addcncf 25463 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
203119, 202eqeltrd 2826 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
204 eqid 2726 . . . . . . . . . 10 (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) = (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠))
205 1cnd 11259 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
206204cdivcncf 24932 . . . . . . . . . . 11 (1 ∈ ℂ → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ))
207205, 206syl 17 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ))
208 velsn 4649 . . . . . . . . . . . . . 14 (𝑠 ∈ {0} ↔ 𝑠 = 0)
20961, 208sylnibr 328 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 ∈ {0})
210111, 209eldifd 3958 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖ {0}))
211210ralrimiva 3136 . . . . . . . . . . 11 (𝜑 → ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖ {0}))
212 dfss3 3968 . . . . . . . . . . 11 ((𝐴(,)𝐵) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖ {0}))
213211, 212sylibr 233 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ (ℂ ∖ {0}))
2149, 62rereccld 12092 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℝ)
215214recnd 11292 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℂ)
216204, 207, 213, 161, 215cncfmptssg 45492 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
217203, 216mulcncf 25465 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
218114, 217eqeltrd 2826 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
21961iffalsed 4544 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
22074recnd 11292 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
221111, 220, 81divrecd 12044 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))
22286, 219, 2213eqtrd 2770 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))
223222mpteq2dva 5253 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))))
224219, 221eqtr2d 2767 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
225224mpteq2dva 5253 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
226 eqid 2726 . . . . . . . . . 10 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
227 cncfss 24910 . . . . . . . . . . . 12 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ))
228106, 160, 227mp2an 690 . . . . . . . . . . 11 ((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ)
229226fourierdlem62 45789 . . . . . . . . . . . 12 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ)
230229a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ))
231228, 230sselid 3977 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℂ))
23283recnd 11292 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
233226, 231, 41, 161, 232cncfmptssg 45492 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
234225, 233eqeltrd 2826 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
235223, 234eqeltrd 2826 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
236218, 235mulcncf 25465 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻𝑠) · (𝐾𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
237108, 236eqeltrd 2826 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
238101mpteq2dva 5253 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))))
239 sincn 26474 . . . . . . . 8 sin ∈ (ℂ–cn→ℂ)
240239a1i 11 . . . . . . 7 (𝜑 → sin ∈ (ℂ–cn→ℂ))
241 halfre 12478 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
242241a1i 11 . . . . . . . . . . 11 (𝜑 → (1 / 2) ∈ ℝ)
24393, 242readdcld 11293 . . . . . . . . . 10 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
244243recnd 11292 . . . . . . . . 9 (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
245146, 244, 161constcncfg 45493 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
246146, 161idcncfg 45494 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) ∈ ((𝐴(,)𝐵)–cn→ℂ))
247245, 246mulcncf 25465 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
248240, 247cncfmpt1f 24925 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
249238, 248eqeltrd 2826 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
250237, 249mulcncf 25465 . . . 4 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
251 cncfcdm 24909 . . . 4 ((ℝ ⊆ ℂ ∧ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ))
252107, 250, 251syl2anc 582 . . 3 (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ))
253105, 252mpbird 256 . 2 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ))
25443, 253eqeltrd 2826 1 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  wne 2930  wral 3051  cdif 3944  wss 3947  ifcif 4533  {csn 4633   class class class wbr 5153  cmpt 5236  cres 5684  wf 6550  cfv 6554  (class class class)co 7424  cc 11156  cr 11157  0cc0 11158  1c1 11159   + caddc 11161   · cmul 11163  *cxr 11297   < clt 11298  cle 11299  cmin 11494  -cneg 11495   / cdiv 11921  2c2 12319  (,)cioo 13378  [,]cicc 13381  sincsin 16065  πcpi 16068  cnccncf 24887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236  ax-addf 11237
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-tp 4638  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-supp 8175  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-er 8734  df-map 8857  df-pm 8858  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9406  df-fi 9454  df-sup 9485  df-inf 9486  df-oi 9553  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12611  df-dec 12730  df-uz 12875  df-q 12985  df-rp 13029  df-xneg 13146  df-xadd 13147  df-xmul 13148  df-ioo 13382  df-ioc 13383  df-ico 13384  df-icc 13385  df-fz 13539  df-fzo 13682  df-fl 13812  df-mod 13890  df-seq 14022  df-exp 14082  df-fac 14291  df-bc 14320  df-hash 14348  df-shft 15072  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-limsup 15473  df-clim 15490  df-rlim 15491  df-sum 15691  df-ef 16069  df-sin 16071  df-cos 16072  df-pi 16074  df-struct 17149  df-sets 17166  df-slot 17184  df-ndx 17196  df-base 17214  df-ress 17243  df-plusg 17279  df-mulr 17280  df-starv 17281  df-sca 17282  df-vsca 17283  df-ip 17284  df-tset 17285  df-ple 17286  df-ds 17288  df-unif 17289  df-hom 17290  df-cco 17291  df-rest 17437  df-topn 17438  df-0g 17456  df-gsum 17457  df-topgen 17458  df-pt 17459  df-prds 17462  df-xrs 17517  df-qtop 17522  df-imas 17523  df-xps 17525  df-mre 17599  df-mrc 17600  df-acs 17602  df-mgm 18633  df-sgrp 18712  df-mnd 18728  df-submnd 18774  df-mulg 19062  df-cntz 19311  df-cmn 19780  df-psmet 21335  df-xmet 21336  df-met 21337  df-bl 21338  df-mopn 21339  df-fbas 21340  df-fg 21341  df-cnfld 21344  df-top 22887  df-topon 22904  df-topsp 22926  df-bases 22940  df-cld 23014  df-ntr 23015  df-cls 23016  df-nei 23093  df-lp 23131  df-perf 23132  df-cn 23222  df-cnp 23223  df-t1 23309  df-haus 23310  df-cmp 23382  df-tx 23557  df-hmeo 23750  df-fil 23841  df-fm 23933  df-flim 23934  df-flf 23935  df-xms 24317  df-ms 24318  df-tms 24319  df-cncf 24889  df-limc 25886  df-dv 25887
This theorem is referenced by:  fourierdlem88  45815
  Copyright terms: Public domain W3C validator