Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem66 Structured version   Visualization version   GIF version

Theorem fourierdlem66 44058
Description: Value of the 𝐺 function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem66.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem66.x (𝜑𝑋 ∈ ℝ)
fourierdlem66.y (𝜑𝑌 ∈ ℝ)
fourierdlem66.w (𝜑𝑊 ∈ ℝ)
fourierdlem66.d 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
fourierdlem66.h 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
fourierdlem66.k 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
fourierdlem66.u 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
fourierdlem66.s 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠)))
fourierdlem66.g 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠)))
fourierdlem66.a 𝐴 = ((-π[,]π) ∖ {0})
Assertion
Ref Expression
fourierdlem66 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝐺𝑠) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷𝑛)‘𝑠))))
Distinct variable groups:   𝑛,𝑠   𝜑,𝑠
Allowed substitution hints:   𝜑(𝑛)   𝐴(𝑛,𝑠)   𝐷(𝑛,𝑠)   𝑆(𝑛,𝑠)   𝑈(𝑛,𝑠)   𝐹(𝑛,𝑠)   𝐺(𝑛,𝑠)   𝐻(𝑛,𝑠)   𝐾(𝑛,𝑠)   𝑊(𝑛,𝑠)   𝑋(𝑛,𝑠)   𝑌(𝑛,𝑠)

Proof of Theorem fourierdlem66
StepHypRef Expression
1 fourierdlem66.a . . . . . . . 8 𝐴 = ((-π[,]π) ∖ {0})
21eqimssi 3990 . . . . . . 7 𝐴 ⊆ ((-π[,]π) ∖ {0})
3 difss 4078 . . . . . . 7 ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)
42, 3sstri 3941 . . . . . 6 𝐴 ⊆ (-π[,]π)
54a1i 11 . . . . 5 (𝜑𝐴 ⊆ (-π[,]π))
65sselda 3932 . . . 4 ((𝜑𝑠𝐴) → 𝑠 ∈ (-π[,]π))
76adantlr 712 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → 𝑠 ∈ (-π[,]π))
8 fourierdlem66.f . . . . . . . 8 (𝜑𝐹:ℝ⟶ℝ)
98adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
10 fourierdlem66.x . . . . . . . 8 (𝜑𝑋 ∈ ℝ)
1110adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ ℝ)
12 fourierdlem66.y . . . . . . . 8 (𝜑𝑌 ∈ ℝ)
1312adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑌 ∈ ℝ)
14 fourierdlem66.w . . . . . . . 8 (𝜑𝑊 ∈ ℝ)
1514adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
16 fourierdlem66.h . . . . . . 7 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
17 fourierdlem66.k . . . . . . 7 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
18 fourierdlem66.u . . . . . . 7 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻𝑠) · (𝐾𝑠)))
199, 11, 13, 15, 16, 17, 18fourierdlem55 44047 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → 𝑈:(-π[,]π)⟶ℝ)
2019adantr 481 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → 𝑈:(-π[,]π)⟶ℝ)
2120, 7ffvelcdmd 7018 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝑈𝑠) ∈ ℝ)
22 nnre 12081 . . . . . . 7 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
23 fourierdlem66.s . . . . . . . 8 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠)))
2423fourierdlem5 43998 . . . . . . 7 (𝑛 ∈ ℝ → 𝑆:(-π[,]π)⟶ℝ)
2522, 24syl 17 . . . . . 6 (𝑛 ∈ ℕ → 𝑆:(-π[,]π)⟶ℝ)
2625ad2antlr 724 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → 𝑆:(-π[,]π)⟶ℝ)
2726, 7ffvelcdmd 7018 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝑆𝑠) ∈ ℝ)
2821, 27remulcld 11106 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ)
29 fourierdlem66.g . . . 4 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈𝑠) · (𝑆𝑠)))
3029fvmpt2 6942 . . 3 ((𝑠 ∈ (-π[,]π) ∧ ((𝑈𝑠) · (𝑆𝑠)) ∈ ℝ) → (𝐺𝑠) = ((𝑈𝑠) · (𝑆𝑠)))
317, 28, 30syl2anc 584 . 2 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝐺𝑠) = ((𝑈𝑠) · (𝑆𝑠)))
328, 10, 12, 14, 16fourierdlem9 44002 . . . . . . . . 9 (𝜑𝐻:(-π[,]π)⟶ℝ)
3332adantr 481 . . . . . . . 8 ((𝜑𝑠𝐴) → 𝐻:(-π[,]π)⟶ℝ)
3433, 6ffvelcdmd 7018 . . . . . . 7 ((𝜑𝑠𝐴) → (𝐻𝑠) ∈ ℝ)
3517fourierdlem43 44036 . . . . . . . . 9 𝐾:(-π[,]π)⟶ℝ
3635a1i 11 . . . . . . . 8 ((𝜑𝑠𝐴) → 𝐾:(-π[,]π)⟶ℝ)
3736, 6ffvelcdmd 7018 . . . . . . 7 ((𝜑𝑠𝐴) → (𝐾𝑠) ∈ ℝ)
3834, 37remulcld 11106 . . . . . 6 ((𝜑𝑠𝐴) → ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ)
3918fvmpt2 6942 . . . . . 6 ((𝑠 ∈ (-π[,]π) ∧ ((𝐻𝑠) · (𝐾𝑠)) ∈ ℝ) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
406, 38, 39syl2anc 584 . . . . 5 ((𝜑𝑠𝐴) → (𝑈𝑠) = ((𝐻𝑠) · (𝐾𝑠)))
41 0red 11079 . . . . . . . . 9 ((𝜑𝑠𝐴) → 0 ∈ ℝ)
428adantr 481 . . . . . . . . . . . 12 ((𝜑𝑠𝐴) → 𝐹:ℝ⟶ℝ)
4310adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑠𝐴) → 𝑋 ∈ ℝ)
44 pire 25721 . . . . . . . . . . . . . . . . 17 π ∈ ℝ
4544renegcli 11383 . . . . . . . . . . . . . . . 16 -π ∈ ℝ
46 iccssre 13262 . . . . . . . . . . . . . . . 16 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
4745, 44, 46mp2an 689 . . . . . . . . . . . . . . 15 (-π[,]π) ⊆ ℝ
484sseli 3928 . . . . . . . . . . . . . . 15 (𝑠𝐴𝑠 ∈ (-π[,]π))
4947, 48sselid 3930 . . . . . . . . . . . . . 14 (𝑠𝐴𝑠 ∈ ℝ)
5049adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑠𝐴) → 𝑠 ∈ ℝ)
5143, 50readdcld 11105 . . . . . . . . . . . 12 ((𝜑𝑠𝐴) → (𝑋 + 𝑠) ∈ ℝ)
5242, 51ffvelcdmd 7018 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
5312, 14ifcld 4519 . . . . . . . . . . . 12 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5453adantr 481 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℝ)
5552, 54resubcld 11504 . . . . . . . . . 10 ((𝜑𝑠𝐴) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℝ)
56 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑠𝐴) → 𝑠𝐴)
572, 56sselid 3930 . . . . . . . . . . . . 13 ((𝜑𝑠𝐴) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
5857eldifbd 3911 . . . . . . . . . . . 12 ((𝜑𝑠𝐴) → ¬ 𝑠 ∈ {0})
59 velsn 4589 . . . . . . . . . . . 12 (𝑠 ∈ {0} ↔ 𝑠 = 0)
6058, 59sylnib 327 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → ¬ 𝑠 = 0)
6160neqned 2947 . . . . . . . . . 10 ((𝜑𝑠𝐴) → 𝑠 ≠ 0)
6255, 50, 61redivcld 11904 . . . . . . . . 9 ((𝜑𝑠𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℝ)
6341, 62ifcld 4519 . . . . . . . 8 ((𝜑𝑠𝐴) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ)
6416fvmpt2 6942 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℝ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
656, 63, 64syl2anc 584 . . . . . . 7 ((𝜑𝑠𝐴) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
6660iffalsed 4484 . . . . . . 7 ((𝜑𝑠𝐴) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
6765, 66eqtrd 2776 . . . . . 6 ((𝜑𝑠𝐴) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
68 1red 11077 . . . . . . . . 9 ((𝜑𝑠𝐴) → 1 ∈ ℝ)
69 2re 12148 . . . . . . . . . . . 12 2 ∈ ℝ
7069a1i 11 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → 2 ∈ ℝ)
7150rehalfcld 12321 . . . . . . . . . . . 12 ((𝜑𝑠𝐴) → (𝑠 / 2) ∈ ℝ)
7271resincld 15951 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → (sin‘(𝑠 / 2)) ∈ ℝ)
7370, 72remulcld 11106 . . . . . . . . . 10 ((𝜑𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
74 2cnd 12152 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → 2 ∈ ℂ)
7572recnd 11104 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → (sin‘(𝑠 / 2)) ∈ ℂ)
76 2ne0 12178 . . . . . . . . . . . 12 2 ≠ 0
7776a1i 11 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → 2 ≠ 0)
78 fourierdlem44 44037 . . . . . . . . . . . 12 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
796, 61, 78syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑠𝐴) → (sin‘(𝑠 / 2)) ≠ 0)
8074, 75, 77, 79mulne0d 11728 . . . . . . . . . 10 ((𝜑𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
8150, 73, 80redivcld 11904 . . . . . . . . 9 ((𝜑𝑠𝐴) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
8268, 81ifcld 4519 . . . . . . . 8 ((𝜑𝑠𝐴) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ)
8317fvmpt2 6942 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℝ) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
846, 82, 83syl2anc 584 . . . . . . 7 ((𝜑𝑠𝐴) → (𝐾𝑠) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8560iffalsed 4484 . . . . . . 7 ((𝜑𝑠𝐴) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
8684, 85eqtrd 2776 . . . . . 6 ((𝜑𝑠𝐴) → (𝐾𝑠) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
8767, 86oveq12d 7355 . . . . 5 ((𝜑𝑠𝐴) → ((𝐻𝑠) · (𝐾𝑠)) = ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
8855recnd 11104 . . . . . 6 ((𝜑𝑠𝐴) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
8950recnd 11104 . . . . . 6 ((𝜑𝑠𝐴) → 𝑠 ∈ ℂ)
9074, 75mulcld 11096 . . . . . 6 ((𝜑𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
9188, 89, 90, 61, 80dmdcan2d 11882 . . . . 5 ((𝜑𝑠𝐴) → ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / (2 · (sin‘(𝑠 / 2)))))
9240, 87, 913eqtrd 2780 . . . 4 ((𝜑𝑠𝐴) → (𝑈𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / (2 · (sin‘(𝑠 / 2)))))
9392adantlr 712 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝑈𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / (2 · (sin‘(𝑠 / 2)))))
9422ad2antlr 724 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → 𝑛 ∈ ℝ)
95 1red 11077 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → 1 ∈ ℝ)
9695rehalfcld 12321 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (1 / 2) ∈ ℝ)
9794, 96readdcld 11105 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝑛 + (1 / 2)) ∈ ℝ)
9849adantl 482 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → 𝑠 ∈ ℝ)
9997, 98remulcld 11106 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((𝑛 + (1 / 2)) · 𝑠) ∈ ℝ)
10099resincld 15951 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℝ)
10123fvmpt2 6942 . . . 4 ((𝑠 ∈ (-π[,]π) ∧ (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℝ) → (𝑆𝑠) = (sin‘((𝑛 + (1 / 2)) · 𝑠)))
1027, 100, 101syl2anc 584 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝑆𝑠) = (sin‘((𝑛 + (1 / 2)) · 𝑠)))
10393, 102oveq12d 7355 . 2 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((𝑈𝑠) · (𝑆𝑠)) = ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / (2 · (sin‘(𝑠 / 2)))) · (sin‘((𝑛 + (1 / 2)) · 𝑠))))
10488adantlr 712 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
10590adantlr 712 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
106100recnd 11104 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℂ)
10780adantlr 712 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
108104, 105, 106, 107div32d 11875 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / (2 · (sin‘(𝑠 / 2)))) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2))))))
10922adantr 481 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → 𝑛 ∈ ℝ)
110 halfre 12288 . . . . . . . . . . . . . 14 (1 / 2) ∈ ℝ
111110a1i 11 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (1 / 2) ∈ ℝ)
112109, 111readdcld 11105 . . . . . . . . . . . 12 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (𝑛 + (1 / 2)) ∈ ℝ)
11349adantl 482 . . . . . . . . . . . 12 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → 𝑠 ∈ ℝ)
114112, 113remulcld 11106 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((𝑛 + (1 / 2)) · 𝑠) ∈ ℝ)
115114resincld 15951 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℝ)
116115recnd 11104 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (sin‘((𝑛 + (1 / 2)) · 𝑠)) ∈ ℂ)
11769a1i 11 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → 2 ∈ ℝ)
118113rehalfcld 12321 . . . . . . . . . . . 12 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (𝑠 / 2) ∈ ℝ)
119118resincld 15951 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (sin‘(𝑠 / 2)) ∈ ℝ)
120117, 119remulcld 11106 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
121120recnd 11104 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
122 picn 25722 . . . . . . . . . 10 π ∈ ℂ
123122a1i 11 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → π ∈ ℂ)
124 2cnd 12152 . . . . . . . . . . 11 (𝑠𝐴 → 2 ∈ ℂ)
125 rehalfcl 12300 . . . . . . . . . . . . 13 (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℝ)
126 resincl 15948 . . . . . . . . . . . . 13 ((𝑠 / 2) ∈ ℝ → (sin‘(𝑠 / 2)) ∈ ℝ)
12749, 125, 1263syl 18 . . . . . . . . . . . 12 (𝑠𝐴 → (sin‘(𝑠 / 2)) ∈ ℝ)
128127recnd 11104 . . . . . . . . . . 11 (𝑠𝐴 → (sin‘(𝑠 / 2)) ∈ ℂ)
12976a1i 11 . . . . . . . . . . 11 (𝑠𝐴 → 2 ≠ 0)
130 eldifsni 4737 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ≠ 0)
131130, 1eleq2s 2855 . . . . . . . . . . . 12 (𝑠𝐴𝑠 ≠ 0)
13248, 131, 78syl2anc 584 . . . . . . . . . . 11 (𝑠𝐴 → (sin‘(𝑠 / 2)) ≠ 0)
133124, 128, 129, 132mulne0d 11728 . . . . . . . . . 10 (𝑠𝐴 → (2 · (sin‘(𝑠 / 2))) ≠ 0)
134133adantl 482 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
135 0re 11078 . . . . . . . . . . 11 0 ∈ ℝ
136 pipos 25723 . . . . . . . . . . 11 0 < π
137135, 136gtneii 11188 . . . . . . . . . 10 π ≠ 0
138137a1i 11 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → π ≠ 0)
139116, 121, 123, 134, 138divdiv1d 11883 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) / π) = ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · (sin‘(𝑠 / 2))) · π)))
140 2cnd 12152 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → 2 ∈ ℂ)
141128adantl 482 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (sin‘(𝑠 / 2)) ∈ ℂ)
142140, 141, 123mulassd 11099 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((2 · (sin‘(𝑠 / 2))) · π) = (2 · ((sin‘(𝑠 / 2)) · π)))
143142oveq2d 7353 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · (sin‘(𝑠 / 2))) · π)) = ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · ((sin‘(𝑠 / 2)) · π))))
144141, 123mulcomd 11097 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘(𝑠 / 2)) · π) = (π · (sin‘(𝑠 / 2))))
145144oveq2d 7353 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (2 · ((sin‘(𝑠 / 2)) · π)) = (2 · (π · (sin‘(𝑠 / 2)))))
146140, 123, 141mulassd 11099 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((2 · π) · (sin‘(𝑠 / 2))) = (2 · (π · (sin‘(𝑠 / 2)))))
147145, 146eqtr4d 2779 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (2 · ((sin‘(𝑠 / 2)) · π)) = ((2 · π) · (sin‘(𝑠 / 2))))
148147oveq2d 7353 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · ((sin‘(𝑠 / 2)) · π))) = ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))
149139, 143, 1483eqtrd 2780 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) / π) = ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))
150149oveq2d 7353 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (π · (((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) / π)) = (π · ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))
151115, 120, 134redivcld 11904 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
152151recnd 11104 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
153152, 123, 138divcan2d 11854 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (π · (((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) / π)) = ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))))
154 fourierdlem66.d . . . . . . . . . 10 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
155154dirkerval2 43980 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ) → ((𝐷𝑛)‘𝑠) = if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))
15649, 155sylan2 593 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((𝐷𝑛)‘𝑠) = if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))
157 fourierdlem24 44017 . . . . . . . . . . . 12 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 mod (2 · π)) ≠ 0)
158157, 1eleq2s 2855 . . . . . . . . . . 11 (𝑠𝐴 → (𝑠 mod (2 · π)) ≠ 0)
159158neneqd 2945 . . . . . . . . . 10 (𝑠𝐴 → ¬ (𝑠 mod (2 · π)) = 0)
160159adantl 482 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ¬ (𝑠 mod (2 · π)) = 0)
161160iffalsed 4484 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))) = ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))
162156, 161eqtr2d 2777 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))) = ((𝐷𝑛)‘𝑠))
163162oveq2d 7353 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (π · ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))) = (π · ((𝐷𝑛)‘𝑠)))
164150, 153, 1633eqtr3d 2784 . . . . 5 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2)))) = (π · ((𝐷𝑛)‘𝑠)))
165164oveq2d 7353 . . . 4 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2))))) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (π · ((𝐷𝑛)‘𝑠))))
166165adantll 711 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / (2 · (sin‘(𝑠 / 2))))) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (π · ((𝐷𝑛)‘𝑠))))
167122a1i 11 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → π ∈ ℂ)
168154dirkerre 43981 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℝ) → ((𝐷𝑛)‘𝑠) ∈ ℝ)
16949, 168sylan2 593 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((𝐷𝑛)‘𝑠) ∈ ℝ)
170169recnd 11104 . . . . 5 ((𝑛 ∈ ℕ ∧ 𝑠𝐴) → ((𝐷𝑛)‘𝑠) ∈ ℂ)
171170adantll 711 . . . 4 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((𝐷𝑛)‘𝑠) ∈ ℂ)
172104, 167, 171mul12d 11285 . . 3 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · (π · ((𝐷𝑛)‘𝑠))) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷𝑛)‘𝑠))))
173108, 166, 1723eqtrd 2780 . 2 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → ((((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / (2 · (sin‘(𝑠 / 2)))) · (sin‘((𝑛 + (1 / 2)) · 𝑠))) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷𝑛)‘𝑠))))
17431, 103, 1733eqtrd 2780 1 (((𝜑𝑛 ∈ ℕ) ∧ 𝑠𝐴) → (𝐺𝑠) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷𝑛)‘𝑠))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1540  wcel 2105  wne 2940  cdif 3895  wss 3898  ifcif 4473  {csn 4573   class class class wbr 5092  cmpt 5175  wf 6475  cfv 6479  (class class class)co 7337  cc 10970  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   · cmul 10977   < clt 11110  cmin 11306  -cneg 11307   / cdiv 11733  cn 12074  2c2 12129  [,]cicc 13183   mod cmo 13690  sincsin 15872  πcpi 15875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ioc 13185  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-mod 13691  df-seq 13823  df-exp 13884  df-fac 14089  df-bc 14118  df-hash 14146  df-shft 14877  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-limsup 15279  df-clim 15296  df-rlim 15297  df-sum 15497  df-ef 15876  df-sin 15878  df-cos 15879  df-pi 15881  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-submnd 18528  df-mulg 18797  df-cntz 19019  df-cmn 19483  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137
This theorem is referenced by:  fourierdlem95  44087
  Copyright terms: Public domain W3C validator