Step |
Hyp |
Ref |
Expression |
1 |
|
itgperiod.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
2 |
|
itgperiod.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
3 |
|
itgperiod.aleb |
⊢ ( 𝜑 → 𝐴 ≤ 𝐵 ) |
4 |
|
itgperiod.t |
⊢ ( 𝜑 → 𝑇 ∈ ℝ+ ) |
5 |
|
itgperiod.f |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ ) |
6 |
|
itgperiod.fper |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
7 |
|
itgperiod.fcn |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) |
8 |
4
|
rpred |
⊢ ( 𝜑 → 𝑇 ∈ ℝ ) |
9 |
1 2 8 3
|
leadd1dd |
⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) |
10 |
9
|
ditgpos |
⊢ ( 𝜑 → ⨜ [ ( 𝐴 + 𝑇 ) → ( 𝐵 + 𝑇 ) ] ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 + 𝑇 ) (,) ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |
11 |
1 8
|
readdcld |
⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) ∈ ℝ ) |
12 |
2 8
|
readdcld |
⊢ ( 𝜑 → ( 𝐵 + 𝑇 ) ∈ ℝ ) |
13 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐹 : ℝ ⟶ ℂ ) |
14 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ ) |
15 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ ) |
16 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
17 |
|
eliccre |
⊢ ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℝ ) |
18 |
14 15 16 17
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℝ ) |
19 |
13 18
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) |
20 |
11 12 19
|
itgioo |
⊢ ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) (,) ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |
21 |
10 20
|
eqtr2d |
⊢ ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ⨜ [ ( 𝐴 + 𝑇 ) → ( 𝐵 + 𝑇 ) ] ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |
22 |
|
eqid |
⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 + 𝑇 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 + 𝑇 ) ) |
23 |
8
|
recnd |
⊢ ( 𝜑 → 𝑇 ∈ ℂ ) |
24 |
22
|
addccncf |
⊢ ( 𝑇 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 + 𝑇 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
25 |
23 24
|
syl |
⊢ ( 𝜑 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 + 𝑇 ) ) ∈ ( ℂ –cn→ ℂ ) ) |
26 |
1 2
|
iccssred |
⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
27 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
28 |
26 27
|
sstrdi |
⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) |
29 |
11 12
|
iccssred |
⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ⊆ ℝ ) |
30 |
29 27
|
sstrdi |
⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ⊆ ℂ ) |
31 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ ) |
32 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ ) |
33 |
26
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ℝ ) |
34 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑇 ∈ ℝ ) |
35 |
33 34
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 + 𝑇 ) ∈ ℝ ) |
36 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ ) |
37 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) |
38 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ ) |
39 |
|
elicc2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) ) |
40 |
36 38 39
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) ) |
41 |
37 40
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) |
42 |
41
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑦 ) |
43 |
36 33 34 42
|
leadd1dd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 + 𝑇 ) ≤ ( 𝑦 + 𝑇 ) ) |
44 |
41
|
simp3d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ≤ 𝐵 ) |
45 |
33 38 34 44
|
leadd1dd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) |
46 |
31 32 35 43 45
|
eliccd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
47 |
22 25 28 30 46
|
cncfmptssg |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 + 𝑇 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) |
48 |
|
eqeq1 |
⊢ ( 𝑤 = 𝑥 → ( 𝑤 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑧 + 𝑇 ) ) ) |
49 |
48
|
rexbidv |
⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) |
50 |
|
oveq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 + 𝑇 ) = ( 𝑦 + 𝑇 ) ) |
51 |
50
|
eqeq2d |
⊢ ( 𝑧 = 𝑦 → ( 𝑥 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑦 + 𝑇 ) ) ) |
52 |
51
|
cbvrexvw |
⊢ ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑦 + 𝑇 ) ) |
53 |
49 52
|
syl6bb |
⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑦 + 𝑇 ) ) ) |
54 |
53
|
cbvrabv |
⊢ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑦 + 𝑇 ) } |
55 |
5
|
ffdmd |
⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ ) |
56 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → 𝑤 = ( 𝑧 + 𝑇 ) ) |
57 |
26
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ∈ ℝ ) |
58 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑇 ∈ ℝ ) |
59 |
57 58
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ ) |
60 |
59
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ ) |
61 |
56 60
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → 𝑤 ∈ ℝ ) |
62 |
61
|
rexlimdv3a |
⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ ℝ ) ) |
63 |
62
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑤 ∈ ℂ ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ ℝ ) ) |
64 |
|
rabss |
⊢ ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ⊆ ℝ ↔ ∀ 𝑤 ∈ ℂ ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ ℝ ) ) |
65 |
63 64
|
sylibr |
⊢ ( 𝜑 → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ⊆ ℝ ) |
66 |
5
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = ℝ ) |
67 |
65 66
|
sseqtrrd |
⊢ ( 𝜑 → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ⊆ dom 𝐹 ) |
68 |
28 8 54 55 67 6 7
|
cncfperiod |
⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) ∈ ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) ) |
69 |
49
|
elrab |
⊢ ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↔ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) |
70 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) |
71 |
|
nfv |
⊢ Ⅎ 𝑧 𝜑 |
72 |
|
nfv |
⊢ Ⅎ 𝑧 𝑥 ∈ ℂ |
73 |
|
nfre1 |
⊢ Ⅎ 𝑧 ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) |
74 |
72 73
|
nfan |
⊢ Ⅎ 𝑧 ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) |
75 |
71 74
|
nfan |
⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) |
76 |
|
nfv |
⊢ Ⅎ 𝑧 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) |
77 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 = ( 𝑧 + 𝑇 ) ) |
78 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ ) |
79 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) |
80 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ ) |
81 |
|
elicc2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵 ) ) ) |
82 |
78 80 81
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵 ) ) ) |
83 |
79 82
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵 ) ) |
84 |
83
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑧 ) |
85 |
78 57 58 84
|
leadd1dd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ) |
86 |
83
|
simp3d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ≤ 𝐵 ) |
87 |
57 80 58 86
|
leadd1dd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) |
88 |
59 85 87
|
3jca |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) ) |
89 |
88
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) ) |
90 |
11
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝐴 + 𝑇 ) ∈ ℝ ) |
91 |
12
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝐵 + 𝑇 ) ∈ ℝ ) |
92 |
|
elicc2 |
⊢ ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ) → ( ( 𝑧 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) ) ) |
93 |
90 91 92
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( ( 𝑧 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( ( 𝑧 + 𝑇 ) ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ ( 𝑧 + 𝑇 ) ∧ ( 𝑧 + 𝑇 ) ≤ ( 𝐵 + 𝑇 ) ) ) ) |
94 |
89 93
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 + 𝑇 ) ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
95 |
77 94
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
96 |
95
|
3exp |
⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑥 = ( 𝑧 + 𝑇 ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) ) |
97 |
96
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑥 = ( 𝑧 + 𝑇 ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) ) |
98 |
75 76 97
|
rexlimd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → ( ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) |
99 |
70 98
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
100 |
69 99
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
101 |
18
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ ℂ ) |
102 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 ∈ ℝ ) |
103 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐵 ∈ ℝ ) |
104 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑇 ∈ ℝ ) |
105 |
18 104
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ∈ ℝ ) |
106 |
1
|
recnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
107 |
106 23
|
pncand |
⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) − 𝑇 ) = 𝐴 ) |
108 |
107
|
eqcomd |
⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 + 𝑇 ) − 𝑇 ) ) |
109 |
108
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 = ( ( 𝐴 + 𝑇 ) − 𝑇 ) ) |
110 |
|
elicc2 |
⊢ ( ( ( 𝐴 + 𝑇 ) ∈ ℝ ∧ ( 𝐵 + 𝑇 ) ∈ ℝ ) → ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐵 + 𝑇 ) ) ) ) |
111 |
14 15 110
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐵 + 𝑇 ) ) ) ) |
112 |
16 111
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝐴 + 𝑇 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐵 + 𝑇 ) ) ) |
113 |
112
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝐴 + 𝑇 ) ≤ 𝑥 ) |
114 |
14 18 104 113
|
lesub1dd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐴 + 𝑇 ) − 𝑇 ) ≤ ( 𝑥 − 𝑇 ) ) |
115 |
109 114
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝐴 ≤ ( 𝑥 − 𝑇 ) ) |
116 |
112
|
simp3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ≤ ( 𝐵 + 𝑇 ) ) |
117 |
18 15 104 116
|
lesub1dd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ≤ ( ( 𝐵 + 𝑇 ) − 𝑇 ) ) |
118 |
2
|
recnd |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
119 |
118 23
|
pncand |
⊢ ( 𝜑 → ( ( 𝐵 + 𝑇 ) − 𝑇 ) = 𝐵 ) |
120 |
119
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝐵 + 𝑇 ) − 𝑇 ) = 𝐵 ) |
121 |
117 120
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ≤ 𝐵 ) |
122 |
102 103 105 115 121
|
eliccd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) |
123 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑇 ∈ ℂ ) |
124 |
101 123
|
npcand |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ( ( 𝑥 − 𝑇 ) + 𝑇 ) = 𝑥 ) |
125 |
124
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 = ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) |
126 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑥 − 𝑇 ) → ( 𝑧 + 𝑇 ) = ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) |
127 |
126
|
rspceeqv |
⊢ ( ( ( 𝑥 − 𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 = ( ( 𝑥 − 𝑇 ) + 𝑇 ) ) → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) |
128 |
122 125 127
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑥 = ( 𝑧 + 𝑇 ) ) |
129 |
101 128 69
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) → 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) |
130 |
100 129
|
impbida |
⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ↔ 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) |
131 |
130
|
eqrdv |
⊢ ( 𝜑 → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } = ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) |
132 |
131
|
reseq2d |
⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) = ( 𝐹 ↾ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) ) |
133 |
131 67
|
eqsstrrd |
⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ⊆ dom 𝐹 ) |
134 |
55 133
|
feqresmpt |
⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ) = ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
135 |
132 134
|
eqtr2d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) ) |
136 |
1 2 8
|
iccshift |
⊢ ( 𝜑 → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } ) |
137 |
136
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) –cn→ ℂ ) = ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) ) |
138 |
68 135 137
|
3eltr4d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) –cn→ ℂ ) ) |
139 |
|
ioosscn |
⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ |
140 |
139
|
a1i |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ ) |
141 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
142 |
|
ssid |
⊢ ℂ ⊆ ℂ |
143 |
142
|
a1i |
⊢ ( 𝜑 → ℂ ⊆ ℂ ) |
144 |
140 141 143
|
constcncfg |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) |
145 |
|
fconstmpt |
⊢ ( ( 𝐴 (,) 𝐵 ) × { 1 } ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) |
146 |
|
ioombl |
⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol |
147 |
146
|
a1i |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol ) |
148 |
|
ioovolcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) |
149 |
1 2 148
|
syl2anc |
⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) |
150 |
|
iblconst |
⊢ ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ∧ 1 ∈ ℂ ) → ( ( 𝐴 (,) 𝐵 ) × { 1 } ) ∈ 𝐿1 ) |
151 |
147 149 141 150
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) × { 1 } ) ∈ 𝐿1 ) |
152 |
145 151
|
eqeltrrid |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ 𝐿1 ) |
153 |
144 152
|
elind |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ∈ ( ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ∩ 𝐿1 ) ) |
154 |
26
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 + 𝑇 ) ) ) |
155 |
154
|
eqcomd |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 + 𝑇 ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ) |
156 |
155
|
oveq2d |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 + 𝑇 ) ) ) = ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ) ) |
157 |
27
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
158 |
157
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ ) |
159 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑇 ∈ ℂ ) |
160 |
158 159
|
addcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 𝑇 ) ∈ ℂ ) |
161 |
160
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) : ℝ ⟶ ℂ ) |
162 |
|
ssid |
⊢ ℝ ⊆ ℝ |
163 |
162
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℝ ) |
164 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
165 |
164
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
166 |
164 165
|
dvres |
⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ) |
167 |
157 161 163 26 166
|
syl22anc |
⊢ ( 𝜑 → ( ℝ D ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ) |
168 |
156 167
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 + 𝑇 ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) ) |
169 |
|
iccntr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) |
170 |
1 2 169
|
syl2anc |
⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) ) |
171 |
170
|
reseq2d |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ) |
172 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
173 |
172
|
a1i |
⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } ) |
174 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ ) |
175 |
173
|
dvmptid |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) ) |
176 |
|
0cnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 0 ∈ ℂ ) |
177 |
173 23
|
dvmptc |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑇 ) ) = ( 𝑦 ∈ ℝ ↦ 0 ) ) |
178 |
173 158 174 175 159 176 177
|
dvmptadd |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 1 + 0 ) ) ) |
179 |
178
|
reseq1d |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 1 + 0 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) ) |
180 |
|
ioossre |
⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ |
181 |
180
|
a1i |
⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) |
182 |
181
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 1 + 0 ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 + 0 ) ) ) |
183 |
|
1p0e1 |
⊢ ( 1 + 0 ) = 1 |
184 |
183
|
mpteq2i |
⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 + 0 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) |
185 |
184
|
a1i |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 + 0 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ) |
186 |
179 182 185
|
3eqtrd |
⊢ ( 𝜑 → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝑦 + 𝑇 ) ) ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ) |
187 |
168 171 186
|
3eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 + 𝑇 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 1 ) ) |
188 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑦 + 𝑇 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) ) |
189 |
|
oveq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 + 𝑇 ) = ( 𝐴 + 𝑇 ) ) |
190 |
|
oveq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 + 𝑇 ) = ( 𝐵 + 𝑇 ) ) |
191 |
1 2 3 47 138 153 187 188 189 190 11 12
|
itgsubsticc |
⊢ ( 𝜑 → ⨜ [ ( 𝐴 + 𝑇 ) → ( 𝐵 + 𝑇 ) ] ( 𝐹 ‘ 𝑥 ) d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 ) |
192 |
3
|
ditgpos |
⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 ) |
193 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℂ ) |
194 |
193 35
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) ∈ ℂ ) |
195 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 1 ∈ ℂ ) |
196 |
194 195
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) ∈ ℂ ) |
197 |
1 2 196
|
itgioo |
⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 ) |
198 |
|
fvoveq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) ) |
199 |
198
|
oveq1d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) = ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) · 1 ) ) |
200 |
199
|
cbvitgv |
⊢ ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) · 1 ) d 𝑥 |
201 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℂ ) |
202 |
26
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ ) |
203 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑇 ∈ ℝ ) |
204 |
202 203
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 + 𝑇 ) ∈ ℝ ) |
205 |
201 204
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) ∈ ℂ ) |
206 |
205
|
mulid1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) · 1 ) = ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) ) |
207 |
206 6
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) · 1 ) = ( 𝐹 ‘ 𝑥 ) ) |
208 |
207
|
itgeq2dv |
⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) · 1 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |
209 |
200 208
|
syl5eq |
⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |
210 |
192 197 209
|
3eqtrd |
⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) · 1 ) d 𝑦 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |
211 |
21 191 210
|
3eqtrd |
⊢ ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 ) |