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 46140
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 5999 . . 3 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))) ↾ (𝐴(,)𝐵)))
4 pire 26515 . . . . . . . . 9 π ∈ ℝ
54renegcli 11568 . . . . . . . 8 -π ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ∈ ℝ)
74a1i 11 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → π ∈ ℝ)
8 elioore 13414 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
98adantl 481 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
105a1i 11 . . . . . . . . . . . 12 (𝜑 → -π ∈ ℝ)
114a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℝ)
1210, 11iccssred 13471 . . . . . . . . . . 11 (𝜑 → (-π[,]π) ⊆ ℝ)
13 fourierdlem78.a . . . . . . . . . . 11 (𝜑𝐴 ∈ (-π[,]π))
1412, 13sseldd 3996 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
1514adantr 480 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
165, 4elicc2i 13450 . . . . . . . . . . . 12 (𝐴 ∈ (-π[,]π) ↔ (𝐴 ∈ ℝ ∧ -π ≤ 𝐴𝐴 ≤ π))
1716simp2bi 1145 . . . . . . . . . . 11 (𝐴 ∈ (-π[,]π) → -π ≤ 𝐴)
1813, 17syl 17 . . . . . . . . . 10 (𝜑 → -π ≤ 𝐴)
1918adantr 480 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝐴)
2015rexrd 11309 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ*)
21 fourierdlem78.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (-π[,]π))
2212, 21sseldd 3996 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2322rexrd 11309 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ*)
2423adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ*)
25 simpr 484 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
26 ioogtlb 45448 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
2720, 24, 25, 26syl3anc 1370 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
286, 15, 9, 19, 27lelttrd 11417 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π < 𝑠)
296, 9, 28ltled 11407 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝑠)
3022adantr 480 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
31 iooltub 45463 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
3220, 24, 25, 31syl3anc 1370 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
335, 4elicc2i 13450 . . . . . . . . . . . 12 (𝐵 ∈ (-π[,]π) ↔ (𝐵 ∈ ℝ ∧ -π ≤ 𝐵𝐵 ≤ π))
3433simp3bi 1146 . . . . . . . . . . 11 (𝐵 ∈ (-π[,]π) → 𝐵 ≤ π)
3521, 34syl 17 . . . . . . . . . 10 (𝜑𝐵 ≤ π)
3635adantr 480 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ π)
379, 30, 7, 32, 36ltletrd 11419 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < π)
389, 7, 37ltled 11407 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≤ π)
396, 7, 9, 29, 38eliccd 45457 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π))
4039ex 412 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ (-π[,]π)))
4140ssrdv 4001 . . . 4 (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
4241resmptd 6060 . . 3 (𝜑 → ((𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))))
433, 42eqtrd 2775 . 2 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))))
44 0red 11262 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
45 fourierdlem78.f . . . . . . . . . . . . . . 15 (𝜑𝐹:ℝ⟶ℝ)
4645adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
47 fourierdlem78.x . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ)
4847adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
4948, 9readdcld 11288 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
5046, 49ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
51 fourierdlem78.y . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ)
52 fourierdlem78.w . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ ℝ)
5351, 52ifcld 4577 . . . . . . . . . . . . . 14 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5453adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5550, 54resubcld 11689 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ)
56 eleq1 2827 . . . . . . . . . . . . . . . 16 (𝑠 = 0 → (𝑠 ∈ (𝐴(,)𝐵) ↔ 0 ∈ (𝐴(,)𝐵)))
5756biimpac 478 . . . . . . . . . . . . . . 15 ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
5857adantll 714 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
59 fourierdlem78.nxelab . . . . . . . . . . . . . . 15 (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
6059ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵))
6158, 60pm2.65da 817 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0)
6261neqned 2945 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)
6355, 9, 62redivcld 12093 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℝ)
6444, 63ifcld 4577 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ)
65 fourierdlem78.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6665fvmpt2 7027 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6739, 64, 66syl2anc 584 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6867, 64eqeltrd 2839 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) ∈ ℝ)
69 1red 11260 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ)
70 2re 12338 . . . . . . . . . . . . . 14 2 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
729rehalfcld 12511 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ)
7372resincld 16176 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ)
7471, 73remulcld 11289 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
7571recnd 11287 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
7673recnd 11287 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
77 2ne0 12368 . . . . . . . . . . . . . 14 2 ≠ 0
7877a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
79 fourierdlem44 46107 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
8039, 62, 79syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
8175, 76, 78, 80mulne0d 11913 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
829, 74, 81redivcld 12093 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
8369, 82ifcld 4577 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ)
84 fourierdlem78.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8584fvmpt2 7027 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8639, 83, 85syl2anc 584 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8786, 83eqeltrd 2839 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) ∈ ℝ)
8868, 87remulcld 11289 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ)
89 fourierdlem78.u . . . . . . . 8 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
9089fvmpt2 7027 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
9139, 88, 90syl2anc 584 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
9291, 88eqeltrd 2839 . . . . 5 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑈𝑠) ∈ ℝ)
93 fourierdlem78.n . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
9493adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑁 ∈ ℝ)
9571, 78rereccld 12092 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈ ℝ)
9694, 95readdcld 11288 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℝ)
9796, 9remulcld 11289 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑠) ∈ ℝ)
9897resincld 16176 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ)
99 fourierdlem78.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))
10099fvmpt2 7027 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ) → (𝑆𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠)))
10139, 98, 100syl2anc 584 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑆𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠)))
102101, 98eqeltrd 2839 . . . . 5 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑆𝑠) ∈ ℝ)
10392, 102remulcld 11289 . . . 4 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ)
104 eqid 2735 . . . 4 (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠)))
105103, 104fmptd 7134 . . 3 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ)
106 ax-resscn 11210 . . . . 5 ℝ ⊆ ℂ
107106a1i 11 . . . 4 (𝜑 → ℝ ⊆ ℂ)
10891mpteq2dva 5248 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻𝑠) · (𝐾𝑠))))
10961iffalsed 4542 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
11055recnd 11287 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
1119recnd 11287 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ)
112110, 111, 62divrecd 12044 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))
11367, 109, 1123eqtrd 2779 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))
114113mpteq2dva 5248 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))))
11550recnd 11287 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
11654recnd 11287 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
117115, 116negsubd 11624 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
118117eqcomd 2741 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)))
119118mpteq2dva 5248 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))))
12014, 47readdcld 11288 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + 𝑋) ∈ ℝ)
121120rexrd 11309 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 + 𝑋) ∈ ℝ*)
122121adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) ∈ ℝ*)
12322, 47readdcld 11288 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵 + 𝑋) ∈ ℝ)
124123rexrd 11309 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + 𝑋) ∈ ℝ*)
125124adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐵 + 𝑋) ∈ ℝ*)
12614recnd 11287 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℂ)
12747recnd 11287 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℂ)
128126, 127addcomd 11461 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + 𝑋) = (𝑋 + 𝐴))
129128adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) = (𝑋 + 𝐴))
13015, 9, 48, 27ltadd2dd 11418 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
131129, 130eqbrtrd 5170 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) < (𝑋 + 𝑠))
1329, 30, 48, 32ltadd2dd 11418 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
13322recnd 11287 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℂ)
134127, 133addcomd 11461 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 + 𝐵) = (𝐵 + 𝑋))
135134adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) = (𝐵 + 𝑋))
136132, 135breqtrd 5174 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝐵 + 𝑋))
137122, 125, 49, 131, 136eliood 45451 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))
138 fvres 6926 . . . . . . . . . . . . . . 15 ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
139137, 138syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
140139eqcomd 2741 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)))
141140mpteq2dva 5248 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))))
142 ioosscn 13446 . . . . . . . . . . . . . 14 ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ)
144 fourierdlem78.fcn . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ))
145 ioosscn 13446 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ℂ
146145a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
147143, 144, 146, 127, 137fourierdlem23 46086 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
148141, 147eqeltrd 2839 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
149 0red 11262 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
15014ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
1518adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
152 simplr 769 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝐴)
15327adantlr 715 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
154149, 150, 151, 152, 153lelttrd 11417 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 < 𝑠)
155154iftrued 4539 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
156155negeqd 11500 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑌)
157156mpteq2dva 5248 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌))
15851renegcld 11688 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑌 ∈ ℝ)
159158recnd 11287 . . . . . . . . . . . . . . 15 (𝜑 → -𝑌 ∈ ℂ)
160 ssid 4018 . . . . . . . . . . . . . . . 16 ℂ ⊆ ℂ
161160a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ⊆ ℂ)
162146, 159, 161constcncfg 45828 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ))
163162adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ))
164157, 163eqeltrd 2839 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
165 simpl 482 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝜑)
16614rexrd 11309 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
167166ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 ∈ ℝ*)
16823ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ*)
169 0red 11262 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ ℝ)
170 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → ¬ 0 ≤ 𝐴)
17114adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 ∈ ℝ)
172 0red 11262 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 0 ∈ ℝ)
173171, 172ltnled 11406 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝐴 < 0 ↔ ¬ 0 ≤ 𝐴))
174170, 173mpbird 257 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 < 0)
175174adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 < 0)
176 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → ¬ 𝐵 ≤ 0)
177 0red 11262 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 ∈ ℝ)
17822adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ)
179177, 178ltnled 11406 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0))
180176, 179mpbird 257 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵)
181180adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵)
182167, 168, 169, 175, 181eliood 45451 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ (𝐴(,)𝐵))
18359ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → ¬ 0 ∈ (𝐴(,)𝐵))
184182, 183condan 818 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐵 ≤ 0)
1858adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
186 0red 11262 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
18722ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
18832adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
189 simplr 769 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ 0)
190185, 187, 186, 188, 189ltletrd 11419 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 0)
191185, 186, 190ltnsymd 11408 . . . . . . . . . . . . . . . . 17 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 0 < 𝑠)
192191iffalsed 4542 . . . . . . . . . . . . . . . 16 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
193192negeqd 11500 . . . . . . . . . . . . . . 15 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑊)
194193mpteq2dva 5248 . . . . . . . . . . . . . 14 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊))
19552recnd 11287 . . . . . . . . . . . . . . . . 17 (𝜑𝑊 ∈ ℂ)
196195negcld 11605 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑊 ∈ ℂ)
197146, 196, 161constcncfg 45828 . . . . . . . . . . . . . . 15 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ))
198197adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ))
199194, 198eqeltrd 2839 . . . . . . . . . . . . 13 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
200165, 184, 199syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
201164, 200pm2.61dan 813 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
202148, 201addcncf 25492 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
203119, 202eqeltrd 2839 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
204 eqid 2735 . . . . . . . . . 10 (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) = (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠))
205 1cnd 11254 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
206204cdivcncf 24961 . . . . . . . . . . 11 (1 ∈ ℂ → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ))
207205, 206syl 17 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ))
208 velsn 4647 . . . . . . . . . . . . . 14 (𝑠 ∈ {0} ↔ 𝑠 = 0)
20961, 208sylnibr 329 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 ∈ {0})
210111, 209eldifd 3974 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖ {0}))
211210ralrimiva 3144 . . . . . . . . . . 11 (𝜑 → ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖ {0}))
212 dfss3 3984 . . . . . . . . . . 11 ((𝐴(,)𝐵) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖ {0}))
213211, 212sylibr 234 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ (ℂ ∖ {0}))
2149, 62rereccld 12092 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℝ)
215214recnd 11287 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℂ)
216204, 207, 213, 161, 215cncfmptssg 45827 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
217203, 216mulcncf 25494 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
218114, 217eqeltrd 2839 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
21961iffalsed 4542 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
22074recnd 11287 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
221111, 220, 81divrecd 12044 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))
22286, 219, 2213eqtrd 2779 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))
223222mpteq2dva 5248 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))))
224219, 221eqtr2d 2776 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
225224mpteq2dva 5248 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
226 eqid 2735 . . . . . . . . . 10 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
227 cncfss 24939 . . . . . . . . . . . 12 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ))
228106, 160, 227mp2an 692 . . . . . . . . . . 11 ((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ)
229226fourierdlem62 46124 . . . . . . . . . . . 12 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ)
230229a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ))
231228, 230sselid 3993 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℂ))
23283recnd 11287 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
233226, 231, 41, 161, 232cncfmptssg 45827 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
234225, 233eqeltrd 2839 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
235223, 234eqeltrd 2839 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
236218, 235mulcncf 25494 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻𝑠) · (𝐾𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
237108, 236eqeltrd 2839 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
238101mpteq2dva 5248 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))))
239 sincn 26503 . . . . . . . 8 sin ∈ (ℂ–cn→ℂ)
240239a1i 11 . . . . . . 7 (𝜑 → sin ∈ (ℂ–cn→ℂ))
241 halfre 12478 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
242241a1i 11 . . . . . . . . . . 11 (𝜑 → (1 / 2) ∈ ℝ)
24393, 242readdcld 11288 . . . . . . . . . 10 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
244243recnd 11287 . . . . . . . . 9 (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
245146, 244, 161constcncfg 45828 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
246146, 161idcncfg 45829 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) ∈ ((𝐴(,)𝐵)–cn→ℂ))
247245, 246mulcncf 25494 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
248240, 247cncfmpt1f 24954 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
249238, 248eqeltrd 2839 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
250237, 249mulcncf 25494 . . . 4 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
251 cncfcdm 24938 . . . 4 ((ℝ ⊆ ℂ ∧ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ))
252107, 250, 251syl2anc 584 . . 3 (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ))
253105, 252mpbird 257 . 2 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ))
25443, 253eqeltrd 2839 1 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wne 2938  wral 3059  cdif 3960  wss 3963  ifcif 4531  {csn 4631   class class class wbr 5148  cmpt 5231  cres 5691  wf 6559  cfv 6563  (class class class)co 7431  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158  *cxr 11292   < clt 11293  cle 11294  cmin 11490  -cneg 11491   / cdiv 11918  2c2 12319  (,)cioo 13384  [,]cicc 13387  sincsin 16096  πcpi 16099  cnccncf 24916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  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 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ioc 13389  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-fac 14310  df-bc 14339  df-hash 14367  df-shft 15103  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-limsup 15504  df-clim 15521  df-rlim 15522  df-sum 15720  df-ef 16100  df-sin 16102  df-cos 16103  df-pi 16105  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17469  df-topn 17470  df-0g 17488  df-gsum 17489  df-topgen 17490  df-pt 17491  df-prds 17494  df-xrs 17549  df-qtop 17554  df-imas 17555  df-xps 17557  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-mulg 19099  df-cntz 19348  df-cmn 19815  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-fbas 21379  df-fg 21380  df-cnfld 21383  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-cld 23043  df-ntr 23044  df-cls 23045  df-nei 23122  df-lp 23160  df-perf 23161  df-cn 23251  df-cnp 23252  df-t1 23338  df-haus 23339  df-cmp 23411  df-tx 23586  df-hmeo 23779  df-fil 23870  df-fm 23962  df-flim 23963  df-flf 23964  df-xms 24346  df-ms 24347  df-tms 24348  df-cncf 24918  df-limc 25916  df-dv 25917
This theorem is referenced by:  fourierdlem88  46150
  Copyright terms: Public domain W3C validator