Step | Hyp | Ref
| Expression |
1 | | i1ff 24783 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
2 | 1 | feqmptd 6824 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) |
3 | | i1fmbf 24782 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) |
4 | 2, 3 | eqeltrrd 2838 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈
MblFn) |
5 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 𝑥 ∈
ℝ) |
6 | 5 | biantrurd 532 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 ≤ (𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))) |
7 | 6 | ifbid 4484 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) = if((𝑥 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)), (𝐹‘𝑥), 0)) |
8 | 7 | mpteq2dva 5175 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
(𝐹‘𝑥)), (𝐹‘𝑥), 0))) |
9 | 8 | fveq2d 6765 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ ℝ ∧
0 ≤ (𝐹‘𝑥)), (𝐹‘𝑥), 0)))) |
10 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
11 | 10 | i1fpos 24814 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom
∫1) |
12 | | 0re 10924 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
13 | 1 | ffvelrnda 6948 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℝ) |
14 | | max1 12864 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0)) |
15 | 12, 13, 14 | sylancr 586 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
16 | 15 | ralrimiva 3106 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) |
17 | | reex 10909 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) |
19 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ∈ ℝ) |
20 | | fvex 6774 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
21 | | c0ex 10916 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
22 | 20, 21 | ifex 4511 |
. . . . . . . . . 10
⊢ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V) |
24 | | fconstmpt 5645 |
. . . . . . . . . 10
⊢ (ℝ
× {0}) = (𝑥 ∈
ℝ ↦ 0) |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) = (𝑥 ∈ ℝ ↦ 0)) |
26 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
27 | 18, 19, 23, 25, 26 | ofrfval2 7537 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
28 | 16, 27 | mpbird 256 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
29 | | ax-resscn 10875 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ℝ ⊆ ℂ) |
31 | 22, 10 | fnmpti 6565 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ) |
33 | 30, 32 | 0pledm 24780 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
34 | 28, 33 | mpbird 256 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) |
35 | | itg2itg1 24844 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
36 | 11, 34, 35 | syl2anc 583 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
37 | 9, 36 | eqtr3d 2779 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
(𝐹‘𝑥)), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) |
38 | | itg1cl 24792 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) ∈ ℝ) |
39 | 11, 38 | syl 17 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) ∈ ℝ) |
40 | 37, 39 | eqeltrd 2837 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
(𝐹‘𝑥)), (𝐹‘𝑥), 0))) ∈ ℝ) |
41 | 5 | biantrurd 532 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 ≤ -(𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ -(𝐹‘𝑥)))) |
42 | 41 | ifbid 4484 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) = if((𝑥 ∈ ℝ ∧ 0 ≤ -(𝐹‘𝑥)), -(𝐹‘𝑥), 0)) |
43 | 42 | mpteq2dva 5175 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
-(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) |
44 | 43 | fveq2d 6765 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ ℝ ∧
0 ≤ -(𝐹‘𝑥)), -(𝐹‘𝑥), 0)))) |
45 | | neg1rr 12034 |
. . . . . . . . . . 11
⊢ -1 ∈
ℝ |
46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -1 ∈ ℝ) |
47 | | fconstmpt 5645 |
. . . . . . . . . . 11
⊢ (ℝ
× {-1}) = (𝑥 ∈
ℝ ↦ -1) |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {-1}) = (𝑥 ∈ ℝ ↦ -1)) |
49 | 18, 46, 13, 48, 2 | offval2 7536 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) = (𝑥 ∈ ℝ ↦ (-1 · (𝐹‘𝑥)))) |
50 | 13 | recnd 10950 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℂ) |
51 | 50 | mulm1d 11373 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (-1 · (𝐹‘𝑥)) = -(𝐹‘𝑥)) |
52 | 51 | mpteq2dva 5175 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (-1 · (𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) |
53 | 49, 52 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) |
54 | | id 22 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈ dom
∫1) |
55 | 45 | a1i 11 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ -1 ∈ ℝ) |
56 | 54, 55 | i1fmulc 24811 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) ∈ dom
∫1) |
57 | 53, 56 | eqeltrrd 2838 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ -(𝐹‘𝑥)) ∈ dom
∫1) |
58 | 57 | i1fposd 24815 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom
∫1) |
59 | 13 | renegcld 11348 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -(𝐹‘𝑥) ∈
ℝ) |
60 | | max1 12864 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
61 | 12, 59, 60 | sylancr 586 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
62 | 61 | ralrimiva 3106 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
63 | | negex 11165 |
. . . . . . . . . . 11
⊢ -(𝐹‘𝑥) ∈ V |
64 | 63, 21 | ifex 4511 |
. . . . . . . . . 10
⊢ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V |
65 | 64 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V) |
66 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
67 | 18, 19, 65, 25, 66 | ofrfval2 7537 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
68 | 62, 67 | mpbird 256 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
69 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) |
70 | 64, 69 | fnmpti 6565 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ |
71 | 70 | a1i 11 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ) |
72 | 30, 71 | 0pledm 24780 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
73 | 68, 72 | mpbird 256 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) |
74 | | itg2itg1 24844 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
75 | 58, 73, 74 | syl2anc 583 |
. . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
76 | 44, 75 | eqtr3d 2779 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
-(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) |
77 | | itg1cl 24792 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 →
(∫1‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∈ ℝ) |
78 | 58, 77 | syl 17 |
. . . 4
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) ∈ ℝ) |
79 | 76, 78 | eqeltrd 2837 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
-(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) ∈ ℝ) |
80 | 13 | iblrelem 24898 |
. . 3
⊢ (𝐹 ∈ dom ∫1
→ ((𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈ 𝐿1
↔ ((𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)), (𝐹‘𝑥), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤ -(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) ∈ ℝ))) |
81 | 4, 40, 79, 80 | mpbir3and 1340 |
. 2
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈
𝐿1) |
82 | 2, 81 | eqeltrd 2837 |
1
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
𝐿1) |