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