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∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
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∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
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 ffvelcdmd ⊢φ∧s∈−ππ→F⁡X+s∈ℝ
17 16 adantr ⊢φ∧s∈−ππ∧¬s=0→F⁡X+s∈ℝ
18 3 4 ifcld ⊢φ→if0<sYW∈ℝ
19 18 ad2antrr ⊢φ∧s∈−ππ∧¬s=0→if0<sYW∈ℝ
20 17 19 resubcld ⊢φ∧s∈−ππ∧¬s=0→F⁡X+s−if0<sYW∈ℝ
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−if0<sYWs∈ℝ
25 6 24 ifclda ⊢φ∧s∈−ππ→ifs=00F⁡X+s−if0<sYWs∈ℝ
26 25 5 fmptd ⊢φ→H:−ππ⟶ℝ