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 39708
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 5355 . . 3 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))) ↾ (𝐴(,)𝐵)))
4 pire 24114 . . . . . . . . 9 π ∈ ℝ
54renegcli 10286 . . . . . . . 8 -π ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ∈ ℝ)
74a1i 11 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → π ∈ ℝ)
8 elioore 12147 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
98adantl 482 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
105a1i 11 . . . . . . . . . . . 12 (𝜑 → -π ∈ ℝ)
114a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℝ)
1210, 11iccssred 39138 . . . . . . . . . . 11 (𝜑 → (-π[,]π) ⊆ ℝ)
13 fourierdlem78.a . . . . . . . . . . 11 (𝜑𝐴 ∈ (-π[,]π))
1412, 13sseldd 3584 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
1514adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
165, 4elicc2i 12181 . . . . . . . . . . . 12 (𝐴 ∈ (-π[,]π) ↔ (𝐴 ∈ ℝ ∧ -π ≤ 𝐴𝐴 ≤ π))
1716simp2bi 1075 . . . . . . . . . . 11 (𝐴 ∈ (-π[,]π) → -π ≤ 𝐴)
1813, 17syl 17 . . . . . . . . . 10 (𝜑 → -π ≤ 𝐴)
1918adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝐴)
2015rexrd 10033 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ*)
21 fourierdlem78.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (-π[,]π))
2212, 21sseldd 3584 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2322rexrd 10033 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ*)
2423adantr 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ*)
25 simpr 477 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
26 ioogtlb 39128 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
2720, 24, 25, 26syl3anc 1323 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
286, 15, 9, 19, 27lelttrd 10139 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π < 𝑠)
296, 9, 28ltled 10129 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → -π ≤ 𝑠)
3022adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
31 iooltub 39146 . . . . . . . . . 10 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
3220, 24, 25, 31syl3anc 1323 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
335, 4elicc2i 12181 . . . . . . . . . . . 12 (𝐵 ∈ (-π[,]π) ↔ (𝐵 ∈ ℝ ∧ -π ≤ 𝐵𝐵 ≤ π))
3433simp3bi 1076 . . . . . . . . . . 11 (𝐵 ∈ (-π[,]π) → 𝐵 ≤ π)
3521, 34syl 17 . . . . . . . . . 10 (𝜑𝐵 ≤ π)
3635adantr 481 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ π)
379, 30, 7, 32, 36ltletrd 10141 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < π)
389, 7, 37ltled 10129 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≤ π)
396, 7, 9, 29, 38eliccd 39137 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π))
4039ex 450 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ (-π[,]π)))
4140ssrdv 3589 . . . 4 (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
4241resmptd 5411 . . 3 (𝜑 → ((𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))))
433, 42eqtrd 2655 . 2 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))))
44 0red 9985 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
45 fourierdlem78.f . . . . . . . . . . . . . . 15 (𝜑𝐹:ℝ⟶ℝ)
4645adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
47 fourierdlem78.x . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℝ)
4847adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
4948, 9readdcld 10013 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
5046, 49ffvelrnd 6316 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
51 fourierdlem78.y . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ)
52 fourierdlem78.w . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ ℝ)
5351, 52ifcld 4103 . . . . . . . . . . . . . 14 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5453adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5550, 54resubcld 10402 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ)
56 eleq1 2686 . . . . . . . . . . . . . . . 16 (𝑠 = 0 → (𝑠 ∈ (𝐴(,)𝐵) ↔ 0 ∈ (𝐴(,)𝐵)))
5756biimpac 503 . . . . . . . . . . . . . . 15 ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
5857adantll 749 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
59 fourierdlem78.nxelab . . . . . . . . . . . . . . 15 (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
6059ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵))
6158, 60pm2.65da 599 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0)
6261neqned 2797 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)
6355, 9, 62redivcld 10797 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℝ)
6444, 63ifcld 4103 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ)
65 fourierdlem78.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6665fvmpt2 6248 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6739, 64, 66syl2anc 692 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6867, 64eqeltrd 2698 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) ∈ ℝ)
69 1red 9999 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ)
70 2re 11034 . . . . . . . . . . . . . 14 2 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
729rehalfcld 11223 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ)
7372resincld 14798 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ)
7471, 73remulcld 10014 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
7571recnd 10012 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
7673recnd 10012 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
77 2ne0 11057 . . . . . . . . . . . . . 14 2 ≠ 0
7877a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
79 fourierdlem44 39675 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
8039, 62, 79syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
8175, 76, 78, 80mulne0d 10623 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
829, 74, 81redivcld 10797 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
8369, 82ifcld 4103 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ)
84 fourierdlem78.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8584fvmpt2 6248 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8639, 83, 85syl2anc 692 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8786, 83eqeltrd 2698 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) ∈ ℝ)
8868, 87remulcld 10014 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ)
89 fourierdlem78.u . . . . . . . 8 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
9089fvmpt2 6248 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
9139, 88, 90syl2anc 692 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
9291, 88eqeltrd 2698 . . . . 5 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑈𝑠) ∈ ℝ)
93 fourierdlem78.n . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
9493adantr 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑁 ∈ ℝ)
9571, 78rereccld 10796 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 2) ∈ ℝ)
9694, 95readdcld 10013 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑁 + (1 / 2)) ∈ ℝ)
9796, 9remulcld 10014 . . . . . . . 8 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝑁 + (1 / 2)) · 𝑠) ∈ ℝ)
9897resincld 14798 . . . . . . 7 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ)
99 fourierdlem78.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))
10099fvmpt2 6248 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ (sin‘((𝑁 + (1 / 2)) · 𝑠)) ∈ ℝ) → (𝑆𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠)))
10139, 98, 100syl2anc 692 . . . . . 6 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑆𝑠) = (sin‘((𝑁 + (1 / 2)) · 𝑠)))
102101, 98eqeltrd 2698 . . . . 5 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑆𝑠) ∈ ℝ)
10392, 102remulcld 10014 . . . 4 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ)
104 eqid 2621 . . . 4 (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠)))
105103, 104fmptd 6340 . . 3 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ)
106 ax-resscn 9937 . . . . 5 ℝ ⊆ ℂ
107106a1i 11 . . . 4 (𝜑 → ℝ ⊆ ℂ)
10891mpteq2dva 4704 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻𝑠) · (𝐾𝑠))))
10961iffalsed 4069 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
11055recnd 10012 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
1119recnd 10012 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ)
112110, 111, 62divrecd 10748 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))
11367, 109, 1123eqtrd 2659 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠)))
114113mpteq2dva 4704 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))))
11550recnd 10012 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
11654recnd 10012 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
117115, 116negsubd 10342 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
118117eqcomd 2627 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊)))
119118mpteq2dva 4704 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))))
12014, 47readdcld 10013 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + 𝑋) ∈ ℝ)
121120rexrd 10033 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 + 𝑋) ∈ ℝ*)
122121adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) ∈ ℝ*)
12322, 47readdcld 10013 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵 + 𝑋) ∈ ℝ)
124123rexrd 10033 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + 𝑋) ∈ ℝ*)
125124adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐵 + 𝑋) ∈ ℝ*)
12614recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℂ)
12747recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℂ)
128126, 127addcomd 10182 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + 𝑋) = (𝑋 + 𝐴))
129128adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) = (𝑋 + 𝐴))
13015, 9, 48, 27ltadd2dd 10140 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
131129, 130eqbrtrd 4635 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐴 + 𝑋) < (𝑋 + 𝑠))
1329, 30, 48, 32ltadd2dd 10140 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
13322recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℂ)
134127, 133addcomd 10182 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 + 𝐵) = (𝐵 + 𝑋))
135134adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) = (𝐵 + 𝑋))
136132, 135breqtrd 4639 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝐵 + 𝑋))
137122, 125, 49, 131, 136eliood 39131 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))
138 fvres 6164 . . . . . . . . . . . . . . 15 ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
139137, 138syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
140139eqcomd 2627 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠)))
141140mpteq2dva 4704 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))))
142 ioosscn 39127 . . . . . . . . . . . . . 14 ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)) ⊆ ℂ)
144 fourierdlem78.fcn . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ))
145 ioosscn 39127 . . . . . . . . . . . . . 14 (𝐴(,)𝐵) ⊆ ℂ
146145a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
147143, 144, 146, 127, 137fourierdlem23 39654 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋)))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
148141, 147eqeltrd 2698 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
149 0red 9985 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
15014ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
1518adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
152 simplr 791 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝐴)
15327adantlr 750 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
154149, 150, 151, 152, 153lelttrd 10139 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 < 𝑠)
155154iftrued 4066 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
156155negeqd 10219 . . . . . . . . . . . . . 14 (((𝜑 ∧ 0 ≤ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑌)
157156mpteq2dva 4704 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌))
15851renegcld 10401 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑌 ∈ ℝ)
159158recnd 10012 . . . . . . . . . . . . . . 15 (𝜑 → -𝑌 ∈ ℂ)
160 ssid 3603 . . . . . . . . . . . . . . . 16 ℂ ⊆ ℂ
161160a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ⊆ ℂ)
162146, 159, 161constcncfg 39387 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ))
163162adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑌) ∈ ((𝐴(,)𝐵)–cn→ℂ))
164157, 163eqeltrd 2698 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
165 simpl 473 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝜑)
16614rexrd 10033 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ*)
167166ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 ∈ ℝ*)
16823ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ*)
169 0red 9985 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ ℝ)
170 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → ¬ 0 ≤ 𝐴)
17114adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 ∈ ℝ)
172 0red 9985 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 0 ∈ ℝ)
173171, 172ltnled 10128 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝐴 < 0 ↔ ¬ 0 ≤ 𝐴))
174170, 173mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐴 < 0)
175174adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 𝐴 < 0)
176 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → ¬ 𝐵 ≤ 0)
177 0red 9985 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 ∈ ℝ)
17822adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 𝐵 ∈ ℝ)
179177, 178ltnled 10128 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0))
180176, 179mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵)
181180adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 < 𝐵)
182167, 168, 169, 175, 181eliood 39131 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → 0 ∈ (𝐴(,)𝐵))
18359ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 0 ≤ 𝐴) ∧ ¬ 𝐵 ≤ 0) → ¬ 0 ∈ (𝐴(,)𝐵))
184182, 183condan 834 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → 𝐵 ≤ 0)
1858adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
186 0red 9985 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
18722ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
18832adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
189 simplr 791 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ≤ 0)
190185, 187, 186, 188, 189ltletrd 10141 . . . . . . . . . . . . . . . . . 18 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 0)
191185, 186, 190ltnsymd 10130 . . . . . . . . . . . . . . . . 17 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 0 < 𝑠)
192191iffalsed 4069 . . . . . . . . . . . . . . . 16 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
193192negeqd 10219 . . . . . . . . . . . . . . 15 (((𝜑𝐵 ≤ 0) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → -if(0 < 𝑠, 𝑌, 𝑊) = -𝑊)
194193mpteq2dva 4704 . . . . . . . . . . . . . 14 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊))
19552recnd 10012 . . . . . . . . . . . . . . . . 17 (𝜑𝑊 ∈ ℂ)
196195negcld 10323 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑊 ∈ ℂ)
197146, 196, 161constcncfg 39387 . . . . . . . . . . . . . . 15 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ))
198197adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -𝑊) ∈ ((𝐴(,)𝐵)–cn→ℂ))
199194, 198eqeltrd 2698 . . . . . . . . . . . . 13 ((𝜑𝐵 ≤ 0) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
200165, 184, 199syl2anc 692 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 0 ≤ 𝐴) → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
201164, 200pm2.61dan 831 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ -if(0 < 𝑠, 𝑌, 𝑊)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
202148, 201addcncf 39389 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) + -if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
203119, 202eqeltrd 2698 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
204 eqid 2621 . . . . . . . . . 10 (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) = (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠))
205 1cnd 10000 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
206204cdivcncf 22628 . . . . . . . . . . 11 (1 ∈ ℂ → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ))
207205, 206syl 17 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑠)) ∈ ((ℂ ∖ {0})–cn→ℂ))
208 velsn 4164 . . . . . . . . . . . . . 14 (𝑠 ∈ {0} ↔ 𝑠 = 0)
20961, 208sylnibr 319 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 ∈ {0})
210111, 209eldifd 3566 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖ {0}))
211210ralrimiva 2960 . . . . . . . . . . 11 (𝜑 → ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖ {0}))
212 dfss3 3573 . . . . . . . . . . 11 ((𝐴(,)𝐵) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ (𝐴(,)𝐵)𝑠 ∈ (ℂ ∖ {0}))
213211, 212sylibr 224 . . . . . . . . . 10 (𝜑 → (𝐴(,)𝐵) ⊆ (ℂ ∖ {0}))
2149, 62rereccld 10796 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℝ)
215214recnd 10012 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (1 / 𝑠) ∈ ℂ)
216204, 207, 213, 161, 215cncfmptssg 39386 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
217203, 216mulcncf 23123 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (1 / 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
218114, 217eqeltrd 2698 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐻𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
21961iffalsed 4069 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
22074recnd 10012 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
221111, 220, 81divrecd 10748 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))
22286, 219, 2213eqtrd 2659 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝐾𝑠) = (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))))
223222mpteq2dva 4704 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))))
224219, 221eqtr2d 2656 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 · (1 / (2 · (sin‘(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
225224mpteq2dva 4704 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
226 eqid 2621 . . . . . . . . . 10 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
227 cncfss 22610 . . . . . . . . . . . 12 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ))
228106, 160, 227mp2an 707 . . . . . . . . . . 11 ((-π[,]π)–cn→ℝ) ⊆ ((-π[,]π)–cn→ℂ)
229226fourierdlem62 39692 . . . . . . . . . . . 12 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ)
230229a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℝ))
231228, 230sseldi 3581 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((-π[,]π)–cn→ℂ))
23283recnd 10012 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝐴(,)𝐵)) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
233226, 231, 41, 161, 232cncfmptssg 39386 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
234225, 233eqeltrd 2698 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 · (1 / (2 · (sin‘(𝑠 / 2)))))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
235223, 234eqeltrd 2698 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
236218, 235mulcncf 23123 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻𝑠) · (𝐾𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
237108, 236eqeltrd 2698 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑈𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
238101mpteq2dva 4704 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))))
239 sincn 24102 . . . . . . . 8 sin ∈ (ℂ–cn→ℂ)
240239a1i 11 . . . . . . 7 (𝜑 → sin ∈ (ℂ–cn→ℂ))
241 halfre 11190 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
242241a1i 11 . . . . . . . . . . 11 (𝜑 → (1 / 2) ∈ ℝ)
24393, 242readdcld 10013 . . . . . . . . . 10 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
244243recnd 10012 . . . . . . . . 9 (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
245146, 244, 161constcncfg 39387 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
246146, 161idcncfg 39388 . . . . . . . 8 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) ∈ ((𝐴(,)𝐵)–cn→ℂ))
247245, 246mulcncf 23123 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑁 + (1 / 2)) · 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
248240, 247cncfmpt1f 22624 . . . . . 6 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
249238, 248eqeltrd 2698 . . . . 5 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑆𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
250237, 249mulcncf 23123 . . . 4 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
251 cncffvrn 22609 . . . 4 ((ℝ ⊆ ℂ ∧ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ))
252107, 250, 251syl2anc 692 . . 3 (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))):(𝐴(,)𝐵)⟶ℝ))
253105, 252mpbird 247 . 2 (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝑈𝑠) · (𝑆𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℝ))
25443, 253eqeltrd 2698 1 (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  cdif 3552  wss 3555  ifcif 4058  {csn 4148   class class class wbr 4613  cmpt 4673  cres 5076  wf 5843  cfv 5847  (class class class)co 6604  cc 9878  cr 9879  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  *cxr 10017   < clt 10018  cle 10019  cmin 10210  -cneg 10211   / cdiv 10628  2c2 11014  (,)cioo 12117  [,]cicc 12120  sincsin 14719  πcpi 14722  cnccncf 22587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ioc 12122  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-fac 13001  df-bc 13030  df-hash 13058  df-shft 13741  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-limsup 14136  df-clim 14153  df-rlim 14154  df-sum 14351  df-ef 14723  df-sin 14725  df-cos 14726  df-pi 14728  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-fbas 19662  df-fg 19663  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-lp 20850  df-perf 20851  df-cn 20941  df-cnp 20942  df-t1 21028  df-haus 21029  df-cmp 21100  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-xms 22035  df-ms 22036  df-tms 22037  df-cncf 22589  df-limc 23536  df-dv 23537
This theorem is referenced by:  fourierdlem88  39718
  Copyright terms: Public domain W3C validator