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 45631
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 5979 . . 3 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ (𝐴(,)𝐡)))
4 pire 26406 . . . . . . . . 9 Ο€ ∈ ℝ
54renegcli 11546 . . . . . . . 8 -Ο€ ∈ ℝ
65a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ∈ ℝ)
74a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Ο€ ∈ ℝ)
8 elioore 13381 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ ℝ)
98adantl 480 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
105a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -Ο€ ∈ ℝ)
114a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ Ο€ ∈ ℝ)
1210, 11iccssred 13438 . . . . . . . . . . 11 (πœ‘ β†’ (-Ο€[,]Ο€) βŠ† ℝ)
13 fourierdlem78.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (-Ο€[,]Ο€))
1412, 13sseldd 3974 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ ℝ)
1514adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
165, 4elicc2i 13417 . . . . . . . . . . . 12 (𝐴 ∈ (-Ο€[,]Ο€) ↔ (𝐴 ∈ ℝ ∧ -Ο€ ≀ 𝐴 ∧ 𝐴 ≀ Ο€))
1716simp2bi 1143 . . . . . . . . . . 11 (𝐴 ∈ (-Ο€[,]Ο€) β†’ -Ο€ ≀ 𝐴)
1813, 17syl 17 . . . . . . . . . 10 (πœ‘ β†’ -Ο€ ≀ 𝐴)
1918adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ≀ 𝐴)
2015rexrd 11289 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ*)
21 fourierdlem78.b . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ (-Ο€[,]Ο€))
2212, 21sseldd 3974 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ℝ)
2322rexrd 11289 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ ℝ*)
2423adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ*)
25 simpr 483 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (𝐴(,)𝐡))
26 ioogtlb 44939 . . . . . . . . . 10 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
2720, 24, 25, 26syl3anc 1368 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
286, 15, 9, 19, 27lelttrd 11397 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ < 𝑠)
296, 9, 28ltled 11387 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -Ο€ ≀ 𝑠)
3022adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
31 iooltub 44954 . . . . . . . . . 10 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
3220, 24, 25, 31syl3anc 1368 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
335, 4elicc2i 13417 . . . . . . . . . . . 12 (𝐡 ∈ (-Ο€[,]Ο€) ↔ (𝐡 ∈ ℝ ∧ -Ο€ ≀ 𝐡 ∧ 𝐡 ≀ Ο€))
3433simp3bi 1144 . . . . . . . . . . 11 (𝐡 ∈ (-Ο€[,]Ο€) β†’ 𝐡 ≀ Ο€)
3521, 34syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ≀ Ο€)
3635adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ≀ Ο€)
379, 30, 7, 32, 36ltletrd 11399 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < Ο€)
389, 7, 37ltled 11387 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ≀ Ο€)
396, 7, 9, 29, 38eliccd 44948 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
4039ex 411 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ (-Ο€[,]Ο€)))
4140ssrdv 3979 . . . 4 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (-Ο€[,]Ο€))
4241resmptd 6040 . . 3 (πœ‘ β†’ ((𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) β†Ύ (𝐴(,)𝐡)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
433, 42eqtrd 2765 . 2 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))))
44 0red 11242 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
45 fourierdlem78.f . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
4645adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐹:β„βŸΆβ„)
47 fourierdlem78.x . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑋 ∈ ℝ)
4847adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑋 ∈ ℝ)
4948, 9readdcld 11268 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ℝ)
5046, 49ffvelcdmd 7088 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
51 fourierdlem78.y . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Œ ∈ ℝ)
52 fourierdlem78.w . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘Š ∈ ℝ)
5351, 52ifcld 4571 . . . . . . . . . . . . . 14 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
5453adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ ℝ)
5550, 54resubcld 11667 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ℝ)
56 eleq1 2813 . . . . . . . . . . . . . . . 16 (𝑠 = 0 β†’ (𝑠 ∈ (𝐴(,)𝐡) ↔ 0 ∈ (𝐴(,)𝐡)))
5756biimpac 477 . . . . . . . . . . . . . . 15 ((𝑠 ∈ (𝐴(,)𝐡) ∧ 𝑠 = 0) β†’ 0 ∈ (𝐴(,)𝐡))
5857adantll 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) ∧ 𝑠 = 0) β†’ 0 ∈ (𝐴(,)𝐡))
59 fourierdlem78.nxelab . . . . . . . . . . . . . . 15 (πœ‘ β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
6059ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) ∧ 𝑠 = 0) β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
6158, 60pm2.65da 815 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 𝑠 = 0)
6261neqned 2937 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 β‰  0)
6355, 9, 62redivcld 12067 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) ∈ ℝ)
6444, 63ifcld 4571 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ ℝ)
65 fourierdlem78.h . . . . . . . . . . 11 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6665fvmpt2 7009 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ ℝ) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6739, 64, 66syl2anc 582 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
6867, 64eqeltrd 2825 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) ∈ ℝ)
69 1red 11240 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 1 ∈ ℝ)
70 2re 12311 . . . . . . . . . . . . . 14 2 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 ∈ ℝ)
729rehalfcld 12484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / 2) ∈ ℝ)
7372resincld 16114 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) ∈ ℝ)
7471, 73remulcld 11269 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ ℝ)
7571recnd 11267 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 ∈ β„‚)
7673recnd 11267 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) ∈ β„‚)
77 2ne0 12341 . . . . . . . . . . . . . 14 2 β‰  0
7877a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 2 β‰  0)
79 fourierdlem44 45598 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ 𝑠 β‰  0) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
8039, 62, 79syl2anc 582 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜(𝑠 / 2)) β‰  0)
8175, 76, 78, 80mulne0d 11891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) β‰  0)
829, 74, 81redivcld 12067 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) ∈ ℝ)
8369, 82ifcld 4571 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ ℝ)
84 fourierdlem78.k . . . . . . . . . . 11 𝐾 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8584fvmpt2 7009 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ ℝ) β†’ (πΎβ€˜π‘ ) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8639, 83, 85syl2anc 582 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
8786, 83eqeltrd 2825 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) ∈ ℝ)
8868, 87remulcld 11269 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ)
89 fourierdlem78.u . . . . . . . 8 π‘ˆ = (𝑠 ∈ (-Ο€[,]Ο€) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9089fvmpt2 7009 . . . . . . 7 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )) ∈ ℝ) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9139, 88, 90syl2anc 582 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘ˆβ€˜π‘ ) = ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ )))
9291, 88eqeltrd 2825 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘ˆβ€˜π‘ ) ∈ ℝ)
93 fourierdlem78.n . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ ℝ)
9493adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑁 ∈ ℝ)
9571, 78rereccld 12066 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 2) ∈ ℝ)
9694, 95readdcld 11268 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑁 + (1 / 2)) ∈ ℝ)
9796, 9remulcld 11269 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((𝑁 + (1 / 2)) Β· 𝑠) ∈ ℝ)
9897resincld 16114 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ℝ)
99 fourierdlem78.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
10099fvmpt2 7009 . . . . . . 7 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ℝ) β†’ (π‘†β€˜π‘ ) = (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
10139, 98, 100syl2anc 582 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘†β€˜π‘ ) = (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠)))
102101, 98eqeltrd 2825 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π‘†β€˜π‘ ) ∈ ℝ)
10392, 102remulcld 11269 . . . 4 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )) ∈ ℝ)
104 eqid 2725 . . . 4 (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ )))
105103, 104fmptd 7117 . . 3 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„)
106 ax-resscn 11190 . . . . 5 ℝ βŠ† β„‚
107106a1i 11 . . . 4 (πœ‘ β†’ ℝ βŠ† β„‚)
10891mpteq2dva 5244 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘ˆβ€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))))
10961iffalsed 4536 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
11055recnd 11267 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ β„‚)
1119recnd 11267 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ β„‚)
112110, 111, 62divrecd 12018 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠)))
11367, 109, 1123eqtrd 2769 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (π»β€˜π‘ ) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠)))
114113mpteq2dva 5244 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π»β€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠))))
11550recnd 11267 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
11654recnd 11267 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
117115, 116negsubd 11602 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)))
118117eqcomd 2731 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š)))
119118mpteq2dva 5244 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š))))
12014, 47readdcld 11268 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 + 𝑋) ∈ ℝ)
121120rexrd 11289 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 + 𝑋) ∈ ℝ*)
122121adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) ∈ ℝ*)
12322, 47readdcld 11268 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐡 + 𝑋) ∈ ℝ)
124123rexrd 11289 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 + 𝑋) ∈ ℝ*)
125124adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐡 + 𝑋) ∈ ℝ*)
12614recnd 11267 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 ∈ β„‚)
12747recnd 11267 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 ∈ β„‚)
128126, 127addcomd 11441 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 + 𝑋) = (𝑋 + 𝐴))
129128adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) = (𝑋 + 𝐴))
13015, 9, 48, 27ltadd2dd 11398 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐴) < (𝑋 + 𝑠))
131129, 130eqbrtrd 5166 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝐴 + 𝑋) < (𝑋 + 𝑠))
1329, 30, 48, 32ltadd2dd 11398 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝑋 + 𝐡))
13322recnd 11267 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ β„‚)
134127, 133addcomd 11441 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑋 + 𝐡) = (𝐡 + 𝑋))
135134adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐡) = (𝐡 + 𝑋))
136132, 135breqtrd 5170 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝐡 + 𝑋))
137122, 125, 49, 131, 136eliood 44942 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))
138 fvres 6909 . . . . . . . . . . . . . . 15 ((𝑋 + 𝑠) ∈ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) β†’ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
139137, 138syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
140139eqcomd 2731 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠)))
141140mpteq2dva 5244 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠))))
142 ioosscn 13413 . . . . . . . . . . . . . 14 ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) βŠ† β„‚
143142a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)) βŠ† β„‚)
144 fourierdlem78.fcn . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐡 + 𝑋))–cnβ†’β„‚))
145 ioosscn 13413 . . . . . . . . . . . . . 14 (𝐴(,)𝐡) βŠ† β„‚
146145a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
147143, 144, 146, 127, 137fourierdlem23 45577 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝐹 β†Ύ ((𝐴 + 𝑋)(,)(𝐡 + 𝑋)))β€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
148141, 147eqeltrd 2825 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
149 0red 11242 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
15014ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
1518adantl 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
152 simplr 767 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ≀ 𝐴)
15327adantlr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
154149, 150, 151, 152, 153lelttrd 11397 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 < 𝑠)
155154iftrued 4533 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Œ)
156155negeqd 11479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 0 ≀ 𝐴) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -if(0 < 𝑠, π‘Œ, π‘Š) = -π‘Œ)
157156mpteq2dva 5244 . . . . . . . . . . . . 13 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ))
15851renegcld 11666 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -π‘Œ ∈ ℝ)
159158recnd 11267 . . . . . . . . . . . . . . 15 (πœ‘ β†’ -π‘Œ ∈ β„‚)
160 ssid 3996 . . . . . . . . . . . . . . . 16 β„‚ βŠ† β„‚
161160a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ β„‚ βŠ† β„‚)
162146, 159, 161constcncfg 45319 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
163162adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Œ) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
164157, 163eqeltrd 2825 . . . . . . . . . . . 12 ((πœ‘ ∧ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
165 simpl 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ πœ‘)
16614rexrd 11289 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ ℝ*)
167166ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐴 ∈ ℝ*)
16823ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐡 ∈ ℝ*)
169 0red 11242 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ ℝ)
170 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ Β¬ 0 ≀ 𝐴)
17114adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐴 ∈ ℝ)
172 0red 11242 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 0 ∈ ℝ)
173171, 172ltnled 11386 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ (𝐴 < 0 ↔ Β¬ 0 ≀ 𝐴))
174170, 173mpbird 256 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐴 < 0)
175174adantr 479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐴 < 0)
176 simpr 483 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ Β¬ 𝐡 ≀ 0)
177 0red 11242 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ ℝ)
17822adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 𝐡 ∈ ℝ)
179177, 178ltnled 11386 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ (0 < 𝐡 ↔ Β¬ 𝐡 ≀ 0))
180176, 179mpbird 256 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 𝐡 ≀ 0) β†’ 0 < 𝐡)
181180adantlr 713 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 < 𝐡)
182167, 168, 169, 175, 181eliood 44942 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ 0 ∈ (𝐴(,)𝐡))
18359ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ Β¬ 0 ≀ 𝐴) ∧ Β¬ 𝐡 ≀ 0) β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
184182, 183condan 816 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ 𝐡 ≀ 0)
1858adantl 480 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
186 0red 11242 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 0 ∈ ℝ)
18722ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
18832adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
189 simplr 767 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ≀ 0)
190185, 187, 186, 188, 189ltletrd 11399 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 0)
191185, 186, 190ltnsymd 11388 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 0 < 𝑠)
192191iffalsed 4536 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Š)
193192negeqd 11479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐡 ≀ 0) ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ -if(0 < 𝑠, π‘Œ, π‘Š) = -π‘Š)
194193mpteq2dva 5244 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š))
19552recnd 11267 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Š ∈ β„‚)
196195negcld 11583 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -π‘Š ∈ β„‚)
197146, 196, 161constcncfg 45319 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
198197adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -π‘Š) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
199194, 198eqeltrd 2825 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐡 ≀ 0) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
200165, 184, 199syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ 0 ≀ 𝐴) β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
201164, 200pm2.61dan 811 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ -if(0 < 𝑠, π‘Œ, π‘Š)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
202148, 201addcncf 25385 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) + -if(0 < 𝑠, π‘Œ, π‘Š))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
203119, 202eqeltrd 2825 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
204 eqid 2725 . . . . . . . . . 10 (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) = (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠))
205 1cnd 11234 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ β„‚)
206204cdivcncf 24854 . . . . . . . . . . 11 (1 ∈ β„‚ β†’ (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) ∈ ((β„‚ βˆ– {0})–cnβ†’β„‚))
207205, 206syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (β„‚ βˆ– {0}) ↦ (1 / 𝑠)) ∈ ((β„‚ βˆ– {0})–cnβ†’β„‚))
208 velsn 4641 . . . . . . . . . . . . . 14 (𝑠 ∈ {0} ↔ 𝑠 = 0)
20961, 208sylnibr 328 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 𝑠 ∈ {0})
210111, 209eldifd 3952 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (β„‚ βˆ– {0}))
211210ralrimiva 3136 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘  ∈ (𝐴(,)𝐡)𝑠 ∈ (β„‚ βˆ– {0}))
212 dfss3 3962 . . . . . . . . . . 11 ((𝐴(,)𝐡) βŠ† (β„‚ βˆ– {0}) ↔ βˆ€π‘  ∈ (𝐴(,)𝐡)𝑠 ∈ (β„‚ βˆ– {0}))
213211, 212sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (β„‚ βˆ– {0}))
2149, 62rereccld 12066 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 𝑠) ∈ ℝ)
215214recnd 11267 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (1 / 𝑠) ∈ β„‚)
216204, 207, 213, 161, 215cncfmptssg 45318 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (1 / 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
217203, 216mulcncf 25387 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) Β· (1 / 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
218114, 217eqeltrd 2825 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π»β€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
21961iffalsed 4536 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) = (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))
22074recnd 11267 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (2 Β· (sinβ€˜(𝑠 / 2))) ∈ β„‚)
221111, 220, 81divrecd 12018 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))) = (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))))
22286, 219, 2213eqtrd 2769 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΎβ€˜π‘ ) = (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))))
223222mpteq2dva 5244 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΎβ€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
224219, 221eqtr2d 2766 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
225224mpteq2dva 5244 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))))
226 eqid 2725 . . . . . . . . . 10 (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))))
227 cncfss 24832 . . . . . . . . . . . 12 ((ℝ βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚))
228106, 160, 227mp2an 690 . . . . . . . . . . 11 ((-Ο€[,]Ο€)–cn→ℝ) βŠ† ((-Ο€[,]Ο€)–cnβ†’β„‚)
229226fourierdlem62 45615 . . . . . . . . . . . 12 (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cn→ℝ)
230229a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cn→ℝ))
231228, 230sselid 3971 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((-Ο€[,]Ο€)–cnβ†’β„‚))
23283recnd 11267 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2))))) ∈ β„‚)
233226, 231, 41, 161, 232cncfmptssg 45318 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ if(𝑠 = 0, 1, (𝑠 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
234225, 233eqeltrd 2825 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑠 Β· (1 / (2 Β· (sinβ€˜(𝑠 / 2)))))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
235223, 234eqeltrd 2825 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΎβ€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
236218, 235mulcncf 25387 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π»β€˜π‘ ) Β· (πΎβ€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
237108, 236eqeltrd 2825 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘ˆβ€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
238101mpteq2dva 5244 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘†β€˜π‘ )) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠))))
239 sincn 26394 . . . . . . . 8 sin ∈ (ℂ–cnβ†’β„‚)
240239a1i 11 . . . . . . 7 (πœ‘ β†’ sin ∈ (ℂ–cnβ†’β„‚))
241 halfre 12451 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
242241a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (1 / 2) ∈ ℝ)
24393, 242readdcld 11268 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 + (1 / 2)) ∈ ℝ)
244243recnd 11267 . . . . . . . . 9 (πœ‘ β†’ (𝑁 + (1 / 2)) ∈ β„‚)
245146, 244, 161constcncfg 45319 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (𝑁 + (1 / 2))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
246146, 161idcncfg 45320 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
247245, 246mulcncf 25387 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((𝑁 + (1 / 2)) Β· 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
248240, 247cncfmpt1f 24847 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (sinβ€˜((𝑁 + (1 / 2)) Β· 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
249238, 248eqeltrd 2825 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (π‘†β€˜π‘ )) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
250237, 249mulcncf 25387 . . . 4 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
251 cncfcdm 24831 . . . 4 ((ℝ βŠ† β„‚ ∧ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚)) β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„))
252107, 250, 251syl2anc 582 . . 3 (πœ‘ β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))):(𝐴(,)𝐡)βŸΆβ„))
253105, 252mpbird 256 . 2 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((π‘ˆβ€˜π‘ ) Β· (π‘†β€˜π‘ ))) ∈ ((𝐴(,)𝐡)–cn→ℝ))
25443, 253eqeltrd 2825 1 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ ((𝐴(,)𝐡)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051   βˆ– cdif 3938   βŠ† wss 3941  ifcif 4525  {csn 4625   class class class wbr 5144   ↦ cmpt 5227   β†Ύ cres 5675  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7413  β„‚cc 11131  β„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   Β· cmul 11138  β„*cxr 11272   < clt 11273   ≀ cle 11274   βˆ’ cmin 11469  -cneg 11470   / cdiv 11896  2c2 12292  (,)cioo 13351  [,]cicc 13354  sincsin 16034  Ο€cpi 16037  β€“cnβ†’ccncf 24809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211  ax-addf 11212
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-iin 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7866  df-1st 7987  df-2nd 7988  df-supp 8159  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9381  df-fi 9429  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-z 12584  df-dec 12703  df-uz 12848  df-q 12958  df-rp 13002  df-xneg 13119  df-xadd 13120  df-xmul 13121  df-ioo 13355  df-ioc 13356  df-ico 13357  df-icc 13358  df-fz 13512  df-fzo 13655  df-fl 13784  df-mod 13862  df-seq 13994  df-exp 14054  df-fac 14260  df-bc 14289  df-hash 14317  df-shft 15041  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-limsup 15442  df-clim 15459  df-rlim 15460  df-sum 15660  df-ef 16038  df-sin 16040  df-cos 16041  df-pi 16043  df-struct 17110  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-rest 17398  df-topn 17399  df-0g 17417  df-gsum 17418  df-topgen 17419  df-pt 17420  df-prds 17423  df-xrs 17478  df-qtop 17483  df-imas 17484  df-xps 17486  df-mre 17560  df-mrc 17561  df-acs 17563  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-submnd 18735  df-mulg 19023  df-cntz 19267  df-cmn 19736  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-fbas 21275  df-fg 21276  df-cnfld 21279  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-perf 23054  df-cn 23144  df-cnp 23145  df-t1 23231  df-haus 23232  df-cmp 23304  df-tx 23479  df-hmeo 23672  df-fil 23763  df-fm 23855  df-flim 23856  df-flf 23857  df-xms 24239  df-ms 24240  df-tms 24241  df-cncf 24811  df-limc 25808  df-dv 25809
This theorem is referenced by:  fourierdlem88  45641
  Copyright terms: Public domain W3C validator