Proof of Theorem itgreval
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iblrelem.1 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) | 
| 2 |  | itgreval.2 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) | 
| 3 | 1, 2 | itgrevallem1 25830 | . 2
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))) | 
| 4 |  | 0re 11263 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 5 |  | ifcl 4571 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) | 
| 6 | 1, 4, 5 | sylancl 586 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) | 
| 7 | 1 | iblrelem 25826 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ))) | 
| 8 | 2, 7 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ)) | 
| 9 | 8 | simp1d 1143 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 10 | 1, 9 | mbfpos 25686 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) | 
| 11 |  | ifan 4579 | . . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) | 
| 12 | 11 | mpteq2i 5247 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)) | 
| 13 | 12 | fveq2i 6909 | . . . . . . 7
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0))) | 
| 14 | 8 | simp2d 1144 | . . . . . . 7
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ) | 
| 15 | 13, 14 | eqeltrrid 2846 | . . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0))) ∈ ℝ) | 
| 16 |  | max1 13227 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) | 
| 17 | 4, 1, 16 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) | 
| 18 | 6, 17 | iblpos 25828 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0))) ∈
ℝ))) | 
| 19 | 10, 15, 18 | mpbir2and 713 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈
𝐿1) | 
| 20 | 6, 19, 17 | itgposval 25831 | . . . 4
⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)))) | 
| 21 | 20, 13 | eqtr4di 2795 | . . 3
⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)))) | 
| 22 | 1 | renegcld 11690 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) | 
| 23 |  | ifcl 4571 | . . . . . 6
⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) | 
| 24 | 22, 4, 23 | sylancl 586 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) | 
| 25 | 1, 9 | mbfneg 25685 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn) | 
| 26 | 22, 25 | mbfpos 25686 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) | 
| 27 |  | ifan 4579 | . . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0) | 
| 28 | 27 | mpteq2i 5247 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0)) | 
| 29 | 28 | fveq2i 6909 | . . . . . . 7
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))) | 
| 30 | 8 | simp3d 1145 | . . . . . . 7
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ) | 
| 31 | 29, 30 | eqeltrrid 2846 | . . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))) ∈ ℝ) | 
| 32 |  | max1 13227 | . . . . . . . 8
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0)) | 
| 33 | 4, 22, 32 | sylancr 587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0)) | 
| 34 | 24, 33 | iblpos 25828 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))) ∈
ℝ))) | 
| 35 | 26, 31, 34 | mpbir2and 713 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈
𝐿1) | 
| 36 | 24, 35, 33 | itgposval 25831 | . . . 4
⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0)))) | 
| 37 | 36, 29 | eqtr4di 2795 | . . 3
⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))) | 
| 38 | 21, 37 | oveq12d 7449 | . 2
⊢ (𝜑 → (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥) = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))) | 
| 39 | 3, 38 | eqtr4d 2780 | 1
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥)) |