| Step |
Hyp |
Ref |
Expression |
| 1 |
|
i1ff |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ ) |
| 2 |
1
|
ffvelrnda |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
| 3 |
1
|
feqmptd |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
| 4 |
|
i1fibl |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1 ) |
| 5 |
3 4
|
eqeltrrd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ) |
| 6 |
2 5
|
itgreval |
⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 − ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 ) ) |
| 7 |
|
0re |
⊢ 0 ∈ ℝ |
| 8 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ ) |
| 9 |
2 7 8
|
sylancl |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ ) |
| 10 |
|
max1 |
⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 11 |
7 2 10
|
sylancr |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 12 |
|
id |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ dom ∫1 ) |
| 13 |
3 12
|
eqeltrrd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ dom ∫1 ) |
| 14 |
13
|
i1fposd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ) |
| 15 |
|
i1fibl |
⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 ) |
| 16 |
14 15
|
syl |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 ) |
| 17 |
9 11 16
|
itgitg2 |
⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 18 |
11
|
ralrimiva |
⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 19 |
|
reex |
⊢ ℝ ∈ V |
| 20 |
19
|
a1i |
⊢ ( 𝐹 ∈ dom ∫1 → ℝ ∈ V ) |
| 21 |
7
|
a1i |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ ) |
| 22 |
|
fconstmpt |
⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) |
| 23 |
22
|
a1i |
⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) ) |
| 24 |
|
eqidd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 25 |
20 21 9 23 24
|
ofrfval2 |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 26 |
18 25
|
mpbird |
⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 27 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
| 28 |
27
|
a1i |
⊢ ( 𝐹 ∈ dom ∫1 → ℝ ⊆ ℂ ) |
| 29 |
9
|
fmpttd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ℝ ) |
| 30 |
29
|
ffnd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ ) |
| 31 |
28 30
|
0pledm |
⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 32 |
26 31
|
mpbird |
⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 33 |
|
itg2itg1 |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 34 |
14 32 33
|
syl2anc |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 35 |
17 34
|
eqtrd |
⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 36 |
2
|
renegcld |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → - ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
| 37 |
|
ifcl |
⊢ ( ( - ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ ) |
| 38 |
36 7 37
|
sylancl |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ ) |
| 39 |
|
max1 |
⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 40 |
7 36 39
|
sylancr |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 41 |
|
neg1rr |
⊢ - 1 ∈ ℝ |
| 42 |
41
|
a1i |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → - 1 ∈ ℝ ) |
| 43 |
|
fconstmpt |
⊢ ( ℝ × { - 1 } ) = ( 𝑥 ∈ ℝ ↦ - 1 ) |
| 44 |
43
|
a1i |
⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { - 1 } ) = ( 𝑥 ∈ ℝ ↦ - 1 ) ) |
| 45 |
20 42 2 44 3
|
offval2 |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ ( - 1 · ( 𝐹 ‘ 𝑥 ) ) ) ) |
| 46 |
2
|
recnd |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) |
| 47 |
46
|
mulm1d |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( - 1 · ( 𝐹 ‘ 𝑥 ) ) = - ( 𝐹 ‘ 𝑥 ) ) |
| 48 |
47
|
mpteq2dva |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( - 1 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) ) |
| 49 |
45 48
|
eqtrd |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) ) |
| 50 |
41
|
a1i |
⊢ ( 𝐹 ∈ dom ∫1 → - 1 ∈ ℝ ) |
| 51 |
12 50
|
i1fmulc |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) ∈ dom ∫1 ) |
| 52 |
49 51
|
eqeltrrd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) ∈ dom ∫1 ) |
| 53 |
52
|
i1fposd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ) |
| 54 |
|
i1fibl |
⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 ) |
| 55 |
53 54
|
syl |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 ) |
| 56 |
38 40 55
|
itgitg2 |
⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 57 |
40
|
ralrimiva |
⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
| 58 |
|
eqidd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 59 |
20 21 38 23 58
|
ofrfval2 |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 60 |
57 59
|
mpbird |
⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 61 |
38
|
fmpttd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ℝ ) |
| 62 |
61
|
ffnd |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ ) |
| 63 |
28 62
|
0pledm |
⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 64 |
60 63
|
mpbird |
⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
| 65 |
|
itg2itg1 |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 66 |
53 64 65
|
syl2anc |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 67 |
56 66
|
eqtrd |
⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 68 |
35 67
|
oveq12d |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 − ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) − ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 69 |
|
itg1sub |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ) → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) − ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 70 |
14 53 69
|
syl2anc |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) − ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 71 |
68 70
|
eqtr4d |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 − ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 ) = ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
| 72 |
|
max0sub |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
| 73 |
2 72
|
syl |
⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) ) |
| 74 |
73
|
mpteq2dva |
⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
| 75 |
20 9 38 24 58
|
offval2 |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
| 76 |
74 75 3
|
3eqtr4d |
⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = 𝐹 ) |
| 77 |
76
|
fveq2d |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( ∫1 ‘ 𝐹 ) ) |
| 78 |
6 71 77
|
3eqtrd |
⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫1 ‘ 𝐹 ) ) |