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 44515
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 5940 . . 3 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ (𝐴(,)𝐡)))
4 pire 25838 . . . . . . . . 9 Ο€ ∈ ℝ
54renegcli 11470 . . . . . . . 8 -Ο€ ∈ ℝ
65a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ∈ ℝ)
74a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Ο€ ∈ ℝ)
8 elioore 13303 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ ℝ)
98adantl 483 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
105a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -Ο€ ∈ ℝ)
114a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ Ο€ ∈ ℝ)
1210, 11iccssred 13360 . . . . . . . . . . 11 (πœ‘ β†’ (-Ο€[,]Ο€) βŠ† ℝ)
13 fourierdlem78.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (-Ο€[,]Ο€))
1412, 13sseldd 3949 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ ℝ)
1514adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
165, 4elicc2i 13339 . . . . . . . . . . . 12 (𝐴 ∈ (-Ο€[,]Ο€) ↔ (𝐴 ∈ ℝ ∧ -Ο€ ≀ 𝐴 ∧ 𝐴 ≀ Ο€))
1716simp2bi 1147 . . . . . . . . . . 11 (𝐴 ∈ (-Ο€[,]Ο€) β†’ -Ο€ ≀ 𝐴)
1813, 17syl 17 . . . . . . . . . 10 (πœ‘ β†’ -Ο€ ≀ 𝐴)
1918adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ≀ 𝐴)
2015rexrd 11213 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ*)
21 fourierdlem78.b . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ (-Ο€[,]Ο€))
2212, 21sseldd 3949 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ℝ)
2322rexrd 11213 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ ℝ*)
2423adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ*)
25 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (𝐴(,)𝐡))
26 ioogtlb 43823 . . . . . . . . . 10 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
2720, 24, 25, 26syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
286, 15, 9, 19, 27lelttrd 11321 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ < 𝑠)
296, 9, 28ltled 11311 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ≀ 𝑠)
3022adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
31 iooltub 43838 . . . . . . . . . 10 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
3220, 24, 25, 31syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
335, 4elicc2i 13339 . . . . . . . . . . . 12 (𝐡 ∈ (-Ο€[,]Ο€) ↔ (𝐡 ∈ ℝ ∧ -Ο€ ≀ 𝐡 ∧ 𝐡 ≀ Ο€))
3433simp3bi 1148 . . . . . . . . . . 11 (𝐡 ∈ (-Ο€[,]Ο€) β†’ 𝐡 ≀ Ο€)
3521, 34syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ≀ Ο€)
3635adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ≀ Ο€)
379, 30, 7, 32, 36ltletrd 11323 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < Ο€)
389, 7, 37ltled 11311 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ≀ Ο€)
396, 7, 9, 29, 38eliccd 43832 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
4039ex 414 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ (-Ο€[,]Ο€)))
4140ssrdv 3954 . . . 4 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (-Ο€[,]Ο€))
4241resmptd 5998 . . 3 (πœ‘ β†’ ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ (𝐴(,)𝐡)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
433, 42eqtrd 2773 . 2 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
44 0red 11166 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
45 fourierdlem78.f . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
4645adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐹:β„βŸΆβ„)
47 fourierdlem78.x . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑋 ∈ ℝ)
4847adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑋 ∈ ℝ)
4948, 9readdcld 11192 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ℝ)
5046, 49ffvelcdmd 7040 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
51 fourierdlem78.y . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Œ ∈ ℝ)
52 fourierdlem78.w . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Š ∈ ℝ)
5351, 52ifcld 4536 . . . . . . . . . . . . . 14 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
5453adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
5550, 54resubcld 11591 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
56 eleq1 2822 . . . . . . . . . . . . . . . 16 (𝑠 = 0 β†’ (𝑠 ∈ (𝐴(,)𝐡) ↔ 0 ∈ (𝐴(,)𝐡)))
5756biimpac 480 . . . . . . . . . . . . . . 15 ((𝑠 ∈ (𝐴(,)𝐡) ∧ 𝑠 = 0) β†’ 0 ∈ (𝐴(,)𝐡))
5857adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) ∧ 𝑠 = 0) β†’ 0 ∈ (𝐴(,)𝐡))
59 fourierdlem78.nxelab . . . . . . . . . . . . . . 15 (πœ‘ β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
6059ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) ∧ 𝑠 = 0) β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
6158, 60pm2.65da 816 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 𝑠 = 0)
6261neqned 2947 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 β‰  0)
6355, 9, 62redivcld 11991 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) ∈ ℝ)
6444, 63ifcld 4536 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ ℝ)
65 fourierdlem78.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6665fvmpt2 6963 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ ℝ) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6739, 64, 66syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6867, 64eqeltrd 2834 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) ∈ ℝ)
69 1red 11164 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 1 ∈ ℝ)
70 2re 12235 . . . . . . . . . . . . . 14 2 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 ∈ ℝ)
729rehalfcld 12408 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / 2) ∈ ℝ)
7372resincld 16033 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) ∈ ℝ)
7471, 73remulcld 11193 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ ℝ)
7571recnd 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 ∈ β„‚)
7673recnd 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) ∈ β„‚)
77 2ne0 12265 . . . . . . . . . . . . . 14 2 β‰  0
7877a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 β‰  0)
79 fourierdlem44 44482 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ 𝑠 β‰  0) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
8039, 62, 79syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
8175, 76, 78, 80mulne0d 11815 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) β‰  0)
829, 74, 81redivcld 11991 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ ℝ)
8369, 82ifcld 4536 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ ℝ)
84 fourierdlem78.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8584fvmpt2 6963 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ ℝ) β†’ (πΎβ€˜π‘ ) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8639, 83, 85syl2anc 585 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8786, 83eqeltrd 2834 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) ∈ ℝ)
8868, 87remulcld 11193 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ)
89 fourierdlem78.u . . . . . . . 8 π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9089fvmpt2 6963 . . . . . . 7 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9139, 88, 90syl2anc 585 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9291, 88eqeltrd 2834 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘ˆβ€˜π‘ ) ∈ ℝ)
93 fourierdlem78.n . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ ℝ)
9493adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑁 ∈ ℝ)
9571, 78rereccld 11990 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 2) ∈ ℝ)
9694, 95readdcld 11192 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑁 + (1 / 2)) ∈ ℝ)
9796, 9remulcld 11193 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((𝑁 + (1 / 2)) Β· 𝑠) ∈ ℝ)
9897resincld 16033 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ℝ)
99 fourierdlem78.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
10099fvmpt2 6963 . . . . . . 7 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ℝ) β†’ (π‘†β€˜π‘ ) = (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
10139, 98, 100syl2anc 585 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘†β€˜π‘ ) = (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
102101, 98eqeltrd 2834 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘†β€˜π‘ ) ∈ ℝ)
10392, 102remulcld 11193 . . . 4 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )) ∈ ℝ)
104 eqid 2733 . . . 4 (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
105103, 104fmptd 7066 . . 3 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„)
106 ax-resscn 11116 . . . . 5 ℝ βŠ† β„‚
107106a1i 11 . . . 4 (πœ‘ β†’ ℝ βŠ† β„‚)
10891mpteq2dva 5209 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘ˆβ€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))))
10961iffalsed 4501 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
11055recnd 11191 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ β„‚)
1119recnd 11191 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ β„‚)
112110, 111, 62divrecd 11942 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠)))
11367, 109, 1123eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠)))
114113mpteq2dva 5209 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π»β€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠))))
11550recnd 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
11654recnd 11191 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
117115, 116negsubd 11526 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)))
118117eqcomd 2739 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š)))
119118mpteq2dva 5209 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š))))
12014, 47readdcld 11192 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 + 𝑋) ∈ ℝ)
121120rexrd 11213 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 + 𝑋) ∈ ℝ*)
122121adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) ∈ ℝ*)
12322, 47readdcld 11192 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 + 𝑋) ∈ ℝ)
124123rexrd 11213 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 + 𝑋) ∈ ℝ*)
125124adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐡 + 𝑋) ∈ ℝ*)
12614recnd 11191 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 ∈ β„‚)
12747recnd 11191 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 ∈ β„‚)
128126, 127addcomd 11365 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 + 𝑋) = (𝑋 + 𝐴))
129128adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) = (𝑋 + 𝐴))
13015, 9, 48, 27ltadd2dd 11322 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐴) < (𝑋 + 𝑠))
131129, 130eqbrtrd 5131 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) < (𝑋 + 𝑠))
1329, 30, 48, 32ltadd2dd 11322 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝑋 + 𝐡))
13322recnd 11191 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ β„‚)
134127, 133addcomd 11365 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑋 + 𝐡) = (𝐡 + 𝑋))
135134adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐡) = (𝐡 + 𝑋))
136132, 135breqtrd 5135 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝐡 + 𝑋))
137122, 125, 49, 131, 136eliood 43826 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))
138 fvres 6865 . . . . . . . . . . . . . . 15 ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) β†’ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
139137, 138syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
140139eqcomd 2739 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)))
141140mpteq2dva 5209 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠))))
142 ioosscn 13335 . . . . . . . . . . . . . 14 ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) βŠ† β„‚
143142a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) βŠ† β„‚)
144 fourierdlem78.fcn . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐡 + 𝑋))–cnβ†’β„‚))
145 ioosscn 13335 . . . . . . . . . . . . . 14 (𝐴(,)𝐡) βŠ† β„‚
146145a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
147143, 144, 146, 127, 137fourierdlem23 44461 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
148141, 147eqeltrd 2834 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
149 0red 11166 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
15014ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
1518adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
152 simplr 768 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ≀ 𝐴)
15327adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
154149, 150, 151, 152, 153lelttrd 11321 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 < 𝑠)
155154iftrued 4498 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Œ)
156155negeqd 11403 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -if(0 < 𝑠, π‘Œ, π‘Š) = -π‘Œ)
157156mpteq2dva 5209 . . . . . . . . . . . . 13 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ))
15851renegcld 11590 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -π‘Œ ∈ ℝ)
159158recnd 11191 . . . . . . . . . . . . . . 15 (πœ‘ β†’ -π‘Œ ∈ β„‚)
160 ssid 3970 . . . . . . . . . . . . . . . 16 β„‚ βŠ† β„‚
161160a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ β„‚ βŠ† β„‚)
162146, 159, 161constcncfg 44203 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
163162adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
164157, 163eqeltrd 2834 . . . . . . . . . . . 12 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
165 simpl 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ πœ‘)
16614rexrd 11213 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ ℝ*)
167166ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐴 ∈ ℝ*)
16823ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐡 ∈ ℝ*)
169 0red 11166 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ ℝ)
170 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ Β¬ 0 ≀ 𝐴)
17114adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐴 ∈ ℝ)
172 0red 11166 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 0 ∈ ℝ)
173171, 172ltnled 11310 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ (𝐴 < 0 ↔ Β¬ 0 ≀ 𝐴))
174170, 173mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐴 < 0)
175174adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐴 < 0)
176 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ Β¬ 𝐡 ≀ 0)
177 0red 11166 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ ℝ)
17822adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐡 ∈ ℝ)
179177, 178ltnled 11310 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ (0 < 𝐡 ↔ Β¬ 𝐡 ≀ 0))
180176, 179mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 0 < 𝐡)
181180adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 < 𝐡)
182167, 168, 169, 175, 181eliood 43826 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ (𝐴(,)𝐡))
18359ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
184182, 183condan 817 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐡 ≀ 0)
1858adantl 483 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
186 0red 11166 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
18722ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
18832adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
189 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ≀ 0)
190185, 187, 186, 188, 189ltletrd 11323 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 0)
191185, 186, 190ltnsymd 11312 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 0 < 𝑠)
192191iffalsed 4501 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Š)
193192negeqd 11403 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -if(0 < 𝑠, π‘Œ, π‘Š) = -π‘Š)
194193mpteq2dva 5209 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š))
19552recnd 11191 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Š ∈ β„‚)
196195negcld 11507 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -π‘Š ∈ β„‚)
197146, 196, 161constcncfg 44203 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
198197adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
199194, 198eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
200165, 184, 199syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
201164, 200pm2.61dan 812 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
202148, 201addcncf 24831 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
203119, 202eqeltrd 2834 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
204 eqid 2733 . . . . . . . . . 10 (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) = (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠))
205 1cnd 11158 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ β„‚)
206204cdivcncf 24307 . . . . . . . . . . 11 (1 ∈ β„‚ β†’ (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) ∈ ((β„‚ βˆ– {0})–cnβ†’β„‚))
207205, 206syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) ∈ ((β„‚ βˆ– {0})–cnβ†’β„‚))
208 velsn 4606 . . . . . . . . . . . . . 14 (𝑠 ∈ {0} ↔ 𝑠 = 0)
20961, 208sylnibr 329 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 𝑠 ∈ {0})
210111, 209eldifd 3925 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (β„‚ βˆ– {0}))
211210ralrimiva 3140 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘  ∈ (𝐴(,)𝐡)𝑠 ∈ (β„‚ βˆ– {0}))
212 dfss3 3936 . . . . . . . . . . 11 ((𝐴(,)𝐡) βŠ† (β„‚ βˆ– {0}) ↔ βˆ€π‘  ∈ (𝐴(,)𝐡)𝑠 ∈ (β„‚ βˆ– {0}))
213211, 212sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (β„‚ βˆ– {0}))
2149, 62rereccld 11990 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 𝑠) ∈ ℝ)
215214recnd 11191 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 𝑠) ∈ β„‚)
216204, 207, 213, 161, 215cncfmptssg 44202 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
217203, 216mulcncf 24833 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
218114, 217eqeltrd 2834 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π»β€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
21961iffalsed 4501 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) = (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))
22074recnd 11191 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ β„‚)
221111, 220, 81divrecd 11942 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) = (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))))
22286, 219, 2213eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) = (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))))
223222mpteq2dva 5209 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΎβ€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
224219, 221eqtr2d 2774 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
225224mpteq2dva 5209 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
226 eqid 2733 . . . . . . . . . 10 (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
227 cncfss 24285 . . . . . . . . . . . 12 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
228106, 160, 227mp2an 691 . . . . . . . . . . 11 ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚)
229226fourierdlem62 44499 . . . . . . . . . . . 12 (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cn→ℝ)
230229a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
231228, 230sselid 3946 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
23283recnd 11191 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ β„‚)
233226, 231, 41, 161, 232cncfmptssg 44202 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
234225, 233eqeltrd 2834 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
235223, 234eqeltrd 2834 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΎβ€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
236218, 235mulcncf 24833 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
237108, 236eqeltrd 2834 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘ˆβ€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
238101mpteq2dva 5209 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘†β€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠))))
239 sincn 25826 . . . . . . . 8 sin ∈ (ℂ–cnβ†’β„‚)
240239a1i 11 . . . . . . 7 (πœ‘ β†’ sin ∈ (ℂ–cnβ†’β„‚))
241 halfre 12375 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
242241a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (1 / 2) ∈ ℝ)
24393, 242readdcld 11192 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 + (1 / 2)) ∈ ℝ)
244243recnd 11191 . . . . . . . . 9 (πœ‘ β†’ (𝑁 + (1 / 2)) ∈ β„‚)
245146, 244, 161constcncfg 44203 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
246146, 161idcncfg 44204 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
247245, 246mulcncf 24833 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
248240, 247cncfmpt1f 24300 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
249238, 248eqeltrd 2834 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘†β€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
250237, 249mulcncf 24833 . . . 4 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
251 cncfcdm 24284 . . . 4 ((ℝ βŠ† β„‚ ∧ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚)) β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„))
252107, 250, 251syl2anc 585 . . 3 (πœ‘ β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„))
253105, 252mpbird 257 . 2 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ))
25443, 253eqeltrd 2834 1 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ ((𝐴(,)𝐡)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061   βˆ– cdif 3911   βŠ† wss 3914  ifcif 4490  {csn 4590   class class class wbr 5109   ↦ cmpt 5192   β†Ύ cres 5639  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064  β„*cxr 11196   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393  -cneg 11394   / cdiv 11820  2c2 12216  (,)cioo 13273  [,]cicc 13276  sincsin 15954  Ο€cpi 15957  β€“cnβ†’ccncf 24262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137  ax-addf 11138  ax-mulf 11139
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-pm 8774  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-z 12508  df-dec 12627  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-ioc 13278  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-fl 13706  df-mod 13784  df-seq 13916  df-exp 13977  df-fac 14183  df-bc 14212  df-hash 14240  df-shft 14961  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-limsup 15362  df-clim 15379  df-rlim 15380  df-sum 15580  df-ef 15958  df-sin 15960  df-cos 15961  df-pi 15963  df-struct 17027  df-sets 17044  df-slot 17062  df-ndx 17074  df-base 17092  df-ress 17121  df-plusg 17154  df-mulr 17155  df-starv 17156  df-sca 17157  df-vsca 17158  df-ip 17159  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-hom 17165  df-cco 17166  df-rest 17312  df-topn 17313  df-0g 17331  df-gsum 17332  df-topgen 17333  df-pt 17334  df-prds 17337  df-xrs 17392  df-qtop 17397  df-imas 17398  df-xps 17400  df-mre 17474  df-mrc 17475  df-acs 17477  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-submnd 18610  df-mulg 18881  df-cntz 19105  df-cmn 19572  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-fbas 20816  df-fg 20817  df-cnfld 20820  df-top 22266  df-topon 22283  df-topsp 22305  df-bases 22319  df-cld 22393  df-ntr 22394  df-cls 22395  df-nei 22472  df-lp 22510  df-perf 22511  df-cn 22601  df-cnp 22602  df-t1 22688  df-haus 22689  df-cmp 22761  df-tx 22936  df-hmeo 23129  df-fil 23220  df-fm 23312  df-flim 23313  df-flf 23314  df-xms 23696  df-ms 23697  df-tms 23698  df-cncf 24264  df-limc 25253  df-dv 25254
This theorem is referenced by:  fourierdlem88  44525
  Copyright terms: Public domain W3C validator