Proof of Theorem ibladdlem
Step | Hyp | Ref
| Expression |
1 | | ifan 4518 |
. . . 4
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) |
2 | | ibladd.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶)) |
3 | | ibladd.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
4 | | ibladd.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
5 | 3, 4 | readdcld 10997 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ) |
6 | 2, 5 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ ℝ) |
7 | | 0re 10970 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
8 | | ifcl 4510 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ) |
9 | 6, 7, 8 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ) |
10 | 9 | rexrd 11018 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈
ℝ*) |
11 | | max1 12910 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐷
∈ ℝ) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)) |
12 | 7, 6, 11 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)) |
13 | | elxrge0 13180 |
. . . . . . 7
⊢ (if(0
≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞) ↔ (if(0 ≤
𝐷, 𝐷, 0) ∈ ℝ* ∧ 0 ≤
if(0 ≤ 𝐷, 𝐷, 0))) |
14 | 10, 12, 13 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞)) |
15 | | 0e0iccpnf 13182 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
16 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
17 | 14, 16 | ifclda 4500 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈
(0[,]+∞)) |
18 | 17 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈
(0[,]+∞)) |
19 | 1, 18 | eqeltrid 2845 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ∈ (0[,]+∞)) |
20 | 19 | fmpttd 6984 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷,
0)):ℝ⟶(0[,]+∞)) |
21 | | reex 10955 |
. . . . . . . 8
⊢ ℝ
∈ V |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
23 | | ifan 4518 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) |
24 | | ifcl 4510 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
25 | 3, 7, 24 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
26 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
27 | 25, 26 | ifclda 4500 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ ℝ) |
28 | 23, 27 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ) |
29 | 28 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ) |
30 | | ifan 4518 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) |
31 | | ifcl 4510 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
32 | 4, 7, 31 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
33 | 32, 26 | ifclda 4500 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ ℝ) |
34 | 30, 33 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ) |
36 | | eqidd 2741 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) |
37 | | eqidd 2741 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) |
38 | 22, 29, 35, 36, 37 | offval2 7545 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) |
39 | | iftrue 4471 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
40 | | ibar 529 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐵 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))) |
41 | 40 | ifbid 4488 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐵, 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) |
42 | | ibar 529 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐶 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))) |
43 | 42 | ifbid 4488 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐶, 𝐶, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) |
44 | 41, 43 | oveq12d 7287 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) |
45 | 39, 44 | eqtr2d 2781 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
46 | | 00id 11142 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
47 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) → 𝑥 ∈ 𝐴) |
48 | 47 | con3i 154 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) |
49 | 48 | iffalsed 4476 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0) |
50 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶) → 𝑥 ∈ 𝐴) |
51 | 50 | con3i 154 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) |
52 | 51 | iffalsed 4476 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0) |
53 | 49, 52 | oveq12d 7287 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (0 + 0)) |
54 | | iffalse 4474 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = 0) |
55 | 46, 53, 54 | 3eqtr4a 2806 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
56 | 45, 55 | pm2.61i 182 |
. . . . . . 7
⊢
(if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) |
57 | 56 | mpteq2i 5184 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
(if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
58 | 38, 57 | eqtrdi 2796 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
59 | 58 | fveq2d 6773 |
. . . 4
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) |
60 | | ibladd.4 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
61 | 60, 3 | mbfdm2 24791 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ dom vol) |
62 | | mblss 24685 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
64 | | rembl 24694 |
. . . . . . 7
⊢ ℝ
∈ dom vol |
65 | 64 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈ dom
vol) |
66 | 28 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ) |
67 | | eldifn 4067 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
68 | 67 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
69 | 68 | intnanrd 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) |
70 | 69 | iffalsed 4476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0) |
71 | 41 | mpteq2ia 5182 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) |
72 | 3, 60 | mbfpos 24805 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) |
73 | 71, 72 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn) |
74 | 63, 65, 66, 70, 73 | mbfss 24800 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn) |
75 | | max1 12910 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
76 | 7, 3, 75 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
77 | | elrege0 13177 |
. . . . . . . . . 10
⊢ (if(0
≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞) ↔ (if(0 ≤
𝐵, 𝐵, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝐵, 𝐵, 0))) |
78 | 25, 76, 77 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞)) |
79 | | 0e0icopnf 13181 |
. . . . . . . . . 10
⊢ 0 ∈
(0[,)+∞) |
80 | 79 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
81 | 78, 80 | ifclda 4500 |
. . . . . . . 8
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈
(0[,)+∞)) |
82 | 23, 81 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞)) |
83 | 82 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞)) |
84 | 83 | fmpttd 6984 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵,
0)):ℝ⟶(0[,)+∞)) |
85 | | ibladd.6 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ) |
86 | 34 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ) |
87 | 68, 52 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0) |
88 | 43 | mpteq2ia 5182 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) |
89 | | ibladd.5 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
90 | 4, 89 | mbfpos 24805 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ MblFn) |
91 | 88, 90 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn) |
92 | 63, 65, 86, 87, 91 | mbfss 24800 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn) |
93 | | max1 12910 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
94 | 7, 4, 93 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
95 | | elrege0 13177 |
. . . . . . . . . 10
⊢ (if(0
≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞) ↔ (if(0 ≤
𝐶, 𝐶, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝐶, 𝐶, 0))) |
96 | 32, 94, 95 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞)) |
97 | 96, 80 | ifclda 4500 |
. . . . . . . 8
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈
(0[,)+∞)) |
98 | 30, 97 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞)) |
99 | 98 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞)) |
100 | 99 | fmpttd 6984 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶,
0)):ℝ⟶(0[,)+∞)) |
101 | | ibladd.7 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ) |
102 | 74, 84, 85, 92, 100, 101 | itg2add 24914 |
. . . 4
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘f + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))) |
103 | 59, 102 | eqtr3d 2782 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) =
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))) |
104 | 85, 101 | readdcld 10997 |
. . 3
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) ∈ ℝ) |
105 | 103, 104 | eqeltrd 2841 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ) |
106 | 25, 32 | readdcld 10997 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ) |
107 | 106 | rexrd 11018 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈
ℝ*) |
108 | 25, 32, 76, 94 | addge0d 11543 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
109 | | elxrge0 13180 |
. . . . . . 7
⊢ ((if(0
≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ (0[,]+∞) ↔ ((if(0
≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ* ∧ 0
≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) |
110 | 107, 108,
109 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈
(0[,]+∞)) |
111 | 110, 16 | ifclda 4500 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈
(0[,]+∞)) |
112 | 111 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈
(0[,]+∞)) |
113 | 112 | fmpttd 6984 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)),
0)):ℝ⟶(0[,]+∞)) |
114 | | max2 12912 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 𝐵
≤ if(0 ≤ 𝐵, 𝐵, 0)) |
115 | 7, 3, 114 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
116 | | max2 12912 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 𝐶
≤ if(0 ≤ 𝐶, 𝐶, 0)) |
117 | 7, 4, 116 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
118 | 3, 4, 25, 32, 115, 117 | le2addd 11586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
119 | 2, 118 | eqbrtrd 5101 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
120 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (𝐷 = if(0 ≤ 𝐷, 𝐷, 0) → (𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) |
121 | | breq1 5082 |
. . . . . . . . . . 11
⊢ (0 = if(0
≤ 𝐷, 𝐷, 0) → (0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) |
122 | 120, 121 | ifboth 4504 |
. . . . . . . . . 10
⊢ ((𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∧ 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
123 | 119, 108,
122 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
124 | | iftrue 4471 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0)) |
125 | 124 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0)) |
126 | 39 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
127 | 123, 125,
126 | 3brtr4d 5111 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
128 | 127 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
129 | | 0le0 12066 |
. . . . . . . . 9
⊢ 0 ≤
0 |
130 | 129 | a1i 11 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
131 | | iffalse 4474 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = 0) |
132 | 130, 131,
54 | 3brtr4d 5111 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
133 | 128, 132 | pm2.61d1 180 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
134 | 1, 133 | eqbrtrid 5114 |
. . . . 5
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
135 | 134 | ralrimivw 3111 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
136 | | eqidd 2741 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) |
137 | | eqidd 2741 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
138 | 22, 19, 112, 136, 137 | ofrfval2 7546 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
139 | 135, 138 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
140 | | itg2le 24894 |
. . 3
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)):ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) |
141 | 20, 113, 139, 140 | syl3anc 1370 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) |
142 | | itg2lecl 24893 |
. 2
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ) |
143 | 20, 105, 141, 142 | syl3anc 1370 |
1
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ) |