Proof of Theorem itgreval
Step | Hyp | Ref
| Expression |
1 | | iblrelem.1 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
2 | | itgreval.2 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
3 | 1, 2 | itgrevallem1 24959 |
. 2
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))) |
4 | | 0re 10977 |
. . . . . 6
⊢ 0 ∈
ℝ |
5 | | ifcl 4504 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
6 | 1, 4, 5 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
7 | 1 | iblrelem 24955 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ))) |
8 | 2, 7 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ)) |
9 | 8 | simp1d 1141 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
10 | 1, 9 | mbfpos 24815 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) |
11 | | ifan 4512 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) |
12 | 11 | mpteq2i 5179 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)) |
13 | 12 | fveq2i 6777 |
. . . . . . 7
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0))) |
14 | 8 | simp2d 1142 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ) |
15 | 13, 14 | eqeltrrid 2844 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0))) ∈ ℝ) |
16 | | max1 12919 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
17 | 4, 1, 16 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
18 | 6, 17 | iblpos 24957 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0))) ∈
ℝ))) |
19 | 10, 15, 18 | mpbir2and 710 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈
𝐿1) |
20 | 6, 19, 17 | itgposval 24960 |
. . . 4
⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0)))) |
21 | 20, 13 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)))) |
22 | 1 | renegcld 11402 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
23 | | ifcl 4504 |
. . . . . 6
⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
24 | 22, 4, 23 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
25 | 1, 9 | mbfneg 24814 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn) |
26 | 22, 25 | mbfpos 24815 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) |
27 | | ifan 4512 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0) |
28 | 27 | mpteq2i 5179 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0)) |
29 | 28 | fveq2i 6777 |
. . . . . . 7
⊢
(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))) |
30 | 8 | simp3d 1143 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ) |
31 | 29, 30 | eqeltrrid 2844 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))) ∈ ℝ) |
32 | | max1 12919 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0)) |
33 | 4, 22, 32 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0)) |
34 | 24, 33 | iblpos 24957 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0))) ∈
ℝ))) |
35 | 26, 31, 34 | mpbir2and 710 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈
𝐿1) |
36 | 24, 35, 33 | itgposval 24960 |
. . . 4
⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ -𝐵, -𝐵, 0), 0)))) |
37 | 36, 29 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))) |
38 | 21, 37 | oveq12d 7293 |
. 2
⊢ (𝜑 → (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥) = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) −
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))))) |
39 | 3, 38 | eqtr4d 2781 |
1
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥)) |