Metamath Proof Explorer

Theorem fourierdlem9

Description: H is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem9.f ⊢ φ → F : ℝ ⟶ ℝ
fourierdlem9.x ⊢ φ → X ∈ ℝ
fourierdlem9.r ⊢ φ → Y ∈ ℝ
fourierdlem9.w ⊢ φ → W ∈ ℝ
fourierdlem9.h ⊢ H = s ∈ − π π ⟼ if s = 0 0 F ⁡ X + s − if 0 < s Y W s
Assertion fourierdlem9 ⊢ φ → H : − π π ⟶ ℝ

Proof

Step Hyp Ref Expression
1 fourierdlem9.f ⊢ φ → F : ℝ ⟶ ℝ
2 fourierdlem9.x ⊢ φ → X ∈ ℝ
3 fourierdlem9.r ⊢ φ → Y ∈ ℝ
4 fourierdlem9.w ⊢ φ → W ∈ ℝ
5 fourierdlem9.h ⊢ H = s ∈ − π π ⟼ if s = 0 0 F ⁡ X + s − if 0 < s Y W s
6 0red ⊢ φ ∧ s ∈ − π π ∧ s = 0 → 0 ∈ ℝ
7 1 adantr ⊢ φ ∧ s ∈ − π π → F : ℝ ⟶ ℝ
8 2 adantr ⊢ φ ∧ s ∈ − π π → X ∈ ℝ
9 pire ⊢ π ∈ ℝ
10 9 renegcli ⊢ − π ∈ ℝ
11 iccssre ⊢ − π ∈ ℝ ∧ π ∈ ℝ → − π π ⊆ ℝ
12 10 9 11 mp2an ⊢ − π π ⊆ ℝ
13 12 sseli ⊢ s ∈ − π π → s ∈ ℝ
14 13 adantl ⊢ φ ∧ s ∈ − π π → s ∈ ℝ
15 8 14 readdcld ⊢ φ ∧ s ∈ − π π → X + s ∈ ℝ
16 7 15 ffvelrnd ⊢ φ ∧ s ∈ − π π → F ⁡ X + s ∈ ℝ
17 16 adantr ⊢ φ ∧ s ∈ − π π ∧ ¬ s = 0 → F ⁡ X + s ∈ ℝ
18 3 4 ifcld ⊢ φ → if 0 < s Y W ∈ ℝ
19 18 ad2antrr ⊢ φ ∧ s ∈ − π π ∧ ¬ s = 0 → if 0 < s Y W ∈ ℝ
20 17 19 resubcld ⊢ φ ∧ s ∈ − π π ∧ ¬ s = 0 → F ⁡ X + s − if 0 < s Y W ∈ ℝ
21 14 adantr ⊢ φ ∧ s ∈ − π π ∧ ¬ s = 0 → s ∈ ℝ
22 neqne ⊢ ¬ s = 0 → s ≠ 0
23 22 adantl ⊢ φ ∧ s ∈ − π π ∧ ¬ s = 0 → s ≠ 0
24 20 21 23 redivcld ⊢ φ ∧ s ∈ − π π ∧ ¬ s = 0 → F ⁡ X + s − if 0 < s Y W s ∈ ℝ
25 6 24 ifclda ⊢ φ ∧ s ∈ − π π → if s = 0 0 F ⁡ X + s − if 0 < s Y W s ∈ ℝ
26 25 5 fmptd ⊢ φ → H : − π π ⟶ ℝ