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 45485
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 5978 . . 3 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ (𝐴(,)𝐡)))
4 pire 26367 . . . . . . . . 9 Ο€ ∈ ℝ
54renegcli 11537 . . . . . . . 8 -Ο€ ∈ ℝ
65a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ∈ ℝ)
74a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Ο€ ∈ ℝ)
8 elioore 13372 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ ℝ)
98adantl 481 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
105a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -Ο€ ∈ ℝ)
114a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ Ο€ ∈ ℝ)
1210, 11iccssred 13429 . . . . . . . . . . 11 (πœ‘ β†’ (-Ο€[,]Ο€) βŠ† ℝ)
13 fourierdlem78.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (-Ο€[,]Ο€))
1412, 13sseldd 3979 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ ℝ)
1514adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
165, 4elicc2i 13408 . . . . . . . . . . . 12 (𝐴 ∈ (-Ο€[,]Ο€) ↔ (𝐴 ∈ ℝ ∧ -Ο€ ≀ 𝐴 ∧ 𝐴 ≀ Ο€))
1716simp2bi 1144 . . . . . . . . . . 11 (𝐴 ∈ (-Ο€[,]Ο€) β†’ -Ο€ ≀ 𝐴)
1813, 17syl 17 . . . . . . . . . 10 (πœ‘ β†’ -Ο€ ≀ 𝐴)
1918adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ≀ 𝐴)
2015rexrd 11280 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ*)
21 fourierdlem78.b . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ (-Ο€[,]Ο€))
2212, 21sseldd 3979 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ℝ)
2322rexrd 11280 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ ℝ*)
2423adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ*)
25 simpr 484 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (𝐴(,)𝐡))
26 ioogtlb 44793 . . . . . . . . . 10 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
2720, 24, 25, 26syl3anc 1369 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
286, 15, 9, 19, 27lelttrd 11388 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ < 𝑠)
296, 9, 28ltled 11378 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ≀ 𝑠)
3022adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
31 iooltub 44808 . . . . . . . . . 10 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
3220, 24, 25, 31syl3anc 1369 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
335, 4elicc2i 13408 . . . . . . . . . . . 12 (𝐡 ∈ (-Ο€[,]Ο€) ↔ (𝐡 ∈ ℝ ∧ -Ο€ ≀ 𝐡 ∧ 𝐡 ≀ Ο€))
3433simp3bi 1145 . . . . . . . . . . 11 (𝐡 ∈ (-Ο€[,]Ο€) β†’ 𝐡 ≀ Ο€)
3521, 34syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ≀ Ο€)
3635adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ≀ Ο€)
379, 30, 7, 32, 36ltletrd 11390 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < Ο€)
389, 7, 37ltled 11378 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ≀ Ο€)
396, 7, 9, 29, 38eliccd 44802 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
4039ex 412 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ (-Ο€[,]Ο€)))
4140ssrdv 3984 . . . 4 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (-Ο€[,]Ο€))
4241resmptd 6038 . . 3 (πœ‘ β†’ ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ (𝐴(,)𝐡)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
433, 42eqtrd 2767 . 2 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
44 0red 11233 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
45 fourierdlem78.f . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
4645adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐹:β„βŸΆβ„)
47 fourierdlem78.x . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑋 ∈ ℝ)
4847adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑋 ∈ ℝ)
4948, 9readdcld 11259 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ℝ)
5046, 49ffvelcdmd 7089 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
51 fourierdlem78.y . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Œ ∈ ℝ)
52 fourierdlem78.w . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Š ∈ ℝ)
5351, 52ifcld 4570 . . . . . . . . . . . . . 14 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
5453adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
5550, 54resubcld 11658 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
56 eleq1 2816 . . . . . . . . . . . . . . . 16 (𝑠 = 0 β†’ (𝑠 ∈ (𝐴(,)𝐡) ↔ 0 ∈ (𝐴(,)𝐡)))
5756biimpac 478 . . . . . . . . . . . . . . 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 2942 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 β‰  0)
6355, 9, 62redivcld 12058 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) ∈ ℝ)
6444, 63ifcld 4570 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ ℝ)
65 fourierdlem78.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6665fvmpt2 7010 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ ℝ) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6739, 64, 66syl2anc 583 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6867, 64eqeltrd 2828 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) ∈ ℝ)
69 1red 11231 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 1 ∈ ℝ)
70 2re 12302 . . . . . . . . . . . . . 14 2 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 ∈ ℝ)
729rehalfcld 12475 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / 2) ∈ ℝ)
7372resincld 16105 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) ∈ ℝ)
7471, 73remulcld 11260 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ ℝ)
7571recnd 11258 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 ∈ β„‚)
7673recnd 11258 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) ∈ β„‚)
77 2ne0 12332 . . . . . . . . . . . . . 14 2 β‰  0
7877a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 β‰  0)
79 fourierdlem44 45452 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ 𝑠 β‰  0) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
8039, 62, 79syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
8175, 76, 78, 80mulne0d 11882 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) β‰  0)
829, 74, 81redivcld 12058 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ ℝ)
8369, 82ifcld 4570 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ ℝ)
84 fourierdlem78.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8584fvmpt2 7010 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ ℝ) β†’ (πΎβ€˜π‘ ) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8639, 83, 85syl2anc 583 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8786, 83eqeltrd 2828 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) ∈ ℝ)
8868, 87remulcld 11260 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ)
89 fourierdlem78.u . . . . . . . 8 π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9089fvmpt2 7010 . . . . . . 7 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9139, 88, 90syl2anc 583 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9291, 88eqeltrd 2828 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘ˆβ€˜π‘ ) ∈ ℝ)
93 fourierdlem78.n . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ ℝ)
9493adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑁 ∈ ℝ)
9571, 78rereccld 12057 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 2) ∈ ℝ)
9694, 95readdcld 11259 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑁 + (1 / 2)) ∈ ℝ)
9796, 9remulcld 11260 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((𝑁 + (1 / 2)) Β· 𝑠) ∈ ℝ)
9897resincld 16105 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ℝ)
99 fourierdlem78.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
10099fvmpt2 7010 . . . . . . 7 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ℝ) β†’ (π‘†β€˜π‘ ) = (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
10139, 98, 100syl2anc 583 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘†β€˜π‘ ) = (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
102101, 98eqeltrd 2828 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘†β€˜π‘ ) ∈ ℝ)
10392, 102remulcld 11260 . . . 4 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )) ∈ ℝ)
104 eqid 2727 . . . 4 (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
105103, 104fmptd 7118 . . 3 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„)
106 ax-resscn 11181 . . . . 5 ℝ βŠ† β„‚
107106a1i 11 . . . 4 (πœ‘ β†’ ℝ βŠ† β„‚)
10891mpteq2dva 5242 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘ˆβ€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))))
10961iffalsed 4535 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
11055recnd 11258 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ β„‚)
1119recnd 11258 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ β„‚)
112110, 111, 62divrecd 12009 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠)))
11367, 109, 1123eqtrd 2771 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠)))
114113mpteq2dva 5242 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π»β€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠))))
11550recnd 11258 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
11654recnd 11258 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
117115, 116negsubd 11593 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)))
118117eqcomd 2733 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š)))
119118mpteq2dva 5242 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š))))
12014, 47readdcld 11259 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 + 𝑋) ∈ ℝ)
121120rexrd 11280 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 + 𝑋) ∈ ℝ*)
122121adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) ∈ ℝ*)
12322, 47readdcld 11259 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 + 𝑋) ∈ ℝ)
124123rexrd 11280 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 + 𝑋) ∈ ℝ*)
125124adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐡 + 𝑋) ∈ ℝ*)
12614recnd 11258 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 ∈ β„‚)
12747recnd 11258 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 ∈ β„‚)
128126, 127addcomd 11432 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 + 𝑋) = (𝑋 + 𝐴))
129128adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) = (𝑋 + 𝐴))
13015, 9, 48, 27ltadd2dd 11389 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐴) < (𝑋 + 𝑠))
131129, 130eqbrtrd 5164 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) < (𝑋 + 𝑠))
1329, 30, 48, 32ltadd2dd 11389 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝑋 + 𝐡))
13322recnd 11258 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ β„‚)
134127, 133addcomd 11432 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑋 + 𝐡) = (𝐡 + 𝑋))
135134adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐡) = (𝐡 + 𝑋))
136132, 135breqtrd 5168 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝐡 + 𝑋))
137122, 125, 49, 131, 136eliood 44796 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))
138 fvres 6910 . . . . . . . . . . . . . . 15 ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) β†’ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
139137, 138syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
140139eqcomd 2733 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)))
141140mpteq2dva 5242 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠))))
142 ioosscn 13404 . . . . . . . . . . . . . 14 ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) βŠ† β„‚
143142a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) βŠ† β„‚)
144 fourierdlem78.fcn . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐡 + 𝑋))–cnβ†’β„‚))
145 ioosscn 13404 . . . . . . . . . . . . . 14 (𝐴(,)𝐡) βŠ† β„‚
146145a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
147143, 144, 146, 127, 137fourierdlem23 45431 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
148141, 147eqeltrd 2828 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
149 0red 11233 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
15014ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
1518adantl 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
152 simplr 768 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ≀ 𝐴)
15327adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
154149, 150, 151, 152, 153lelttrd 11388 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 < 𝑠)
155154iftrued 4532 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Œ)
156155negeqd 11470 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -if(0 < 𝑠, π‘Œ, π‘Š) = -π‘Œ)
157156mpteq2dva 5242 . . . . . . . . . . . . 13 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ))
15851renegcld 11657 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -π‘Œ ∈ ℝ)
159158recnd 11258 . . . . . . . . . . . . . . 15 (πœ‘ β†’ -π‘Œ ∈ β„‚)
160 ssid 4000 . . . . . . . . . . . . . . . 16 β„‚ βŠ† β„‚
161160a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ β„‚ βŠ† β„‚)
162146, 159, 161constcncfg 45173 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
163162adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
164157, 163eqeltrd 2828 . . . . . . . . . . . 12 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
165 simpl 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ πœ‘)
16614rexrd 11280 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ ℝ*)
167166ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐴 ∈ ℝ*)
16823ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐡 ∈ ℝ*)
169 0red 11233 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ ℝ)
170 simpr 484 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ Β¬ 0 ≀ 𝐴)
17114adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐴 ∈ ℝ)
172 0red 11233 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 0 ∈ ℝ)
173171, 172ltnled 11377 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ (𝐴 < 0 ↔ Β¬ 0 ≀ 𝐴))
174170, 173mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐴 < 0)
175174adantr 480 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐴 < 0)
176 simpr 484 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ Β¬ 𝐡 ≀ 0)
177 0red 11233 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ ℝ)
17822adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐡 ∈ ℝ)
179177, 178ltnled 11377 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ (0 < 𝐡 ↔ Β¬ 𝐡 ≀ 0))
180176, 179mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 0 < 𝐡)
181180adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 < 𝐡)
182167, 168, 169, 175, 181eliood 44796 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ (𝐴(,)𝐡))
18359ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
184182, 183condan 817 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐡 ≀ 0)
1858adantl 481 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
186 0red 11233 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
18722ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
18832adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
189 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ≀ 0)
190185, 187, 186, 188, 189ltletrd 11390 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 0)
191185, 186, 190ltnsymd 11379 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 0 < 𝑠)
192191iffalsed 4535 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Š)
193192negeqd 11470 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -if(0 < 𝑠, π‘Œ, π‘Š) = -π‘Š)
194193mpteq2dva 5242 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š))
19552recnd 11258 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Š ∈ β„‚)
196195negcld 11574 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -π‘Š ∈ β„‚)
197146, 196, 161constcncfg 45173 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
198197adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
199194, 198eqeltrd 2828 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
200165, 184, 199syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
201164, 200pm2.61dan 812 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
202148, 201addcncf 25346 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
203119, 202eqeltrd 2828 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
204 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) = (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠))
205 1cnd 11225 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ β„‚)
206204cdivcncf 24815 . . . . . . . . . . 11 (1 ∈ β„‚ β†’ (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) ∈ ((β„‚ βˆ– {0})–cnβ†’β„‚))
207205, 206syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) ∈ ((β„‚ βˆ– {0})–cnβ†’β„‚))
208 velsn 4640 . . . . . . . . . . . . . 14 (𝑠 ∈ {0} ↔ 𝑠 = 0)
20961, 208sylnibr 329 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 𝑠 ∈ {0})
210111, 209eldifd 3955 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (β„‚ βˆ– {0}))
211210ralrimiva 3141 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘  ∈ (𝐴(,)𝐡)𝑠 ∈ (β„‚ βˆ– {0}))
212 dfss3 3966 . . . . . . . . . . 11 ((𝐴(,)𝐡) βŠ† (β„‚ βˆ– {0}) ↔ βˆ€π‘  ∈ (𝐴(,)𝐡)𝑠 ∈ (β„‚ βˆ– {0}))
213211, 212sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (β„‚ βˆ– {0}))
2149, 62rereccld 12057 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 𝑠) ∈ ℝ)
215214recnd 11258 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 𝑠) ∈ β„‚)
216204, 207, 213, 161, 215cncfmptssg 45172 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
217203, 216mulcncf 25348 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
218114, 217eqeltrd 2828 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π»β€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
21961iffalsed 4535 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) = (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))
22074recnd 11258 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ β„‚)
221111, 220, 81divrecd 12009 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) = (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))))
22286, 219, 2213eqtrd 2771 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) = (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))))
223222mpteq2dva 5242 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΎβ€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
224219, 221eqtr2d 2768 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
225224mpteq2dva 5242 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
226 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
227 cncfss 24793 . . . . . . . . . . . 12 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
228106, 160, 227mp2an 691 . . . . . . . . . . 11 ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚)
229226fourierdlem62 45469 . . . . . . . . . . . 12 (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cn→ℝ)
230229a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
231228, 230sselid 3976 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
23283recnd 11258 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ β„‚)
233226, 231, 41, 161, 232cncfmptssg 45172 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
234225, 233eqeltrd 2828 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
235223, 234eqeltrd 2828 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΎβ€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
236218, 235mulcncf 25348 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
237108, 236eqeltrd 2828 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘ˆβ€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
238101mpteq2dva 5242 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘†β€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠))))
239 sincn 26355 . . . . . . . 8 sin ∈ (ℂ–cnβ†’β„‚)
240239a1i 11 . . . . . . 7 (πœ‘ β†’ sin ∈ (ℂ–cnβ†’β„‚))
241 halfre 12442 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
242241a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (1 / 2) ∈ ℝ)
24393, 242readdcld 11259 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 + (1 / 2)) ∈ ℝ)
244243recnd 11258 . . . . . . . . 9 (πœ‘ β†’ (𝑁 + (1 / 2)) ∈ β„‚)
245146, 244, 161constcncfg 45173 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
246146, 161idcncfg 45174 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
247245, 246mulcncf 25348 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
248240, 247cncfmpt1f 24808 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
249238, 248eqeltrd 2828 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘†β€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
250237, 249mulcncf 25348 . . . 4 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
251 cncfcdm 24792 . . . 4 ((ℝ βŠ† β„‚ ∧ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚)) β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„))
252107, 250, 251syl2anc 583 . . 3 (πœ‘ β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„))
253105, 252mpbird 257 . 2 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ))
25443, 253eqeltrd 2828 1 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ ((𝐴(,)𝐡)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056   βˆ– cdif 3941   βŠ† wss 3944  ifcif 4524  {csn 4624   class class class wbr 5142   ↦ cmpt 5225   β†Ύ cres 5674  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  β„‚cc 11122  β„cr 11123  0cc0 11124  1c1 11125   + caddc 11127   Β· cmul 11129  β„*cxr 11263   < clt 11264   ≀ cle 11265   βˆ’ cmin 11460  -cneg 11461   / cdiv 11887  2c2 12283  (,)cioo 13342  [,]cicc 13345  sincsin 16025  Ο€cpi 16028  β€“cnβ†’ccncf 24770
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 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-inf2 9650  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202  ax-addf 11203
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7677  df-om 7863  df-1st 7985  df-2nd 7986  df-supp 8158  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-er 8716  df-map 8836  df-pm 8837  df-ixp 8906  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-fsupp 9376  df-fi 9420  df-sup 9451  df-inf 9452  df-oi 9519  df-card 9948  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-3 12292  df-4 12293  df-5 12294  df-6 12295  df-7 12296  df-8 12297  df-9 12298  df-n0 12489  df-z 12575  df-dec 12694  df-uz 12839  df-q 12949  df-rp 12993  df-xneg 13110  df-xadd 13111  df-xmul 13112  df-ioo 13346  df-ioc 13347  df-ico 13348  df-icc 13349  df-fz 13503  df-fzo 13646  df-fl 13775  df-mod 13853  df-seq 13985  df-exp 14045  df-fac 14251  df-bc 14280  df-hash 14308  df-shft 15032  df-cj 15064  df-re 15065  df-im 15066  df-sqrt 15200  df-abs 15201  df-limsup 15433  df-clim 15450  df-rlim 15451  df-sum 15651  df-ef 16029  df-sin 16031  df-cos 16032  df-pi 16034  df-struct 17101  df-sets 17118  df-slot 17136  df-ndx 17148  df-base 17166  df-ress 17195  df-plusg 17231  df-mulr 17232  df-starv 17233  df-sca 17234  df-vsca 17235  df-ip 17236  df-tset 17237  df-ple 17238  df-ds 17240  df-unif 17241  df-hom 17242  df-cco 17243  df-rest 17389  df-topn 17390  df-0g 17408  df-gsum 17409  df-topgen 17410  df-pt 17411  df-prds 17414  df-xrs 17469  df-qtop 17474  df-imas 17475  df-xps 17477  df-mre 17551  df-mrc 17552  df-acs 17554  df-mgm 18585  df-sgrp 18664  df-mnd 18680  df-submnd 18726  df-mulg 19008  df-cntz 19252  df-cmn 19721  df-psmet 21251  df-xmet 21252  df-met 21253  df-bl 21254  df-mopn 21255  df-fbas 21256  df-fg 21257  df-cnfld 21260  df-top 22770  df-topon 22787  df-topsp 22809  df-bases 22823  df-cld 22897  df-ntr 22898  df-cls 22899  df-nei 22976  df-lp 23014  df-perf 23015  df-cn 23105  df-cnp 23106  df-t1 23192  df-haus 23193  df-cmp 23265  df-tx 23440  df-hmeo 23633  df-fil 23724  df-fm 23816  df-flim 23817  df-flf 23818  df-xms 24200  df-ms 24201  df-tms 24202  df-cncf 24772  df-limc 25769  df-dv 25770
This theorem is referenced by:  fourierdlem88  45495
  Copyright terms: Public domain W3C validator