Metamath Proof Explorer

Theorem fourierdlem9

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

Ref Expression
Hypotheses fourierdlem9.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem9.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem9.r ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
fourierdlem9.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
fourierdlem9.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
Assertion fourierdlem9 ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 fourierdlem9.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem9.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem9.r ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
4 fourierdlem9.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
5 fourierdlem9.h ⊢ 𝐻 = ( 𝑠 ∈ ( - π [,] π ) ↦ if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) )
6 0red ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ 𝑠 = 0 ) → 0 ∈ ℝ )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝐹 : ℝ ⟶ ℝ )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑋 ∈ ℝ )
9 pire ⊢ π ∈ ℝ
10 9 renegcli ⊢ - π ∈ ℝ
11 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
12 10 9 11 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
13 12 sseli ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ℝ )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ℝ )
15 8 14 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
16 7 15 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ ¬ 𝑠 = 0 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
18 3 4 ifcld ⊢ ( 𝜑 → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ ¬ 𝑠 = 0 ) → if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ∈ ℝ )
20 17 19 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ ¬ 𝑠 = 0 ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) ∈ ℝ )
21 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ∈ ℝ )
22 neqne ⊢ ( ¬ 𝑠 = 0 → 𝑠 ≠ 0 )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ ¬ 𝑠 = 0 ) → 𝑠 ≠ 0 )
24 20 21 23 redivcld ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) ∧ ¬ 𝑠 = 0 ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ∈ ℝ )
25 6 24 ifclda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → if ( 𝑠 = 0 , 0 , ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − if ( 0 < 𝑠 , 𝑌 , 𝑊 ) ) / 𝑠 ) ) ∈ ℝ )
26 25 5 fmptd ⊢ ( 𝜑 → 𝐻 : ( - π [,] π ) ⟶ ℝ )