This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
37 36 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
38 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) → ( 𝐷 ‘ 𝑦 ) ∈ ℝ )
39 15 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ ℂ )
40 0red ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 0 ∈ ℝ )
41 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
42 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
43 41 42 eleqtri ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
44 43 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
45 2 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
46 8 44 45 dvmptconst ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑋 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
47 17 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑠 ∈ ℂ )
48 8 44 dvmptidg ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝑠 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
49 8 39 40 46 47 32 48 dvmptadd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 0 + 1 ) ) )
50 0p1e1 ⊢ ( 0 + 1 ) = 1
51 50 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 0 + 1 ) = 1 )
52 51 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 0 + 1 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
53 49 52 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) )
54 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
55 54 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
56 ioossre ⊢ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ
57 56 a1i ⊢ ( 𝜑 → ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⊆ ℝ )
58 57 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) = ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
59 55 58 eqtr2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) )
60 59 oveq2d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) )
61 5 eqcomi ⊢ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = 𝐷
62 61 a1i ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ) ) = 𝐷 )
63 6 feqmptd ⊢ ( 𝜑 → 𝐷 = ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐷 ‘ 𝑦 ) ) )
64 60 62 63 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ↦ ( 𝐷 ‘ 𝑦 ) ) )
65 fveq2 ⊢ ( 𝑦 = ( 𝑋 + 𝑠 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
66 fveq2 ⊢ ( 𝑦 = ( 𝑋 + 𝑠 ) → ( 𝐷 ‘ 𝑦 ) = ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) )
67 8 8 31 32 37 38 53 64 65 66 dvmptco ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) · 1 ) ) )
68 6 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 : ( ( 𝑋 + 𝐴 ) (,) ( 𝑋 + 𝐵 ) ) ⟶ ℝ )
69 68 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
70 69 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
71 70 mulridd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) · 1 ) = ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) )
72 71 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) · 1 ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ) )
73 67 72 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ) = ( 𝑠 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐷 ‘ ( 𝑋 + 𝑠 ) ) ) )