Proof of Theorem itgitg1
Step | Hyp | Ref
| Expression |
1 | | i1ff 23443 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
2 | 1 | ffvelrnda 6359 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℝ) |
3 | 1 | feqmptd 6249 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
4 | | i1fibl 23574 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
𝐿1) |
5 | 3, 4 | eqeltrrd 2702 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈
𝐿1) |
6 | 2, 5 | itgreval 23563 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝ(𝐹‘𝑥) d𝑥 = (∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 − ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥)) |
7 | | 0re 10040 |
. . . . . . 7
⊢ 0 ∈
ℝ |
8 | | ifcl 4130 |
. . . . . . 7
⊢ (((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ ℝ) |
9 | 2, 7, 8 | sylancl 694 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ ℝ) |
10 | | max1 12016 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0)) |
11 | 7, 2, 10 | sylancr 695 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
12 | | id 22 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈ dom
∫1) |
13 | 3, 12 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈ dom
∫1) |
14 | 13 | i1fposd 23474 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom
∫1) |
15 | | i1fibl 23574 |
. . . . . . 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 23573 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
18 | 11 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
19 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) |
21 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ∈ ℝ) |
22 | | fconstmpt 5163 |
. . . . . . . . . 10
⊢ (ℝ
× {0}) = (𝑥 ∈
ℝ ↦ 0) |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) = (𝑥 ∈ ℝ ↦ 0)) |
24 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
25 | 20, 21, 9, 23, 24 | ofrfval2 6915 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
26 | 18, 25 | mpbird 247 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
27 | | ax-resscn 9993 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
28 | 27 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ℝ ⊆ ℂ) |
29 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
30 | 9, 29 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥),
0)):ℝ⟶ℝ) |
31 | | ffn 6045 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)):ℝ⟶ℝ → (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ) |
33 | 28, 32 | 0pledm 23440 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
34 | 26, 33 | mpbird 247 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
35 | | itg2itg1 23503 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
36 | 14, 34, 35 | syl2anc 693 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
37 | 17, 36 | eqtrd 2656 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
38 | 2 | renegcld 10457 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -(𝐹‘𝑥) ∈
ℝ) |
39 | | ifcl 4130 |
. . . . . . 7
⊢ ((-(𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ ℝ) |
40 | 38, 7, 39 | sylancl 694 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ ℝ) |
41 | | max1 12016 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
42 | 7, 38, 41 | sylancr 695 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
43 | | neg1rr 11125 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -1 ∈ ℝ) |
45 | | fconstmpt 5163 |
. . . . . . . . . . . 12
⊢ (ℝ
× {-1}) = (𝑥 ∈
ℝ ↦ -1) |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {-1}) = (𝑥 ∈ ℝ ↦ -1)) |
47 | 20, 44, 2, 46, 3 | offval2 6914 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘𝑓 · 𝐹) = (𝑥 ∈ ℝ ↦ (-1 · (𝐹‘𝑥)))) |
48 | 2 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℂ) |
49 | 48 | mulm1d 10482 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (-1 · (𝐹‘𝑥)) = -(𝐹‘𝑥)) |
50 | 49 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (-1 · (𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) |
51 | 47, 50 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘𝑓 · 𝐹) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) |
52 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ -1 ∈ ℝ) |
53 | 12, 52 | i1fmulc 23470 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘𝑓 · 𝐹) ∈ dom
∫1) |
54 | 51, 53 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ -(𝐹‘𝑥)) ∈ dom
∫1) |
55 | 54 | i1fposd 23474 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom
∫1) |
56 | | i1fibl 23574 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 →
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈
𝐿1) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈
𝐿1) |
58 | 40, 42, 57 | itgitg2 23573 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
59 | 42 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
60 | | eqidd 2623 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
61 | 20, 21, 40, 23, 60 | ofrfval2 6915 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
62 | 59, 61 | mpbird 247 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
63 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
64 | 40, 63 | fmptd 6385 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥),
0)):ℝ⟶ℝ) |
65 | | ffn 6045 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)):ℝ⟶ℝ → (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ) |
66 | 64, 65 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ) |
67 | 28, 66 | 0pledm 23440 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
68 | 62, 67 | mpbird 247 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
69 | | itg2itg1 23503 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
70 | 55, 68, 69 | syl2anc 693 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
71 | 58, 70 | eqtrd 2656 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥 = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
72 | 37, 71 | oveq12d 6668 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 − ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥) = ((∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) −
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
73 | | itg1sub 23476 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1) →
(∫1‘((𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘𝑓 −
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) −
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
74 | 14, 55, 73 | syl2anc 693 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘((𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘𝑓 −
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) = ((∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) −
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
75 | 72, 74 | eqtr4d 2659 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ (∫ℝif(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) d𝑥 − ∫ℝif(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) d𝑥) = (∫1‘((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘𝑓 −
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))))) |
76 | | max0sub 12027 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ ℝ → (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
77 | 2, 76 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝐹‘𝑥)) |
78 | 77 | mpteq2dva 4744 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
79 | 20, 9, 40, 24, 60 | offval2 6914 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ ((𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘𝑓 −
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ (if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) − if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
80 | 78, 79, 3 | 3eqtr4d 2666 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ ((𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘𝑓 −
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = 𝐹) |
81 | 80 | fveq2d 6195 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘((𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∘𝑓 −
(𝑥 ∈ ℝ ↦
if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) = (∫1‘𝐹)) |
82 | 6, 75, 81 | 3eqtrd 2660 |
1
⊢ (𝐹 ∈ dom ∫1
→ ∫ℝ(𝐹‘𝑥) d𝑥 = (∫1‘𝐹)) |