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 ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ) )