Proof of Theorem ibladdlem
Step | Hyp | Ref
| Expression |
1 | | ifan 4084 |
. . . 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 9948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ) |
6 | 2, 5 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ ℝ) |
7 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
8 | | ifcl 4080 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ) |
9 | 6, 7, 8 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ ℝ) |
10 | 9 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈
ℝ*) |
11 | | max1 11890 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝐷
∈ ℝ) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)) |
12 | 7, 6, 11 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐷, 𝐷, 0)) |
13 | | elxrge0 12152 |
. . . . . . 7
⊢ (if(0
≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞) ↔ (if(0 ≤
𝐷, 𝐷, 0) ∈ ℝ* ∧ 0 ≤
if(0 ≤ 𝐷, 𝐷, 0))) |
14 | 10, 12, 13 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ∈ (0[,]+∞)) |
15 | | 0e0iccpnf 12154 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
16 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
17 | 14, 16 | ifclda 4070 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈
(0[,]+∞)) |
18 | 17 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ∈
(0[,]+∞)) |
19 | 1, 18 | syl5eqel 2692 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ∈ (0[,]+∞)) |
20 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) |
21 | 19, 20 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷,
0)):ℝ⟶(0[,]+∞)) |
22 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
V) |
24 | | ifan 4084 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) |
25 | | ifcl 4080 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
26 | 3, 7, 25 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
27 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ ℝ) |
28 | 26, 27 | ifclda 4070 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈ ℝ) |
29 | 24, 28 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ) |
30 | 29 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ) |
31 | | ifan 4084 |
. . . . . . . . 9
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) |
32 | | ifcl 4080 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
33 | 4, 7, 32 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
34 | 33, 27 | ifclda 4070 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈ ℝ) |
35 | 31, 34 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ) |
37 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) |
38 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) |
39 | 23, 30, 36, 37, 38 | offval2 6812 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) |
40 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
41 | | ibar 524 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐵 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))) |
42 | 41 | ifbid 4058 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐵, 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) |
43 | | ibar 524 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (0 ≤ 𝐶 ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))) |
44 | 43 | ifbid 4058 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(0 ≤ 𝐶, 𝐶, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) |
45 | 42, 44 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) |
46 | 40, 45 | eqtr2d 2645 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
47 | | 00id 10090 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
48 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) → 𝑥 ∈ 𝐴) |
49 | 48 | con3i 149 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) |
50 | 49 | iffalsed 4047 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0) |
51 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶) → 𝑥 ∈ 𝐴) |
52 | 51 | con3i 149 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) |
53 | 52 | iffalsed 4047 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0) |
54 | 50, 53 | oveq12d 6567 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (0 + 0)) |
55 | | iffalse 4045 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = 0) |
56 | 47, 54, 55 | 3eqtr4a 2670 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → (if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
57 | 46, 56 | pm2.61i 175 |
. . . . . . 7
⊢
(if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) |
58 | 57 | mpteq2i 4669 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
(if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) + if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
59 | 39, 58 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
60 | 59 | fveq2d 6107 |
. . . 4
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) |
61 | | ibladd.4 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
62 | 61, 3 | mbfdm2 23211 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ dom vol) |
63 | | mblss 23106 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
64 | 62, 63 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
65 | | rembl 23115 |
. . . . . . 7
⊢ ℝ
∈ dom vol |
66 | 65 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ∈ dom
vol) |
67 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ ℝ) |
68 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℝ ∖ 𝐴) → ¬ 𝑥 ∈ 𝐴) |
69 | 68 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ 𝑥 ∈ 𝐴) |
70 | 69 | intnanrd 954 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → ¬ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵)) |
71 | 70 | iffalsed 4047 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = 0) |
72 | 42 | mpteq2ia 4668 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) |
73 | 3, 61 | mbfpos 23224 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) |
74 | 72, 73 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn) |
75 | 64, 66, 67, 71, 74 | mbfss 23219 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∈ MblFn) |
76 | | max1 11890 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
77 | 7, 3, 76 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
78 | | elrege0 12149 |
. . . . . . . . . 10
⊢ (if(0
≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞) ↔ (if(0 ≤
𝐵, 𝐵, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝐵, 𝐵, 0))) |
79 | 26, 77, 78 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ (0[,)+∞)) |
80 | | 0e0icopnf 12153 |
. . . . . . . . . 10
⊢ 0 ∈
(0[,)+∞) |
81 | 80 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
82 | 79, 81 | ifclda 4070 |
. . . . . . . 8
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐵, 𝐵, 0), 0) ∈
(0[,)+∞)) |
83 | 24, 82 | syl5eqel 2692 |
. . . . . . 7
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞)) |
84 | 83 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) ∈ (0[,)+∞)) |
85 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) |
86 | 84, 85 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵,
0)):ℝ⟶(0[,)+∞)) |
87 | | ibladd.6 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ) |
88 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ ℝ) |
89 | 69, 53 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) = 0) |
90 | 44 | mpteq2ia 4668 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) = (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) |
91 | | ibladd.5 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
92 | 4, 91 | mbfpos 23224 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ MblFn) |
93 | 90, 92 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn) |
94 | 64, 66, 88, 89, 93 | mbfss 23219 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) ∈ MblFn) |
95 | | max1 11890 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
96 | 7, 4, 95 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
97 | | elrege0 12149 |
. . . . . . . . . 10
⊢ (if(0
≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞) ↔ (if(0 ≤
𝐶, 𝐶, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝐶, 𝐶, 0))) |
98 | 33, 96, 97 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ (0[,)+∞)) |
99 | 98, 81 | ifclda 4070 |
. . . . . . . 8
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐶, 𝐶, 0), 0) ∈
(0[,)+∞)) |
100 | 31, 99 | syl5eqel 2692 |
. . . . . . 7
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞)) |
101 | 100 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0) ∈ (0[,)+∞)) |
102 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)) |
103 | 101, 102 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶,
0)):ℝ⟶(0[,)+∞)) |
104 | | ibladd.7 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ) |
105 | 75, 86, 87, 94, 103, 104 | itg2add 23332 |
. . . 4
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) = ((∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))) |
106 | 60, 105 | eqtr3d 2646 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) =
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))))) |
107 | 87, 104 | readdcld 9948 |
. . 3
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) + (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0)))) ∈ ℝ) |
108 | 106, 107 | eqeltrd 2688 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ ℝ) |
109 | 26, 33 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ) |
110 | 109 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈
ℝ*) |
111 | 26, 33, 77, 96 | addge0d 10482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
112 | | elxrge0 12152 |
. . . . . . 7
⊢ ((if(0
≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ (0[,]+∞) ↔ ((if(0
≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ* ∧ 0
≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) |
113 | 110, 111,
112 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈
(0[,]+∞)) |
114 | 113, 16 | ifclda 4070 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈
(0[,]+∞)) |
115 | 114 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) ∈
(0[,]+∞)) |
116 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
117 | 115, 116 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)),
0)):ℝ⟶(0[,]+∞)) |
118 | | max2 11892 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 𝐵
≤ if(0 ≤ 𝐵, 𝐵, 0)) |
119 | 7, 3, 118 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
120 | | max2 11892 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 𝐶
≤ if(0 ≤ 𝐶, 𝐶, 0)) |
121 | 7, 4, 120 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
122 | 3, 4, 26, 33, 119, 121 | le2addd 10525 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
123 | 2, 122 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
124 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝐷 = if(0 ≤ 𝐷, 𝐷, 0) → (𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) |
125 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (0 = if(0
≤ 𝐷, 𝐷, 0) → (0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) |
126 | 124, 125 | ifboth 4074 |
. . . . . . . . . 10
⊢ ((𝐷 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∧ 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
127 | 123, 111,
126 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐷, 𝐷, 0) ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
128 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0)) |
129 | 128 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = if(0 ≤ 𝐷, 𝐷, 0)) |
130 | 40 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) |
131 | 127, 129,
130 | 3brtr4d 4615 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
132 | 131 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
133 | | 0le0 10987 |
. . . . . . . . 9
⊢ 0 ≤
0 |
134 | 133 | a1i 11 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
135 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) = 0) |
136 | 134, 135,
55 | 3brtr4d 4615 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
137 | 132, 136 | pm2.61d1 170 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, if(0 ≤ 𝐷, 𝐷, 0), 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
138 | 1, 137 | syl5eqbr 4618 |
. . . . 5
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
139 | 138 | ralrimivw 2950 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) |
140 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) |
141 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
142 | 23, 19, 115, 140, 141 | ofrfval2 6813 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0) ≤ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
143 | 139, 142 | mpbird 246 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) |
144 | | itg2le 23312 |
. . 3
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)):ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) |
145 | 21, 117, 143, 144 | syl3anc 1318 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ≤ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0)))) |
146 | | itg2lecl 23311 |
. 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))) ∈ ℝ) |
147 | 21, 108, 145, 146 | syl3anc 1318 |
1
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ) |