Metamath Proof Explorer

Theorem fourierdlem28

Description: Derivative of ( F( X + s ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem28.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem28.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem28.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem28.3b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem28.d ⊢ 𝐷 = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
fourierdlem28.df ⊢ ( 𝜑 → 𝐷 : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
Assertion fourierdlem28 ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem28.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem28.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem28.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 fourierdlem28.3b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 fourierdlem28.d ⊢ 𝐷 = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
6 fourierdlem28.df ⊢ ( 𝜑 → 𝐷 : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
7 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
8 7 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
9 2 3 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ )
10 9 rexrd ⊢ ( 𝜑 → ( 𝑋 + 𝐴 ) ∈ ℝ* )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) ∈ ℝ* )
12 2 4 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ )
13 12 rexrd ⊢ ( 𝜑 → ( 𝑋 + 𝐵 ) ∈ ℝ* )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐵 ) ∈ ℝ* )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℝ )
16 elioore ⊢ ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) → 𝑠 ∈ ℝ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℝ )
18 15 17 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
19 3 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
20 19 rexrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
21 4 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
24 ioogtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
25 20 22 23 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑠 )
26 19 17 15 25 ltadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝐴 ) < ( 𝑋 + 𝑠 ) )
27 4 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
28 iooltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
29 20 22 23 28 syl3anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 < 𝐵 )
30 17 27 15 29 ltadd2dd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + 𝐵 ) )
31 11 14 18 26 30 eliood ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) )
32 1red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
33 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → 𝐹 : ℝ ⟶ ℝ )
34 elioore ⊢ ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) → 𝑦 ∈ ℝ )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → 𝑦 ∈ ℝ )
36 33 35 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
37 36 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
38 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( 𝐷 ‘ 𝑦 ) ∈ ℝ )
39 15 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℂ )
40 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
41 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
42 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
43 42 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
44 41 43 eleqtri ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
45 44 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
46 2 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
47 8 45 46 dvmptconst ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑋 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
48 17 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
49 8 45 dvmptidg ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
50 8 39 40 47 48 32 49 dvmptadd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 0 + 1 ) ) )
51 0p1e1 ⊢ ( 0 + 1 ) = 1
52 51 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 + 1 ) = 1 )
53 52 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 0 + 1 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
54 50 53 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
55 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
56 55 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
57 ioossre ⊢ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ
58 57 a1i ⊢ ( 𝜑 → ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ )
59 58 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
60 56 59 eqtr2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
61 60 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) )
62 5 eqcomi ⊢ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = 𝐷
63 62 a1i ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = 𝐷 )
64 6 feqmptd ⊢ ( 𝜑 → 𝐷 = ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐷 ‘ 𝑦 ) ) )
65 61 63 64 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐷 ‘ 𝑦 ) ) )
66 fveq2 ⊢ ( 𝑦 = ( 𝑋 + 𝑠 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
67 fveq2 ⊢ ( 𝑦 = ( 𝑋 + 𝑠 ) → ( 𝐷 ‘ 𝑦 ) = ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) )
68 8 8 31 32 37 38 54 65 66 67 dvmptco ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) · 1 ) ) )
69 6 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
70 69 31 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
71 70 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
72 71 mulid1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) · 1 ) = ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) )
73 72 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) · 1 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ) )
74 68 73 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ) )