Step |
Hyp |
Ref |
Expression |
1 |
|
itg2cn.1 |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ) |
2 |
|
itg2cn.2 |
⊢ ( 𝜑 → 𝐹 ∈ MblFn ) |
3 |
|
itg2cn.3 |
⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ ) |
4 |
|
itg2cn.4 |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
5 |
|
itg2cn.5 |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
6 |
|
itg2cn.6 |
⊢ ( 𝜑 → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) |
7 |
4
|
rphalfcld |
⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ+ ) |
8 |
5
|
nnrpd |
⊢ ( 𝜑 → 𝑀 ∈ ℝ+ ) |
9 |
7 8
|
rpdivcld |
⊢ ( 𝜑 → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ+ ) |
10 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 ∈ dom vol ) |
11 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 ∈ MblFn ) |
12 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
13 |
|
fss |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ ) |
14 |
1 12 13
|
sylancl |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
15 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ℝ ) |
16 |
|
mbfima |
⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) |
17 |
11 15 16
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) |
18 |
|
inmbl |
⊢ ( ( 𝑢 ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) → ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
19 |
10 17 18
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
20 |
|
difmbl |
⊢ ( ( 𝑢 ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
21 |
10 17 20
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
22 |
|
inass |
⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ( 𝑢 ∩ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) |
23 |
|
disjdif |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅ |
24 |
23
|
ineq2i |
⊢ ( 𝑢 ∩ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( 𝑢 ∩ ∅ ) |
25 |
|
in0 |
⊢ ( 𝑢 ∩ ∅ ) = ∅ |
26 |
22 24 25
|
3eqtri |
⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅ |
27 |
26
|
fveq2i |
⊢ ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( vol* ‘ ∅ ) |
28 |
|
ovol0 |
⊢ ( vol* ‘ ∅ ) = 0 |
29 |
27 28
|
eqtri |
⊢ ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 |
30 |
29
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 ) |
31 |
|
inundif |
⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = 𝑢 |
32 |
31
|
eqcomi |
⊢ 𝑢 = ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
33 |
32
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 = ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) |
34 |
|
mblss |
⊢ ( 𝑢 ∈ dom vol → 𝑢 ⊆ ℝ ) |
35 |
10 34
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 ⊆ ℝ ) |
36 |
35
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → 𝑥 ∈ ℝ ) |
37 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ) |
38 |
37
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
39 |
|
elrege0 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
40 |
38 39
|
sylib |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
41 |
40
|
simpld |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
42 |
41
|
rexrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) |
43 |
40
|
simprd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) ) |
44 |
|
elxrge0 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
45 |
42 43 44
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
46 |
36 45
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) |
47 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
48 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
49 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
50 |
|
0e0iccpnf |
⊢ 0 ∈ ( 0 [,] +∞ ) |
51 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
52 |
45 50 51
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
53 |
52
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
54 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ ) |
55 |
|
icossicc |
⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) |
56 |
|
fss |
⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ) |
57 |
37 55 56
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ) |
58 |
41
|
leidd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
59 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
60 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
61 |
59 60
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
62 |
58 43 61
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
63 |
62
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
64 |
|
reex |
⊢ ℝ ∈ V |
65 |
64
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ℝ ∈ V ) |
66 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
67 |
37
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) |
68 |
65 52 41 66 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
69 |
63 68
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
70 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
71 |
53 57 69 70
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
72 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
73 |
53 54 71 72
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
74 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
75 |
45 50 74
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
76 |
75
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
77 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
78 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
79 |
77 78
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
80 |
58 43 79
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
81 |
80
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
82 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
83 |
65 75 41 82 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
84 |
81 83
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
85 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
86 |
76 57 84 85
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
87 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
88 |
76 54 86 87
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
89 |
19 21 30 33 46 47 48 49 73 88
|
itg2split |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
90 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐶 ∈ ℝ+ ) |
91 |
90
|
rphalfcld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝐶 / 2 ) ∈ ℝ+ ) |
92 |
91
|
rpred |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝐶 / 2 ) ∈ ℝ ) |
93 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
94 |
45 50 93
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
95 |
94
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
96 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
97 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
98 |
96 97
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
99 |
58 43 98
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
100 |
99
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
101 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
102 |
65 94 45 101 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
103 |
100 102
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
104 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
105 |
95 57 103 104
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
106 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
107 |
95 54 105 106
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
108 |
|
0red |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ ) |
109 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) |
110 |
109
|
a1i |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
111 |
|
ifle |
⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
112 |
41 108 43 110 111
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
113 |
112
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
114 |
65 52 94 66 101
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
115 |
113 114
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
116 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
117 |
53 95 115 116
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
118 |
67
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) ) |
119 |
|
cmmbl |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
120 |
17 119
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol ) |
121 |
|
disjdif |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅ |
122 |
121
|
fveq2i |
⊢ ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( vol* ‘ ∅ ) |
123 |
122 28
|
eqtri |
⊢ ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 |
124 |
123
|
a1i |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 ) |
125 |
|
undif2 |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) |
126 |
|
mblss |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ) |
127 |
17 126
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ) |
128 |
|
ssequn1 |
⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ↔ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) = ℝ ) |
129 |
127 128
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) = ℝ ) |
130 |
125 129
|
eqtr2id |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ℝ = ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) |
131 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
132 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
133 |
|
iftrue |
⊢ ( 𝑥 ∈ ℝ → if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) ) |
134 |
133
|
mpteq2ia |
⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) |
135 |
134
|
eqcomi |
⊢ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
136 |
|
ifcl |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
137 |
45 50 136
|
sylancl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) ) |
138 |
137
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
139 |
|
breq1 |
⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
140 |
|
breq1 |
⊢ ( 0 = if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
141 |
139 140
|
ifboth |
⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
142 |
58 43 141
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
143 |
142
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
144 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
145 |
65 137 45 144 67
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
146 |
143 145
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) |
147 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
148 |
138 57 146 147
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) |
149 |
|
itg2lecl |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
150 |
138 54 148 149
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) |
151 |
17 120 124 130 45 131 132 135 107 150
|
itg2split |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
152 |
118 151
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
153 |
|
eldif |
⊢ ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
154 |
153
|
baib |
⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
155 |
154
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
156 |
1
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ℝ ) |
157 |
156
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn ℝ ) |
158 |
|
elpreima |
⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
159 |
157 158
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
160 |
41
|
biantrurd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) ) |
161 |
5
|
nnred |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
162 |
161
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℝ ) |
163 |
162
|
rexrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℝ* ) |
164 |
|
elioopnf |
⊢ ( 𝑀 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) ) |
165 |
163 164
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) ) |
166 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ ) |
167 |
166
|
biantrurd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
168 |
160 165 167
|
3bitr2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) ) |
169 |
162 41
|
ltnled |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
170 |
159 168 169
|
3bitr2rd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
171 |
170
|
con1bid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
172 |
155 171
|
bitrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
173 |
172
|
ifbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) |
174 |
173
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) |
175 |
174
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
176 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) |
177 |
175 176
|
eqnbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) |
178 |
54 92
|
resubcld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ∈ ℝ ) |
179 |
178 150
|
ltnled |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ↔ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) ) |
180 |
177 179
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) |
181 |
54 92 150
|
ltsubadd2d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ↔ ( ∫2 ‘ 𝐹 ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) ) |
182 |
180 181
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
183 |
152 182
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) |
184 |
107 92 150
|
ltadd1d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ↔ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) ) |
185 |
183 184
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ) |
186 |
73 107 92 117 185
|
lelttrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ) |
187 |
161
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℝ ) |
188 |
|
mblvol |
⊢ ( 𝑢 ∈ dom vol → ( vol ‘ 𝑢 ) = ( vol* ‘ 𝑢 ) ) |
189 |
10 188
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) = ( vol* ‘ 𝑢 ) ) |
190 |
9
|
rpred |
⊢ ( 𝜑 → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ) |
191 |
190
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ) |
192 |
|
ovolcl |
⊢ ( 𝑢 ⊆ ℝ → ( vol* ‘ 𝑢 ) ∈ ℝ* ) |
193 |
35 192
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ* ) |
194 |
191
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ* ) |
195 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) |
196 |
189 195
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) |
197 |
193 194 196
|
xrltled |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ≤ ( ( 𝐶 / 2 ) / 𝑀 ) ) |
198 |
|
ovollecl |
⊢ ( ( 𝑢 ⊆ ℝ ∧ ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ∧ ( vol* ‘ 𝑢 ) ≤ ( ( 𝐶 / 2 ) / 𝑀 ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ ) |
199 |
35 191 197 198
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ ) |
200 |
189 199
|
eqeltrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) ∈ ℝ ) |
201 |
187 200
|
remulcld |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑀 · ( vol ‘ 𝑢 ) ) ∈ ℝ ) |
202 |
187
|
rexrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℝ* ) |
203 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℕ ) |
204 |
203
|
nnnn0d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℕ0 ) |
205 |
204
|
nn0ge0d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 ≤ 𝑀 ) |
206 |
|
elxrge0 |
⊢ ( 𝑀 ∈ ( 0 [,] +∞ ) ↔ ( 𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀 ) ) |
207 |
202 205 206
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ( 0 [,] +∞ ) ) |
208 |
|
ifcl |
⊢ ( ( 𝑀 ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) ) |
209 |
207 50 208
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) ) |
210 |
209
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) ) |
211 |
210
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ) |
212 |
|
eldifn |
⊢ ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) |
213 |
212
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) |
214 |
|
difssd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ⊆ 𝑢 ) |
215 |
214
|
sselda |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → 𝑥 ∈ 𝑢 ) |
216 |
36 170
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
217 |
215 216
|
syldan |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) |
218 |
217
|
con1bid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) ) |
219 |
213 218
|
mpbid |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) |
220 |
|
iftrue |
⊢ ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) ) |
221 |
220
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) ) |
222 |
215
|
iftrued |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) = 𝑀 ) |
223 |
219 221 222
|
3brtr4d |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
224 |
|
iffalse |
⊢ ( ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 ) |
225 |
224
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 ) |
226 |
|
0le0 |
⊢ 0 ≤ 0 |
227 |
|
breq2 |
⊢ ( 𝑀 = if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) → ( 0 ≤ 𝑀 ↔ 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
228 |
|
breq2 |
⊢ ( 0 = if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
229 |
227 228
|
ifboth |
⊢ ( ( 0 ≤ 𝑀 ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
230 |
205 226 229
|
sylancl |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
231 |
230
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
232 |
225 231
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
233 |
223 232
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
234 |
233
|
ralrimivw |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) |
235 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
236 |
65 75 210 82 235
|
ofrfval2 |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
237 |
234 236
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) |
238 |
|
itg2le |
⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) ) |
239 |
76 211 237 238
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) ) |
240 |
|
elrege0 |
⊢ ( 𝑀 ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) ) |
241 |
187 205 240
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ( 0 [,) +∞ ) ) |
242 |
|
itg2const |
⊢ ( ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) ∈ ℝ ∧ 𝑀 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) = ( 𝑀 · ( vol ‘ 𝑢 ) ) ) |
243 |
10 200 241 242
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) = ( 𝑀 · ( vol ‘ 𝑢 ) ) ) |
244 |
239 243
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( 𝑀 · ( vol ‘ 𝑢 ) ) ) |
245 |
203
|
nngt0d |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 < 𝑀 ) |
246 |
|
ltmuldiv2 |
⊢ ( ( ( vol ‘ 𝑢 ) ∈ ℝ ∧ ( 𝐶 / 2 ) ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) |
247 |
200 92 187 245 246
|
syl112anc |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) |
248 |
195 247
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ) |
249 |
88 201 92 244 248
|
lelttrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ) |
250 |
73 88 92 92 186 249
|
lt2addd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) ) |
251 |
89 250
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) ) |
252 |
90
|
rpcnd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐶 ∈ ℂ ) |
253 |
252
|
2halvesd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) = 𝐶 ) |
254 |
251 253
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) |
255 |
254
|
expr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom vol ) → ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |
256 |
255
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |
257 |
|
breq2 |
⊢ ( 𝑑 = ( ( 𝐶 / 2 ) / 𝑀 ) → ( ( vol ‘ 𝑢 ) < 𝑑 ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) |
258 |
257
|
rspceaimv |
⊢ ( ( ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ+ ∧ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |
259 |
9 256 258
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) |