| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | i1ff 25712 | . . 3
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) | 
| 2 | 1 | feqmptd 6976 | . 2
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) | 
| 3 |  | i1fmbf 25711 | . . . 4
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) | 
| 4 | 2, 3 | eqeltrrd 2841 | . . 3
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈
MblFn) | 
| 5 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 𝑥 ∈
ℝ) | 
| 6 | 5 | biantrurd 532 | . . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 ≤ (𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))) | 
| 7 | 6 | ifbid 4548 | . . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) = if((𝑥 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)), (𝐹‘𝑥), 0)) | 
| 8 | 7 | mpteq2dva 5241 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
(𝐹‘𝑥)), (𝐹‘𝑥), 0))) | 
| 9 | 8 | fveq2d 6909 | . . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ ℝ ∧
0 ≤ (𝐹‘𝑥)), (𝐹‘𝑥), 0)))) | 
| 10 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) | 
| 11 | 10 | i1fpos 25742 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom
∫1) | 
| 12 |  | 0re 11264 | . . . . . . . . . 10
⊢ 0 ∈
ℝ | 
| 13 | 1 | ffvelcdmda 7103 | . . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℝ) | 
| 14 |  | max1 13228 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0)) | 
| 15 | 12, 13, 14 | sylancr 587 | . . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) | 
| 16 | 15 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) | 
| 17 |  | reex 11247 | . . . . . . . . . 10
⊢ ℝ
∈ V | 
| 18 | 17 | a1i 11 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ℝ ∈ V) | 
| 19 | 12 | a1i 11 | . . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ∈ ℝ) | 
| 20 |  | fvex 6918 | . . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V | 
| 21 |  | c0ex 11256 | . . . . . . . . . . 11
⊢ 0 ∈
V | 
| 22 | 20, 21 | ifex 4575 | . . . . . . . . . 10
⊢ if(0 ≤
(𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V | 
| 23 | 22 | a1i 11 | . . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0) ∈ V) | 
| 24 |  | fconstmpt 5746 | . . . . . . . . . 10
⊢ (ℝ
× {0}) = (𝑥 ∈
ℝ ↦ 0) | 
| 25 | 24 | a1i 11 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) = (𝑥 ∈ ℝ ↦ 0)) | 
| 26 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) | 
| 27 | 18, 19, 23, 25, 26 | ofrfval2 7719 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) | 
| 28 | 16, 27 | mpbird 257 | . . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) | 
| 29 |  | ax-resscn 11213 | . . . . . . . . 9
⊢ ℝ
⊆ ℂ | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ℝ ⊆ ℂ) | 
| 31 | 22, 10 | fnmpti 6710 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ | 
| 32 | 31 | a1i 11 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) Fn ℝ) | 
| 33 | 30, 32 | 0pledm 25709 | . . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) | 
| 34 | 28, 33 | mpbird 257 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) | 
| 35 |  | itg2itg1 25772 | . . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) | 
| 36 | 11, 34, 35 | syl2anc 584 | . . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) | 
| 37 | 9, 36 | eqtr3d 2778 | . . . 4
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
(𝐹‘𝑥)), (𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ (𝐹‘𝑥), (𝐹‘𝑥), 0)))) | 
| 38 |  | itg1cl 25721 | . . . . 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 2840 | . . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
(𝐹‘𝑥)), (𝐹‘𝑥), 0))) ∈ ℝ) | 
| 41 | 5 | biantrurd 532 | . . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 ≤ -(𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ -(𝐹‘𝑥)))) | 
| 42 | 41 | ifbid 4548 | . . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) = if((𝑥 ∈ ℝ ∧ 0 ≤ -(𝐹‘𝑥)), -(𝐹‘𝑥), 0)) | 
| 43 | 42 | mpteq2dva 5241 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
-(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) | 
| 44 | 43 | fveq2d 6909 | . . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ ℝ ∧
0 ≤ -(𝐹‘𝑥)), -(𝐹‘𝑥), 0)))) | 
| 45 |  | neg1rr 12382 | . . . . . . . . . . 11
⊢ -1 ∈
ℝ | 
| 46 | 45 | a1i 11 | . . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -1 ∈ ℝ) | 
| 47 |  | fconstmpt 5746 | . . . . . . . . . . 11
⊢ (ℝ
× {-1}) = (𝑥 ∈
ℝ ↦ -1) | 
| 48 | 47 | a1i 11 | . . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {-1}) = (𝑥 ∈ ℝ ↦ -1)) | 
| 49 | 18, 46, 13, 48, 2 | offval2 7718 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) = (𝑥 ∈ ℝ ↦ (-1 · (𝐹‘𝑥)))) | 
| 50 | 13 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝐹‘𝑥) ∈
ℂ) | 
| 51 | 50 | mulm1d 11716 | . . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (-1 · (𝐹‘𝑥)) = -(𝐹‘𝑥)) | 
| 52 | 51 | mpteq2dva 5241 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (-1 · (𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -(𝐹‘𝑥))) | 
| 53 | 49, 52 | eqtrd 2776 | . . . . . . . 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 25739 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {-1}) ∘f · 𝐹) ∈ dom
∫1) | 
| 57 | 53, 56 | eqeltrrd 2841 | . . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ -(𝐹‘𝑥)) ∈ dom
∫1) | 
| 58 | 57 | i1fposd 25743 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom
∫1) | 
| 59 | 13 | renegcld 11691 | . . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -(𝐹‘𝑥) ∈
ℝ) | 
| 60 |  | max1 13228 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ -(𝐹‘𝑥) ∈ ℝ) → 0 ≤ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0)) | 
| 61 | 12, 59, 60 | sylancr 587 | . . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) | 
| 62 | 61 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ∀𝑥 ∈
ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) | 
| 63 |  | negex 11507 | . . . . . . . . . . 11
⊢ -(𝐹‘𝑥) ∈ V | 
| 64 | 63, 21 | ifex 4575 | . . . . . . . . . 10
⊢ if(0 ≤
-(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V | 
| 65 | 64 | a1i 11 | . . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0) ∈ V) | 
| 66 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) | 
| 67 | 18, 19, 65, 25, 66 | ofrfval2 7719 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) | 
| 68 | 62, 67 | mpbird 257 | . . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (ℝ × {0}) ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) | 
| 69 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) | 
| 70 | 64, 69 | fnmpti 6710 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ | 
| 71 | 70 | a1i 11 | . . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) Fn ℝ) | 
| 72 | 30, 71 | 0pledm 25709 | . . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) | 
| 73 | 68, 72 | mpbird 257 | . . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) | 
| 74 |  | itg2itg1 25772 | . . . . . 6
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) | 
| 75 | 58, 73, 74 | syl2anc 584 | . . . . 5
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if(0 ≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) | 
| 76 | 44, 75 | eqtr3d 2778 | . . . 4
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
-(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) = (∫1‘(𝑥 ∈ ℝ ↦ if(0
≤ -(𝐹‘𝑥), -(𝐹‘𝑥), 0)))) | 
| 77 |  | itg1cl 25721 | . . . . 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 2840 | . . 3
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤
-(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) ∈ ℝ) | 
| 80 | 13 | iblrelem 25827 | . . 3
⊢ (𝐹 ∈ dom ∫1
→ ((𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈ 𝐿1
↔ ((𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)), (𝐹‘𝑥), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ ℝ ∧ 0 ≤ -(𝐹‘𝑥)), -(𝐹‘𝑥), 0))) ∈ ℝ))) | 
| 81 | 4, 40, 79, 80 | mpbir3and 1342 | . 2
⊢ (𝐹 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (𝐹‘𝑥)) ∈
𝐿1) | 
| 82 | 2, 81 | eqeltrd 2840 | 1
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
𝐿1) |