Proof of Theorem itgitg1
Step | Hyp | Ref
| Expression |
1 | | i1ff 24428 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
2 | 1 | ffvelrnda 6861 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℝ) |
3 | 1 | feqmptd 6737 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
4 | | i1fibl 24560 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
𝐿1) |
5 | 3, 4 | eqeltrrd 2834 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈
𝐿1) |
6 | 2, 5 | itgreval 24549 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝ(𝐹‘𝑥) d𝑥 = (∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 − ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥)) |
7 | | 0re 10721 |
. . . . . . 7
⊢ 0 ∈
ℝ |
8 | | ifcl 4459 |
. . . . . . 7
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ ℝ) |
9 | 2, 7, 8 | sylancl 589 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ ℝ) |
10 | | max1 12661 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0)) |
11 | 7, 2, 10 | sylancr 590 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
12 | | id 22 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈ dom
∫1) |
13 | 3, 12 | eqeltrrd 2834 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈ dom
∫1) |
14 | 13 | i1fposd 24460 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom
∫1) |
15 | | i1fibl 24560 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 →
(𝑥 ∈ ℝ ↦
if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈
𝐿1) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈
𝐿1) |
17 | 9, 11, 16 | itgitg2 24559 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
18 | 11 | ralrimiva 3096 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
19 | | reex 10706 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) |
21 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ∈ ℝ) |
22 | | fconstmpt 5585 |
. . . . . . . . . 10
⊢ (ℝ
× {0}) = (𝑥 ∈
ℝ ↦ 0) |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) = (𝑥 ∈ ℝ ↦ 0)) |
24 | | eqidd 2739 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
25 | 20, 21, 9, 23, 24 | ofrfval2 7445 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
26 | 18, 25 | mpbird 260 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
27 | | ax-resscn 10672 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ℝ ⊆ ℂ) |
29 | 9 | fmpttd 6889 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥),
0)):ℝ⟶ℝ) |
30 | 29 | ffnd 6505 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ) |
31 | 28, 30 | 0pledm 24425 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
32 | 26, 31 | mpbird 260 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
33 | | itg2itg1 24489 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
34 | 14, 32, 33 | syl2anc 587 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
35 | 17, 34 | eqtrd 2773 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
36 | 2 | renegcld 11145 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -(𝐹‘𝑥) ∈
ℝ) |
37 | | ifcl 4459 |
. . . . . . 7
⊢ ((-(𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ ℝ) |
38 | 36, 7, 37 | sylancl 589 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ ℝ) |
39 | | max1 12661 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
40 | 7, 36, 39 | sylancr 590 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
41 | | neg1rr 11831 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -1 ∈ ℝ) |
43 | | fconstmpt 5585 |
. . . . . . . . . . . 12
⊢ (ℝ
× {-1}) = (𝑥 ∈
ℝ ↦ -1) |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {-1}) = (𝑥 ∈ ℝ ↦ -1)) |
45 | 20, 42, 2, 44, 3 | offval2 7444 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) = (𝑥 ∈ ℝ ↦ (-1 · (𝐹‘𝑥)))) |
46 | 2 | recnd 10747 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℂ) |
47 | 46 | mulm1d 11170 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (-1 · (𝐹‘𝑥)) = -(𝐹‘𝑥)) |
48 | 47 | mpteq2dva 5125 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (-1 · (𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) |
49 | 45, 48 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) |
50 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ -1 ∈ ℝ) |
51 | 12, 50 | i1fmulc 24456 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) ∈ dom
∫1) |
52 | 49, 51 | eqeltrrd 2834 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ -(𝐹‘𝑥)) ∈ dom
∫1) |
53 | 52 | i1fposd 24460 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom
∫1) |
54 | | i1fibl 24560 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 →
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈
𝐿1) |
55 | 53, 54 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈
𝐿1) |
56 | 38, 40, 55 | itgitg2 24559 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
57 | 40 | ralrimiva 3096 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
58 | | eqidd 2739 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
59 | 20, 21, 38, 23, 58 | ofrfval2 7445 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
60 | 57, 59 | mpbird 260 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
61 | 38 | fmpttd 6889 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥),
0)):ℝ⟶ℝ) |
62 | 61 | ffnd 6505 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ) |
63 | 28, 62 | 0pledm 24425 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
64 | 60, 63 | mpbird 260 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
65 | | itg2itg1 24489 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
66 | 53, 64, 65 | syl2anc 587 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
67 | 56, 66 | eqtrd 2773 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥 = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
68 | 35, 67 | oveq12d 7188 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 − ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥) = ((∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) −
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
69 | | itg1sub 24462 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦ 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 587 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘((𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘f − (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) −
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
71 | 68, 70 | eqtr4d 2776 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ (∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 − ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥) = (∫1‘((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘f − (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
72 | | max0sub 12672 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ ℝ → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
73 | 2, 72 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
74 | 73 | mpteq2dva 5125 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
75 | 20, 9, 38, 24, 58 | offval2 7444 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ((𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘f − (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
76 | 74, 75, 3 | 3eqtr4d 2783 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ ((𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘f − (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = 𝐹) |
77 | 76 | fveq2d 6678 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘((𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘f − (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) = (∫1‘𝐹)) |
78 | 6, 71, 77 | 3eqtrd 2777 |
1
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝ(𝐹‘𝑥) d𝑥 = (∫1‘𝐹)) |